diff options
| author | lianah <lianahady@gmail.com> | 2013-03-21 12:38:51 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-03-21 12:38:51 -0400 |
| commit | 020ce7845a6ba4417616eedd072e3b73df3e8b38 (patch) | |
| tree | 42e925680f64095bc848c809c2ec91f88b9521a1 /src/theory/bv/theory_bv.cpp | |
| parent | 80697ed7280ac2462ec05e29754a0a563f19de44 (diff) | |
added regression test for constant eval
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 135b944ad..2d390b7b9 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -122,13 +122,13 @@ void TheoryBV::check(Effort e) } Assert (!ok == inConflict()); - if (!inConflict() && !d_coreSolver.isCoreTheory()) { - ok = d_inequalitySolver.check(e); - } + // if (!inConflict() && !d_coreSolver.isCoreTheory()) { + // ok = d_inequalitySolver.check(e); + // } Assert (!ok == inConflict()); - // if (!inConflict() && !d_coreSolver.isCoreTheory()) { - if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) { + if (!inConflict() && !d_coreSolver.isCoreTheory()) { + //if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) { ok = d_bitblastSolver.check(e); } |