diff options
Diffstat (limited to 'test/regress/regress0/bv')
| -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 |