bv3.smt2 « tests « lfsc « src - smtcoq - Fork of https://github.com/smtcoq/smtcoq.

about summary refs log tree commit diff stats

path: root/src/lfsc/tests/bv3.smt2

blob: b16d58cba48cf23d30ad81021739456cc1ba8e8d (plain)

(set-logic QF_BV)
(declare-fun a () (_ BitVec 2))
(declare-fun b () (_ BitVec 2))
(assert (and (= a b) (not (= a b))))
(check-sat)
(exit)