From 22c89dae0078a89b2c95d07c98e7ae29b5586ebd Mon Sep 17 00:00:00 2001 From: lianah Date: Sun, 15 Jun 2014 20:36:12 -0400 Subject: [PATCH] fixed bv bug due to applying equisatisfiable transformations in ppRewrite --- src/theory/bv/theory_bv.cpp | 4 +--- src/theory/bv/theory_bv_rewrite_rules_simplification.h | 4 ++-- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 5ae07466a..d3da10a90 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -578,9 +578,7 @@ Node TheoryBV::ppRewrite(TNode t) } else { res = t; } - } else if (RewriteRule::applies(t)) { - res = RewriteRule::run(t); - } + } // if(t.getKind() == kind::EQUAL && diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 33994782a..c8705e121 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1195,8 +1195,8 @@ Node RewriteRule::apply(TNode node) { /** * x ^(x-1) = 0 => 1 << sk - * Note: only to be called in ppRewrite and not rewrite! - * (it calls the rewriter) + * WARNING: this is an **EQUISATISFIABLE** transformation! + * Only to be called on top level assertions. * * @param node * -- 2.30.2