// constant Set_empty : (func(1, [int; Set_Set @(0)]))
constant Set_sng : (func(1, [@(0); (Set_Set @(0))]))
bind 1 m1 : {v : Set_Set Int | v = Set_empty 0}
bind 2 m2 : {v : Set_Set Int | v = (Set_cup (Set_cup m1 (Set_sng 10)) (Set_sng 20)) }
bind 3 m3 : {v : Set_Set Int | v = (Set_cup (Set_cup m1 (Set_sng 20)) (Set_sng 10)) }
bind 4 m4 : {v : Set_Set Int | v = (Set_cup m1 (Set_sng 10)) }
bind 5 m5 : {v : Set_Set Int | v = (Set_cup m1 (Set_sng 20)) }
constraint:
env [ 1 ]
lhs {v : int | true }
rhs {v : int | (Set_mem 100 m1) }
id 1 tag []
constraint:
env [ 1; 2 ]
lhs {v : int | true }
rhs {v : int | not (Set_mem 100 m2) }
id 2 tag []
constraint:
env [ 1; 2 ]
lhs {v : int | true }
rhs {v : int | Set_mem 10 m2 }
id 3 tag []
constraint:
env [ 1; 2; 3 ]
lhs {v : int | true }
rhs {v : int | m2 = m3 }
id 4 tag []
constraint:
env [ 1; 2; 3; 4; 5 ]
lhs {v : int | true }
rhs {v : int | m2 = Set_cup m4 m5 }
id 5 tag []