mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix #6270
MBQI asserts auxiliary function definitions to handle models of arrays. This is unsound if the definition contains a model value.
This commit is contained in:
parent
a0d4a8c21c
commit
e0aa32e6c5
|
@ -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) {
|
||||
|
|
Loading…
Reference in a new issue