Refactor regressions (#1581)

1 files changed, 48 insertions, 0 deletions

diff --git a/test/regress/regress1/fmf/issue916-fmf-or.smt2 b/test/regress/regress1/fmf/issue916-fmf-or.smt2
new file mode 100644
index 000000000..0c51e39af
--- /dev/null
+++ b/test/regress/regress1/fmf/issue916-fmf-or.smt2
@@ -0,0 +1,48 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+
+(set-logic UFDTLIA)
+(set-info :smt-lib-version 2.5)
+
+(define-funs-rec
+  (
+    (validIdValue ((x Int)(v Int)) Bool)
+  )
+  (
+    (or 
+        (and (= x 0) (< (- 10) v 10) )
+        (and (= x 1) (<= (- 100) v (- 10)) )
+        (and (= x 2) (<= 10 v 100) )
+        (and (= x 3) (< (- 1000) v (- 100)) )
+        (and (= x 4) (< 100 v 1000) )
+        (and (= x 5) (<= (- 1000) v) )
+        (and (= x 6) (<= v 1000) )
+            (validIdValue (- x 7) v)
+    )
+  )
+)
+
+(declare-datatypes (T) ( (List (Nil) (Cstr (head T) (tail List) ) ) ) )
+(declare-datatypes (T S) ( (Pair (Pair (first T) (second S)) ) ) )
+
+(define-funs-rec
+  (
+    (validList ((l (List (Pair Int Int)))) Bool)
+  )
+  (
+    (ite (= l (as Nil (List (Pair Int Int))) )
+        true
+        (let ((hd (head l))) (and (>= (first hd) 0) 
+                                  (validIdValue (first hd) (second hd)) 
+                                  (validList (tail l))
+                              )
+        )
+    )
+  )
+)
+
+
+(declare-const myList (List (Pair Int Int)))
+(assert (distinct myList (as Nil (List (Pair Int Int)))))
+(assert (validList myList))
+(check-sat)