diff options
| author |  qadeer <unknown> | 2013-08-07 16:57:02 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2013-08-07 16:57:02 -0700 |
| commit | 2fd1db9218ebc55ad0f26c5f3faddcdf4eef2c85 (patch) | |
| tree | ee58fbfdd972b0bdf5b5883e6c894da623fc1a60 /Test/test0 | |
| parent | a9c60110139c15ec65c50360763c75014b9eef82 (diff) | |
cleaned up the OG code
enabled it to be always on
Diffstat (limited to 'Test/test0')
| -rw-r--r-- | Test/test0/Answer | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/test0/Answer b/Test/test0/Answer index 8c7ce4c7..f92dd1dc 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -123,8 +123,8 @@ axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x Boogie program verifier finished with 0 verified, 0 errors
Boogie program verifier finished with 0 verified, 0 errors
-Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q
-Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q
+Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
2 type checking errors detected in Arrays1.bpl
Types0.bpl(6,18): error: expected identifier before ':'
Types0.bpl(6,12): error: expecting an identifier as parameter name
|