diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-05 19:51:59 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-05 19:51:59 +0100 |
commit | 3b38b009d086c601cae884ad62ceeb9bb16ae5d5 (patch) | |
tree | 3c06797a3003d92166606a8ddd12881f412d076f /Test/test0/PrettyPrint.bpl.expect | |
parent | ccf94ed737752c21edff3cab8a71de0766a48d1c (diff) |
Enabled most of the name resolution lit tests. They don't all pass
yet due to a bug in -useBaseNameForFileName.
Diffstat (limited to 'Test/test0/PrettyPrint.bpl.expect')
-rw-r--r-- | Test/test0/PrettyPrint.bpl.expect | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/Test/test0/PrettyPrint.bpl.expect b/Test/test0/PrettyPrint.bpl.expect new file mode 100644 index 00000000..f6f0f995 --- /dev/null +++ b/Test/test0/PrettyPrint.bpl.expect @@ -0,0 +1,93 @@ +const x: int; + +const y: int; + +const z: int; + +const r: real; + +const s: real; + +const t: real; + +const P: bool; + +const Q: bool; + +const R: bool; + +axiom x * (y + z) == x + y * z; + +axiom x * y + z == (x + y) * z; + +axiom x * y * z == x * y * z; + +axiom x * y * z * x == x * y * z; + +axiom x div y div z == x div (y div z); + +axiom x div y div (z div x) == x div y div z; + +axiom x + y mod z == y mod z + x; + +axiom (x + y) mod z == x mod z + y mod z; + +axiom x / y / z == x / (y / z); + +axiom x / y / (z / x) == x / y / z; + +axiom x / s / z == x / (s / z); + +axiom x / s / (z / x) == x / s / z; + +axiom r / s / t == r / (s / t); + +axiom r / s / (t / r) == r / s / t; + +axiom r * s / t == r * s / t; + +axiom r / s * t == r / s * t; + +axiom (r * s) ** t == r ** t * s ** t; + +axiom r ** (s + t) == r ** s * r ** t; + +axiom int(real(x)) == x; + +axiom r >= 0e0 ==> real(int(r)) <= r; + +axiom int(0e0 - 2e-2) == 0; + +axiom int(0e0 - 35e0) == -35; + +axiom int(27e-1) == 2; + +axiom x - y - z == x - (y - z); + +axiom x - y - (z - x) == x - y - z; + +axiom x + y - z - x + y == 0; + +axiom x + y - z - x + y == x + y - (z - (x + y)); + +axiom P ==> Q ==> R <==> P ==> Q ==> R; + +axiom (P ==> Q) ==> R ==> P <==> (P ==> Q) ==> R; + +axiom P <==> Q <==> R; + +axiom P ==> Q <==> Q ==> R <==> R ==> P; + +axiom (P && Q) || (Q && R); + +axiom (P || Q) && (Q || R); + +axiom P || Q || Q || R; + +axiom P && Q && Q && R; + +function f(int) : int; + +axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x + x) } { f(x) * f(x) } {:nopats f(x + x + x) } f(f(x)) < 200); + +Boogie program verifier finished with 0 verified, 0 errors |