diff options
Diffstat (limited to 'Test/test15/InterpretedFunctionTests.bpl')
-rw-r--r-- | Test/test15/InterpretedFunctionTests.bpl | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/Test/test15/InterpretedFunctionTests.bpl b/Test/test15/InterpretedFunctionTests.bpl index 33db52ef..5712595e 100644 --- a/Test/test15/InterpretedFunctionTests.bpl +++ b/Test/test15/InterpretedFunctionTests.bpl @@ -1,19 +1,19 @@ -// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure addition(x: int, y: int) {
- assume x == 1;
- assume y == 2;
- assert x + y == 4;
-}
-
-procedure subtraction(x: int, y: int) {
- assume x == 1;
- assume y == 2;
- assert x - y == 4; //only shows x-y == -1 when run with /method:subtraction, WHY???
-}
-
-procedure multiplication(x: int, y: int) {
- assume x == 1;
- assume y == 2;
- assert x * y == 4;
-}
+// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure addition(x: int, y: int) { + assume x == 1; + assume y == 2; + assert x + y == 4; +} + +procedure subtraction(x: int, y: int) { + assume x == 1; + assume y == 2; + assert x - y == 4; //only shows x-y == -1 when run with /method:subtraction, WHY??? +} + +procedure multiplication(x: int, y: int) { + assume x == 1; + assume y == 2; + assert x * y == 4; +} |