mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
simplify
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
6a2d54b31e
commit
0628711c4a
|
@ -377,11 +377,7 @@ namespace qe {
|
|||
for (auto const& def : defs) {
|
||||
expr_safe_replace rep(m);
|
||||
rep.insert(def.var, def.term);
|
||||
for (unsigned j = 0; j < lits.size(); ++j) {
|
||||
expr_ref tmp(m);
|
||||
rep(lits.get(j), tmp);
|
||||
lits[j] = tmp;
|
||||
}
|
||||
rep(lits);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue