summaryrefslogtreecommitdiff
path: root/test/regress/regress0/ho/issue4990-care-graph.smt2
blob: 93c87d3c9c0ae663fcd204ab312e5dea5f905f35 (plain) 
1
2
3
4
5
6
7
8

; EXPECT: sat
(set-logic HO_QF_AUFBVLIA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c (Int) Int)
(declare-fun d (Int Int) Int)
(assert (xor (= c (d a)) (= c (d b))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback