1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
-- rumur_flags: smt_args()
-- skip_reason: 'no SMT solver available' if smt_args() is None else None
-- slight variant on smt-array-range.m with a pre-defined type
type
r: 0 .. 1;
t: array[r] of r;
var
x: t;
y: boolean;
startstate begin
y := true;
end;
rule begin
/* if the SMT bridge is working correctly, it will simplify the condition in
* the following expression to `true` avoiding the read of an undefined
* variable
*/
if x[0] = x[0] then
y := !y;
end;
end;
|
