summaryrefslogtreecommitdiff
path: root/test/regress/regress0/issue5947.smt2
blob: 4fbcfb00bce64941d5a019dda44d672b03e516f2 (plain) 
1
2
3
4
5
6
7
8

; COMMAND-LINE: -q --check-models
(set-logic QF_UFBVLIA)
(set-info :status sat)
(declare-fun f ((_ BitVec 3)) Int)
(declare-fun x () (_ BitVec 3))
(declare-fun y () (_ BitVec 3))
(assert (not (= (f (bvxor x y)) (f (bvxnor x y)))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback