mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 06:43:40 +00:00
Code Activity

mbp_array: Fix set_model_completion bug

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-31 11:29:39 -07:00
parent cdba0721e7
commit 1e54237880
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/qe/qe_arrays.cpp
View file

@ -1147,6 +1147,7 @@ namespace qe {
if (arr_vars.empty()) return; if (arr_vars.empty()) return;
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;
@ -1169,7 +1170,6 @@ 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 ();