Fix for printing success with echo (cvc5#10272)

Fixes cvc5#10257.
ajreynol · Jan 11, 2024 · 62a9a00 · 62a9a00
1 parent 745a942
commit 62a9a00
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 10 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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")