Why3 Proof Results for Project "blocking_semantics5"
Theory "Syntax": fully verified
Obligations | Alt-Ergo (0.95.1) |
mident_decide | 0.01 |
ident_decide | 0.00 |
decide_is_skip | 0.01 |
Theory "SemOp": fully verified
Obligations | Alt-Ergo (0.95.1) | CVC3 (2.2) | CVC3 (2.4.1) | Coq (8.4pl2) | Z3 (3.2) | Z3 (4.3.1) |
get_stack_eq | 0.01 | 0.03 | 0.02 | --- | 0.04 | 0.03 |
get_stack_neq | 0.02 | 0.03 | 0.02 | --- | 0.20 | 0.20 |
steps_non_neg | --- | --- | --- | 1.02 | --- | --- |
Theory "TestSemantics": fully verified
Obligations | Alt-Ergo (0.95.1) | CVC3 (2.4.1) | CVC4 (1.2) | Coq (8.4pl2) |
Test13 | 0.02 | --- | 0.03 | --- |
Test42 | 0.03 | --- | --- | --- |
Test0 | 0.05 | --- | --- | --- |
Test55 | --- | --- | 0.04 | --- |
Ass42 | 0.05 | 0.05 | --- | --- |
If42 | --- | --- | --- | 1.85 |
Theory "TypingAndSemantics": fully verified
Obligations | Alt-Ergo (0.95.1) | CVC3 (2.2) | CVC3 (2.4.1) | Coq (8.4pl2) | Z3 (3.2) | Z3 (4.3.1) |
type_inversion | 0.02 | 0.04 | 0.93 | 1.65 | Timeout (5s) | Timeout (5s) |
induction_ty_lex | | | | | | |
| 1. | 0.08 | 0.04 | 0.10 | --- | 0.07 | 0.07 |
eval_type_term | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. | 0.07 | 0.04 | 0.06 | --- | Timeout (5s) | Timeout (5s) |
2. | 0.06 | 0.04 | 0.04 | --- | Timeout (5s) | Timeout (5s) |
3. | 0.08 | 0.04 | 0.05 | --- | Timeout (5s) | Timeout (5s) |
4. | Timeout (5s) | --- | Timeout (5s) | 2.52 | Timeout (5s) | Timeout (5s) |
type_preservation | --- | --- | --- | 2.53 | --- | --- |
Theory "FreshVariables": fully verified
Obligations | Alt-Ergo (0.95.1) | CVC3 (2.2) | CVC3 (2.4.1) | Coq (8.4pl2) | Z3 (3.2) | Z3 (4.3.1) |
Cons_append | 0.03 | --- | --- | --- | --- | --- |
Append_nil_l | 0.03 | --- | --- | --- | --- | --- |
eval_msubst_term | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. | 0.04 | 0.04 | 0.04 | --- | Timeout (5s) | Timeout (5s) |
2. | 0.04 | 0.04 | 0.04 | --- | Timeout (5s) | Timeout (5s) |
3. | 0.05 | 0.04 | 0.04 | --- | Timeout (5s) | Timeout (5s) |
4. | 0.12 | 0.05 | 0.06 | --- | Timeout (5s) | Timeout (5s) |
eval_msubst | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. | 0.05 | 0.06 | 0.10 | --- | Timeout (30s) | Out Of Memory (1000M) |
2. | 0.04 | 0.06 | 0.08 | --- | Timeout (30s) | Out Of Memory (1000M) |
3. | 0.04 | 0.08 | Timeout (30s) | --- | Timeout (30s) | Out Of Memory (1000M) |
4. | 0.06 | 0.10 | Timeout (30s) | --- | Timeout (30s) | Out Of Memory (1000M) |
5. | 0.04 | 0.08 | 0.55 | --- | Timeout (30s) | Out Of Memory (1000M) |
6. | 0.04 | 0.08 | Timeout (30s) | --- | Timeout (30s) | Out Of Memory (1000M) |
7. | 0.07 | 0.09 | 0.30 | --- | Timeout (30s) | Out Of Memory (1000M) |
8. | 0.03 | 0.09 | Timeout (30s) | --- | Timeout (30s) | Out Of Memory (1000M) |
9. | 1.52 | 0.70 | 5.75 | 1.36 | Timeout (30s) | Out Of Memory (1000M) |
10. | 0.17 | 1.10 | Timeout (30s) | --- | Timeout (30s) | Out Of Memory (1000M) |
11. | Out Of Memory (1000M) | Timeout (30s) | Timeout (30s) | 2.57 | Out Of Memory (1000M) | Out Of Memory (1000M) |
12. | 0.77 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Out Of Memory (1000M) |
eval_swap_term | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. | 0.04 | 0.04 | 0.08 | --- | Timeout (30s) | Timeout (30s) |
2. | Timeout (30s) | Timeout (30s) | Timeout (30s) | 2.00 | Timeout (30s) | Timeout (30s) |
3. | 0.05 | 0.06 | 0.05 | --- | Timeout (30s) | Timeout (30s) |
4. | 0.03 | 0.05 | 0.25 | --- | Timeout (30s) | Timeout (30s) |
eval_swap_gen | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. | 0.04 | 0.05 | 0.24 | --- | Timeout (30s) | Timeout (30s) |
2. | 0.15 | 0.05 | 0.23 | --- | Timeout (30s) | Timeout (30s) |
3. | 0.10 | 0.26 | 0.43 | --- | Timeout (30s) | Timeout (30s) |
4. | 0.11 | 0.27 | 0.46 | --- | Timeout (30s) | Timeout (30s) |
5. | 0.05 | 0.22 | 0.37 | --- | Timeout (30s) | Timeout (30s) |
6. | 0.16 | 0.21 | 0.34 | --- | Timeout (30s) | Timeout (30s) |
7. | 0.04 | 0.25 | 0.41 | --- | Timeout (30s) | Timeout (30s) |
8. | 0.04 | 0.24 | 0.42 | --- | Timeout (30s) | Timeout (30s) |
9. | 0.14 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Timeout (30s) |
10. | 0.15 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Timeout (30s) |
11. | 9.52 | Timeout (30s) | Timeout (30s) | 2.00 | Timeout (30s) | Timeout (30s) |
12. | 8.60 | Timeout (30s) | Timeout (30s) | 2.00 | Timeout (30s) | Timeout (30s) |
eval_swap | Timeout (5s) | Timeout (5s) | Timeout (5s) | 1.07 | Timeout (5s) | Timeout (5s) |
eval_term_change_free | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. | 0.04 | 0.04 | 0.05 | --- | Timeout (20s) | Out Of Memory (1000M) |
2. | 0.04 | 0.11 | 0.06 | --- | Timeout (20s) | Out Of Memory (1000M) |
3. | 0.04 | 0.03 | 0.04 | --- | Timeout (30s) | Out Of Memory (1000M) |
4. | 0.07 | 0.03 | 0.05 | --- | Timeout (30s) | Out Of Memory (1000M) |
eval_change_free | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. | 0.05 | 0.05 | 0.06 | --- | Timeout (30s) | Out Of Memory (1000M) |
2. | 0.06 | 0.04 | 0.15 | --- | Timeout (30s) | Out Of Memory (1000M) |
3. | 0.08 | 0.05 | 0.07 | --- | Timeout (30s) | Out Of Memory (1000M) |
4. | 0.12 | 0.06 | 0.07 | --- | Timeout (30s) | Out Of Memory (1000M) |
5. | 0.05 | 0.05 | 0.06 | --- | Timeout (20s) | Out Of Memory (1000M) |
6. | 0.06 | 0.05 | 0.06 | --- | Timeout (30s) | Out Of Memory (1000M) |
7. | 0.07 | 0.06 | 0.07 | --- | Timeout (30s) | Out Of Memory (1000M) |
8. | 0.04 | 0.06 | 0.07 | --- | Timeout (30s) | Out Of Memory (1000M) |
9. | 0.58 | --- | 0.29 | 1.11 | Timeout (20s) | Out Of Memory (1000M) |
10. | 0.07 | 0.39 | 0.50 | 1.12 | Timeout (20s) | Out Of Memory (1000M) |
11. | Timeout (30s) | Timeout (30s) | Timeout (30s) | 2.00 | Timeout (30s) | Out Of Memory (1000M) |
12. | 0.18 | Timeout (30s) | Timeout (30s) | 1.53 | Timeout (30s) | Out Of Memory (1000M) |
Theory "HoareLogic": fully verified
Obligations | CVC3 (2.2) | CVC3 (2.4.1) | Coq (8.4pl2) | Z3 (3.2) | Z3 (4.3.1) |
many_steps_seq | --- | --- | 1.73 | --- | --- |
consequence_rule | 0.08 | 0.15 | --- | --- | --- |
skip_rule | --- | --- | 1.14 | --- | --- |
assign_rule | --- | --- | 1.96 | --- | --- |
seq_rule | --- | --- | --- | 0.09 | 0.06 |
if_rule | --- | --- | 1.71 | --- | --- |
assert_rule | --- | --- | 1.23 | --- | --- |
assert_rule_ext | --- | --- | 1.47 | --- | --- |
while_rule | --- | --- | 1.39 | --- | --- |
Theory "WP": fully verified
Obligations | Alt-Ergo (0.95.1) | CVC3 (2.2) | CVC3 (2.4.1) | CVC4 (1.2) | Coq (8.4pl2) | Eprover (1.6) | Vampire (0.6) | Z3 (3.2) | Z3 (4.3.1) |
monotonicity | --- | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | | |
| 1. | 0.04 | 0.06 | 0.08 | --- | --- | --- | --- | 0.09 | 0.10 |
2. | Timeout (5s) | Timeout (5s) | Timeout (5s) | --- | 1.67 | --- | --- | Timeout (5s) | Timeout (5s) |
3. | 0.06 | 0.11 | 0.14 | --- | --- | --- | --- | Timeout (5s) | Timeout (5s) |
4. | --- | --- | 0.24 | Timeout (5s) | 1.64 | --- | --- | --- | Timeout (5s) |
5. | Timeout (5s) | 0.07 | 0.09 | --- | --- | --- | --- | Timeout (5s) | Timeout (5s) |
6. | Timeout (5s) | Timeout (5s) | Timeout (5s) | --- | 1.16 | --- | --- | Timeout (5s) | Timeout (5s) |
distrib_conj | --- | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | | |
| 1. | 0.06 | 0.06 | 0.07 | --- | --- | --- | --- | Timeout (5s) | Timeout (5s) |
2. | 6.07 | Timeout (5s) | Timeout (5s) | --- | 2.03 | --- | --- | Timeout (5s) | Timeout (5s) |
3. | Timeout (5s) | Timeout (5s) | Timeout (5s) | --- | 1.62 | --- | --- | Timeout (5s) | Timeout (5s) |
4. | 0.96 | 0.58 | Timeout (5s) | 0.08 | --- | --- | --- | Timeout (5s) | Timeout (5s) |
5. | 0.40 | 0.27 | 0.27 | --- | --- | --- | --- | Timeout (5s) | Timeout (5s) |
6. | Timeout (5s) | Timeout (5s) | Timeout (5s) | --- | 1.31 | --- | --- | Timeout (5s) | Timeout (5s) |
wp_preserved_by_reduction | --- | --- | --- | --- | 4.74 | --- | --- | --- | --- |
progress | --- | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | | |
| 1. | 0.04 | 0.05 | 0.06 | --- | --- | --- | --- | 0.00 | 0.00 |
2. | Timeout (5s) | Timeout (5s) | Timeout (5s) | --- | 1.17 | --- | --- | Timeout (5s) | Timeout (5s) |
3. | Timeout (5s) | Timeout (5s) | Timeout (5s) | --- | 1.56 | --- | --- | Timeout (5s) | Timeout (5s) |
4. | Timeout (5s) | --- | Timeout (5s) | Timeout (5s) | 1.45 | --- | --- | Timeout (5s) | Timeout (5s) |
5. | --- | 0.31 | --- | --- | 1.15 | 0.20 | 0.34 | --- | --- |
6. | Timeout (5s) | Timeout (5s) | Timeout (5s) | --- | 1.19 | --- | --- | Timeout (5s) | Timeout (5s) |
wp_soundness | Timeout (5s) | Timeout (5s) | Timeout (5s) | --- | 1.27 | --- | --- | Timeout (5s) | Timeout (5s) |