From 5d06fa23479d33fa81ba0751d4cd9e8aad94ea14 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 25 Oct 2018 17:29:09 -0500 Subject: [PATCH] fix #1901 Signed-off-by: Nikolaj Bjorner --- src/model/model.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/model/model.cpp b/src/model/model.cpp index 60441054c..2efc39db8 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -410,8 +410,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) } else if (f->is_skolem() && can_inline_def(ts, f) && (fi = get_func_interp(f)) && fi->get_interp() && (!ts.partition_ids().find(f, pid) || pid != current_partition)) { - var_subst vs(m); - // ? TBD args.reverse(); + var_subst vs(m, false); new_t = vs(fi->get_interp(), args.size(), args.c_ptr()); } #if 0