summaryrefslogtreecommitdiff
path: root/test/regress/regress1/ho/issue5078-small.smt2
blob: 21077434aee353c0c1fea74a3e41038bb1d2fcaf (plain) 
1
2
3
4
5
6
7
8

(set-logic HO_QF_UFLIA)
(set-info :status sat)
(declare-fun a (Int Int) Int)
(declare-fun d () Int)
(declare-fun e () Int)
(assert (= (a d 0) (a 0 1)))
(assert (= d (mod e 3)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback