Why3 Proof Results for Project "matrices"
Theory "matrices.FixedMatrix": fully verified in 0.00 s
Obligations | Alt-Ergo (1.01) |
rows_and_cols_nonnegative | 0.00 |
Theory "matrices.SquareFixedMatrix": fully verified in 0.00 s
Obligations | Alt-Ergo (1.01) |
r_and_c_nonnegative | 0.00 |
Theory "matrices.MatrixArithmetic": fully verified in 11.75 s
Obligations | Alt-Ergo (1.01) | CVC4 (1.4) |
zero_neutral | --- | --- |
split_goal_wp | | |
| 1. | 0.02 | --- |
2. | 0.02 | --- |
add_commutative | --- | --- |
split_goal_wp | | |
| 1. | 0.03 | --- |
2. | 0.01 | --- |
add_associative | --- | --- |
split_goal_wp | | |
| 1. | 0.14 | --- |
2. | 0.01 | --- |
add_opposite | --- | --- |
split_goal_wp | | |
| 1. | 0.12 | --- |
2. | 0.01 | --- |
opp_involutive | --- | 0.07 |
opposite_add | --- | 0.25 |
VC for mul_assoc_get | --- | --- |
split_goal_wp | | |
| 1. precondition | 0.02 | --- |
2. precondition | 2.40 | --- |
3. assertion | 0.06 | --- |
4. precondition | 0.05 | --- |
5. assertion | 0.04 | --- |
6. postcondition | 0.02 | --- |
mul_assoc | --- | --- |
split_goal_wp | | |
| 1. | 0.02 | --- |
2. | 0.01 | --- |
VC for mul_distr_right_get | --- | --- |
split_goal_wp | | |
| 1. assertion | 0.06 | --- |
2. precondition | 0.10 | --- |
3. postcondition | 0.06 | --- |
mul_distr_right | --- | --- |
split_goal_wp | | |
| 1. | 0.05 | --- |
2. | 0.01 | --- |
VC for mul_distr_left_get | --- | --- |
split_goal_wp | | |
| 1. assertion | 0.06 | --- |
2. precondition | 0.05 | --- |
3. postcondition | 0.05 | --- |
mul_distr_left | --- | --- |
split_goal_wp | | |
| 1. | 0.04 | --- |
2. | 0.01 | --- |
mul_zero_right | 1.91 | --- |
mul_zero_left | 1.65 | --- |
mul_opp | --- | --- |
split_goal_wp | | |
| 1. | 0.36 | --- |
2. | --- | 0.08 |
3. | --- | 0.04 |
4. | 3.92 | --- |
Theory "matrices.BlockMul": fully verified in 2.81 s
Obligations | Alt-Ergo (1.01) |
VC for block_mul_ij | 2.31 |
VC for mul_split | 0.29 |
VC for mul_block_cell | --- |
split_goal_wp | |
| 1. precondition | 0.03 |
2. postcondition | 0.12 |
mul_block | --- |
split_goal_wp | |
| 1. | 0.04 |
2. | 0.02 |