blob: 9e93495ff0957d2c93cc810fde7a6a8f65e55d6f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t
// RUN: %diff %s.expect %t
function {:existential true} b0(x:bool): bool;
var g: int;
procedure main()
modifies g;
ensures b0(g == old(g));
{
if(*) { g := 5; }
assume g != 5;
}
|
