mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

#6303

Browse source 
handle more array instantiation cases for quantifier instantiation
This commit is contained in:
Nikolaj Bjorner 2022-08-30 09:46:19 -07:00
parent 0f475f45b5
commit 45d8d73fce
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/smt_model_checker.cpp
View file

@ -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;