diff options
Diffstat (limited to 'test/regress/regress0/bv/issue-4076.smt2')
| -rw-r--r-- | test/regress/regress0/bv/issue-4076.smt2 | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/issue-4076.smt2 b/test/regress/regress0/bv/issue-4076.smt2 new file mode 100644 index 000000000..3a80dc5f0 --- /dev/null +++ b/test/regress/regress0/bv/issue-4076.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +(set-logic ALL) +(set-option :produce-models true) +(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) |