#5778

src/sat/smt/arith_solver.cpp

@@ -561,6 +561,8 @@ namespace arith {
     }
 
     void solver::dbg_finalize_model(model& mdl) {
+        if (m_not_handled)
+            return;
         bool found_bad = false;
         for (unsigned v = 0; v < get_num_vars(); ++v) {
             if (!is_bool(v))

src/sat/smt/arith_solver.h

@@ -448,6 +448,7 @@ namespace arith {
         lbool get_phase(bool_var v) override;
         bool include_func_interp(func_decl* f) const override;
         bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_add(n->get_expr()); }
+        bool has_unhandled() const override { return m_not_handled != nullptr; }
 
         // bounds and equality propagation callbacks
         lp::lar_solver& lp() { return *m_solver; }

src/sat/smt/euf_model.cpp

@@ -294,6 +294,11 @@ namespace euf {
     }
 
     void solver::validate_model(model& mdl) {
+        if (!m_unhandled_functions.empty())
+            return;
+        for (auto* s : m_solvers)
+            if (s && s->has_unhandled())
+                return;
         model_evaluator ev(mdl);
         ev.set_model_completion(true);
         TRACE("model",

src/sat/smt/sat_th.h

@@ -95,6 +95,11 @@ namespace euf {
           \brief conclude model building
         */
         virtual void finalize_model(model& mdl) {}
+
+        /**
+        * \brief does solver have an unhandled function.
+        */
+        virtual bool has_unhandled() const { return false; }
     };
 
     class th_solver : public sat::extension, public th_model_builder, public th_decompile, public th_internalizer {