From abe3ef2382ef3b36baf9c8827b4e57e16a328f91 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 19 May 2021 10:33:23 -0700
Subject: [PATCH] #5215

---
 src/sat/smt/bv_internalize.cpp |  3 +--
 src/sat/smt/bv_solver.cpp      | 20 +++++++++++++-------
 src/sat/tactic/goal2sat.cpp    | 20 +-------------------
 3 files changed, 15 insertions(+), 28 deletions(-)

diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index d6c3d4e64..f06d2d0df 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -284,7 +284,6 @@ namespace bv {
     }
 
     void solver::register_true_false_bit(theory_var v, unsigned idx) {
-        SASSERT(s().value(m_bits[v][idx]) != l_undef);
         sat::literal l = m_bits[v][idx];
         SASSERT(l == mk_true() || ~l == mk_true());
         bool is_true = l == mk_true();
@@ -369,7 +368,7 @@ namespace bv {
     sat::literal solver::mk_true() {
         if (m_true == sat::null_literal) {
             ctx.push(value_trail<sat::literal>(m_true));
-            m_true = ctx.internalize(m.mk_true(), false, false, false);
+            m_true = ctx.internalize(m.mk_true(), false, true, false);
         }
         return m_true;
     }
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index 3a35a73d5..0c57508ef 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -95,14 +95,20 @@ namespace bv {
         result.reset();
         unsigned i = 0;
         for (literal b : m_bits[v]) {
-            switch (ctx.s().value(b)) {
-            case l_false:
-                break;
-            case l_undef:
-                return false;
-            case l_true:
+            if (b == ~m_true) 
+                ;
+            else if (b == m_true) 
                 result += power2(i);
-                break;
+            else {
+                switch (ctx.s().value(b)) {
+                case l_false:
+                    break;
+                case l_undef:
+                    return false;
+                case l_true:
+                    result += power2(i);
+                    break;
+                }
             }
             ++i;
         }
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 9cb21c769..c08944bee 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -75,7 +75,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
     expr_ref_vector             m_trail;
     func_decl_ref_vector        m_unhandled_funs;
     bool                        m_default_external;
-    bool                        m_xor_solver { false };
     bool                        m_euf { false };
     bool                        m_drat { false };
     bool                        m_is_redundant { false };
@@ -108,7 +107,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         sat_params sp(p);
         m_ite_extra  = p.get_bool("ite_extra", true);
         m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
-        m_xor_solver = p.get_bool("xor_solver", false);
         m_euf = sp.euf();
         m_drat = sp.drat_file().is_non_empty_string();
     }
@@ -576,7 +574,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     }
 
-    void convert_iff2(app * t, bool root, bool sign) {
+    void convert_iff(app * t, bool root, bool sign) {
         if (t->get_num_args() != 2)
             throw default_exception("unexpected number of arguments to xor");
         SASSERT(t->get_num_args() == 2);
@@ -611,13 +609,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     }
 
-    void convert_iff(app * t, bool root, bool sign) {
-        if (!m_euf && is_xor(t))
-            convert_ba(t, root, sign);
-        else               
-            convert_iff2(t, root, sign);
-    }
-
     func_decl_ref_vector const& interpreted_funs() {
         auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
         if (ext)
@@ -723,10 +714,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     }
 
-    bool is_xor(app* t) const {
-        return m_xor_solver && m.is_iff(t) && m.is_iff(t->get_arg(1));
-    }
-
     struct scoped_stack {
         imp& i;
         sat::literal_vector& r;
@@ -784,11 +771,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 visit(t->get_arg(0), root, !sign);
                 continue;
             }
-            if (!m_euf && is_xor(t)) {
-                convert_ba(t, root, sign);
-                m_frame_stack.pop_back();
-                continue;
-            }
             unsigned num = t->get_num_args();
             while (m_frame_stack[fsz-1].m_idx < num) {
                 expr * arg = t->get_arg(m_frame_stack[fsz-1].m_idx);