From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 7 May 2021 20:28:44 +0000 (-0300)
Subject: Properly printing INST_PATTERN_LIST by itself (#6507)
X-Git-Tag: cvc5-1.0.0~1783
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bf62473ea3bed27f13f0eb320cea404ebadb490e;p=cvc5.git

Properly printing INST_PATTERN_LIST by itself (#6507)

Previously the SMT2 printer would print pattern lists wrong when they were not printed as part of a binder containing it. This commit fixes this by removing an unused hardcoded restriction that led to issues when printing the ASTs of proof nodes containing patterns.
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 9f9492cec..ae8d37713 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -528,8 +528,7 @@ void Smt2Printer::toStream(std::ostream& out,
   bool stillNeedToPrintParams = true;
   bool forceBinary = false; // force N-ary to binary when outputing children
   // operator
-  if (n.getNumChildren() != 0 && k != kind::INST_PATTERN_LIST
-      && k != kind::CONSTRUCTOR_TYPE)
+  if (n.getNumChildren() != 0 && k != kind::CONSTRUCTOR_TYPE)
   {
     out << '(';
   }