Why3 Proof Results for Project "matrices"

Theory "matrices.FixedMatrix": fully verified in 0.00 s

ObligationsAlt-Ergo (1.01)
rows_and_cols_nonnegative0.00

Theory "matrices.SquareFixedMatrix": fully verified in 0.00 s

ObligationsAlt-Ergo (1.01)
r_and_c_nonnegative0.00

Theory "matrices.MatrixArithmetic": fully verified in 11.75 s

ObligationsAlt-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. precondition0.02---
2. precondition2.40---
3. assertion0.06---
4. precondition0.05---
5. assertion0.04---
6. postcondition0.02---
mul_assoc------
split_goal_wp
  1.0.02---
2.0.01---
VC for mul_distr_right_get------
split_goal_wp
  1. assertion0.06---
2. precondition0.10---
3. postcondition0.06---
mul_distr_right------
split_goal_wp
  1.0.05---
2.0.01---
VC for mul_distr_left_get------
split_goal_wp
  1. assertion0.06---
2. precondition0.05---
3. postcondition0.05---
mul_distr_left------
split_goal_wp
  1.0.04---
2.0.01---
mul_zero_right1.91---
mul_zero_left1.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

ObligationsAlt-Ergo (1.01)
VC for block_mul_ij2.31
VC for mul_split0.29
VC for mul_block_cell---
split_goal_wp
  1. precondition0.03
2. postcondition0.12
mul_block---
split_goal_wp
  1.0.04
2.0.02