From bc08d6ada809232678abe605dc30386888da2c27 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 16 Dec 2021 11:50:25 -0600
Subject: [PATCH] Minor fix for print benchmark. (#7821)

Also adds benchmark that triggered this issue.
---
 src/smt/print_benchmark.cpp                     |  6 +++---
 test/regress/CMakeLists.txt                     |  1 +
 .../regress0/datatypes/mutual-rec-param-dt.smt2 | 17 +++++++++++++++++
 3 files changed, 21 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/regress0/datatypes/mutual-rec-param-dt.smt2

diff --git a/src/smt/print_benchmark.cpp b/src/smt/print_benchmark.cpp
index 598cb9afc..778a431ab 100644
--- a/src/smt/print_benchmark.cpp
+++ b/src/smt/print_benchmark.cpp
@@ -55,11 +55,11 @@ void PrintBenchmark::printAssertions(std::ostream& out,
       std::vector<TypeNode> datatypeBlock;
       for (const TypeNode& ctn : connectedTypes)
       {
-        if (stc.isSort())
+        if (ctn.isSort())
         {
-          d_printer->toStreamCmdDeclareType(out, stc);
+          d_printer->toStreamCmdDeclareType(out, ctn);
         }
-        else if (stc.isDatatype())
+        else if (ctn.isDatatype())
         {
           datatypeBlock.push_back(ctn);
         }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f2f2c77f6..4addbd8d1 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -509,6 +509,7 @@ set(regress_0_tests
   regress0/datatypes/list-update.smt2
   regress0/datatypes/list-update-sat.smt2
   regress0/datatypes/model-subterms-min.smt2
+  regress0/datatypes/mutual-rec-param-dt.smt2
   regress0/datatypes/mutually-recursive.cvc.smt2
   regress0/datatypes/pair-bool-bool.cvc.smt2
   regress0/datatypes/pair-real-bool.smt2
diff --git a/test/regress/regress0/datatypes/mutual-rec-param-dt.smt2 b/test/regress/regress0/datatypes/mutual-rec-param-dt.smt2
new file mode 100644
index 000000000..e87b06de4
--- /dev/null
+++ b/test/regress/regress0/datatypes/mutual-rec-param-dt.smt2
@@ -0,0 +1,17 @@
+
+
+(set-logic ALL)
+(set-option :produce-models true)
+(set-info :status sat)
+(declare-datatypes ( (List 1) (List2 1) ) (
+(par ( X ) 
+( (cons (head X) (tail (List2 X))) (nil))
+)
+(par ( Y ) 
+( (cons2 (head2 Y) (tail2 (List Y))) (nil))
+)
+))
+(declare-fun a () (List Int))
+(declare-fun b () (List Int))
+(assert (= (head a) 5))
+(check-sat)
-- 
2.30.2