From bf62473ea3bed27f13f0eb320cea404ebadb490e Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 7 May 2021 17:28:44 -0300 Subject: [PATCH] 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. --- src/printer/smt2/smt2_printer.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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 << '('; } -- 2.30.2