Quote unsat core names if applicable, fixes bug 816.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 247ef2431014e29cb9ac7aab4588af719d21fcbf..fd77535116a437f4889a6e99c301134b16bcb541 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1067,7 +1067,7 @@ void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core, const std::
     if(j == names.end()) {
       out << *i << endl;
     } else {
-      out << (*j).second << endl;
+      out << maybeQuoteSymbol((*j).second) << endl;
     }
   }
   out << ")" << endl;