Commits

Nadia Polikarpova  committed d56b6dc Draft

Edited online

  • Participants
  • Parent commits 5e4f5f6

Comments (0)

Files changed (1)

 If instead you test this program with Boogaloo, like so:
 
 {{{
-boogaloo test --proc F McCarthy-91.bpl
+boogaloo test McCarthy-91.bpl
 }}}
 
 it will produce the following output:
 
 {{{
-Test cases: 8
-Passed: 0
-Invalid: 0
-Non executable: 0
-Failed: 8 (1 unique)
-
-Failure 0
-F(0) failed
-
-Postcondition "n <= 100 ==> r == 91" defined at McCarthy-91.bpl line 2 violated at McCarthy-91.bpl line 1 with
-    n = 100
-    r = 90
-in call to F at examples/McCarthy-91.bpl line 8
-...
+Execution 0: F(100) failed
+Postcondition "n <= 100 ==> r == 91" defined at McCarthy-91.bpl line 2 
+violated at McCarthy-91.bpl line 1 with
+    n -> 100
+    r -> 90
+in call to F
 }}}
 
 The failing test case hints us at the problem: