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

; COMMAND-LINE: --uf-ho
; EXPECT: sat
(set-logic QF_AUFBVLIA)
(set-option :uf-ho true)
(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