From 64e8ad696a1accdf489a3073cc480f591be04c39 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 26 Sep 2019 21:53:45 -0500
Subject: CVC print support for recoverable failure (#3323)

---
 src/printer/cvc/cvc_printer.cpp            | 17 +++++++++++++----
 test/regress/CMakeLists.txt                |  1 +
 test/regress/regress0/cvc-rerror-print.cvc |  7 +++++++
 3 files changed, 21 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/regress0/cvc-rerror-print.cvc

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 630d8bdd7..0b7c569b7 100644
--- 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 a1be9ad62..d4cc9b293 100644
--- 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
index 000000000..dd05723d2
--- /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;
-- 
cgit v1.2.3