From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 2 Nov 2021 21:45:44 +0000 (-0500)
Subject: Move `fmf.card` printing code. (#7559)
X-Git-Tag: cvc5-1.0.0~905
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0c16abf2d7fe9a18494d3c9867567c43a1655200;p=cvc5.git

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 d6e6fc4eb..da8e56448 100644
--- 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: