mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix model reconstruction ordering for elim_unconstrained

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-09 15:18:19 -08:00
parent 30e0f78c16
commit 64ec8acd30
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -357,6 +357,7 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
trail.hide(entry.m_f);
break;
case generic_model_converter::instruction::ADD:
// trail.push(entry.m_f, entry.m_def, nullptr, old_fmls);
break;
}
}
@ -364,7 +365,8 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
scoped_ptr<expr_substitution> sub = alloc(expr_substitution, m, true, false);
rp->set_substitution(sub.get());
expr_ref new_def(m);
for (auto const& entry : mc.entries()) {
for (unsigned i = mc.entries().size(); i-- > 0; ) {
auto const& entry = mc.entries()[i];
switch (entry.m_instruction) {
case generic_model_converter::instruction::HIDE:
break;