mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
This commit is contained in:
parent
46107022f7
commit
fea14245a0
|
@ -552,10 +552,13 @@ namespace mbp {
|
|||
if (fmls.empty() || defs.empty())
|
||||
return;
|
||||
expr_safe_replace subst(m);
|
||||
for (auto const& d : defs)
|
||||
subst.insert(d.var, d.term);
|
||||
unsigned j = 0;
|
||||
expr_ref tmp(m);
|
||||
for (unsigned i = defs.size(); i-- > 0; ) {
|
||||
auto const& d = defs[i];
|
||||
subst(d.term, tmp);
|
||||
subst.insert(d.var, tmp);
|
||||
}
|
||||
unsigned j = 0;
|
||||
for (expr* fml : fmls) {
|
||||
subst(fml, tmp);
|
||||
fmls[j++] = tmp;
|
||||
|
|
|
@ -321,7 +321,7 @@ namespace q {
|
|||
eqs.push_back(m.mk_eq(v, val));
|
||||
}
|
||||
rep(fmls);
|
||||
TRACE("q", tout << "generated formulas\n" << fmls << "\ngenerated eqs:\n" << eqs;);
|
||||
TRACE("q", tout << "generated formulas\n" << fmls << "\ngenerated eqs:\n" << eqs << "\n";);
|
||||
return mk_and(fmls);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue