From d7042c234f32607c01324da7a3bbf74384d0aaab Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Nov 2017 09:34:44 -0800
Subject: [PATCH] fix #1371

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 62a569e2b..3b69d4846 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4366,8 +4366,9 @@ namespace smt {
                 SASSERT(is_app(fn));
                 // reverse argument order so that variable 0 starts at the beginning.
                 expr_ref_vector subst(m);
+                unsigned idx = 0;
                 for (expr* arg : *to_app(fn)) {
-                    subst.push_back(arg);
+                    subst.push_back(m.mk_var(idx++, m.get_sort(arg)));
                 }
                 expr_ref bodyr(m);
                 var_subst sub(m, true);