blob: e1d582a4e6f4d161411202e5f7d42317bd535ffb (
plain)
1
2
3
4
5
6
7
|
(set-logic QF_BV)
(declare-fun a () (_ BitVec 2))
(declare-fun b () (_ BitVec 2))
(declare-fun c () (_ BitVec 2))
(assert (and (= c a) (and (= b a) (not (= c b)))))
(check-sat)
(exit)
|