Move `fmf.card` printing code. (#7559)

The code for printing fmf.card does not run in its current location. This PR moves the code to a different switch statement to ensure that it runs.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index d6e6fc4eb466e62f828da037e67cd3602c2a05da..da8e564485b10d66a3483b4a4cccf4e16ceadbca 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -332,13 +332,6 @@ void Smt2Printer::toStream(std::ostream& out,
       out << ss.str();
       break;
     }
-    case kind::CARDINALITY_CONSTRAINT:
-      out << "(_ fmf.card ";
-      out << n.getConst<CardinalityConstraint>().getType();
-      out << " ";
-      out << n.getConst<CardinalityConstraint>().getUpperBound();
-      out << ")";
-      break;
     case kind::EMPTYSET:
       out << "(as emptyset ";
       toStreamType(out, n.getConst<EmptySet>().getType());
@@ -818,6 +811,15 @@ void Smt2Printer::toStream(std::ostream& out,
     out << "(as sep.nil " << n.getType() << ")";
     break;
 
+  // cardinality constraints.
+  case kind::CARDINALITY_CONSTRAINT:
+    out << "(_ fmf.card ";
+    out << n.getOperator().getConst<CardinalityConstraint>().getType();
+    out << " ";
+    out << n.getOperator().getConst<CardinalityConstraint>().getUpperBound();
+    out << ")";
+    return;
+
     // quantifiers
   case kind::FORALL:
   case kind::EXISTS: