diff options
| -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 * |