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

% 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback