Commit e3231d7f authored by Martin Clochard's avatar Martin Clochard

verifythis_2016_matrix_multiplication: updating provers/moving out of to_port

parent ccb98dc9
......@@ -227,7 +227,7 @@ goods examples/WP_revisited
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-L examples/bitvectors"
goods examples/avl "-L examples/avl"
goods examples/to_port/verifythis_2016_matrix_multiplication "-L examples/to_port/verifythis_2016_matrix_multiplication"
goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication"
goods examples/double_wp "-L examples/double_wp"
goods examples/ring_decision "-L examples/ring_decision"
goods examples/in_progress
......
......@@ -72,6 +72,7 @@ run_dir double_wp "-L double_wp"
run_dir avl "-L avl"
run_dir foveoos11-cm
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
run_dir verifythis_2016_matrix_multiplication "-L verifythis_2016_matrix_multiplication"
run_dir WP_revisited
echo ""
......@@ -81,7 +82,6 @@ echo ""
echo "=== Programs that remain to be ported ==="
echo ""
run_dir prover "-L prover --debug ignore_unused_vars"
run_dir to_port/verifythis_2016_matrix_multiplication "-L to_port/verifythis_2016_matrix_multiplication"
echo ""
echo "=== Standard Library ==="
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../matrices.mlw">
<theory name="MatrixGen" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Matrix" sum="ba7eca602ee03df2a98f7a686c251c65">
<goal name="set_def1">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="set_def2">
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="set_def3">
<proof prover="2"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="set_def4">
<proof prover="2"><result status="valid" time="0.00" steps="22"/></proof>
</goal>
</theory>
<theory name="FixedMatrix" sum="5d486d0188577a056ee4b579fa3069c2">
<goal name="rows_and_cols_nonnegative">
<proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
</theory>
<theory name="SquareFixedMatrix" sum="d58222172e1753dccc191aaf22a115ae">
<goal name="r_and_c_nonnegative">
<proof prover="2"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
<theory name="MatrixArithmetic" sum="51e672c189e950ed33557df63dcd9958">
<goal name="zero_neutral">
<transf name="split_goal_wp">
<goal name="zero_neutral.1" expl="1.">
<proof prover="2"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="zero_neutral.2" expl="2.">
<proof prover="2"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
</transf>
</goal>
<goal name="add_commutative">
<transf name="split_goal_wp">
<goal name="add_commutative.1" expl="1.">
<proof prover="2"><result status="valid" time="0.03" steps="73"/></proof>
</goal>
<goal name="add_commutative.2" expl="2.">
<proof prover="2"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
</transf>
</goal>
<goal name="add_associative">
<transf name="split_goal_wp">
<goal name="add_associative.1" expl="1.">
<proof prover="2"><result status="valid" time="0.14" steps="499"/></proof>
</goal>
<goal name="add_associative.2" expl="2.">
<proof prover="2"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
</transf>
</goal>
<goal name="add_opposite">
<transf name="split_goal_wp">
<goal name="add_opposite.1" expl="1.">
<proof prover="2"><result status="valid" time="0.12" steps="217"/></proof>
</goal>
<goal name="add_opposite.2" expl="2.">
<proof prover="2"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
</transf>
</goal>
<goal name="opp_involutive">
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="opposite_add">
<proof prover="0"><result status="valid" time="0.49"/></proof>
</goal>
<goal name="VC mul_assoc_get" expl="VC for mul_assoc_get">
<transf name="split_goal_wp">
<goal name="VC mul_assoc_get.1" expl="1. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC mul_assoc_get.2" expl="2. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.04" steps="30"/></proof>
</goal>
<goal name="VC mul_assoc_get.3" expl="3. assertion">
<proof prover="2" timelimit="1"><result status="valid" time="0.05" steps="52"/></proof>
</goal>
<goal name="VC mul_assoc_get.4" expl="4. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.05" steps="35"/></proof>
</goal>
<goal name="VC mul_assoc_get.5" expl="5. assertion">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="VC mul_assoc_get.6" expl="6. postcondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
</transf>
</goal>
<goal name="mul_assoc">
<transf name="split_goal_wp">
<goal name="mul_assoc.1" expl="1.">
<proof prover="2"><result status="valid" time="0.02" steps="103"/></proof>
</goal>
<goal name="mul_assoc.2" expl="2.">
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mul_distr_right_get" expl="VC for mul_distr_right_get">
<transf name="split_goal_wp">
<goal name="VC mul_distr_right_get.1" expl="1. assertion">
<proof prover="2" timelimit="1"><result status="valid" time="0.15" steps="274"/></proof>
</goal>
<goal name="VC mul_distr_right_get.2" expl="2. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.03" steps="46"/></proof>
</goal>
<goal name="VC mul_distr_right_get.3" expl="3. postcondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.13" steps="112"/></proof>
</goal>
</transf>
</goal>
<goal name="mul_distr_right">
<transf name="split_goal_wp">
<goal name="mul_distr_right.1" expl="1.">
<proof prover="2"><result status="valid" time="0.05" steps="297"/></proof>
</goal>
<goal name="mul_distr_right.2" expl="2.">
<proof prover="2"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mul_distr_left_get" expl="VC for mul_distr_left_get">
<transf name="split_goal_wp">
<goal name="VC mul_distr_left_get.1" expl="1. assertion">
<proof prover="2" timelimit="1"><result status="valid" time="0.10" steps="286"/></proof>
</goal>
<goal name="VC mul_distr_left_get.2" expl="2. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.04" steps="46"/></proof>
</goal>
<goal name="VC mul_distr_left_get.3" expl="3. postcondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.03" steps="45"/></proof>
</goal>
</transf>
</goal>
<goal name="mul_distr_left">
<transf name="split_goal_wp">
<goal name="mul_distr_left.1" expl="1.">
<proof prover="2"><result status="valid" time="0.04" steps="288"/></proof>
</goal>
<goal name="mul_distr_left.2" expl="2.">
<proof prover="2"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
</transf>
</goal>
<goal name="mul_zero_right">
<proof prover="2"><result status="valid" time="0.15" steps="315"/></proof>
</goal>
<goal name="mul_zero_left">
<proof prover="2"><result status="valid" time="0.16" steps="315"/></proof>
</goal>
<goal name="mul_opp">
<transf name="split_goal_wp">
<goal name="mul_opp.1" expl="1.">
<proof prover="2"><result status="valid" time="0.20" steps="502"/></proof>
</goal>
<goal name="mul_opp.2" expl="2.">
<proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="mul_opp.3" expl="3.">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="mul_opp.4" expl="4.">
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="BlockMul" sum="4b4a8b669c6aee7d1b50429c51fc5e29">
<goal name="VC block_mul_ij" expl="VC for block_mul_ij">
<transf name="split_goal_wp">
<goal name="VC block_mul_ij.1" expl="1. assertion">
<proof prover="2" timelimit="1"><result status="valid" time="0.08" steps="79"/></proof>
</goal>
<goal name="VC block_mul_ij.2" expl="2. variant decrease">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC block_mul_ij.3" expl="3. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC block_mul_ij.4" expl="4. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC block_mul_ij.5" expl="5. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC block_mul_ij.6" expl="6. postcondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.20" steps="118"/></proof>
</goal>
<goal name="VC block_mul_ij.7" expl="7. postcondition">
<proof prover="0"><result status="valid" time="1.48"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mul_split" expl="VC for mul_split">
<transf name="split_goal_wp">
<goal name="VC mul_split.1" expl="1. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="VC mul_split.2" expl="2. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="VC mul_split.3" expl="3. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="VC mul_split.4" expl="4. assertion">
<proof prover="2" timelimit="1"><result status="valid" time="0.20" steps="317"/></proof>
</goal>
<goal name="VC mul_split.5" expl="5. postcondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mul_block_cell" expl="VC for mul_block_cell">
<transf name="split_goal_wp">
<goal name="VC mul_block_cell.1" expl="1. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
<goal name="VC mul_block_cell.2" expl="2. postcondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.13" steps="136"/></proof>
</goal>
</transf>
</goal>
<goal name="mul_block">
<transf name="split_goal_wp">
<goal name="mul_block.1" expl="1.">
<proof prover="2"><result status="valid" time="0.04" steps="108"/></proof>
</goal>
<goal name="mul_block.2" expl="2.">
<proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../matrices_ring_simp.mlw">
<theory name="Symb" sum="a198129a81430b3cb64fea46b424b98e">
<goal name="LOCAL.VC l_mdl_ok" expl="VC for l_mdl_ok">
<proof prover="2"><result status="valid" time="0.04" steps="110"/></proof>
</goal>
<goal name="LOCAL.VC m_mdl_ok" expl="VC for m_mdl_ok">
<proof prover="2"><result status="valid" time="0.03" steps="39"/></proof>
</goal>
<goal name="LOCAL.VC lm_mdl_ok" expl="VC for lm_mdl_ok">
<proof prover="2"><result status="valid" time="0.04" steps="124"/></proof>
</goal>
<goal name="LOCAL.VC lm_mdl_same" expl="VC for lm_mdl_same">
<proof prover="2"><result status="valid" time="0.06" steps="179"/></proof>
</goal>
<goal name="LOCAL.VC l_compare_zero" expl="VC for l_compare_zero">
<proof prover="2"><result status="valid" time="0.04" steps="83"/></proof>
</goal>
<goal name="LOCAL.VC m_collapse_ok" expl="VC for m_collapse_ok">
<proof prover="0"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="LOCAL.VC lm_collapse_ok" expl="VC for lm_collapse_ok">
<proof prover="2"><result status="valid" time="0.21" steps="549"/></proof>
</goal>
<goal name="LOCAL.VC cat_rev_ok" expl="VC for cat_rev_ok">
<proof prover="2"><result status="valid" time="0.19" steps="484"/></proof>
</goal>
<goal name="LOCAL.VC lm_dump_ok" expl="VC for lm_dump_ok">
<proof prover="2"><result status="valid" time="0.22" steps="591"/></proof>
</goal>
<goal name="LOCAL.VC lm_merge_ok" expl="VC for lm_merge_ok">
<proof prover="2" timelimit="5"><result status="valid" time="3.29" steps="6371"/></proof>
</goal>
<goal name="LOCAL.VC cat_ok" expl="VC for cat_ok">
<proof prover="2"><result status="valid" time="0.17" steps="548"/></proof>
</goal>
<goal name="LOCAL.VC m_mul_ok" expl="VC for m_mul_ok">
<proof prover="2"><result status="valid" time="0.09" steps="261"/></proof>
</goal>
<goal name="LOCAL.VC m_distribute_ok" expl="VC for m_distribute_ok">
<proof prover="2"><result status="valid" time="0.12" steps="542"/></proof>
</goal>
<goal name="LOCAL.VC lm_distribute_ok" expl="VC for lm_distribute_ok">
<proof prover="2"><result status="valid" time="0.42" steps="831"/></proof>
</goal>
<goal name="LOCAL.VC lm_opp_ok" expl="VC for lm_opp_ok">
<proof prover="2" timelimit="5"><result status="valid" time="1.57" steps="3415"/></proof>
</goal>
<goal name="extends_rw">
<proof prover="2"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="VC symb_env" expl="VC for symb_env">
<proof prover="2"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="VC symb_reg" expl="VC for symb_reg">
<proof prover="2"><result status="valid" time="0.04" steps="63"/></proof>
</goal>
<goal name="VC symb_opp" expl="VC for symb_opp">
<proof prover="2"><result status="valid" time="0.04" steps="25"/></proof>
</goal>
<goal name="VC symb_add" expl="VC for symb_add">
<proof prover="2"><result status="valid" time="0.10" steps="166"/></proof>
</goal>
<goal name="VC symb_sub" expl="VC for symb_sub">
<proof prover="2"><result status="valid" time="0.04" steps="33"/></proof>
</goal>
<goal name="VC symb_mul" expl="VC for symb_mul">
<proof prover="2"><result status="valid" time="0.05" steps="50"/></proof>
</goal>
<goal name="VC harness" expl="VC for harness">
<transf name="split_goal_wp">
<goal name="VC harness.1" expl="1. precondition">
<transf name="compute_specified">
<goal name="VC harness.1.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="VC harness.1.1.1" expl="1. precondition">
<transf name="compute_specified">
<goal name="VC harness.1.1.1.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.03" steps="51"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC harness.2" expl="2. precondition">
<proof prover="2"><result status="valid" time="0.05" steps="98"/></proof>
</goal>
<goal name="VC harness.3" expl="3. precondition">
<transf name="compute_specified">
<goal name="VC harness.3.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="VC harness.3.1.1" expl="1. precondition">
<transf name="compute_specified">
<goal name="VC harness.3.1.1.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.04" steps="55"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC harness.4" expl="4. precondition">
<proof prover="2"><result status="valid" time="0.07" steps="109"/></proof>
</goal>
<goal name="VC harness.5" expl="5. precondition">
<proof prover="2"><result status="valid" time="0.03" steps="41"/></proof>
</goal>
<goal name="VC harness.6" expl="6. precondition">
<proof prover="2"><result status="valid" time="0.04" steps="80"/></proof>
</goal>
<goal name="VC harness.7" expl="7. precondition">
<transf name="compute_specified">
<goal name="VC harness.7.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="VC harness.7.1.1" expl="1. precondition">
<transf name="compute_specified">
<goal name="VC harness.7.1.1.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.04" steps="63"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC harness.8" expl="8. precondition">
<proof prover="2"><result status="valid" time="0.06" steps="129"/></proof>
</goal>
<goal name="VC harness.9" expl="9. precondition">
<transf name="compute_specified">
<goal name="VC harness.9.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="VC harness.9.1.1" expl="1. precondition">
<transf name="compute_specified">
<goal name="VC harness.9.1.1.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.04" steps="66"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC harness.10" expl="10. precondition">
<proof prover="2"><result status="valid" time="0.06" steps="153"/></proof>
</goal>
<goal name="VC harness.11" expl="11. precondition">
<transf name="compute_specified">
<goal name="VC harness.11.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="VC harness.11.1.1" expl="1. precondition">
<transf name="compute_specified">
<goal name="VC harness.11.1.1.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.05" steps="70"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC harness.12" expl="12. precondition">
<proof prover="2"><result status="valid" time="0.08" steps="148"/></proof>
</goal>
<goal name="VC harness.13" expl="13. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="53"/></proof>
</goal>
<goal name="VC harness.14" expl="14. precondition">
<proof prover="2"><result status="valid" time="0.05" steps="104"/></proof>
</goal>
<goal name="VC harness.15" expl="15. precondition">
<transf name="compute_specified">
<goal name="VC harness.15.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="VC harness.15.1.1" expl="1. precondition">
<transf name="compute_specified">
<goal name="VC harness.15.1.1.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.05" steps="78"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC harness.16" expl="16. precondition">
<proof prover="2"><result status="valid" time="0.09" steps="167"/></proof>
</goal>
<goal name="VC harness.17" expl="17. precondition">
<transf name="compute_specified">
<goal name="VC harness.17.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="VC harness.17.1.1" expl="1. precondition">
<transf name="compute_specified">
<goal name="VC harness.17.1.1.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.07" steps="82"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC harness.18" expl="18. precondition">
<proof prover="2"><result status="valid" time="0.11" steps="176"/></proof>
</goal>
<goal name="VC harness.19" expl="19. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="62"/></proof>
</goal>
<goal name="VC harness.20" expl="20. precondition">
<proof prover="2"><result status="valid" time="0.13" steps="213"/></proof>
</goal>
<goal name="VC harness.21" expl="21. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="65"/></proof>
</goal>
<goal name="VC harness.22" expl="22. precondition">
<proof prover="2"><result status="valid" time="0.25" steps="290"/></proof>
</goal>
<goal name="VC harness.23" expl="23. precondition">
<proof prover="2"><result status="valid" time="0.03" steps="68"/></proof>
</goal>
<goal name="VC harness.24" expl="24. precondition">
<proof prover="2"><result status="valid" time="0.13" steps="203"/></proof>
</goal>
<goal name="VC harness.25" expl="25. precondition">
<proof prover="2"><result status="valid" time="0.04" steps="71"/></proof>
</goal>
<goal name="VC harness.26" expl="26. precondition">
<proof prover="2"><result status="valid" time="0.53" steps="618"/></proof>
</goal>
<goal name="VC harness.27" expl="27. precondition">
<transf name="compute_specified">
<goal name="VC harness.27.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="VC harness.27.1.1" expl="1. precondition">
<transf name="compute_specified">
<goal name="VC harness.27.1.1.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.12" steps="100"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC harness.28" expl="28. precondition">
<proof prover="2"><result status="valid" time="0.06" steps="146"/></proof>
</goal>
<goal name="VC harness.29" expl="29. precondition">
<transf name="compute_specified">
<goal name="VC harness.29.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="VC harness.29.1.1" expl="1. precondition">
<transf name="compute_specified">
<goal name="VC harness.29.1.1.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.08" steps="104"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC harness.30" expl="30. precondition">
<proof prover="2"><result status="valid" time="0.05" steps="152"/></proof>
</goal>
<goal name="VC harness.31" expl="31. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="80"/></proof>
</goal>
<goal name="VC harness.32" expl="32. precondition">
<proof prover="2"><result status="valid" time="0.10" steps="239"/></proof>
</goal>
<goal name="VC harness.33" expl="33. assertion">
<transf name="compute_specified">
<goal name="VC harness.33.1" expl="1. assertion">
<transf name="introduce_premises">
<goal name="VC harness.33.1.1" expl="1. assertion">
<transf name="compute_specified">
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../naive.mlw">
<theory name="MatrixMultiplication" sum="911c4e0a5b3fe8cc6dacaa3acb684928">
<goal name="VC mult_naive" expl="VC for mult_naive">
<transf name="split_goal_wp">
<goal name="VC mult_naive.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC mult_naive.2" expl="2. loop bounds">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="VC mult_naive.3" expl="3. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="VC mult_naive.4" expl="4. loop invariant init">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC mult_naive.5" expl="5. loop bounds">
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="VC mult_naive.6" expl="6. loop invariant init">
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC mult_naive.7" expl="7. loop invariant init">
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC mult_naive.8" expl="8. loop bounds">
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC mult_naive.9" expl="9. loop invariant init">
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC mult_naive.10" expl="10. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC mult_naive.11" expl="11. index in matrix bounds">
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC mult_naive.12" expl="12. index in matrix bounds">
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC mult_naive.13" expl="13. index in matrix bounds">
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC mult_naive.14" expl="14. index in matrix bounds">
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC mult_naive.15" expl="15. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
<goal name="VC mult_naive.16" expl="16. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.09" steps="77"/></proof>
</goal>
<goal name="VC mult_naive.17" expl="17. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC mult_naive.18" expl="18. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="VC mult_naive.19" expl="19. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="VC mult_naive.20" expl="20. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="52"/></proof>
</goal>
<goal name="VC mult_naive.21" expl="21. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC mult_naive.22" expl="22. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>