From e0aa32e6c59047109f25dc8c0273a68b5ab54a60 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 15 Aug 2022 00:13:32 -0700
Subject: [PATCH] fix #6270

MBQI asserts auxiliary function definitions to handle models of arrays. This is unsound if the definition contains a model value.
---
 src/smt/smt_model_checker.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 039416f73..0ffe8108d 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -218,7 +218,7 @@ namespace smt {
             TRACE("model_checker", tout << "Got some value " << sk_value << "\n";);
 
             if (use_inv) {
-	            unsigned sk_term_gen = 0;
+                unsigned sk_term_gen = 0;
                 expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen);
                 if (sk_term != nullptr) {
                     TRACE("model_checker", tout << "Found inverse " << mk_pp(sk_term, m) << "\n";);
@@ -243,6 +243,8 @@ namespace smt {
             func_decl * f = nullptr;
             if (autil.is_as_array(sk_value, f) && cex->get_func_interp(f) && cex->get_func_interp(f)->get_interp()) {
                 expr_ref body(cex->get_func_interp(f)->get_interp(), m);
+                if (contains_model_value(body))
+                    return false;                    
                 ptr_vector<sort> sorts(f->get_arity(), f->get_domain());
                 svector<symbol> names;
                 for (unsigned i = 0; i < f->get_arity(); ++i) {