From 31ff658f5e3a91d70f8bd2f97a8e35cb6832210c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 19 Mar 2020 08:54:08 -0700
Subject: [PATCH] fix #3416

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

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 489a1c607..461745caf 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2384,7 +2384,6 @@ namespace smt {
        \warning This method will not invoke reset_cache_generation.
     */
     unsigned context::pop_scope_core(unsigned num_scopes) {
-
         unsigned units_to_reassert_lim;
 
         try {
@@ -3871,7 +3870,6 @@ namespace smt {
     final_check_status context::final_check() {
         TRACE("final_check", tout << "final_check inconsistent: " << inconsistent() << "\n"; display(tout); display_normalized_enodes(tout););
         CASSERT("relevancy", check_relevancy());
-
         
         if (m_fparams.m_model_on_final_check) {
             mk_proto_model();
@@ -4458,6 +4456,11 @@ namespace smt {
     bool context::update_model(bool refinalize) {
         final_check_status fcs = FC_DONE;
         if (refinalize) {
+            bool_var var;
+            lbool phase = l_undef;
+            m_case_split_queue->next_case_split(var, phase);
+            if (var != null_bool_var) 
+                return false;
             fcs = final_check();
         }
         TRACE("opt", tout << (refinalize?"refinalize":"no-op") << " " << fcs << "\n";);
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index c8922475c..6de681ab8 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -2172,6 +2172,7 @@ namespace smt {
         TRACE("pb", display(tout << "validate: ", c, true);
               tout << "sum: " << sum << " " << maxsum << " ";
               tout << ctx.get_assignment(c.lit()) << "\n";
+              ctx.display(tout);
               );
 
         SASSERT(sum <= maxsum);