diff options
| author | lianah <lianahady@gmail.com> | 2014-06-15 20:36:12 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2014-06-15 20:39:13 -0400 |
| commit | 22c89dae0078a89b2c95d07c98e7ae29b5586ebd (patch) | |
| tree | 2834a7a4003350755b07b615cfd1392c6af99f9b | |
| parent | 39a863a248db14d3956b975d0e9c531b96f2baa4 (diff) | |
fixed bv bug due to applying equisatisfiable transformations in ppRewrite
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 4 | ||||
| -rw-r--r-- | 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<IsPowerOfTwo>::applies(t)) { - res = RewriteRule<IsPowerOfTwo>::run<false>(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<UltPlusOne>::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 * |