summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus/issue3645-grammar-sets.smt2
blob: 22a5e07d425e8547a218f2c28aa27e49d1cab1d7 (plain) 
1
2
3
4
5
6
7

; EXPECT: sat
; COMMAND-LINE: --sygus-inference
(set-logic ALL)
(declare-fun a () (Set (_ BitVec 2)))
(declare-fun b () (Set (_ BitVec 2)))
(assert (= a b))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback