From 45d8d73fce8409a6e9ac71c86abde1fb3a0cdba0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Aug 2022 09:46:19 -0700 Subject: [PATCH] #6303 handle more array instantiation cases for quantifier instantiation --- src/smt/smt_model_checker.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 0ffe8108d65..f2e83426257 100644 --- 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;