test/regress/regress0/bug322.cvc


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

% EXPECT: sat
% Preamble  --------------
DATATYPE UNIT = Unit END;
DATATYPE BOOL = Truth | Falsity END;

% Decls     --------------
node$type: TYPE;
value$type: TYPE;
Nodes$elem$type: TYPE = node$type;
Nodes$t$type: TYPE;
node_pair_set$type: TYPE = ARRAY node$type OF ARRAY node$type OF BOOL;
failure_pattern$type: TYPE = node_pair_set$type;
is_faulty:(node$type, failure_pattern$type) -> BOOL = (LAMBDA (p: node$type, 
                                                               deliver: failure_pattern$type): 
                                                      (IF (EXISTS (q: node$type): 
                                                          (NOT ((((deliver)[
                                                                 (p)])[
                                                                (q)]) = 
                                                               (Truth)))) THEN 
                                                      (Truth) ELSE (Falsity) ENDIF));

CHECKSAT;