Enabled the inline lit tests. In order to support expansion2.bpl

we now require the OutputCheck tool. The lit.site.cfg file has
been taught to require that this tool is in the user's PATH
before testing starts.

1 files changed, 5 insertions, 0 deletions

diff --git a/Test/inline/expansion2.bpl b/Test/inline/expansion2.bpl
index b6ed19ed..da13d50f 100644
--- a/Test/inline/expansion2.bpl
+++ b/Test/inline/expansion2.bpl
@@ -1,3 +1,6 @@
+// RUN: %boogie -proverLog:%T/expand2.sx %s > %t

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

+// RUN: %OutputCheck --file-to-check=%T/expand2.sx %s

 function {:inline true} xxgz(x:int) returns(bool)

  { x > 0 }

 function {:inline true} xxf1(x:int,y:bool) returns(int)

@@ -8,7 +11,9 @@ axiom (forall y:int, x:bool :: xxf1(y, x) > 1 ==> y > 0);
 

 procedure foo()

 {

+  // CHECK-NOT-L: xxgz

   assert xxgz(12);

+  // CHECK-NOT-L: xxf1

   assert xxf1(3,true) == 4;

 }