diff options
Diffstat (limited to 'test/regress/regress0/fmf/issue916-fmf-or.smt2')
-rw-r--r-- | test/regress/regress0/fmf/issue916-fmf-or.smt2 | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/test/regress/regress0/fmf/issue916-fmf-or.smt2 b/test/regress/regress0/fmf/issue916-fmf-or.smt2 new file mode 100644 index 000000000..0c51e39af --- /dev/null +++ b/test/regress/regress0/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) |