diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-05-17 18:42:13 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-05-17 18:42:13 +0000 |
| commit | 1703b160511396cd23be5203d9af86641b45766e (patch) | |
| tree | e1f085382022f853c068cef7990cd68fa3126f1b /test/regress/regress0/aufbv | |
| parent | a6f69a821e2d26f8901662193da5ee8dc74b158a (diff) | |
Fixed bug 338:
- fixed buggy rewrite rules assuming certain nodes only had 2 children
- added support for bv-rewrite dump
- fixed smt2_printer for bv constants
Diffstat (limited to 'test/regress/regress0/aufbv')
| -rw-r--r-- | test/regress/regress0/aufbv/bug338.smt2 | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/aufbv/bug338.smt2 b/test/regress/regress0/aufbv/bug338.smt2 new file mode 100644 index 000000000..b245228be --- /dev/null +++ b/test/regress/regress0/aufbv/bug338.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_AUFBV) +(declare-sort U 0) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun memory_0 () (Array (_ BitVec 32) (_ BitVec 8))) +(set-info :status sat) + +(set-info :notes "RewriteRule <ExtractBitwise>; expect unsat") + +(assert (not (= ((_ extract 7 0) (bvor (_ bv65536 32) (concat (_ bv0 25) ((_ extract 7 1) (select memory_0 (_ bv1 32)))) (concat (_ bv0 24) (select memory_0 (_ bv1 32))))) (bvor ((_ extract 7 0) (_ bv65536 32)) ((_ extract 7 0) (concat (_ bv0 25) ((_ extract 7 1) (select memory_0 (_ bv1 32))))))))) +(check-sat) + + +(exit) |