#7344

Z3Prover · Aug 26, 2024 · 349ebd0 · 349ebd0
1 parent 84da614
commit 349ebd0
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 2 deletions.
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
@@ -1858,8 +1858,10 @@ namespace smt {
             lbool phase = l_undef;
             m_case_split_queue->next_case_split(var, phase);
             used_queue = true;
-            if (var == null_bool_var)
+            if (var == null_bool_var) {
+                push_trail(value_trail(m_has_case_split, false));
                 return false;
+            }
 
             TRACE_CODE({
                 static unsigned counter = 0;
@@ -4642,6 +4644,9 @@ namespace smt {
     }
 
     bool context::has_case_splits() {
+        if (!m_has_case_split)
+            return false;
+
         for (unsigned i = get_num_b_internalized(); i-- > 0; ) {
             if (is_relevant(i) && get_assignment(i) == l_undef)
                 return true;

diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
@@ -1155,6 +1155,7 @@ namespace smt {
         bool guess(bool_var var, lbool phase);
 
     protected:
+        bool m_has_case_split = true;
         bool decide();
 
         void update_phase_cache_counter();

diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
@@ -99,7 +99,6 @@ namespace smt {
                 if (m.is_bool(s)) {
                     CTRACE("model", m_context->get_assignment(r) == l_undef, 
                            tout << mk_pp(r->get_expr(), m) << "\n";);
-                    SASSERT(m_context->get_assignment(r) != l_undef);
                     if (m_context->get_assignment(r) == l_true)
                         proc = alloc(expr_wrapper_proc, m.mk_true());
                     else