added regression test for constant eval

1 files changed, 15 insertions, 0 deletions

diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2
new file mode 100644
index 000000000..c7a5a605f
--- /dev/null
+++ b/test/regress/regress0/bv/core/constant_core.smt2
@@ -0,0 +1,15 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x () (_ BitVec 3))
+(assert (and 
+(= ((_ extract 1 0) x) (concat ((_ extract 1 1) x) ((_ extract 0 0) x)))
+(= ((_ extract 0 0) x) ((_ extract 1 1) x))
+(= ((_ extract 2 2) x) ((_ extract 1 1) x))
+(= (_ bv0 1) ((_ extract 0 0) x))
+(= x (concat ((_ extract 2 2) x) ((_ extract 1 0) x)))
+(not (= (_ bv0 3) x))
+))
+(check-sat)
+(exit)
\ No newline at end of file