AbsHoudini: Added support for /inlineDepth, and fixed the regression tests

(all pass)

1 files changed, 9 insertions, 7 deletions

diff --git a/Test/AbsHoudini/test1.bpl b/Test/AbsHoudini/test1.bpl
index e6ce06c9..5884cf7b 100644
--- a/Test/AbsHoudini/test1.bpl
+++ b/Test/AbsHoudini/test1.bpl
@@ -2,7 +2,7 @@ var g: bool;
 

 procedure foo() 

 modifies g;

-ensures b0 ==> (!old(g) ==> old(g) == g);

+ensures b0() || (!old(g) ==> old(g) == g);

 {

   call AcquireLock();

   call ReleaseLock();

@@ -10,14 +10,14 @@ ensures b0 ==> (!old(g) ==> old(g) == g);
 

 procedure AcquireLock()

 modifies g;

-ensures b1 ==> old(g) == g;

+ensures b1() || old(g) == g;

 {

   g := true;

 }

 

 procedure ReleaseLock()

 modifies g;

-ensures b2 ==> old(g) == g;

+ensures b2() || old(g) == g;

 {

   g := false;

 }

@@ -27,10 +27,12 @@ modifies g;
 {

   g := false;

   call foo();

-  assert !g;

+  assert Assert() || !g;

 }

 

-const {:existential true} b0: bool;

-const {:existential true} b1: bool;

-const {:existential true } b2: bool;

+function {:existential true} b0(): bool;

+function {:existential true} b1(): bool;

+function {:existential true } b2(): bool;

+function {:existential true} Assert(): bool;

 

+// Expected: b0 = false, b1 = true, b2 = true, Assert = false