more minor fix to test case houdini\testUnsatCore.bpl

1 files changed, 16 insertions, 1 deletions

diff --git a/Test/houdini/testUnsatCore.bpl b/Test/houdini/testUnsatCore.bpl
index 9c7ef8ad..19066269 100644
--- a/Test/houdini/testUnsatCore.bpl
+++ b/Test/houdini/testUnsatCore.bpl
@@ -1,6 +1,7 @@
 // RUN: %boogie -noinfer -contractInfer -printAssignment -useUnsatCoreForContractInfer "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

-var g: bool;

+

+// Example to exercise the unsatcore to optimize houdini

 

 procedure foo(x:int, y:int, z:int)

 //requires

@@ -13,6 +14,11 @@ ensures  be0 ==> x == 1;
    

 }

 

+procedure bar()

+{

+   call foo(1, 2, 3);

+

+}

 

 const {:existential true} br0: bool;

 const {:existential true} br1: bool;

@@ -20,3 +26,12 @@ const {:existential true} br2: bool;
 const {:existential true} be0: bool;

 

 

+// The output does not have any details to illustrate the flag (its an optimization)

+// One way to make sure it works is to run with -trace

+//

+// $boogie_codeplex\binaries\boogie.exe -noinfer -contractInfer -printAssignment -trace testUnsatCore.bpl

+//

+// and lookout for the following lines

+//

+// Number of unsat core prover queries = 2

+// Number of unsat core prunings = 2
\ No newline at end of file