SMT-LIBv2 compliance regarding outputting "unknown".

Thanks to Peter Collingbourne for the report, and the patch!

(this commit was certified error- and warning-free by the test-and-commit script.)

2 files changed, 8 insertions, 0 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8356f9e49..e41fd9c65 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -590,6 +590,13 @@ void Smt2Printer::toStream(std::ostream& out, Model* m, Command* c, int c_type )
   }
 }
 
+void Smt2Printer::toStream(std::ostream& out, const Result& r) const throw() {
+  if (r.getType() == Result::TYPE_SAT && r.isSat() == Result::SAT_UNKNOWN) {
+    out << "unknown";
+  } else {
+    Printer::toStream(out, r);
+  }
+}
 
 static void toStream(std::ostream& out, const AssertCommand* c) throw() {
   out << "(assert " << c->getExpr() << ")";
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 30c0ce647..475479095 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -37,6 +37,7 @@ public:
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   //for models
   void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw();
+  void toStream(std::ostream& out, const Result& r) const throw();
 };/* class Smt2Printer */
 
 }/* CVC4::printer::smt2 namespace */