Why3 Proof Results for Project "blocking_semantics5"

Theory "Syntax": fully verified

ObligationsAlt-Ergo (0.93.1)Alt-Ergo (0.94)
mident_decide0.010.00
ident_decide0.000.01
decide_is_skip0.010.01

Theory "SemOp": fully verified

ObligationsAlt-Ergo (0.93.1)Alt-Ergo (0.94)CVC3 (2.2)CVC3 (2.4.1)Coq (8.3pl4)Z3 (3.2)Z3 (4.2)
get_stack_eq0.010.010.030.02---Timeout (5s)Timeout (5s)
get_stack_neq0.020.010.030.02---Timeout (5s)Timeout (5s)
steps_non_neg------------0.53------

Theory "TestSemantics": fully verified

ObligationsAlt-Ergo (0.93.1)Alt-Ergo (0.94)Coq (8.3pl4)
Test130.020.02---
Test420.030.02---
Test00.050.03---
Test550.57------
Ass420.460.10---
If42------1.33

Theory "TypingAndSemantics": fully verified

ObligationsAlt-Ergo (0.93.1)Alt-Ergo (0.94)CVC3 (2.2)CVC3 (2.4.1)Coq (8.3pl4)Z3 (3.2)Z3 (4.2)
type_inversion0.030.020.04Timeout (5s)1.02Timeout (5s)Timeout (5s)
induction_ty_lex
  1.0.080.050.04Timeout (5s)---0.070.07
eval_type_term---------------------
induction_ty_lex
  1.---------------------
split_goal_wp
  1.0.500.130.180.23---Timeout (5s)Timeout (5s)
2.0.620.140.270.31---Timeout (5s)Timeout (5s)
3.0.660.220.060.07---Timeout (5s)Timeout (5s)
4.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)4.14Timeout (5s)Timeout (5s)
type_preservation------------7.04------

Theory "FreshVariables": fully verified

ObligationsAlt-Ergo (0.93.1)Alt-Ergo (0.94)CVC3 (2.2)CVC3 (2.4.1)Coq (8.3pl4)Z3 (3.2)Z3 (4.2)
Cons_append0.03------------------
Append_nil_l0.03------------------
eval_msubst_term---------------------
induction_ty_lex
  1.---------------------
split_goal_wp
  1.0.040.030.040.04---Timeout (5s)Timeout (5s)
2.0.040.020.040.04---Timeout (5s)Timeout (5s)
3.0.050.030.040.04---Timeout (5s)Timeout (5s)
4.0.120.03Timeout (5s)Timeout (5s)---Timeout (5s)Timeout (5s)
eval_msubst---------------------
induction_ty_lex
  1.---------------------
split_goal_wp
  1.0.050.02Timeout (30s)Timeout (30s)---Timeout (30s)Timeout (30s)
2.0.040.02Timeout (30s)Timeout (30s)---Timeout (30s)Timeout (30s)
3.0.200.05Timeout (30s)Timeout (30s)---Timeout (30s)Out Of Memory (1000M)
4.0.060.04Timeout (30s)Timeout (30s)---Timeout (30s)Timeout (30s)
5.0.040.03Timeout (30s)Timeout (30s)---Timeout (30s)Timeout (30s)
6.0.040.03Timeout (30s)Timeout (30s)---Timeout (30s)Timeout (30s)
7.0.070.03Timeout (30s)Timeout (30s)---Timeout (30s)Out Of Memory (1000M)
8.0.030.04Timeout (30s)Timeout (30s)---Timeout (30s)Timeout (30s)
9.Timeout (5s)4.15Timeout (30s)Timeout (30s)0.78Timeout (30s)Out Of Memory (1000M)
10.0.330.11Timeout (30s)Timeout (30s)---Timeout (30s)Timeout (30s)
11.Timeout (5s)Timeout (30s)Timeout (30s)Timeout (30s)1.99Timeout (30s)Timeout (30s)
12.2.550.80Timeout (30s)Timeout (30s)---Timeout (30s)Out Of Memory (1000M)
eval_swap_term---------------------
induction_ty_lex
  1.---------------------
split_goal_wp
  1.0.040.030.040.08---Out Of Memory (1000M)Out Of Memory (1000M)
2.Timeout (5s)Timeout (30s)Timeout (30s)Timeout (30s)1.26Out Of Memory (1000M)Out Of Memory (1000M)
3.0.050.030.060.05---Out Of Memory (1000M)Out Of Memory (1000M)
4.0.180.0719.4624.35---Out Of Memory (1000M)Out Of Memory (1000M)
eval_swap_gen---------------------
induction_ty_lex
  1.---------------------
split_goal_wp
  1.0.160.070.410.46---Timeout (30s)Timeout (30s)
2.0.150.060.440.47---Timeout (30s)Timeout (30s)
3.0.380.138.868.79---Timeout (30s)Timeout (30s)
4.0.380.144.209.18---Timeout (30s)Timeout (30s)
5.0.170.074.684.82---Timeout (30s)Timeout (30s)
6.0.160.075.055.21---Timeout (30s)Timeout (30s)
7.0.040.044.199.03---Timeout (30s)Timeout (30s)
8.0.040.048.518.96---Timeout (30s)Timeout (30s)
9.1.140.39Timeout (30s)Timeout (30s)---Timeout (30s)Timeout (30s)
10.1.070.41Timeout (30s)Timeout (30s)---Timeout (30s)Timeout (30s)
11.8.81Timeout (30s)Timeout (30s)Timeout (30s)1.93Timeout (30s)Timeout (30s)
12.8.88Timeout (30s)Timeout (30s)Timeout (30s)1.86Timeout (30s)Timeout (30s)
eval_swapTimeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)0.52Timeout (5s)Timeout (5s)
eval_term_change_free---------------------
induction_ty_lex
  1.---------------------
split_goal_wp
  1.0.040.030.040.05---Timeout (20s)Timeout (20s)
2.0.040.030.110.21---Timeout (20s)Timeout (20s)
3.0.040.030.030.04---Out Of Memory (1000M)Timeout (30s)
4.0.070.033.313.76---Out Of Memory (1000M)Timeout (30s)
eval_change_free---------------------
induction_ty_lex
  1.---------------------
split_goal_wp
  1.0.050.040.200.25---Out Of Memory (1000M)Timeout (30s)
2.0.060.040.180.15---Out Of Memory (1000M)Timeout (30s)
3.0.080.042.012.05---Out Of Memory (1000M)Timeout (30s)
4.0.120.052.492.77---Out Of Memory (1000M)Timeout (30s)
5.0.050.031.071.09---Timeout (20s)Timeout (20s)
6.0.060.041.331.46---Timeout (30s)Timeout (30s)
7.0.070.042.122.28---Out Of Memory (1000M)Timeout (30s)
8.0.040.032.712.62---Out Of Memory (1000M)Timeout (30s)
9.0.630.18---Timeout (30s)0.55Timeout (20s)Timeout (20s)
10.0.230.08Timeout (30s)Timeout (30s)0.54Timeout (20s)Timeout (20s)
11.Timeout (30s)Timeout (30s)Timeout (30s)Timeout (30s)1.63Timeout (30s)Timeout (30s)
12.3.020.37Timeout (30s)Timeout (30s)1.11Timeout (30s)Timeout (30s)

Theory "HoareLogic": fully verified

ObligationsCoq (8.3pl4)Z3 (3.2)Z3 (4.2)
many_steps_seq1.16------
consequence_rule---0.270.26
skip_rule0.66------
assign_rule1.70------
seq_rule---0.240.24
if_rule1.11------
assert_rule0.86------
assert_rule_ext0.76------
while_rule0.84------

Theory "WP": fully verified

ObligationsAlt-Ergo (0.93.1)Alt-Ergo (0.94)CVC3 (2.2)CVC3 (2.4.1)Coq (8.3pl4)Z3 (3.2)Z3 (4.2)
monotonicity---------------------
induction_ty_lex
  1.---------------------
split_goal_wp
  1.0.040.040.060.08---0.090.10
2.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)1.05Timeout (5s)Timeout (5s)
3.0.060.050.110.14---Timeout (5s)Timeout (5s)
4.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)0.97Timeout (5s)Timeout (5s)
5.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)---1.401.91
6.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)0.75Timeout (5s)Timeout (5s)
distrib_conj---------------------
induction_ty_lex
  1.---------------------
split_goal_wp
  1.0.060.040.060.07---0.140.12
2.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)1.38Timeout (5s)Timeout (5s)
3.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)1.05Timeout (5s)Timeout (5s)
4.2.330.16Timeout (5s)Timeout (5s)---Timeout (5s)Timeout (5s)
5.0.530.08Timeout (5s)Timeout (5s)---Timeout (5s)Timeout (5s)
6.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)0.70Timeout (5s)Timeout (5s)
wp_preserved_by_reduction------------6.78------
progress---------------------
induction_ty_lex
  1.---------------------
split_goal_wp
  1.0.040.030.050.06---0.000.00
2.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)0.56Timeout (5s)Timeout (5s)
3.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)1.12Timeout (5s)Timeout (5s)
4.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)0.73Timeout (5s)Timeout (5s)
5.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)0.70Timeout (5s)Timeout (5s)
6.Timeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)0.75Timeout (5s)Timeout (5s)
wp_soundnessTimeout (5s)Timeout (5s)Timeout (5s)Timeout (5s)0.70Timeout (5s)Timeout (5s)