#5778

src/sat/smt/euf_model.cpp

@@ -63,9 +63,17 @@ namespace euf {
         }
     };
 
+    void solver::save_model(model_ref& mdl) {
+        m_qmodel = mdl;
+    }
+
     void solver::update_model(model_ref& mdl) {
         TRACE("model", tout << "create model\n";);
-        mdl->reset_eval_cache();
+        if (m_qmodel) {
+            mdl = m_qmodel;
+            return;
+        }
+        mdl->reset_eval_cache();        
         for (auto* mb : m_solvers)
             mb->init_model();
         m_values.reset();

src/sat/smt/euf_solver.h

@@ -154,6 +154,7 @@ namespace euf {
         // model building
         expr_ref_vector m_values;
         obj_map<expr, enode*> m_values2root;        
+        model_ref m_qmodel;
         bool include_func_interp(func_decl* f);
         void register_macros(model& mdl);
         void dependencies2values(user_sort& us, deps_t& deps, model_ref& mdl);
@@ -395,6 +396,7 @@ namespace euf {
         relevancy& get_relevancy() { return m_relevancy; }
 
         // model construction
+        void save_model(model_ref& mdl);
         void update_model(model_ref& mdl);
         obj_map<expr, enode*> const& values2root();
         void model_updated(model_ref& mdl);

src/sat/smt/q_mbi.cpp

@@ -48,6 +48,7 @@ namespace q {
     lbool mbqi::operator()() {
         lbool result = l_true;
         m_model = nullptr;
+        ctx.save_model(m_model);
         m_instantiations.reset();
         for (sat::literal lit : m_qs.m_universal) {
             quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var()));
@@ -73,6 +74,9 @@ namespace q {
             m_qs.add_clause(~qlit, ~lit);
         }
         m_instantiations.reset();
+        if (result != l_true)
+            m_model = nullptr;
+        ctx.save_model(m_model);
         return result;
     }