diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index b1719577b..a4e9f192e 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -29,6 +29,7 @@ Revision History:
 #include"substitution.h"
 #include"ast_counter.h"
 #include"statistics.h"
+#include"stopwatch.h"
 #include"lbool.h"
 
 namespace datalog {
diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h
index 160eb7b94..196f5268c 100644
--- a/src/muz/rel/dl_instruction.h
+++ b/src/muz/rel/dl_instruction.h
@@ -30,7 +30,6 @@ Revision History:
 
 namespace datalog {
 
-    class execution_context;
     class instruction_block;
     class rel_context;
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index bc28221a9..c80b75ba6 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -3500,7 +3500,13 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
     }
 
     bool solver::check_domain(literal lit, literal lit2) {
-        return m_antecedents.contains(lit2.var());
+        if (!m_antecedents.contains(lit2.var())) {
+            m_todo_antecedents.push_back(lit2);
+            return false;
+        }
+        else {
+            return true;
+        }
     }
 
     bool solver::extract_assumptions(literal lit, index_set& s) {
@@ -3565,8 +3571,16 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
             s.insert(lit.index());
         }
         else {
+            SASSERT(m_todo_antecedents.empty());
             if (!extract_assumptions(lit, s)) {
-                return false;
+                SASSERT(!m_todo_antecedents.empty());
+                while (!m_todo_antecedents.empty()) {
+                    index_set s1;
+                    if (extract_assumptions(m_todo_antecedents.back(), s1)) {
+                        m_todo_antecedents.pop_back();
+                    }
+                }
+                VERIFY (extract_assumptions(lit, s));
             }
             add_assumption(lit);
         }
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index c7f472a60..091162f23 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -481,6 +481,7 @@ namespace sat {
         typedef hashtable<unsigned, u_hash, u_eq> index_set;
 
         u_map<index_set>       m_antecedents;
+        literal_vector         m_todo_antecedents;
         vector<literal_vector> m_binary_clause_graph;
 
         bool extract_assumptions(literal lit, index_set& s);