Why3 Proof Results for Project "blocking_semantics5"
Theory "Syntax": fully verified
Obligations | Alt-Ergo (0.93.1) | Alt-Ergo (0.94) |
mident_decide | 0.01 | 0.00 |
ident_decide | 0.00 | 0.01 |
decide_is_skip | 0.01 | 0.01 |
Theory "SemOp": fully verified
Obligations | Alt-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_eq | 0.01 | 0.01 | 0.03 | 0.02 | --- | Timeout (5s) | Timeout (5s) |
get_stack_neq | 0.02 | 0.01 | 0.03 | 0.02 | --- | Timeout (5s) | Timeout (5s) |
steps_non_neg | --- | --- | --- | --- | 0.53 | --- | --- |
Theory "TestSemantics": fully verified
Obligations | Alt-Ergo (0.93.1) | Alt-Ergo (0.94) | Coq (8.3pl4) |
Test13 | 0.02 | 0.02 | --- |
Test42 | 0.03 | 0.02 | --- |
Test0 | 0.05 | 0.03 | --- |
Test55 | 0.57 | --- | --- |
Ass42 | 0.46 | 0.10 | --- |
If42 | --- | --- | 1.33 |
Theory "TypingAndSemantics": fully verified
Obligations | Alt-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_inversion | 0.03 | 0.02 | 0.04 | Timeout (5s) | 1.02 | Timeout (5s) | Timeout (5s) |
induction_ty_lex | | | | | | | |
| 1. | 0.08 | 0.05 | 0.04 | Timeout (5s) | --- | 0.07 | 0.07 |
eval_type_term | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | |
| 1. | 0.50 | 0.13 | 0.18 | 0.23 | --- | Timeout (5s) | Timeout (5s) |
2. | 0.62 | 0.14 | 0.27 | 0.31 | --- | Timeout (5s) | Timeout (5s) |
3. | 0.66 | 0.22 | 0.06 | 0.07 | --- | Timeout (5s) | Timeout (5s) |
4. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 4.14 | Timeout (5s) | Timeout (5s) |
type_preservation | --- | --- | --- | --- | 7.04 | --- | --- |
Theory "FreshVariables": fully verified
Obligations | Alt-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_append | 0.03 | --- | --- | --- | --- | --- | --- |
Append_nil_l | 0.03 | --- | --- | --- | --- | --- | --- |
eval_msubst_term | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | |
| 1. | 0.04 | 0.03 | 0.04 | 0.04 | --- | Timeout (5s) | Timeout (5s) |
2. | 0.04 | 0.02 | 0.04 | 0.04 | --- | Timeout (5s) | Timeout (5s) |
3. | 0.05 | 0.03 | 0.04 | 0.04 | --- | Timeout (5s) | Timeout (5s) |
4. | 0.12 | 0.03 | Timeout (5s) | Timeout (5s) | --- | Timeout (5s) | Timeout (5s) |
eval_msubst | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | |
| 1. | 0.05 | 0.02 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Timeout (30s) |
2. | 0.04 | 0.02 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Timeout (30s) |
3. | 0.20 | 0.05 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Out Of Memory (1000M) |
4. | 0.06 | 0.04 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Timeout (30s) |
5. | 0.04 | 0.03 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Timeout (30s) |
6. | 0.04 | 0.03 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Timeout (30s) |
7. | 0.07 | 0.03 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Out Of Memory (1000M) |
8. | 0.03 | 0.04 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Timeout (30s) |
9. | Timeout (5s) | 4.15 | Timeout (30s) | Timeout (30s) | 0.78 | Timeout (30s) | Out Of Memory (1000M) |
10. | 0.33 | 0.11 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Timeout (30s) |
11. | Timeout (5s) | Timeout (30s) | Timeout (30s) | Timeout (30s) | 1.99 | Timeout (30s) | Timeout (30s) |
12. | 2.55 | 0.80 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Out Of Memory (1000M) |
eval_swap_term | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | |
| 1. | 0.04 | 0.03 | 0.04 | 0.08 | --- | Out Of Memory (1000M) | Out Of Memory (1000M) |
2. | Timeout (5s) | Timeout (30s) | Timeout (30s) | Timeout (30s) | 1.26 | Out Of Memory (1000M) | Out Of Memory (1000M) |
3. | 0.05 | 0.03 | 0.06 | 0.05 | --- | Out Of Memory (1000M) | Out Of Memory (1000M) |
4. | 0.18 | 0.07 | 19.46 | 24.35 | --- | Out Of Memory (1000M) | Out Of Memory (1000M) |
eval_swap_gen | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | |
| 1. | 0.16 | 0.07 | 0.41 | 0.46 | --- | Timeout (30s) | Timeout (30s) |
2. | 0.15 | 0.06 | 0.44 | 0.47 | --- | Timeout (30s) | Timeout (30s) |
3. | 0.38 | 0.13 | 8.86 | 8.79 | --- | Timeout (30s) | Timeout (30s) |
4. | 0.38 | 0.14 | 4.20 | 9.18 | --- | Timeout (30s) | Timeout (30s) |
5. | 0.17 | 0.07 | 4.68 | 4.82 | --- | Timeout (30s) | Timeout (30s) |
6. | 0.16 | 0.07 | 5.05 | 5.21 | --- | Timeout (30s) | Timeout (30s) |
7. | 0.04 | 0.04 | 4.19 | 9.03 | --- | Timeout (30s) | Timeout (30s) |
8. | 0.04 | 0.04 | 8.51 | 8.96 | --- | Timeout (30s) | Timeout (30s) |
9. | 1.14 | 0.39 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Timeout (30s) |
10. | 1.07 | 0.41 | Timeout (30s) | Timeout (30s) | --- | Timeout (30s) | Timeout (30s) |
11. | 8.81 | Timeout (30s) | Timeout (30s) | Timeout (30s) | 1.93 | Timeout (30s) | Timeout (30s) |
12. | 8.88 | Timeout (30s) | Timeout (30s) | Timeout (30s) | 1.86 | Timeout (30s) | Timeout (30s) |
eval_swap | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 0.52 | Timeout (5s) | Timeout (5s) |
eval_term_change_free | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | |
| 1. | 0.04 | 0.03 | 0.04 | 0.05 | --- | Timeout (20s) | Timeout (20s) |
2. | 0.04 | 0.03 | 0.11 | 0.21 | --- | Timeout (20s) | Timeout (20s) |
3. | 0.04 | 0.03 | 0.03 | 0.04 | --- | Out Of Memory (1000M) | Timeout (30s) |
4. | 0.07 | 0.03 | 3.31 | 3.76 | --- | Out Of Memory (1000M) | Timeout (30s) |
eval_change_free | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | |
| 1. | 0.05 | 0.04 | 0.20 | 0.25 | --- | Out Of Memory (1000M) | Timeout (30s) |
2. | 0.06 | 0.04 | 0.18 | 0.15 | --- | Out Of Memory (1000M) | Timeout (30s) |
3. | 0.08 | 0.04 | 2.01 | 2.05 | --- | Out Of Memory (1000M) | Timeout (30s) |
4. | 0.12 | 0.05 | 2.49 | 2.77 | --- | Out Of Memory (1000M) | Timeout (30s) |
5. | 0.05 | 0.03 | 1.07 | 1.09 | --- | Timeout (20s) | Timeout (20s) |
6. | 0.06 | 0.04 | 1.33 | 1.46 | --- | Timeout (30s) | Timeout (30s) |
7. | 0.07 | 0.04 | 2.12 | 2.28 | --- | Out Of Memory (1000M) | Timeout (30s) |
8. | 0.04 | 0.03 | 2.71 | 2.62 | --- | Out Of Memory (1000M) | Timeout (30s) |
9. | 0.63 | 0.18 | --- | Timeout (30s) | 0.55 | Timeout (20s) | Timeout (20s) |
10. | 0.23 | 0.08 | Timeout (30s) | Timeout (30s) | 0.54 | Timeout (20s) | Timeout (20s) |
11. | Timeout (30s) | Timeout (30s) | Timeout (30s) | Timeout (30s) | 1.63 | Timeout (30s) | Timeout (30s) |
12. | 3.02 | 0.37 | Timeout (30s) | Timeout (30s) | 1.11 | Timeout (30s) | Timeout (30s) |
Theory "HoareLogic": fully verified
Obligations | Coq (8.3pl4) | Z3 (3.2) | Z3 (4.2) |
many_steps_seq | 1.16 | --- | --- |
consequence_rule | --- | 0.27 | 0.26 |
skip_rule | 0.66 | --- | --- |
assign_rule | 1.70 | --- | --- |
seq_rule | --- | 0.24 | 0.24 |
if_rule | 1.11 | --- | --- |
assert_rule | 0.86 | --- | --- |
assert_rule_ext | 0.76 | --- | --- |
while_rule | 0.84 | --- | --- |
Theory "WP": fully verified
Obligations | Alt-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.04 | 0.04 | 0.06 | 0.08 | --- | 0.09 | 0.10 |
2. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 1.05 | Timeout (5s) | Timeout (5s) |
3. | 0.06 | 0.05 | 0.11 | 0.14 | --- | Timeout (5s) | Timeout (5s) |
4. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 0.97 | Timeout (5s) | Timeout (5s) |
5. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | --- | 1.40 | 1.91 |
6. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 0.75 | Timeout (5s) | Timeout (5s) |
distrib_conj | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | |
| 1. | 0.06 | 0.04 | 0.06 | 0.07 | --- | 0.14 | 0.12 |
2. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 1.38 | Timeout (5s) | Timeout (5s) |
3. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 1.05 | Timeout (5s) | Timeout (5s) |
4. | 2.33 | 0.16 | Timeout (5s) | Timeout (5s) | --- | Timeout (5s) | Timeout (5s) |
5. | 0.53 | 0.08 | Timeout (5s) | Timeout (5s) | --- | Timeout (5s) | Timeout (5s) |
6. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 0.70 | Timeout (5s) | Timeout (5s) |
wp_preserved_by_reduction | --- | --- | --- | --- | 6.78 | --- | --- |
progress | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | |
| 1. | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | |
| 1. | 0.04 | 0.03 | 0.05 | 0.06 | --- | 0.00 | 0.00 |
2. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 0.56 | Timeout (5s) | Timeout (5s) |
3. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 1.12 | Timeout (5s) | Timeout (5s) |
4. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 0.73 | Timeout (5s) | Timeout (5s) |
5. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 0.70 | Timeout (5s) | Timeout (5s) |
6. | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 0.75 | Timeout (5s) | Timeout (5s) |
wp_soundness | Timeout (5s) | Timeout (5s) | Timeout (5s) | Timeout (5s) | 0.70 | Timeout (5s) | Timeout (5s) |