diff options
| author |  Rustan Leino <leino@microsoft.com> | 2013-01-17 19:06:42 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2013-01-17 19:06:42 -0800 |
| commit | 30daf75f78b331e971ba08cf794ec006441a722b (patch) | |
| tree | b35c1ced50bb4a63c27c0a85ade91c4d5ea63747 /Test/inline | |
| parent | ce2acb7725a7ccc51405e966174796b3f54a8673 (diff) | |
Refactored code that generates an axiom for a function, and changed the pretty printing to always reflect when a function body is inlined
Diffstat (limited to 'Test/inline')
| -rw-r--r-- | Test/inline/Answer | 2 |
1 files changed, 0 insertions, 2 deletions
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
|