From 00520041fec1f5c6daefcc0ffea6b9e083df29e3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 22 Mar 2020 13:02:08 -0700
Subject: [PATCH] fix #3436

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp      | 16 ++++++++++------
 src/smt/smt_internalizer.cpp |  2 +-
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 8600a3d3a..8ca5ea887 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1947,6 +1947,7 @@ namespace smt {
         m_region.push_scope();
         m_scopes.push_back(scope());
         scope & s = m_scopes.back();
+        TRACE("context", tout << "push " << m_scope_lvl << "\n";);
 
         m_relevancy_propagator->push();
         s.m_assigned_literals_lim    = m_assigned_literals.size();
@@ -3357,7 +3358,9 @@ namespace smt {
        \brief Execute some finalization code after performing the search.
     */
     lbool context::check_finalize(lbool r) {
-        TRACE("after_search", display(tout << "result: " << r << "\n"););
+        TRACE("after_search", display(tout << "result: " << r << "\n");
+              m_case_split_queue->display(tout << "case splits\n");
+              );
         display_profile(verbose_stream());
         if (r == l_true && get_cancel_flag()) {
             r = l_undef;
@@ -3584,7 +3587,7 @@ namespace smt {
     }
 
     void context::end_search() {
-        m_case_split_queue ->end_search_eh();
+        m_case_split_queue->end_search_eh();
     }
 
     void context::inc_limits() {
@@ -4503,10 +4506,11 @@ namespace smt {
     }
 
     bool context::has_case_splits() {
-        bool_var var;
-        lbool phase = l_undef;
-        m_case_split_queue->next_case_split(var, phase);
-        return (var != null_bool_var); 
+        for (unsigned i = get_num_b_internalized(); i-- > 0; ) {
+            if (get_assignment(i) == l_undef)
+                return true;
+        }
+        return false;
     }
 
     void context::get_model(model_ref & m) {
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 26e0737c5..aa9c214ea 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -420,13 +420,13 @@ namespace smt {
        \brief Internalize an equality.
     */
     void context::internalize_eq(app * n, bool gate_ctx) {
-        TRACE("internalize", tout << mk_pp(n, m) << "\n";);
         SASSERT(!b_internalized(n));
         SASSERT(m.is_eq(n));
         internalize_formula_core(n, gate_ctx);
         bool_var v        = get_bool_var(n);
         bool_var_data & d = get_bdata(v);
         d.set_eq_flag();
+        TRACE("internalize", tout << mk_pp(n, m) << " " << literal(v, false) << "\n";);
         
         sort * s    = m.get_sort(n->get_arg(0));
         theory * th = m_theories.get_plugin(s->get_family_id());