From 7e68d546bad299d26beb8cde4627af61b9fb3651 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 11 Nov 2020 17:37:00 -0800
Subject: [PATCH] na

---
 src/ast/euf/euf_egraph.cpp      |  2 +-
 src/sat/smt/euf_solver.cpp      |  2 ++
 src/sat/smt/sat_dual_solver.cpp |  7 +++----
 src/sat/tactic/goal2sat.cpp     | 10 +++++-----
 4 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 2e55b7865..bc2dafaa5 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -735,7 +735,7 @@ SASSERT(false);
     }
 
     std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
-        out << n->get_expr_id() << " := ";
+        out << "#" << n->get_expr_id() << " := ";
         expr* f = n->get_expr();
         if (is_app(f))
             out << mk_bounded_pp(f, m, 1) << " ";
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 863750779..28ced2898 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -149,6 +149,8 @@ namespace euf {
     }
 
     bool solver::is_external(bool_var v) {
+        if (s().is_external(v))
+            return true;
         if (nullptr != m_bool_var2expr.get(v, nullptr))
             return true;
         for (auto* s : m_solvers)
diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp
index 96881bc5c..52d60c80b 100644
--- a/src/sat/smt/sat_dual_solver.cpp
+++ b/src/sat/smt/sat_dual_solver.cpp
@@ -105,24 +105,23 @@ namespace sat {
                 m_core.push_back(lit2ext(lit));        
         if (is_sat == l_true) {
             IF_VERBOSE(0, display(s, verbose_stream()));
+            s.display(verbose_stream());
             UNREACHABLE();
+            return false;
         }
         TRACE("dual", m_solver.display(tout << "is-sat: " << is_sat << " core: " << m_core << "\n"););
         m_solver.user_pop(1);
         return is_sat == l_false;
     }
 
-
     std::ostream& dual_solver::display(solver const& s, std::ostream& out) const {
-        for (auto r : m_roots)
-            out << r << " " << m_solver.value(r) << "\n";
         for (unsigned v = 0; v < m_solver.num_vars(); ++v) {
             bool_var w = m_var2ext.get(v, null_bool_var);
             if (w == null_bool_var)
                 continue;
             lbool v1 = m_solver.value(v);
             lbool v2 = s.value(w);
-            if (v1 == v2)
+            if (v1 == v2 || v2 == l_undef)
                 continue;
             out << w << " " << v1 << " " << v2 << "\n";
         }
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 8b8e87bcf..2684aa1b0 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -278,12 +278,12 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 l = sign ? mk_true() : ~mk_true();
             }
             else {                
+                if (m_euf) {
+                    convert_euf(t, root, sign);  
+                    return;
+                }
                 if (!is_uninterp_const(t)) {
-                    if (m_euf) {
-                        convert_euf(t, root, sign);  
-                        return;
-                    }
-                    else if (!is_app(t)) {
+                    if (!is_app(t)) {
                         std::ostringstream strm;
                         strm << mk_ismt2_pp(t, m);
                         throw_op_not_handled(strm.str());