3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
This commit is contained in:
Nikolaj Bjorner 2018-10-01 15:52:25 -07:00
commit 808d2eb60f

View file

@ -245,6 +245,9 @@ expr_ref fpa2bv_converter::extra_quantify(expr * e)
nv = uv.get_num_vars();
subst_map.resize(uv.get_max_found_var_idx_plus_1());
if (nv == 0)
return expr_ref(e, m);
for (unsigned i = 0; i < nv; i++)
{
if (uv.contains(i)) {