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