From 48ec7c1175af91f8e43ab51153f8cc289b9e96dd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 1 Oct 2018 17:25:02 +0100 Subject: [PATCH 1/3] Follow-up fix for fpa2bv_converter. --- src/ast/fpa/fpa2bv_converter.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 055f751c1..1dc13ff9e 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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)) { From f145873603ca8b83a5a84e299528b7dfad7c845b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 1 Oct 2018 20:22:20 +0100 Subject: [PATCH 2/3] CI Test From aaae3118de5d3faadffcdc9344089f377b6ecae6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 1 Oct 2018 20:26:05 +0100 Subject: [PATCH 3/3] CI Test