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

(all pass)

1 files changed, 11 insertions, 8 deletions

diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl
index abb993f7..a30c3159 100644
--- a/Test/AbsHoudini/test10.bpl
+++ b/Test/AbsHoudini/test10.bpl
@@ -1,9 +1,9 @@
 var sdv_7: int;

 var sdv_21: int;

-const {:existential true} b1: bool;

-const{:existential true}  b2: bool;

-const{:existential true}  b3: bool;

-const{:existential true}  b4: bool;

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

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

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

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

 

 procedure push(a:int)

 modifies sdv_7, sdv_21;

@@ -21,8 +21,8 @@ modifies sdv_7, sdv_21;
 

 procedure foo()

 modifies sdv_7, sdv_21;

-requires {:candidate} b1 ==> (sdv_7 == 0);

-ensures{:candidate}  b2 ==> (sdv_7 == old(sdv_7));

+requires {:candidate} b1() || (sdv_7 == 0);

+ensures{:candidate}  b2() || (sdv_7 == old(sdv_7));

 {

    call push(2);

    call pop();

@@ -30,8 +30,8 @@ ensures{:candidate}  b2 ==> (sdv_7 == old(sdv_7));
 }

 

 procedure bar()

-requires{:candidate} b3 ==> (sdv_7 == 0);

-ensures{:candidate}  b4 ==> (sdv_7 == old(sdv_7));

+requires{:candidate} b3() || (sdv_7 == 0);

+ensures{:candidate}  b4() || (sdv_7 == old(sdv_7));

 modifies sdv_7, sdv_21;

 {

    call push(1);

@@ -45,3 +45,6 @@ modifies sdv_7, sdv_21;
    call foo();

 }

 

+// Expected: All false

+

+