summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/cvc/cvc_printer.cpp7
-rw-r--r--src/printer/smt2/smt2_printer.cpp2
2 files changed, 8 insertions, 1 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 55e19510b..bc59e37ba 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -793,6 +793,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
return;
break;
}
+ case kind::CARD: {
+ out << "||";
+ toStream(out, n[0], depth, types, false);
+ out << "||";
+ return;
+ break;
+ }
// Quantifiers
case kind::FORALL:
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 62153571c..4defc7691 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -977,7 +977,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
static std::string quoteSymbol(TNode n) {
-#warning "check the old implementation. It seems off."
+ // #warning "check the old implementation. It seems off."
std::stringstream ss;
ss << language::SetLanguage(language::output::LANG_SMTLIB_V2_5);
return CVC4::quoteSymbol(ss.str());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback