From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 25 Sep 2019 15:05:45 +0000 (-0500)
Subject: Fix printing of instantiation patterns (#3305)
X-Git-Tag: cvc5-1.0.0~3936
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b2261930d0fa97f0b40e4f96313db957e8ab9418;p=cvc5.git

Fix printing of instantiation patterns (#3305)
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 37a73db2d..df9bee981 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -861,7 +861,8 @@ void Smt2Printer::toStream(std::ostream& out,
     out << ')';
     return;
   }
-  case kind::INST_PATTERN: break;
+  case kind::INST_PATTERN:
+  case kind::INST_NO_PATTERN: break;
   case kind::INST_PATTERN_LIST:
   {
     for (const Node& nc : n)
@@ -873,10 +874,14 @@ void Smt2Printer::toStream(std::ostream& out,
           out << ":fun-def";
         }
       }
-      else
+      else if (nc.getKind() == kind::INST_PATTERN)
       {
         out << ":pattern " << nc;
       }
+      else if (nc.getKind() == kind::INST_NO_PATTERN)
+      {
+        out << ":no-pattern " << nc[0];
+      }
     }
     return;
     break;