Fix for the main bug that was bugging me -- Bug 49. The assertions queue in the theories didn't get cleared on SatSolver backtracking so there were unasserted literals being returned as part of some conflicts. Sat solver now explicitely calls in the theory engine after it backtracks in order to clear the queues (clearAssertionQueues).

Also, changed the let.smt as it used to exibit "single literal conflict" problem. The sat solve can not except conflicts similar to (x != x), these should be rewritten to false during pre-processing. 

Adding 3 more small problems from the library that we can solve now to the regressions.

3 files changed, 29 insertions, 5 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 51992a31c..634ba00d4 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -98,10 +98,8 @@ Node CnfStream::getNode(const SatLiteral& literal) {
 
 SatLiteral CnfStream::getLiteral(const TNode& node) {
   TranslationCache::iterator find = d_translationCache.find(node);
-  SatLiteral literal;
-  if(find != d_translationCache.end()) {
-    literal = find->second;
-  }
+  Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
+  SatLiteral literal = find->second;
   Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
   return literal;
 }
diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index e54884925..0f8622cb8 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -182,6 +182,8 @@ void Solver::cancelUntil(int level) {
         trail.shrink(trail.size() - trail_lim[level]);
         trail_lim.shrink(trail_lim.size() - level);
     }
+    // Now, clear the TheoryEngine queue
+    proxy->clearAssertionQueues();
 }
 
 
@@ -442,7 +444,25 @@ Clause* Solver::propagateTheory()
   Clause* c = NULL;
   SatClause clause;
   proxy->theoryCheck(clause);
-  if (clause.size() > 0) {
+  int clause_size = clause.size();
+  Assert(clause_size != 1, "Can't handle unit clause explanations");
+  if(clause_size > 0) {
+    // Find the max level of the conflict
+    int max_level = 0;
+    for (int i = 0; i < clause_size; ++i) {
+      int current_level = level[var(clause[i])];
+      Debug("minisat") << "Literal: " << clause[i] << " with reason " << reason[var(clause[i])] << " at level " << current_level << std::endl;
+      Assert(toLbool(assigns[var(clause[i])]) != l_Undef, "Got an unassigned literal in conflict!");
+      if (current_level > max_level) max_level = current_level;
+    }
+    // If smaller than the decision level then pop back so we can analyse
+    Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl;
+    Assert(max_level <= decisionLevel(), "What is going on, can't get literals of a higher level as conflict!");
+    if (max_level < decisionLevel()) {
+      Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl;
+      cancelUntil(max_level);
+    }
+    // Create the new clause and attach all the information
     c = Clause_new(clause, true);
     learnts.push(c);
     attachClause(*c);
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 922d596be..f10531080 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -93,6 +93,8 @@ public:
   inline void enqueueTheoryLiteral(const SatLiteral& l);
 
   inline void setCnfStream(CnfStream* cnfStream);
+
+  inline void clearAssertionQueues();
 };
 
 }/* CVC4::prop namespace */
@@ -207,6 +209,10 @@ void SatSolver::setCnfStream(CnfStream* cnfStream) {
 }
 
 
+void SatSolver::clearAssertionQueues() {
+  d_theoryEngine->clearAssertionQueues();
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */