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