blob: 6a77ae078f2854e2d1bea7541f04d90a41318ee1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
; COMMAND-LINE: -i --bv-solver=bitblast --bv-assert-input
(set-logic QF_BV)
(set-option :global-declarations true)
(declare-const a (_ BitVec 8))
(declare-const b (_ BitVec 8))
(declare-const c (_ BitVec 8))
(declare-const d (_ BitVec 8))
(assert (distinct (bvadd a d) (bvadd b c)))
(set-info :status sat)
(check-sat)
(reset-assertions)
(assert (= (bvadd a d) (bvadd b c)))
(set-info :status sat)
(check-sat)
|
