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 27 28
|
-- rumur_flags: self.config['SMT_ARGS']
-- skip_reason: 'no SMT solver available' if self.config['SMT_ARGS'] is None else None
-- test whether the SMT bridge can simplify expressions involving records with
-- boolean fields
type
t: record
x: boolean;
end;
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.x = x.x then
y := !y;
end;
end;
|