From d7b9cc70d003ae9ad75062c89293be6f05fc3b99 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 25 Sep 2022 18:03:16 -0700
Subject: [PATCH] smc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/q_mbi.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index a87be2dee..8be75f03c 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -355,8 +355,10 @@ namespace q {
                     return expr_ref(m);
                     
             }
-            else if (!(*p)(*m_model, vars, fmls))
+            else if (!(*p)(*m_model, vars, fmls)) {
+                TRACE("q", tout << "theory projection failed\n");
                 return expr_ref(m);
+            }
         }
         for (app* v : vars) {
             expr_ref term(m);
@@ -581,6 +583,7 @@ namespace q {
         binding.reset();
         auto const& nodes = ctx.get_egraph().nodes();
         m_model->reset_eval_cache();
+        model::scoped_model_completion _sc(*m_model, true);
         for (unsigned j = 0; j < offsets.size(); ++j) {
             unsigned offset = offsets[j];
             binding.push_back(nodes[offset]->get_expr());