diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-09 05:19:22 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-09 05:19:22 +0000 |
| commit | 04fd25e4201130776015fd3179631a97f27da12a (patch) | |
| tree | d3559b078c2a1c0e95a1bf49142a81c80cf69814 /src/prop/minisat/simp | |
| parent | cf4d347cbbbb4c1a1e1db99337cfd2b22b84b756 (diff) | |
Diffstat (limited to 'src/prop/minisat/simp')
| -rw-r--r-- | src/prop/minisat/simp/SimpSolver.C | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C index a2e46e2e4..057dfdbe2 100644 --- a/src/prop/minisat/simp/SimpSolver.C +++ b/src/prop/minisat/simp/SimpSolver.C @@ -65,7 +65,7 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) { n_occ .push(0); n_occ .push(0); occurs .push(); - frozen .push((char)false); + frozen .push((char)theoryAtom); touched .push(0); elim_heap.insert(v); elimtable.push(); @@ -156,6 +156,7 @@ bool SimpSolver::addClause(vec<Lit>& ps) void SimpSolver::removeClause(Clause& c) { + Debug("minisat") << "SimpSolver::removeClause(" << c << ")" << std::endl; assert(!c.learnt()); if (use_simplification) |