From 84a95435ef3d92ea6ee969a574b9fa98d569f93f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 17 Sep 2021 19:49:51 -0500
Subject: [PATCH] Fix printer for datatype udpater (#7208)

---
 src/printer/smt2/smt2_printer.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b92d8fa43..6217276b1 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -786,6 +786,7 @@ void Smt2Printer::toStream(std::ostream& out,
   break;
   case kind::APPLY_UPDATER:
   {
+    stillNeedToPrintParams = false;
     Node op = n.getOperator();
     size_t index = DType::indexOf(op);
     const DType& dt = DType::datatypeOf(op);
-- 
2.30.2