From 535f4426550d8d1f764aad89b3386e60d27b0e9e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Aug 2021 12:13:27 -0700 Subject: [PATCH] #5518 regression from adding lambdas in model --- src/ast/normal_forms/defined_names.cpp | 2 ++ src/smt/theory_array_base.cpp | 14 +------------- 2 files changed, 3 insertions(+), 13 deletions(-) diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp index 5aef5c07511..ad5f8348693 100644 --- a/src/ast/normal_forms/defined_names.cpp +++ b/src/ast/normal_forms/defined_names.cpp @@ -114,6 +114,8 @@ app * defined_names::impl::gen_name(expr * e, sort_ref_buffer & var_sorts, buffe var_sorts.push_back(s); } else { + domain.push_back(m.mk_bool_sort()); + new_args.push_back(m.mk_true()); var_sorts.push_back(m.mk_bool_sort()); // could be any sort. } var_names.push_back(symbol(i)); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index ab3570872c5..79b38067158 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -389,19 +389,7 @@ namespace smt { if (q) { // the variables in q are maybe not consecutive. var_subst sub(m, false); - expr_free_vars fv; - fv(q); - expr_ref_vector es(m); - es.resize(fv.size()); - for (unsigned i = 0, j = 0; i < e->get_num_args(); ++i) { - SASSERT(j < es.size()); - while (!fv[j]) { - ++j; - SASSERT(j < es.size()); - } - es[j++] = e->get_arg(i); - } - f = sub(q, es.size(), es.data()); + f = sub(q, e->get_num_args(), e->get_args()); } return f; }