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

(all pass)

1 files changed, 6 insertions, 2 deletions

diff --git a/Test/AbsHoudini/test8.bpl b/Test/AbsHoudini/test8.bpl
index 12eab481..6c55016a 100644
--- a/Test/AbsHoudini/test8.bpl
+++ b/Test/AbsHoudini/test8.bpl
@@ -1,3 +1,5 @@
+function {:existential true} Assert(): bool;

+

 var g: int;

 

 procedure main() 

@@ -5,7 +7,7 @@ modifies g;
 {

   g := 0;

   call foo();

-  assert g == 1;

+  assert Assert() || g == 1;

 }

 

 procedure {:inline 1} foo() 

@@ -18,4 +20,6 @@ procedure bar()
 modifies g;

 {

   g := g + 1;

-}
\ No newline at end of file
+}

+

+// Expected: Assert = false