3 files changed, 10 insertions, 6 deletions

diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index 5ad647baa..e54884925 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -141,6 +141,7 @@ void Solver::attachClause(Clause& c) {
 
 
 void Solver::detachClause(Clause& c) {
+    Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
     assert(c.size() > 1);
     assert(find(watches[toInt(~c[0])], &c));
     assert(find(watches[toInt(~c[1])], &c));
@@ -151,8 +152,10 @@ void Solver::detachClause(Clause& c) {
 
 
 void Solver::removeClause(Clause& c) {
+    Debug("minisat") << "Solver::removeClause(" << c << ")" << std::endl;
     detachClause(c);
-    free(&c); }
+    free(&c);
+}
 
 
 bool Solver::satisfied(const Clause& c) const {
@@ -440,8 +443,8 @@ Clause* Solver::propagateTheory()
   SatClause clause;
   proxy->theoryCheck(clause);
   if (clause.size() > 0) {
-    Clause* c = Clause_new(clause, false);
-    clauses.push(c);
+    c = Clause_new(clause, true);
+    learnts.push(c);
     attachClause(*c);
   }
   return c;
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)
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 96154063d..ef28a4ac6 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -66,14 +66,14 @@ void PropEngine::assertLemma(TNode node) {
 
 Result PropEngine::checkSat() {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
-  Debug("prop") << "solve()" << endl;
+  Debug("prop") << "PropEngine::checkSat()" << endl;
   // Mark that we are in the checkSat
   d_inCheckSat = true;
   // Check the problem
   bool result = d_satSolver->solve();
   // Not in checkSat any more
   d_inCheckSat = false;
-  Debug("prop") << "solve() => " << (result ? "true" : "false") << endl;
+  Debug("prop") << "PropEngine::checkSat() => " << (result ? "true" : "false") << endl;
   return Result(result ? Result::SAT : Result::UNSAT);
 }