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 /src/theory/bv/theory_bv.cpp | |
| parent | 39a863a248db14d3956b975d0e9c531b96f2baa4 (diff) | |
fixed bv bug due to applying equisatisfiable transformations in ppRewrite
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 4 |
1 files changed, 1 insertions, 3 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 && |