From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Test/z3api/boog16.bpl | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'Test/z3api/boog16.bpl') diff --git a/Test/z3api/boog16.bpl b/Test/z3api/boog16.bpl index a002c166..6e741cbf 100644 --- a/Test/z3api/boog16.bpl +++ b/Test/z3api/boog16.bpl @@ -1,12 +1,12 @@ -type ref; -function choose(a:bool, b:int, c:int) returns (x:int); -axiom(forall a:bool, b:int, c:int :: - {choose(a,b,c)} !a ==> choose(a,b,c) == c); - -var myInt:int; -procedure main() -modifies myInt; -ensures myInt==5; -{ - myInt:=4; +type ref; +function choose(a:bool, b:int, c:int) returns (x:int); +axiom(forall a:bool, b:int, c:int :: + {choose(a,b,c)} !a ==> choose(a,b,c) == c); + +var myInt:int; +procedure main() +modifies myInt; +ensures myInt==5; +{ + myInt:=4; } \ No newline at end of file -- cgit v1.2.3