From 2fd1db9218ebc55ad0f26c5f3faddcdf4eef2c85 Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 7 Aug 2013 16:57:02 -0700 Subject: cleaned up the OG code enabled it to be always on --- Test/test0/Answer | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/test0') 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 -- cgit v1.2.3