From 62a9a001ed74c389e2efd2f2a304f55d1c4b40b6 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 11 Jan 2024 14:37:55 -0600
Subject: [PATCH] Fix for printing success with echo (#10272)

Fixes #10257.
---
 src/parser/commands.cpp                             |  9 ++-------
 src/parser/commands.h                               |  5 ++---
 test/regress/cli/CMakeLists.txt                     |  1 +
 test/regress/cli/regress0/parser/print-success.smt2 | 12 ++++++++++++
 4 files changed, 17 insertions(+), 10 deletions(-)
 create mode 100644 test/regress/cli/regress0/parser/print-success.smt2

diff --git a/src/parser/commands.cpp b/src/parser/commands.cpp
index 7ea96211c41..11b8edb521d 100644
--- a/src/parser/commands.cpp
+++ b/src/parser/commands.cpp
@@ -238,19 +238,14 @@ std::string EchoCommand::getOutput() const { return d_output; }
 
 void EchoCommand::invoke(cvc5::Solver* solver, SymManager* sm)
 {
-  /* we don't have an output stream here, nothing to do */
   d_commandStatus = CommandSuccess::instance();
 }
 
-void EchoCommand::invoke(cvc5::Solver* solver,
-                         SymManager* sm,
-                         std::ostream& out)
+void EchoCommand::printResult(cvc5::Solver* solver, std::ostream& out) const
 {
-  out << cvc5::internal::quoteString(d_output) << std::endl;
   Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
                            << std::endl;
-  d_commandStatus = CommandSuccess::instance();
-  printResult(solver, out);
+  out << cvc5::internal::quoteString(d_output) << std::endl;
 }
 
 std::string EchoCommand::getCommandName() const { return "echo"; }
diff --git a/src/parser/commands.h b/src/parser/commands.h
index 0604aed803f..30ab6e64314 100644
--- a/src/parser/commands.h
+++ b/src/parser/commands.h
@@ -180,9 +180,8 @@ class CVC5_EXPORT EchoCommand : public Cmd
   std::string getOutput() const;
 
   void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
-  void invoke(cvc5::Solver* solver,
-              parser::SymManager* sm,
-              std::ostream& out) override;
+  /** The result is the printed string */
+  void printResult(cvc5::Solver* solver, std::ostream& out) const override;
 
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 98e7d289c6d..dfdbcc66c4e 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1049,6 +1049,7 @@ set(regress_0_tests
   regress0/parser/non_well_founded_dt.smt2
   regress0/parser/non_well_founded_dts.smt2
   regress0/parser/parser-line-error.smt2
+  regress0/parser/print-success.smt2
   regress0/parser/proj-issue370-push-pop-global.smt2
   regress0/parser/quoted-define-fun.smt2
   regress0/parser/real-numerals.smt2
diff --git a/test/regress/cli/regress0/parser/print-success.smt2 b/test/regress/cli/regress0/parser/print-success.smt2
new file mode 100644
index 00000000000..213fc047980
--- /dev/null
+++ b/test/regress/cli/regress0/parser/print-success.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --print-success
+; EXPECT: success
+; EXPECT: success
+; EXPECT: true
+; EXPECT: success
+; EXPECT: "done"
+; DISABLE-TESTER: dump
+(set-logic ALL)
+(set-option :produce-proofs true)
+(get-option :produce-proofs)
+(assert false)
+(echo "done")