From 969511ac00830a97f49be9d9585540f33b8aaa7e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 3 Oct 2024 19:35:16 -0700
Subject: [PATCH] fixup std-order / inv-order

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/has_free_vars.cpp       | 3 ++-
 src/ast/rewriter/var_subst.cpp  | 2 +-
 src/parsers/smt2/smt2parser.cpp | 3 ++-
 3 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/ast/has_free_vars.cpp b/src/ast/has_free_vars.cpp
index b1b74c7da..c5f3db027 100644
--- a/src/ast/has_free_vars.cpp
+++ b/src/ast/has_free_vars.cpp
@@ -30,7 +30,7 @@ class contains_vars::imp {
 
     void visit(expr * n, unsigned delta, bool & visited) {
         expr_delta_pair e(n, delta);
-        if (!m_cache.contains(e)) {
+        if (!is_ground(n) && !m_cache.contains(e)) {
             m_todo.push_back(e);
             visited = false;
         }
@@ -74,6 +74,7 @@ public:
         m_todo.push_back(expr_delta_pair(n, begin));
         while (!m_todo.empty()) {
             expr_delta_pair e = m_todo.back();
+            
             if (visit_children(e.m_node, e.m_delta)) {
                 m_cache.insert(e);
                 m_todo.pop_back();
diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp
index 532a49ec5..4d4c17865 100644
--- a/src/ast/rewriter/var_subst.cpp
+++ b/src/ast/rewriter/var_subst.cpp
@@ -59,7 +59,7 @@ expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args)
                 new_args.push_back(arg);
             else {
                 unsigned idx = to_var(arg)->get_idx();
-                new_args.push_back(m_std_order ? args[idx] : args[num_args - idx - 1]);
+                new_args.push_back(m_std_order ? args[num_args - idx - 1] : args[idx]);
             }
         }
         result = m.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.data());
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 48c48d0a9..afa361538 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -116,6 +116,7 @@ namespace smt2 {
         symbol               m_match;
         symbol               m_case;
         symbol               m_underscore;
+        contains_vars        m_has_free_vars;
 
         typedef std::pair<symbol, expr*> named_expr;
         named_expr           m_last_named_expr;
@@ -1031,7 +1032,7 @@ namespace smt2 {
 
         void name_expr(expr * n, symbol const & s) {
             TRACE("name_expr", tout << "naming: " << s << " ->\n" << mk_pp(n, m()) << "\n";);
-            if (!is_ground(n) && has_free_vars(n))
+            if (!is_ground(n) && m_has_free_vars(n))
                 throw parser_exception("invalid named expression, expression contains free variables");
             m_ctx.insert(s, 0, nullptr, n);
             m_last_named_expr.first  = s;