From 30daf75f78b331e971ba08cf794ec006441a722b Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 17 Jan 2013 19:06:42 -0800 Subject: Refactored code that generates an axiom for a function, and changed the pretty printing to always reflect when a function body is inlined --- Test/inline/Answer | 2 -- 1 file changed, 2 deletions(-) (limited to 'Test/inline') diff --git a/Test/inline/Answer b/Test/inline/Answer index ff2a5e71..aaaa138c 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -1517,12 +1517,10 @@ function {:inline true} foo(x: int) : bool function {:inline false} foo2(x: int) : bool; -// autogenerated definition axiom axiom (forall x: int :: {:inline false} { foo2(x): bool } foo2(x): bool == (x > 0)); function foo3(x: int) : bool; -// autogenerated definition axiom axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0)); Boogie program verifier finished with 0 verified, 0 errors -- cgit v1.2.3