1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress0/fmf/bug652.smt2 b/test/regress/regress0/fmf/bug652.smt2
new file mode 100644
index 000000000..13748eeea
--- /dev/null
+++ b/test/regress/regress0/fmf/bug652.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic UFDTSLIA)
+(set-info :smt-lib-version 2.5)
+(set-option :produce-models true)
+
+(declare-datatypes () (
+    (List_boolean (List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean)))
+) )
+
+(define-funs-rec
+  (
+    (f4208$lengthList_boolean((x List_boolean)) Int)
+  )
+  (
+    (ite (is-List_boolean$CNil_boolean x) 0 (+ 1 (f4208$lengthList_boolean (List_boolean$Cstr_boolean$tail x))))
+  )
+)
+
+
+(declare-const boolean Bool)
+(check-sat)