diff options
Diffstat (limited to 'test/regress/regress2/quantifiers/mutualrec2.cvc')
| -rw-r--r-- | test/regress/regress2/quantifiers/mutualrec2.cvc | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress2/quantifiers/mutualrec2.cvc b/test/regress/regress2/quantifiers/mutualrec2.cvc new file mode 100644 index 000000000..66da896ae --- /dev/null +++ b/test/regress/regress2/quantifiers/mutualrec2.cvc @@ -0,0 +1,14 @@ +% EXPECT: unsat +OPTION "fmf-fun"; +REC-FUN iseven : (INT) -> INT, isodd : (INT) -> INT, fact : INT -> INT = +LAMBDA (x : INT): IF (x = 0) THEN 1 ELSE (IF (isodd(x - 1) = 0) THEN 1 ELSE 0 ENDIF) ENDIF, +LAMBDA (y : INT): IF (y = 0) THEN 0 ELSE (IF (iseven(y - 1) = 0) THEN 1 ELSE 0 ENDIF) ENDIF, +LAMBDA (x : INT): IF (x = 0) THEN 1 ELSE x * fact(x - 1) ENDIF; +a,b,x,y,z : INT; +ASSERT 1 = isodd(4); +ASSERT 0 = iseven(4); +ASSERT 0 = isodd(3); +ASSERT 1 = iseven(3); +ASSERT NOT (24 = fact(4)); +CHECKSAT; + |