File tree Expand file tree Collapse file tree 2 files changed +23
-5
lines changed Expand file tree Collapse file tree 2 files changed +23
-5
lines changed Original file line number Diff line number Diff line change
1
+ method main () {
2
+ var x : Int ;
3
+ var y : Int ;
4
+ var z : Int ;
5
+ assume x >= 0 && y >= 0 ;
6
+ z := x - y ;
7
+ match {
8
+ z < 0 = >
9
+ z := z + y ;
10
+ z := z + 2 * x,
11
+ true = >
12
+ z := z - x ;
13
+ z := z + 4 * y,
14
+ };
15
+ // @CheckError
16
+ assert (z < 0 && z == x - y + 2 * x) || (z >= 0 && z == x - y + 4 * y);
17
+ assert (z < 0 && z == x - y + y + 2 * x) || (z >= 0 && z == x - y - x + 4 * y)
18
+ }
Original file line number Diff line number Diff line change @@ -3,14 +3,14 @@ method main () {
3
3
var y : Int ;
4
4
var z : Int ;
5
5
assume x >= 0 && y >= 0 ;
6
- z := x - y ;
6
+ z := x - y ;
7
7
match {
8
8
z < 0 = >
9
9
z := z + y ;
10
- z := z + 2 * x,
10
+ z := z + 2 * x,
11
11
true = >
12
- z := z - x ;
13
- z := z + 4 * y,
12
+ z := z - x ;
13
+ z := z + 4 * y,
14
14
};
15
- assert z <= 3 * x && z <= 3 * y && ( z == 3 * x || z == 3 * y )
15
+ assert z <= 3 * x && z <= 3 * y && ( z == 3 * x || z == 3 * y )
16
16
}
You can’t perform that action at this time.
0 commit comments