From 0643e7c0fca2b16dae9a4799471bc50e66a333a1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 12 Dec 2020 12:40:14 -0800 Subject: [PATCH] fix #4886 Signed-off-by: Nikolaj Bjorner --- src/qe/qsat.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index be4d98fff..6b5871186 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -396,11 +396,11 @@ namespace qe { void pred_abs::mk_concrete(expr_ref_vector& fmls, obj_map const& map) { obj_map cache; - expr_ref_vector trail(m); + expr_ref_vector trail(fmls); expr* p; app_ref r(m); ptr_vector 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) {