blob: 39dace123b729917c9ba4de2a28d542859b75a41 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores
; EXPECT: sat
(set-logic QF_BV)
(declare-fun s () (_ BitVec 64))
(declare-fun t () (_ BitVec 64))
(declare-fun splust () (_ BitVec 64))
(declare-fun shift1 () (_ BitVec 64))
(declare-fun shift2 () (_ BitVec 64))
(declare-fun negshift1 () (_ BitVec 64))
(assert (= shift1 (bvlshr s splust)))
(assert (= shift2 (bvlshr t splust)))
(assert (= negshift1 (bvneg shift1)))
(assert (= splust (bvadd s t)))
(assert (distinct negshift1 shift2))
(check-sat)
|
