3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
This commit is contained in:
Nikolaj Bjorner 2021-05-10 19:14:18 -07:00
parent d27d09f87a
commit cd82205b06

View file

@ -2316,7 +2316,7 @@ public:
if (is_exists(tmp) && to_quantifier(tmp)->get_qid() == qe_lite) {
used_vars used;
tmp = to_quantifier(tmp)->get_expr();
used.process(tmp);
used(tmp);
var_subst vs(m, true);
fml = vs(tmp, vars.size(), (expr*const*)vars.data());
// collect set of variables that were used.