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

(all pass)

1 files changed, 6 insertions, 2 deletions

diff --git a/Test/AbsHoudini/test7.bpl b/Test/AbsHoudini/test7.bpl
index b5c6a4c6..bfe8a32d 100644
--- a/Test/AbsHoudini/test7.bpl
+++ b/Test/AbsHoudini/test7.bpl
@@ -1,3 +1,5 @@
+function {:existential true} Assert() : bool;

+

 var g: int;

 

 procedure main() 

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

   g := 0;

   call foo();

-  assert g == 1;

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

 }

 

 procedure foo() 

 modifies g;

 {

   g := g + 1;

-}
\ No newline at end of file
+}

+

+// Expected: Assert = false