Commit f15f71fd authored by MARCHE Claude's avatar MARCHE Claude

prover: fix sessions, because of negative literals

parent 76873d5b
......@@ -11,7 +11,7 @@
</theory>
<theory name="Logic" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Impl" sum="2bda4510f7ee68d4ff8a07c97868aa43" expanded="true">
<theory name="Impl" sum="cc54a36f74c60b7aac65c403ee116c5e" expanded="true">
<goal name="WP_parameter create" expl="VC for create">
<proof prover="4"><result status="valid" time="0.11" steps="82"/></proof>
</goal>
......@@ -157,7 +157,7 @@
<proof prover="4"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter resize_for.35" expl="assertion">
<proof prover="4"><result status="valid" time="0.35" steps="159"/></proof>
<proof prover="4"><result status="valid" time="0.21" steps="159"/></proof>
</goal>
<goal name="WP_parameter resize_for.36" expl="type invariant">
<proof prover="4"><result status="valid" time="0.03" steps="28"/></proof>
......@@ -448,7 +448,7 @@
<goal name="WP_parameter backtrack.32.1.4" expl="VC for backtrack">
<transf name="inline_goal">
<goal name="WP_parameter backtrack.32.1.4.1" expl="VC for backtrack">
<proof prover="1" timelimit="30"><result status="valid" time="1.41"/></proof>
<proof prover="1" timelimit="30"><result status="valid" time="1.72"/></proof>
</goal>
</transf>
</goal>
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -9,7 +9,7 @@
<file name="../Firstorder_formula_list_impl.mlw">
<theory name="Types" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Logic" sum="da30b17d0000f30a7e34ea3e1a1f9413">
<theory name="Logic" sum="be160d6860d02433476a24625eafc56a">
<goal name="WP_parameter nlsize_positive_lemma_fo_formula_list" expl="VC for nlsize_positive_lemma_fo_formula_list">
<proof prover="4" timelimit="1"><result status="valid" time="0.26" steps="135"/></proof>
</goal>
......@@ -25,10 +25,10 @@
<proof prover="4"><result status="valid" time="0.16" steps="37"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_fo_formula_list.4" expl="assertion">
<proof prover="4" timelimit="1"><result status="valid" time="0.11" steps="30"/></proof>
<proof prover="4" timelimit="1"><result status="valid" time="0.13" steps="30"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_fo_formula_list.5" expl="assertion">
<proof prover="4" timelimit="1"><result status="valid" time="0.11" steps="32"/></proof>
<proof prover="4" timelimit="1"><result status="valid" time="0.12" steps="32"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_fo_formula_list.6" expl="variant decrease">
<proof prover="4" timelimit="1"><result status="valid" time="0.13" steps="18"/></proof>
......@@ -40,10 +40,10 @@
<proof prover="4"><result status="valid" time="0.13" steps="14"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_fo_formula_list.9" expl="assertion">
<proof prover="4" timelimit="1"><result status="valid" time="0.13" steps="14"/></proof>
<proof prover="4" timelimit="1"><result status="valid" time="0.11" steps="14"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_fo_formula_list.10" expl="assertion">
<proof prover="4" timelimit="1"><result status="valid" time="0.12" steps="14"/></proof>
<proof prover="4" timelimit="1"><result status="valid" time="0.11" steps="14"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_fo_formula_list.11" expl="postcondition">
<proof prover="4" timelimit="1"><result status="valid" time="0.12" steps="18"/></proof>
......@@ -103,7 +103,7 @@
</transf>
</goal>
</theory>
<theory name="Impl" sum="e796fc0d600efeb7479ddec8600988fa">
<theory name="Impl" sum="1f4798e69ba6c2e91df1c2bb423f3c5d">
<goal name="WP_parameter bind_var_symbol_in_fo_formula_list" expl="VC for bind_var_symbol_in_fo_formula_list">
<transf name="split_goal_wp">
<goal name="WP_parameter bind_var_symbol_in_fo_formula_list.1" expl="postcondition">
......@@ -125,7 +125,7 @@
<proof prover="4"><result status="valid" time="0.18" steps="38"/></proof>
</goal>
<goal name="WP_parameter bind_var_symbol_in_fo_formula_list.7" expl="assertion">
<proof prover="4"><result status="valid" time="0.16" steps="24"/></proof>
<proof prover="4"><result status="valid" time="0.14" steps="24"/></proof>
</goal>
<goal name="WP_parameter bind_var_symbol_in_fo_formula_list.8" expl="assertion">
<proof prover="4"><result status="valid" time="0.14" steps="13"/></proof>
......@@ -134,7 +134,7 @@
<proof prover="4"><result status="valid" time="0.16" steps="13"/></proof>
</goal>
<goal name="WP_parameter bind_var_symbol_in_fo_formula_list.10" expl="assertion">
<proof prover="4"><result status="valid" time="0.14" steps="13"/></proof>
<proof prover="4"><result status="valid" time="0.16" steps="13"/></proof>
</goal>
<goal name="WP_parameter bind_var_symbol_in_fo_formula_list.11" expl="variant decrease">
<proof prover="4"><result status="valid" time="0.16" steps="18"/></proof>
......@@ -186,7 +186,7 @@
<proof prover="4" timelimit="1"><result status="valid" time="0.10" steps="26"/></proof>
</goal>
<goal name="WP_parameter bind_var_fo_term_in_fo_formula_list.7" expl="assertion">
<proof prover="4" timelimit="1"><result status="valid" time="0.12" steps="24"/></proof>
<proof prover="4" timelimit="1"><result status="valid" time="0.13" steps="24"/></proof>
</goal>
<goal name="WP_parameter bind_var_fo_term_in_fo_formula_list.8" expl="assertion">
<proof prover="4" timelimit="1"><result status="valid" time="0.12" steps="13"/></proof>
......@@ -195,7 +195,7 @@
<proof prover="4" timelimit="1"><result status="valid" time="0.13" steps="13"/></proof>
</goal>
<goal name="WP_parameter bind_var_fo_term_in_fo_formula_list.10" expl="assertion">
<proof prover="4" timelimit="1"><result status="valid" time="0.13" steps="13"/></proof>
<proof prover="4" timelimit="1"><result status="valid" time="0.12" steps="13"/></proof>
</goal>
<goal name="WP_parameter bind_var_fo_term_in_fo_formula_list.11" expl="variant decrease">
<proof prover="4" timelimit="1"><result status="valid" time="0.14" steps="18"/></proof>
......@@ -244,7 +244,7 @@
<proof prover="4"><result status="valid" time="0.16" steps="24"/></proof>
</goal>
<goal name="WP_parameter unbind_var_symbol_in_fo_formula_list.6" expl="assertion">
<proof prover="4"><result status="valid" time="0.19" steps="59"/></proof>
<proof prover="4"><result status="valid" time="0.14" steps="59"/></proof>
</goal>
<goal name="WP_parameter unbind_var_symbol_in_fo_formula_list.7" expl="assertion">
<proof prover="4"><result status="valid" time="0.16" steps="38"/></proof>
......@@ -253,7 +253,7 @@
<proof prover="4"><result status="valid" time="0.14" steps="15"/></proof>
</goal>
<goal name="WP_parameter unbind_var_symbol_in_fo_formula_list.9" expl="assertion">
<proof prover="4"><result status="valid" time="0.14" steps="15"/></proof>
<proof prover="4"><result status="valid" time="0.19" steps="15"/></proof>
</goal>
<goal name="WP_parameter unbind_var_symbol_in_fo_formula_list.10" expl="assertion">
<proof prover="4"><result status="valid" time="0.16" steps="15"/></proof>
......@@ -408,7 +408,7 @@
<proof prover="4"><result status="valid" time="0.17" steps="22"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_fo_formula_list.6" expl="assertion">
<proof prover="4"><result status="valid" time="0.18" steps="54"/></proof>
<proof prover="4"><result status="valid" time="0.16" steps="54"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_fo_formula_list.7" expl="assertion">
<proof prover="4"><result status="valid" time="0.17" steps="35"/></proof>
......@@ -417,7 +417,7 @@
<proof prover="4"><result status="valid" time="0.15" steps="13"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_fo_formula_list.9" expl="assertion">
<proof prover="4"><result status="valid" time="0.16" steps="13"/></proof>
<proof prover="4"><result status="valid" time="0.18" steps="13"/></proof>
</goal>
<goal name="WP_parameter subst_base_symbol_in_fo_formula_list.10" expl="assertion">
<proof prover="4"><result status="valid" time="0.16" steps="13"/></proof>
......@@ -475,7 +475,7 @@
<proof prover="4"><result status="valid" time="0.16" steps="13"/></proof>
</goal>
<goal name="WP_parameter subst_base_fo_term_in_fo_formula_list.6" expl="assertion">
<proof prover="4"><result status="valid" time="0.15" steps="36"/></proof>
<proof prover="4"><result status="valid" time="0.16" steps="36"/></proof>
</goal>
<goal name="WP_parameter subst_base_fo_term_in_fo_formula_list.7" expl="assertion">
<proof prover="4"><result status="valid" time="0.18" steps="27"/></proof>
......@@ -484,7 +484,7 @@
<proof prover="4"><result status="valid" time="0.17" steps="15"/></proof>
</goal>
<goal name="WP_parameter subst_base_fo_term_in_fo_formula_list.9" expl="assertion">
<proof prover="4"><result status="valid" time="0.16" steps="15"/></proof>
<proof prover="4"><result status="valid" time="0.15" steps="15"/></proof>
</goal>
<goal name="WP_parameter subst_base_fo_term_in_fo_formula_list.10" expl="assertion">
<proof prover="4"><result status="valid" time="0.15" steps="15"/></proof>
......
......@@ -27,7 +27,7 @@
<proof prover="7"><result status="valid" time="0.04" steps="64"/></proof>
</goal>
</theory>
<theory name="Impl" sum="7cf2267692e6b261fae23742258ab4ff">
<theory name="Impl" sum="228a7661be7c9f8bc2778969f574e5dc">
<goal name="WP_parameter bind_var_symbol_in_symbol" expl="VC for bind_var_symbol_in_symbol">
<proof prover="7"><result status="valid" time="0.10" steps="216"/></proof>
</goal>
......
......@@ -9,7 +9,7 @@
<file name="../Firstorder_tableau_impl.mlw" expanded="true">
<theory name="Types" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Logic" sum="1fb71e31216b4959515e6fc4962d6521">
<theory name="Logic" sum="f83e56ce608f48274710a1bbf184ebe9">
<goal name="WP_parameter nlsize_positive_lemma_tableau" expl="VC for nlsize_positive_lemma_tableau">
<proof prover="8"><result status="valid" time="0.13" steps="91"/></proof>
</goal>
......@@ -25,22 +25,22 @@
<proof prover="8"><result status="valid" time="0.20" steps="34"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_tableau.4" expl="assertion">
<proof prover="8"><result status="valid" time="0.16" steps="36"/></proof>
<proof prover="8"><result status="valid" time="0.20" steps="36"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_tableau.5" expl="assertion">
<proof prover="8"><result status="valid" time="0.16" steps="29"/></proof>
<proof prover="8"><result status="valid" time="0.17" steps="29"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_tableau.6" expl="assertion">
<proof prover="8"><result status="valid" time="0.16" steps="31"/></proof>
<proof prover="8"><result status="valid" time="0.18" steps="31"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_tableau.7" expl="assertion">
<proof prover="8"><result status="valid" time="0.17" steps="15"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_tableau.8" expl="assertion">
<proof prover="8"><result status="valid" time="0.15" steps="15"/></proof>
<proof prover="8"><result status="valid" time="0.16" steps="15"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_tableau.9" expl="assertion">
<proof prover="8"><result status="valid" time="0.17" steps="15"/></proof>
<proof prover="8"><result status="valid" time="0.20" steps="15"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_tableau.10" expl="assertion">
<proof prover="8"><result status="valid" time="0.17" steps="15"/></proof>
......@@ -49,13 +49,13 @@
<proof prover="8"><result status="valid" time="0.18" steps="16"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_tableau.12" expl="assertion">
<proof prover="8"><result status="valid" time="0.20" steps="16"/></proof>
<proof prover="8"><result status="valid" time="0.15" steps="16"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_tableau.13" expl="assertion">
<proof prover="8"><result status="valid" time="0.20" steps="16"/></proof>
<proof prover="8"><result status="valid" time="0.16" steps="16"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_tableau.14" expl="assertion">
<proof prover="8"><result status="valid" time="0.18" steps="16"/></proof>
<proof prover="8"><result status="valid" time="0.16" steps="16"/></proof>
</goal>
<goal name="WP_parameter nlmodel_subst_commutation_lemma_tableau.15" expl="postcondition">
<proof prover="8"><result status="valid" time="0.21" steps="20"/></proof>
......@@ -130,7 +130,7 @@
</transf>
</goal>
</theory>
<theory name="Impl" sum="d795f16342f977de44df15e712ed8a95">
<theory name="Impl" sum="23d0e8b06bc6f38e10616df06c246495">
<goal name="WP_parameter bind_var_symbol_in_tableau" expl="VC for bind_var_symbol_in_tableau">
<proof prover="9"><result status="valid" time="0.95"/></proof>
</goal>
......@@ -233,7 +233,7 @@
<proof prover="8"><result status="valid" time="0.20" steps="23"/></proof>
</goal>
<goal name="WP_parameter construct_tableau.28" expl="assertion">
<proof prover="8"><result status="valid" time="0.19" steps="23"/></proof>
<proof prover="8"><result status="valid" time="0.21" steps="23"/></proof>
</goal>
<goal name="WP_parameter construct_tableau.29" expl="precondition">
<proof prover="8"><result status="valid" time="0.20" steps="8"/></proof>
......@@ -254,7 +254,7 @@
<proof prover="8"><result status="valid" time="0.18" steps="24"/></proof>
</goal>
<goal name="WP_parameter construct_tableau.35" expl="assertion">
<proof prover="8"><result status="valid" time="0.21" steps="24"/></proof>
<proof prover="8"><result status="valid" time="0.19" steps="24"/></proof>
</goal>
<goal name="WP_parameter construct_tableau.36" expl="precondition">
<proof prover="8"><result status="valid" time="0.19" steps="8"/></proof>
......@@ -429,7 +429,7 @@
<proof prover="8"><result status="valid" time="1.43" steps="3093"/></proof>
</goal>
<goal name="WP_parameter destruct_tableau.50" expl="postcondition">
<proof prover="8"><result status="valid" time="0.28" steps="97"/></proof>
<proof prover="8"><result status="valid" time="0.15" steps="97"/></proof>
</goal>
<goal name="WP_parameter destruct_tableau.51" expl="postcondition">
<proof prover="8"><result status="valid" time="0.18" steps="181"/></proof>
......@@ -483,7 +483,7 @@
<proof prover="8"><result status="valid" time="0.21" steps="35"/></proof>
</goal>
<goal name="WP_parameter nlsubst_symbol_in_tableau.10.6" expl="assertion">
<proof prover="2"><result status="valid" time="2.15"/></proof>
<proof prover="2"><result status="valid" time="2.58"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
......@@ -9,7 +9,7 @@
<file name="../ProverMain.mlw" expanded="true">
<theory name="Types" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Impl" sum="862d58bbd5db5579f0f708b74b41565e" expanded="true">
<theory name="Impl" sum="d7c510b89dcf9223206872390ba2e475" expanded="true">
<goal name="WP_parameter main" expl="VC for main" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter main.1" expl="precondition">
......@@ -47,13 +47,13 @@
<proof prover="2"><result status="valid" time="0.15" steps="46"/></proof>
</goal>
<goal name="WP_parameter main.10" expl="precondition">
<proof prover="2"><result status="valid" time="0.30" steps="93"/></proof>
<proof prover="2"><result status="valid" time="0.17" steps="93"/></proof>
</goal>
<goal name="WP_parameter main.11" expl="precondition">
<proof prover="2"><result status="valid" time="0.24" steps="41"/></proof>
</goal>
<goal name="WP_parameter main.12" expl="precondition">
<proof prover="2"><result status="valid" time="0.25" steps="24"/></proof>
<proof prover="2"><result status="valid" time="0.12" steps="24"/></proof>
</goal>
<goal name="WP_parameter main.13" expl="precondition">
<proof prover="2"><result status="valid" time="0.12" steps="24"/></proof>
......@@ -73,7 +73,7 @@
<goal name="WP_parameter main.18" expl="assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter main.18.1" expl="assertion">
<proof prover="2"><result status="valid" time="0.26" steps="18"/></proof>
<proof prover="2"><result status="valid" time="0.13" steps="18"/></proof>
</goal>
<goal name="WP_parameter main.18.2" expl="assertion">
<proof prover="2"><result status="valid" time="0.14" steps="33"/></proof>
......@@ -94,7 +94,7 @@
<proof prover="4"><result status="valid" time="1.21"/></proof>
</goal>
<goal name="WP_parameter main.20" expl="postcondition">
<proof prover="2"><result status="valid" time="0.27" steps="23"/></proof>
<proof prover="2"><result status="valid" time="0.14" steps="23"/></proof>
</goal>
<goal name="WP_parameter main.21" expl="exceptional postcondition">
<proof prover="2"><result status="valid" time="0.14" steps="23"/></proof>
......
......@@ -8,7 +8,7 @@
<file name="../ProverTest.mlw" expanded="true">
<theory name="Types" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Impl" sum="4d46fc443123844b5fc84ff6141201a4" expanded="true">
<theory name="Impl" sum="14c12b468a1c091bceb7747753a16197" expanded="true">
<goal name="WP_parameter imply" expl="VC for imply">
<proof prover="0"><result status="valid" time="0.15" steps="48"/></proof>
</goal>
......
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment