From d3194bb8a8263e7a69459838b2100924fb441f9a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 2 Aug 2021 11:07:28 -0700
Subject: [PATCH] #5445

---
 src/sat/smt/q_solver.cpp        |  8 ++++++--
 src/sat/smt/sat_dual_solver.cpp | 13 +++++++++----
 src/sat/tactic/goal2sat.cpp     | 14 ++++++++------
 3 files changed, 23 insertions(+), 12 deletions(-)

diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 5769340ee..0f3eaf3d3 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -54,6 +54,11 @@ namespace q {
                     ctx.add_root(~l, lit);
                 }
             }
+            else if (is_ground(q->get_expr())) {
+                auto lit = ctx.internalize(q->get_expr(), l.sign(), false, false);
+                add_clause(~l, lit);
+                ctx.add_root(~l, lit);
+            }
             else {
                 ctx.push_vec(m_universal, l);
                 if (ctx.get_config().m_ematching)
@@ -78,8 +83,7 @@ namespace q {
     }
 
     std::ostream& solver::display(std::ostream& out) const {
-        m_ematch.display(out);
-        return out;
+        return m_ematch.display(out);
     }
 
     std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp
index 00d01b1b7..dcc90ddb0 100644
--- a/src/sat/smt/sat_dual_solver.cpp
+++ b/src/sat/smt/sat_dual_solver.cpp
@@ -93,14 +93,19 @@ namespace sat {
 
     void dual_solver::add_root(unsigned sz, literal const* clause) {      
         flush();
-        if (sz == 1) {
+        if (false && sz == 1) {
             TRACE("dual", tout << "unit: " << clause[0] << "\n";);
             m_units.push_back(clause[0]);
             return;
         }
-        literal root(m_solver.mk_var(), false);
-        for (unsigned i = 0; i < sz; ++i)
-            m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
+        literal root;
+        if (sz == 1) 
+            root = ext2lit(clause[0]);
+        else {
+            root = literal(m_solver.mk_var(), false);
+            for (unsigned i = 0; i < sz; ++i)
+                m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
+        }
         m_roots.push_back(~root);
         TRACE("dual", tout << "root: " << ~root << " => " << literal_vector(sz, clause) << "\n";);
     }
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 4d0cc7880..ddc13f06a 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -216,8 +216,10 @@ 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))) 
+        if (relevancy_enabled() && (m.is_true(t) || m.is_false(t))) {
             add_dual_root(sat::literal(v, m.is_false(t)));
+            ensure_euf()->track_relevancy(v);
+        }
         return v;
     }
 
@@ -289,14 +291,14 @@ struct goal2sat::imp : public sat::sat_internalizer {
         sat::bool_var v = m_map.to_bool_var(t);
         if (v == sat::null_bool_var) {
             if (m.is_true(t)) {
-                sat::literal tt = sat::literal(add_var(false, m.mk_true()), false);
+                sat::literal tt = sat::literal(mk_bool_var(t), false);
                 mk_root_clause(tt);
                 l = sign ? ~tt : tt;
             }
             else if (m.is_false(t)) {
-                sat::literal tt = sat::literal(add_var(false, m.mk_false()), true);
-                mk_root_clause(tt);
-                l = sign ? tt : ~tt;
+                sat::literal ff = sat::literal(mk_bool_var(t), false);
+                mk_root_clause(~ff);
+                l = sign ? ~ff : ff;
             }
             else if (m_euf) {
                 convert_euf(t, root, sign);
@@ -796,7 +798,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 m_frame_stack.pop_back();
                 continue;
             }
-            if (m.is_not(t) && !m.is_not(t->get_arg(0)) && fsz != sz + 1) {
+            if (m.is_not(t) && (root || (!m.is_not(t->get_arg(0)) && fsz != sz + 1))) {
                 m_frame_stack.pop_back();
                 visit(t->get_arg(0), root, !sign);
                 continue;