Fix echo printing. (#6573)

Previously, echo surpressed leading, trailing and escape quotes of the
string to print. However, the SMT-LIB standard states that the string is
to be printed as is, including those quote characters.

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index e4e8aff1a6ba485b22c4aef798f6a92793178cac..02cea842a109c906895af8201e6d9edb573d9da8 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -294,7 +294,18 @@ void EmptyCommand::toStream(std::ostream& out,
 /* class EchoCommand                                                          */
 /* -------------------------------------------------------------------------- */
 
-EchoCommand::EchoCommand(std::string output) : d_output(output) {}
+EchoCommand::EchoCommand(std::string output)
+{
+  // escape all double-quotes
+  size_t pos = 0;
+  while ((pos = output.find('"', pos)) != string::npos)
+  {
+    output.replace(pos, 1, "\"\"");
+    pos += 2;
+  }
+  d_output = '"' + output + '"';
+}
+
 std::string EchoCommand::getOutput() const { return d_output; }
 void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fe034c519adf35b4a30d51bda2d57334d215b267..8cb7f7d1ffcf07dcb4f500a7ce26290041915139 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -542,6 +542,7 @@ set(regress_0_tests
   regress0/define-fun-model.smt2
   regress0/distinct.smtv1.smt2
   regress0/dump-unsat-core-full.smt2
+  regress0/echo.smt2
   regress0/eqrange1.smt2
   regress0/eqrange2.smt2
   regress0/eqrange3.smt2

diff --git a/test/regress/regress0/echo.smt2 b/test/regress/regress0/echo.smt2
new file mode 100644 (file)
index 0000000..a274737
--- /dev/null
+++ b/test/regress/regress0/echo.smt2
@@ -0,0 +1,18 @@
+; EXPECT: "str"""
+; EXPECT: "str""ing"
+; EXPECT: "hi"
+; EXPECT: "str""""ing"
+; EXPECT: "str""i""ng"
+; EXPECT: "str\ing"
+; EXPECT: "str\\ing"
+; EXPECT: "str\"
+; EXPECT: "\u{65}"
+(echo "str""")
+(echo "str""ing")
+(echo "hi")
+(echo "str""""ing")
+(echo "str""i""ng")
+(echo "str\ing")
+(echo "str\\ing")
+(echo "str\")
+(echo "\u{65}")