test/regress/regress1/quantifiers/mutualrec2.cvc


1
2
3
4
5
6
7
8
9
10
11
12
13
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;