mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

array_mbp: turn on model completion

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-30 13:45:48 -07:00
parent 0452bc3d43
commit b50da20531
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/qe/qe_arrays.cpp
View file

@ -631,6 +631,7 @@ namespace qe {
void operator () (model& mdl, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars) { void operator () (model& mdl, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars) {
reset (); reset ();
model_evaluator mev(mdl); model_evaluator mev(mdl);
mev.set_model_completion(true);
M = &mdl; M = &mdl;
m_mev = &mev; m_mev = &mev;
@ -857,6 +858,7 @@ namespace qe {
reset (); reset ();
model_evaluator mev(mdl); model_evaluator mev(mdl);
mev.set_model_completion(true);
M = &mdl; M = &mdl;
m_mev = &mev; m_mev = &mev;
m_reduce_all_selects = reduce_all_selects; m_reduce_all_selects = reduce_all_selects;
@ -1167,6 +1169,7 @@ namespace qe {
TRACE ("qe", tout << "Failed to project arrays\n";); TRACE ("qe", tout << "Failed to project arrays\n";);
} }
mev.set_model_completion(true);
// dealloc // dealloc
for (auto & kv : m_sel_terms) dealloc(kv.m_value); for (auto & kv : m_sel_terms) dealloc(kv.m_value);
m_sel_terms.reset (); m_sel_terms.reset ();