Fix non-termination in datatype type enumerator (#3369)

1 files changed, 22 insertions, 0 deletions

diff --git a/test/regress/regress1/quantifiers/issue3316.smt2 b/test/regress/regress1/quantifiers/issue3316.smt2
new file mode 100644
index 000000000..320a57790
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue3316.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --fmf-fun-rlv --no-check-models
+; EXPECT: sat
+(set-info :smt-lib-version 2.5)
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatypes () ((a0(c0$0)(c0$1(c0$1$0 String)(c0$1$1 Int))(c0$2(c0$2$0 Bool)(c0$2$1 Int)(c0$2$2 String)))
+                       (a1(c1$0)(c1$1)(c1$2))
+                       (a2(c2$0(c2$0$0 Int)(c2$0$1 a0)(c2$0$2 String)(c2$0$3 a3)(c2$0$4 String)(c2$0$5 Bool)))
+                       (a3(c3$0(c3$0$0 a7)(c3$0$1 a1)(c3$0$2 a5)(c3$0$3 a6)(c3$0$4 Int)(c3$0$5 Bool)(c3$0$6 Bool))(c3$1(c3$1$0 String)))
+                       (a4(c4$0(c4$0$0 String)(c4$0$1 a2)(c4$0$2 String))(c4$1(c4$1$0 a0)(c4$1$1 a4)(c4$1$2 a4)(c4$1$3 a7))(c4$2))
+                       (a5(c5$0(c5$0$0 a2))(c5$1)(c5$2)(c5$3(c5$3$0 a0))(c5$4)(c5$5(c5$5$0 a4)(c5$5$1 Int))(c5$6))
+                       (a6(c6$0(c6$0$0 a7)(c6$0$1 a7)(c6$0$2 String))(c6$1)(c6$2)(c6$3)(c6$4)(c6$5)(c6$6))
+                       (a7(c7$0(c7$0$0 a2)(c7$0$1 Int))(c7$1(c7$1$0 a4)(c7$1$1 Int)(c7$1$2 Bool)))))
+(define-funs-rec ((f3((v4 Bool))a7)
+                  (f2()a6)
+                  (f1((v1 a3)(v2 a1)(v3 Bool))String)
+                  (f0((v0 a6))a4))
+                  ((c7$0 (c2$0 0 c0$0 "" (c3$1 "") "" true) 0) 
+                  c6$2 
+                  "" 
+                  c4$2))
+(check-sat)