Fix printer for datatype udpater (#7208)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b92d8fa431fc7842729bbd7662a1c4813b4d30e0..6217276b1698241f4744c945fe4cae305059fe36 100644 (file)
--- 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);