diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp
index 7a48f8809..b392254a1 100644
--- a/src/sat/smt/sat_dual_solver.cpp
+++ b/src/sat/smt/sat_dual_solver.cpp
@@ -101,6 +101,17 @@ namespace sat {
         m_solver.mk_clause(sz, m_lits.data(), status::input());
     }
 
+    void dual_solver::add_assumptions(solver const& s) {
+        m_lits.reset();
+        for (bool_var v : m_tracked_vars)
+            m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
+        for (auto lit : m_units) {
+            bool_var w = m_ext2var.get(lit.var(), null_bool_var);
+            if (w != null_bool_var)
+                m_lits.push_back(ext2lit(lit));            
+        }
+    }
+
     bool dual_solver::operator()(solver const& s) {
         m_core.reset();
         m_core.append(m_units);
@@ -108,9 +119,7 @@ namespace sat {
             return true;
         m_solver.user_push();
         m_solver.add_clause(m_roots.size(), m_roots.data(), status::input());
-        m_lits.reset();
-        for (bool_var v : m_tracked_vars)
-            m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
+        add_assumptions(s);
         lbool is_sat = m_solver.check(m_lits.size(), m_lits.data());
         if (is_sat == l_false) 
             for (literal lit : m_solver.get_core())
diff --git a/src/sat/smt/sat_dual_solver.h b/src/sat/smt/sat_dual_solver.h
index 4e9b59fec..2b040128c 100644
--- a/src/sat/smt/sat_dual_solver.h
+++ b/src/sat/smt/sat_dual_solver.h
@@ -42,6 +42,8 @@ namespace sat {
         literal  ext2lit(literal lit);
         literal  lit2ext(literal lit);
 
+        void add_assumptions(solver const& s);
+
         std::ostream& display(solver const& s, std::ostream& out) const;
 
     public:
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index c08944bee..d7b97b521 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -137,6 +137,10 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (relevancy_enabled())
             ensure_euf()->add_root(n, lits);
     }
+
+    void add_dual_root(sat::literal lit) {
+        add_dual_root(1, &lit);
+    }
     
     void mk_clause(sat::literal l) {
         mk_clause(1, &l);
@@ -199,6 +203,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
             // create fake variable to represent true;
             m_true = sat::literal(add_var(false, m.mk_true()), false);
             mk_clause(m_true); // v is true
+            add_dual_root(1, &m_true);
         }
         return m_true;
     }
@@ -223,6 +228,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (!m_expr2var_replay || !m_expr2var_replay->find(t, v))  
             v = add_var(true, t);
         m_map.insert(t, v);
+        if (relevancy_enabled() && (m.is_true(t) || m.is_false(t))) 
+            add_dual_root(sat::literal(v, m.is_false(t)));
         return v;
     }