diff options
author | lianah <lianahady@gmail.com> | 2013-03-21 12:38:51 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-21 12:38:51 -0400 |
commit | 020ce7845a6ba4417616eedd072e3b73df3e8b38 (patch) | |
tree | 42e925680f64095bc848c809c2ec91f88b9521a1 /test | |
parent | 80697ed7280ac2462ec05e29754a0a563f19de44 (diff) |
added regression test for constant eval
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/bv/core/constant_core.smt2 | 15 |
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 |