fix E instantiation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Nov 12, 2019 · 1281964 · 1281964
1 parent 74cfcc4
commit 1281964
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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);
             }