test/regress/regress0/bv/issue-4076.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

; COMMAND-LINE: --incremental
; COMMAND-LINE: --incremental --bv-solver=bitblast-internal
; EXPECT: sat
; EXPECT: sat
(set-logic ALL)
(declare-fun a ((_ BitVec 2)) Int)
(declare-fun b (Int) (_ BitVec 2))
(declare-const c Int)
(declare-const d Int)
(assert (= (a #b01) 1))
(assert(= 0 (a (bvlshr (b c) (b d)))))
(push)
(check-sat)
(pop)
(check-sat)