#6303

handle more array instantiation cases for quantifier instantiation
Z3Prover · Aug 30, 2022 · 45d8d73 · 45d8d73
1 parent 0f475f4
commit 45d8d73
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
@@ -233,11 +233,19 @@ namespace smt {
             }
             else {
                 expr * sk_term = get_term_from_ctx(sk_value);
+                func_decl * f = nullptr;
                 if (sk_term != nullptr) {
+                    TRACE("model_checker", tout << "sk term " << mk_pp(sk_term, m) << "\n");
                     sk_value = sk_term;
                 }
+                // last ditch: am I an array?
+                else if (autil.is_as_array(sk_value, f) && cex->get_func_interp(f) && cex->get_func_interp(f)->get_array_interp(f)) {
+                    sk_value = cex->get_func_interp(f)->get_array_interp(f);
+                }
+
             }
             if (contains_model_value(sk_value)) {
+                TRACE("model_checker", tout << "type compatible term " << mk_pp(sk_value, m) << "\n");
                 sk_value = get_type_compatible_term(sk_value);
             }
             func_decl * f = nullptr;