From 12819640b7d39608f8dd6cece58d0d1b52ffe3b0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 11 Nov 2019 17:10:47 -0800
Subject: [PATCH] fix E instantiation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/tactic/fd_solver/smtfd_solver.cpp | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index 303bd582a..55cca5787 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -1437,10 +1437,10 @@ namespace smtfd {
unsigned sz = q->get_num_decls();
vars.resize(sz, nullptr);
for (unsigned i = 0; i < sz; ++i) {
- vars[sz - i - 1] = m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i));
+ vars[i] = m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i));
}
var_subst subst(m);
- expr_ref body = subst(tmp, vars.size(), vars.c_ptr());
+ expr_ref body = subst(q->get_expr(), vars.size(), vars.c_ptr());
if (is_exists(q)) {
body = m.mk_implies(q, body);
}