mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
dda4d66325
commit
0643e7c0fc
|
@ -396,11 +396,11 @@ namespace qe {
|
|||
|
||||
void pred_abs::mk_concrete(expr_ref_vector& fmls, obj_map<expr,expr*> const& map) {
|
||||
obj_map<expr,expr*> cache;
|
||||
expr_ref_vector trail(m);
|
||||
expr_ref_vector trail(fmls);
|
||||
expr* p;
|
||||
app_ref r(m);
|
||||
ptr_vector<expr> args;
|
||||
unsigned sz0 = todo.size();
|
||||
unsigned sz0 = todo.size();
|
||||
todo.append(fmls.size(), (expr*const*)fmls.c_ptr());
|
||||
while (sz0 != todo.size()) {
|
||||
app* a = to_app(todo.back());
|
||||
|
@ -438,9 +438,8 @@ namespace qe {
|
|||
todo.pop_back();
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
fmls[i] = to_app(cache.find(fmls[i].get()));
|
||||
}
|
||||
for (unsigned i = 0; i < fmls.size(); ++i)
|
||||
fmls[i] = to_app(cache.find(fmls.get(i)));
|
||||
}
|
||||
|
||||
void pred_abs::pred2lit(expr_ref_vector& fmls) {
|
||||
|
|
Loading…
Reference in a new issue