ESC/Java version ESCJava-2.0a8
    [0.23 s 12407936 bytes]

demo.Testee ...
  Prover started:0.05 s 14582560 bytes
    [1.592 s 14014248 bytes]

demo.Testee: inverse(int) ...
------------------------------------------------------------------------
demo\Testee.java:15: Warning: Possible division by zero (ZeroDiv)
                        return 1/0;  //Represents a real bug in this e ...
                                ^
Execution trace information:
    Executed then branch in "demo\Testee.java", line 14, col 15.

------------------------------------------------------------------------
demo\Testee.java:18: Warning: Possible division by zero (ZeroDiv)
                return 1/i;  //Passing 0 is not a real bug, since it v ...
                        ^
Execution trace information:
    Executed else branch in "demo\Testee.java", line 14, col 2.

------------------------------------------------------------------------
    [0.631 s 14772240 bytes]  failed

demo.Testee: Testee() ...
    [0.02 s 14862760 bytes]  passed
  [2.243 s 14885352 bytes total]
2 warnings
runtime = 4 seconds.
