From cebf83c4605a7d03fb6d90c803eee62232bb96e5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 2 Apr 2021 11:48:44 -0700
Subject: [PATCH] fix #5146

---
 src/cmd_context/cmd_context.cpp |  2 +-
 src/parsers/smt2/smt2parser.cpp | 12 +++++++++++-
 2 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 9c4b2ce40..43d68e82c 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1082,7 +1082,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
               tout << "s: " << s << "\n";
               tout << "body:\n" << mk_ismt2_pp(_t, m()) << "\n";
               tout << "args:\n"; for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n" << mk_pp(args[i]->get_sort(), m()) << "\n";);
-        var_subst subst(m());
+        var_subst subst(m(), false);
         scoped_rlimit no_limit(m().limit(), 0);
         result = subst(_t, coerced_args);
         if (well_sorted_check_enabled() && !is_well_sorted(m(), result))
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 825598f7a..3afe67cb9 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -2276,7 +2276,17 @@ namespace smt2 {
             sort* const* sorts = sort_stack().c_ptr() + sort_spos;
             expr* t = expr_stack().back();
             if (is_fun) {
-                m_ctx.insert(id, num_vars, sorts, t);
+                expr_ref _t(t, m());
+                if (num_vars > 1) {
+                    // variable ordering in macros follow non-standard ordering
+                    // we have to reverse the ordering used by the parser.
+                    var_subst sub(m(), true);
+                    expr_ref_vector vars(m());
+                    for (unsigned i = 0; i < num_vars; ++i)
+                        vars.push_back(m().mk_var(i, sorts[i]));
+                    _t = sub(_t, vars);
+                }
+                m_ctx.insert(id, num_vars, sorts, _t);
             }
             else {
                 m_ctx.model_add(id, num_vars, sorts, t);