From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 25 May 2017 17:44:35 +0000 (-0500)
Subject: Quote unsat core names if applicable, fixes bug 816.
X-Git-Tag: cvc5-1.0.0~5791
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=97443967555b0e7fe6be4e6ab03b81383bc90430;p=cvc5.git

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 247ef2431..fd7753511 100644
--- 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;