blob: 7e0da282ed2067e5f7c1c88c97a023ca442f35a0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
; COMMAND-LINE: --bv-solver=lazy
; EXPECT: unsat
(set-logic QF_BVLIA)
(set-info :status unsat)
(declare-const a (_ BitVec 32))
(declare-const b (_ BitVec 32))
(declare-const c (_ BitVec 32))
(declare-const d (_ BitVec 32))
(declare-const e (_ BitVec 32))
(assert (or (= a b) (= a c) (= a d) (= a e)))
(assert (not (= (bv2nat a) (bv2nat b))))
(assert (not (= (bv2nat a) (bv2nat c))))
(assert (not (= (bv2nat a) (bv2nat d))))
(assert (not (= (bv2nat a) (bv2nat e))))
(check-sat)
|