diff options
Diffstat (limited to 'src/prop/minisat/simp')
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index bf04cec8d..ed2dc04b9 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -98,10 +98,9 @@ SimpSolver::~SimpSolver() Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) { Var v = Solver::newVar(sign, dvar,theoryAtom); - frozen .push((char)theoryAtom); - eliminated.push((char)false); - if (use_simplification){ + frozen .push((char)theoryAtom); + eliminated.push((char)false); n_occ .push(0); n_occ .push(0); occurs .init(v); @@ -159,8 +158,10 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) bool SimpSolver::addClause_(vec<Lit>& ps, bool removable) { #ifndef NDEBUG - for (int i = 0; i < ps.size(); i++) + if (use_simplification) { + for (int i = 0; i < ps.size(); i++) assert(!isEliminated(var(ps[i]))); + } #endif int nclauses = clauses_persistent.size(); |