From 1703b160511396cd23be5203d9af86641b45766e Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Thu, 17 May 2012 18:42:13 +0000 Subject: 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 --- test/regress/regress0/aufbv/bug338.smt2 | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 test/regress/regress0/aufbv/bug338.smt2 (limited to 'test/regress') 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 ; 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) -- cgit v1.2.3