summaryrefslogtreecommitdiff
path: root/test/regress/regress0/preprocess/preprocess_11.cvc
blob: 13a8f532cb28f7f5dcfc783ef9d50cd711f538a8 (plain) 
1
2
3
4
5
6
7
8
9
10
11

% EXPECT: sat

x: REAL;
y: REAL;

ASSERT ((0 = IF TRUE THEN x ELSE 1 ENDIF) AND (0 = IF (x = 0) THEN 0 ELSE 1 ENDIF) AND (x = IF TRUE THEN y ELSE 0 ENDIF) AND (0 = IF TRUE THEN 0 ELSE 0 ENDIF));

CHECKSAT;

% EXIT: 10
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback