From 020ce7845a6ba4417616eedd072e3b73df3e8b38 Mon Sep 17 00:00:00 2001 From: lianah Date: Thu, 21 Mar 2013 12:38:51 -0400 Subject: added regression test for constant eval --- src/theory/bv/theory_bv.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src/theory/bv/theory_bv.cpp') 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); } -- cgit v1.2.3