Fix tuple and record CVC printing (#2818)

1 files changed, 22 insertions, 4 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index e6ff02f10..36d2ddfb7 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -407,12 +407,30 @@ void CvcPrinter::toStream(
     case kind::APPLY_SELECTOR_TOTAL: {
         TypeNode t = n[0].getType();
         Node opn = n.getOperator();
-        if( t.isTuple() ){
+        if (t.isTuple() || t.isRecord())
+        {
           toStream(out, n[0], depth, types, true);
+          out << '.';
           const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
-          int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() );
-          Assert( sindex>=0 );
-          out << '.' << sindex;
+          if (t.isTuple())
+          {
+            int sindex;
+            if (n.getKind() == kind::APPLY_SELECTOR)
+            {
+              sindex = Datatype::indexOf(opn.toExpr());
+            }
+            else
+            {
+              sindex = dt[0].getSelectorIndexInternal(opn.toExpr());
+            }
+            Assert(sindex >= 0);
+            out << sindex;
+          }
+          else
+          {
+            toStream(out, opn, depth, types, false);
+          }
+          return;
         }else{
           toStream(op, opn, depth, types, false);
         }