From d4ca7e53747cb66e4720d49988dbc297e9bb2b35 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 26 Jan 2023 21:39:52 -0800
Subject: [PATCH] #6555

---
 src/ast/ast_smt2_pp.cpp                | 8 ++++++++
 src/ast/ast_smt2_pp.h                  | 1 +
 src/ast/converters/model_converter.cpp | 2 +-
 3 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 927660fbe..74bb871ec 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -1265,6 +1265,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environmen
     return out;
 }
 
+
 std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p, unsigned indent, char const* cmd, bool reverse) {
     if (!f) return out << "null";
     ast_manager & m = env.get_manager();
@@ -1276,6 +1277,13 @@ std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_e
     return out;
 }
 
+std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p, unsigned indent, char const* cmd) {
+    return ast_smt2_pp(out, f, e, env, p, indent, cmd, false);
+}
+
+std::ostream & ast_smt2_pp_rev(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p, unsigned indent, char const* cmd) {
+    return ast_smt2_pp(out, f, e, env, p, indent, cmd, true);
+}
 
 std::ostream & ast_smt2_pp(std::ostream & out, unsigned sz, expr * const* es, smt2_pp_environment & env, params_ref const & p, unsigned indent,
                             unsigned num_vars, char const * var_prefix) {
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index 2b0b2f371..64ea2aec9 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -105,6 +105,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & e
 std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
 std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "declare-fun");
 std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "define-fun", bool reverse = false);
+std::ostream & ast_smt2_pp_rev(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "define-fun");
 std::ostream & ast_smt2_pp(std::ostream & out, symbol const& s, bool is_skolem, smt2_pp_environment & env, params_ref const& p = params_ref());
 std::ostream & ast_smt2_pp_recdefs(std::ostream & out, vector<std::pair<func_decl*, expr*>> const& funs, smt2_pp_environment & env, params_ref const & p = params_ref());
 
diff --git a/src/ast/converters/model_converter.cpp b/src/ast/converters/model_converter.cpp
index 1033cc57b..716970cba 100644
--- a/src/ast/converters/model_converter.cpp
+++ b/src/ast/converters/model_converter.cpp
@@ -26,7 +26,7 @@ Notes:
 void model_converter::display_add(std::ostream& out, smt2_pp_environment& env, ast_manager& m, func_decl* f, expr* e) {
     VERIFY(e);
     VERIFY(f->get_range() == e->get_sort());
-    ast_smt2_pp(out, f, e, env, params_ref(), 0, "model-add", true) << "\n";
+    ast_smt2_pp_rev(out, f, e, env, params_ref(), 0, "model-add") << "\n";
 }
 
 void model_converter::display_add(std::ostream& out, ast_manager& m, func_decl* f, expr* e) const {