mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Follow-up fix for fpa2bv_converter.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2018-10-01 17:25:02 +01:00
parent 2a92de0aee
commit 48ec7c1175
No known key found for this signature in database
GPG key ID: BCF6360F86294467
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/fpa/fpa2bv_converter.cpp
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)) {