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/AbsHoudini/imp1.bpl | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) (limited to 'Test/AbsHoudini/imp1.bpl') diff --git a/Test/AbsHoudini/imp1.bpl b/Test/AbsHoudini/imp1.bpl index 29cbf567..09be87e7 100644 --- a/Test/AbsHoudini/imp1.bpl +++ b/Test/AbsHoudini/imp1.bpl @@ -1,21 +1,21 @@ -function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool; -function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool; - -var x: int; -var flag: bool; - -procedure foo () - modifies x, flag; - ensures b1(flag, x == 0); -{ - flag := true; - x := 0; -} - -procedure bar() - modifies x, flag; - ensures b2(flag, x == 0); -{ - flag := false; - x := 0; -} +function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool; +function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool; + +var x: int; +var flag: bool; + +procedure foo () + modifies x, flag; + ensures b1(flag, x == 0); +{ + flag := true; + x := 0; +} + +procedure bar() + modifies x, flag; + ensures b2(flag, x == 0); +{ + flag := false; + x := 0; +} -- cgit v1.2.3