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