blob: 3affaa80ec102fec6725c69d88379f1fb4c7c7b1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
// The following function gives rise to an inconsistent axiom, except
// for its CanUseFunctionDefs antecedent, which saves the day.
function F(x: int): int
decreases x;
{
F(x) + 1 // error: does not decrease termination metric
}
method M()
{
assert F(5) == 0; // no error is generated here, because of the inconsistent axiom
assert false; // ditto
}
|
