Why3 Proof Results for Project "bts1251"

Theory "Jessie_program": not fully verified

ObligationsAlt-Ergo (0.93.1)Alt-Ergo (0.94)Alt-Ergo (0.95-dev)CVC3 (2.2)CVC3 (2.2 alt)CVC3 (2.4.1)Z3 (2.19)Z3 (2.19 alt)Z3 (3.2)Z3 (4.0)
Function bsearch, default behaviorTimeoutTimeoutFailureTimeoutTimeoutTimeout0.080.080.050.06
split_goal_wp
  check0.040.010.010.030.030.040.020.010.000.00
check0.020.020.020.040.040.040.010.010.010.00
loop invariant init0.320.120.120.040.040.050.060.060.060.06
loop invariant preservationTimeoutTimeoutTimeoutTimeoutTimeoutTimeout0.070.060.060.06
split_goal_wp
  Function bsearch, default behavior0.060.030.040.060.060.07------------
Function bsearch, default behavior0.500.180.18TimeoutTimeoutTimeout------------
Function bsearch, default behavior0.140.050.060.060.060.07------------
Function bsearch, default behavior0.040.030.020.060.060.06------------
loop invariant preservationTimeoutTimeoutTimeoutTimeoutTimeoutTimeout0.060.060.060.06
split_goal_wp
  Function bsearch, default behavior0.430.150.16TimeoutTimeoutTimeout0.060.060.060.06
Function bsearch, default behavior0.050.030.040.060.060.060.060.060.060.05
Function bsearch, default behavior0.040.030.020.060.060.070.050.040.050.04
Function bsearch, default behavior0.140.060.070.060.060.070.050.060.050.06
Function bsearch, Behavior `failure'TimeoutTimeoutFailure0.060.070.070.060.060.050.05
Function bsearch, Behavior `success'0.110.06Failure0.070.070.090.050.060.040.05
Function bsearch, SafetyTimeout2.83Failure0.080.080.090.060.060.050.05
normal postcondition0.020.020.020.030.030.030.000.000.000.00
Function main, SafetyTimeoutTimeoutFailureTimeoutTimeoutTimeoutTimeoutTimeoutTimeoutTimeout
split_goal_wp
  precondition0.040.020.020.030.030.030.000.000.000.00
assertion0.040.030.010.030.030.040.040.040.040.04
precondition0.080.040.040.720.71Timeout0.200.200.090.07
preconditionTimeoutTimeoutTimeoutTimeoutTimeoutTimeoutTimeoutTimeoutTimeoutTimeout