liquid-fixpoint-0.9.6.3.1: tests/pos/maps03.fq
bind 1 m1 : {v : Map_t Int Int | v = Map_default 0}
bind 2 m2 : {v : Map_t Int Int | v = (Map_store (Map_store (Map_store m1 30 3) 10 1) 20 2) }
bind 3 s1 : {v : Set_Set Int | v = (Set_cup (Set_sng 30) (Set_sng 20))}
bind 4 m3 : {v : Map_t Int Int | v = (Map_store (Map_store m1 20 2) 30 3) }
constraint:
env [ 1; 2; 3; 4 ]
lhs {v : Map_t Int Int | v = Map_project s1 m2}
rhs {v : Map_t Int Int | v = m3 }
id 1 tag []