3 files changed, 22 insertions, 4 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index a3ff2fcc7..aa3508798 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -51,7 +51,8 @@ TESTS =	\
 	fmc_unsound_model.smt2 \
 	am-bad-model.cvc \
 	nun-0208-to.smt2 \
-	datatypes-ufinite.smt2
+	datatypes-ufinite.smt2 \
+	datatypes-ufinite-nested.smt2
 
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2 b/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2
new file mode 100644
index 000000000..3ffc36d05
--- /dev/null
+++ b/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(assert (distinct a b c))
+(declare-sort V 0)
+(declare-datatypes () ((ufin1 (cons1 (s11 U) (s13 ufin2))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3))))
+(declare-fun P (ufin1 ufin2) Bool)
+(declare-fun Q (ufin1 ufin1) Bool)
+(assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z))))
+(assert (not (P (cons1 a cons3) cons3)))
+(assert (not (Q (cons1 b cons3) (cons1 a cons3))))
+(check-sat)
diff --git a/test/regress/regress0/fmf/datatypes-ufinite.smt2 b/test/regress/regress0/fmf/datatypes-ufinite.smt2
index d802930fd..3564bff8b 100644
--- a/test/regress/regress0/fmf/datatypes-ufinite.smt2
+++ b/test/regress/regress0/fmf/datatypes-ufinite.smt2
@@ -8,10 +8,10 @@
 (declare-fun d () U)
 (assert (distinct a b c))
 (declare-sort V 0)
-(declare-datatypes () ((ufin1 (cons1 (s11 U) (s12 U) (s13 U))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3))))
+(declare-datatypes () ((ufin1 (cons1 (s11 U) (s12 U))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3))))
 (declare-fun P (ufin1 ufin2) Bool)
 (declare-fun Q (ufin1 ufin1) Bool)
 (assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z))))
-(assert (not (P (cons1 a a a) cons3)))
-(assert (not (Q (cons1 a d a) (cons1 a b c))))
+(assert (not (P (cons1 a a) cons3)))
+(assert (not (Q (cons1 a d) (cons1 a b))))
 (check-sat)