From ee125b4fe3e33f0062ab525da3640038f89b6237 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 23 Mar 2016 19:05:21 -0400 Subject: [PATCH] extend model with the value of a fresh variable --- src/qe/qe_arrays.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index 88b0290d5..162a4fb78 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -309,12 +309,19 @@ namespace qe { expr_ref_vector args(m); sort* range = get_array_range(m.get_sort(s)); for (unsigned i = 0; i < idxs.size(); ++i) { - app_ref var(m); + app_ref var(m), sel(m); + expr_ref val(m); var = m.mk_fresh_const("value", range); vars.push_back(var); args.reset(); - args.push_back(result); + + args.push_back (s); args.append(idxs[i].m_values.size(), idxs[i].m_vars); + sel = a.mk_select (args.size (), args.c_ptr ()); + VERIFY (model.eval (sel, val)); + model.register_decl (var->get_decl (), val); + + args[0] = result; args.push_back(var); result = a.mk_store(args.size(), args.c_ptr()); } @@ -398,6 +405,7 @@ namespace qe { // TBD chase definition of nested array. return l_undef; } + // AG: Shouldn't this be l_false return l_true; } };