diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
commit | d652155ae013f36a1ee17653a8e458baad2d9c2c (patch) | |
tree | 067d600fe3cd1723afc11682935f0123a1eab653 /Test/test2/Axioms.bpl | |
parent | d7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff) |
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Test/test2/Axioms.bpl')
-rw-r--r-- | Test/test2/Axioms.bpl | 62 |
1 files changed, 31 insertions, 31 deletions
diff --git a/Test/test2/Axioms.bpl b/Test/test2/Axioms.bpl index 1fa8fab3..51d9ed00 100644 --- a/Test/test2/Axioms.bpl +++ b/Test/test2/Axioms.bpl @@ -1,31 +1,31 @@ -// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const Seven: int;
-axiom Seven == 7;
-
-function inc(int) returns (int);
-axiom (forall j: int :: inc(j) == j+1);
-
-procedure P()
-{
- start:
- assert 4 <= Seven;
- assert Seven < inc(Seven);
- assert inc(5) + inc(inc(2)) == Seven + 3;
- return;
-}
-
-procedure Q()
-{
- start:
- assert inc(5) + inc(inc(2)) == Seven; // error
- return;
-}
-
-function inc2(x:int) returns(int) { x + 2 }
-
-procedure ExpandTest()
-{
- var q:int;
- assert inc(inc(q)) == inc2(q);
-}
+// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +const Seven: int; +axiom Seven == 7; + +function inc(int) returns (int); +axiom (forall j: int :: inc(j) == j+1); + +procedure P() +{ + start: + assert 4 <= Seven; + assert Seven < inc(Seven); + assert inc(5) + inc(inc(2)) == Seven + 3; + return; +} + +procedure Q() +{ + start: + assert inc(5) + inc(inc(2)) == Seven; // error + return; +} + +function inc2(x:int) returns(int) { x + 2 } + +procedure ExpandTest() +{ + var q:int; + assert inc(inc(q)) == inc2(q); +} |