Minor fix for print benchmark. (#7821)

Also adds benchmark that triggered this issue.

diff --git a/src/smt/print_benchmark.cpp b/src/smt/print_benchmark.cpp
index 598cb9afcf3386cc8d94c266a767261267a0de8d..778a431ab3f622556a6bd43f86fb29b7c0ad3541 100644 (file)
--- 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 f2f2c77f6d92763efb078f1246ce3c77124c9033..4addbd8d1d218c5e864160564733cd43d542bf1a 100644 (file)
--- 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 (file)
index 0000000..e87b06d
--- /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)