diff options
Diffstat (limited to 'Test/VSI-Benchmarks')
| -rw-r--r-- | Test/VSI-Benchmarks/b1.dfy | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy index ba293008..70522aaf 100644 --- a/Test/VSI-Benchmarks/b1.dfy +++ b/Test/VSI-Benchmarks/b1.dfy @@ -35,8 +35,11 @@ class Benchmark1 { method Mul(x: int, y: int) returns (r: int)
ensures r == x*y;
+ decreases x < 0, x;
{
- if (x < 0) {
+ if (x == 0) {
+ r := 0;
+ } else if (x < 0) {
call r := Mul(-x, y);
r := -r;
} else {
|