From a15da8f9ba04b468dbc6313662cc841d5cc4a256 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 16 Jan 2022 19:11:55 -0800
Subject: [PATCH] #5778

---
 src/sat/smt/arith_solver.cpp | 2 ++
 src/sat/smt/arith_solver.h   | 1 +
 src/sat/smt/euf_model.cpp    | 5 +++++
 src/sat/smt/sat_th.h         | 5 +++++
 4 files changed, 13 insertions(+)

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index c9416ad4e..5a102fa14 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/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))
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index b6d6dbef8..d8405ea10 100644
--- a/src/sat/smt/arith_solver.h
+++ b/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; }
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index ffc00a19f..fff7e5989 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/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",
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index 9d1d9ebb1..3b0d478ae 100644
--- a/src/sat/smt/sat_th.h
+++ b/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 {