CVC print support for recoverable failure (#3323)

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 630d8bdd71b74215f77b11dc779108cf35808c3d..0b7c569b70e4676eac5c50b1691fae584066086e 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1048,10 +1048,12 @@ static bool tryToStream(std::ostream& out,
 
 void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const
 {
-  if(tryToStream<CommandSuccess>(out, s, d_cvc3Mode) ||
-     tryToStream<CommandFailure>(out, s, d_cvc3Mode) ||
-     tryToStream<CommandUnsupported>(out, s, d_cvc3Mode) ||
-     tryToStream<CommandInterrupted>(out, s, d_cvc3Mode)) {
+  if (tryToStream<CommandSuccess>(out, s, d_cvc3Mode)
+      || tryToStream<CommandFailure>(out, s, d_cvc3Mode)
+      || tryToStream<CommandRecoverableFailure>(out, s, d_cvc3Mode)
+      || tryToStream<CommandUnsupported>(out, s, d_cvc3Mode)
+      || tryToStream<CommandInterrupted>(out, s, d_cvc3Mode))
+  {
     return;
   }
 
@@ -1554,6 +1556,13 @@ static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode)
   out << s->getMessage() << endl;
 }
 
+static void toStream(std::ostream& out,
+                     const CommandRecoverableFailure* s,
+                     bool cvc3Mode)
+{
+  out << s->getMessage() << endl;
+}
+
 template <class T>
 static bool tryToStream(std::ostream& out,
                         const CommandStatus* s,

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a1be9ad6242c59cfb470904c0a17d1d014e50838..d4cc9b29309a42eb68bd6e561e445da674cb0183 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -332,6 +332,7 @@ set(regress_0_tests
   regress0/cvc3.userdoc.04.cvc
   regress0/cvc3.userdoc.05.cvc
   regress0/cvc3.userdoc.06.cvc
+  regress0/cvc-rerror-print.cvc
   regress0/datatypes/Test1-tup-mp.cvc
   regress0/datatypes/boolean-equality.cvc
   regress0/datatypes/boolean-terms-datatype.cvc

diff --git a/test/regress/regress0/cvc-rerror-print.cvc b/test/regress/regress0/cvc-rerror-print.cvc
new file mode 100644 (file)
index 0000000..dd05723
--- /dev/null
+++ b/test/regress/regress0/cvc-rerror-print.cvc
@@ -0,0 +1,7 @@
+% EXPECT: valid
+% EXPECT: Cannot get model unless immediately preceded by SAT/INVALID or UNKNOWN response.
+OPTION "logic" "ALL";
+OPTION "produce-models" true;
+x : INT;
+QUERY x = x;
+COUNTEREXAMPLE;