Commit 3c35f64e authored by MARCHE Claude's avatar MARCHE Claude

Fix failing Alt-Ergo proof due to steps feature

parent c9aa4b62
# useful script for git bisect
make || exit 125 ; bin/why3config --detect && bin/why3replay examples/bellman_ford.mlw
(autoconf && ./configure --enable-local --disable-coq-libs --disable-isabelle-libs && make) || exit 125 ; bin/why3config --detect && bin/why3replay examples/linear_probing.mlw
......@@ -471,554 +471,554 @@
</goal>
<goal name="WP_parameter copy.2" expl="2. type invariant">
<metas>
<ts_pos name="option" arity="1" id="2591"
<ts_pos name="option" arity="1" id="2587"
ip_theory="Option">
<ip_library name="option"/>
<ip_qualid name="option"/>
</ts_pos>
<ts_pos name="list" arity="1" id="2595"
<ts_pos name="list" arity="1" id="2591"
ip_theory="List">
<ip_library name="list"/>
<ip_qualid name="list"/>
</ts_pos>
<ts_pos name="ref" arity="1" id="4648"
<ts_pos name="ref" arity="1" id="4644"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="ref"/>
</ts_pos>
<ts_pos name="t" arity="0" id="6088"
<ts_pos name="t" arity="0" id="6084"
ip_theory="LinearProbing">
<ip_qualid name="t"/>
</ts_pos>
<ls_pos name="zero" id="432"
<ls_pos name="zero" id="428"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="one" id="433"
<ls_pos name="one" id="429"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="one"/>
</ls_pos>
<ls_pos name="infix &lt;" id="434"
<ls_pos name="infix &lt;" id="430"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &lt;"/>
</ls_pos>
<ls_pos name="infix +" id="1603"
<ls_pos name="infix +" id="1599"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix +"/>
</ls_pos>
<ls_pos name="prefix -" id="1604"
<ls_pos name="prefix -" id="1600"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="prefix -"/>
</ls_pos>
<ls_pos name="infix *" id="1605"
<ls_pos name="infix *" id="1601"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix *"/>
</ls_pos>
<ls_pos name="abs" id="1718"
<ls_pos name="abs" id="1714"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="abs"/>
</ls_pos>
<ls_pos name="div" id="1923"
<ls_pos name="div" id="1919"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="div"/>
</ls_pos>
<ls_pos name="mod" id="1926"
<ls_pos name="mod" id="1922"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="mod"/>
</ls_pos>
<ls_pos name="keym" id="2543"
<ls_pos name="keym" id="2539"
ip_theory="LinearProbing">
<ip_qualid name="HashedTypeWithDummy"/>
<ip_qualid name="keym"/>
</ls_pos>
<ls_pos name="hash" id="2572"
<ls_pos name="hash" id="2568"
ip_theory="LinearProbing">
<ip_qualid name="HashedTypeWithDummy"/>
<ip_qualid name="hash"/>
</ls_pos>
<ls_pos name="dummy" id="2581"
<ls_pos name="dummy" id="2577"
ip_theory="LinearProbing">
<ip_qualid name="HashedTypeWithDummy"/>
<ip_qualid name="dummy"/>
</ls_pos>
<ls_pos name="mem" id="2619"
<ls_pos name="mem" id="2615"
ip_theory="Mem">
<ip_library name="list"/>
<ip_qualid name="mem"/>
</ls_pos>
<ls_pos name="get" id="3269"
<ls_pos name="get" id="3265"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="3272"
<ls_pos name="set" id="3268"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix []" id="3279"
<ls_pos name="mixfix []" id="3275"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="mixfix []"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="3292"
<ls_pos name="mixfix [&lt;-]" id="3288"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="prefix !" id="4654"
<ls_pos name="prefix !" id="4650"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="prefix !"/>
</ls_pos>
<ls_pos name="set" id="4821"
<ls_pos name="set" id="4817"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="4863"
<ls_pos name="mixfix [&lt;-]" id="4859"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="numofd" id="5869"
<ls_pos name="numofd" id="5865"
ip_theory="LinearProbing">
<ip_qualid name="numofd"/>
</ls_pos>
<ls_pos name="next" id="6709"
<ls_pos name="next" id="6705"
ip_theory="LinearProbing">
<ip_qualid name="next"/>
</ls_pos>
<pr_pos name="Assoc" id="1606"
<pr_pos name="Assoc" id="1602"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Unit_def_l" id="1613"
<pr_pos name="Unit_def_l" id="1609"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Unit_def_l"/>
</pr_pos>
<pr_pos name="Unit_def_r" id="1616"
<pr_pos name="Unit_def_r" id="1612"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Unit_def_r"/>
</pr_pos>
<pr_pos name="Inv_def_l" id="1619"
<pr_pos name="Inv_def_l" id="1615"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_l"/>
</pr_pos>
<pr_pos name="Inv_def_r" id="1622"
<pr_pos name="Inv_def_r" id="1618"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_r"/>
</pr_pos>
<pr_pos name="Comm" id="1625"
<pr_pos name="Comm" id="1621"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Assoc" id="1630"
<pr_pos name="Assoc" id="1626"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Assoc"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Mul_distr_l" id="1637"
<pr_pos name="Mul_distr_l" id="1633"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_l"/>
</pr_pos>
<pr_pos name="Mul_distr_r" id="1644"
<pr_pos name="Mul_distr_r" id="1640"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_r"/>
</pr_pos>
<pr_pos name="Comm" id="1662"
<pr_pos name="Comm" id="1658"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Unitary" id="1667"
<pr_pos name="Unitary" id="1663"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Unitary"/>
</pr_pos>
<pr_pos name="NonTrivialRing" id="1670"
<pr_pos name="NonTrivialRing" id="1666"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="NonTrivialRing"/>
</pr_pos>
<pr_pos name="Refl" id="1682"
<pr_pos name="Refl" id="1678"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Refl"/>
</pr_pos>
<pr_pos name="Trans" id="1685"
<pr_pos name="Trans" id="1681"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Trans"/>
</pr_pos>
<pr_pos name="Antisymm" id="1692"
<pr_pos name="Antisymm" id="1688"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Antisymm"/>
</pr_pos>
<pr_pos name="Total" id="1697"
<pr_pos name="Total" id="1693"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Total"/>
</pr_pos>
<pr_pos name="ZeroLessOne" id="1702"
<pr_pos name="ZeroLessOne" id="1698"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="ZeroLessOne"/>
</pr_pos>
<pr_pos name="CompatOrderAdd" id="1703"
<pr_pos name="CompatOrderAdd" id="1699"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderAdd"/>
</pr_pos>
<pr_pos name="CompatOrderMult" id="1710"
<pr_pos name="CompatOrderMult" id="1706"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderMult"/>
</pr_pos>
<pr_pos name="Abs_le" id="1723"
<pr_pos name="Abs_le" id="1719"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="Abs_le"/>
</pr_pos>
<pr_pos name="Abs_pos" id="1728"
<pr_pos name="Abs_pos" id="1724"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="Abs_pos"/>
</pr_pos>
<pr_pos name="Div_mod" id="1929"
<pr_pos name="Div_mod" id="1925"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Div_mod"/>
</pr_pos>
<pr_pos name="Div_bound" id="1934"
<pr_pos name="Div_bound" id="1930"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Div_bound"/>
</pr_pos>
<pr_pos name="Mod_bound" id="1939"
<pr_pos name="Mod_bound" id="1935"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_bound"/>
</pr_pos>
<pr_pos name="Div_sign_pos" id="1944"
<pr_pos name="Div_sign_pos" id="1940"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Div_sign_pos"/>
</pr_pos>
<pr_pos name="Div_sign_neg" id="1949"
<pr_pos name="Div_sign_neg" id="1945"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Div_sign_neg"/>
</pr_pos>
<pr_pos name="Mod_sign_pos" id="1954"
<pr_pos name="Mod_sign_pos" id="1950"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_sign_pos"/>
</pr_pos>
<pr_pos name="Mod_sign_neg" id="1959"
<pr_pos name="Mod_sign_neg" id="1955"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_sign_neg"/>
</pr_pos>
<pr_pos name="Rounds_toward_zero" id="1964"
<pr_pos name="Rounds_toward_zero" id="1960"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Rounds_toward_zero"/>
</pr_pos>
<pr_pos name="Div_1" id="1969"
<pr_pos name="Div_1" id="1965"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Div_1"/>
</pr_pos>
<pr_pos name="Mod_1" id="1972"
<pr_pos name="Mod_1" id="1968"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_1"/>
</pr_pos>
<pr_pos name="Div_inf" id="1975"
<pr_pos name="Div_inf" id="1971"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Div_inf"/>
</pr_pos>
<pr_pos name="Mod_inf" id="1980"
<pr_pos name="Mod_inf" id="1976"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_inf"/>
</pr_pos>
<pr_pos name="Div_mult" id="1985"
<pr_pos name="Div_mult" id="1981"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Div_mult"/>
</pr_pos>
<pr_pos name="Mod_mult" id="1992"
<pr_pos name="Mod_mult" id="1988"
ip_theory="ComputerDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_mult"/>
</pr_pos>
<pr_pos name="hash_nonneg" id="2573"
<pr_pos name="hash_nonneg" id="2569"
ip_theory="LinearProbing">
<ip_qualid name="HashedTypeWithDummy"/>
<ip_qualid name="hash_nonneg"/>
</pr_pos>
<pr_pos name="hash_eq" id="2576"
<pr_pos name="hash_eq" id="2572"
ip_theory="LinearProbing">
<ip_qualid name="HashedTypeWithDummy"/>
<ip_qualid name="hash_eq"/>
</pr_pos>
<pr_pos name="Select_eq" id="3305"
<pr_pos name="Select_eq" id="3301"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="Select_eq"/>
</pr_pos>
<pr_pos name="Select_neq" id="3314"
<pr_pos name="Select_neq" id="3310"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="Select_neq"/>
</pr_pos>
<pr_pos name="bucket_bounds" id="5530"
<pr_pos name="bucket_bounds" id="5526"
ip_theory="LinearProbing">
<ip_qualid name="bucket_bounds"/>
</pr_pos>
<pr_pos name="numof_eq" id="5759"
<pr_pos name="numof_eq" id="5755"
ip_theory="LinearProbing">
<ip_qualid name="NumOfDummy"/>
<ip_qualid name="numof_eq"/>
</pr_pos>
<pr_pos name="dummy_const" id="5865"
<pr_pos name="dummy_const" id="5861"
ip_theory="LinearProbing">
<ip_qualid name="NumOfDummy"/>
<ip_qualid name="dummy_const"/>
</pr_pos>
<meta name="remove_logic">
<meta_arg_ls id="432"/>
<meta_arg_ls id="428"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="433"/>
<meta_arg_ls id="429"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="434"/>
<meta_arg_ls id="430"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1603"/>
<meta_arg_ls id="1599"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1604"/>
<meta_arg_ls id="1600"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1605"/>
<meta_arg_ls id="1601"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1718"/>
<meta_arg_ls id="1714"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1923"/>
<meta_arg_ls id="1919"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1926"/>
<meta_arg_ls id="1922"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2543"/>
<meta_arg_ls id="2539"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2572"/>
<meta_arg_ls id="2568"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2581"/>
<meta_arg_ls id="2577"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2619"/>
<meta_arg_ls id="2615"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3269"/>
<meta_arg_ls id="3265"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3272"/>
<meta_arg_ls id="3268"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3279"/>
<meta_arg_ls id="3275"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3292"/>
<meta_arg_ls id="3288"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="4654"/>
<meta_arg_ls id="4650"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="4821"/>
<meta_arg_ls id="4817"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="4863"/>
<meta_arg_ls id="4859"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="5869"/>
<meta_arg_ls id="5865"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="6709"/>
<meta_arg_ls id="6705"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1606"/>
<meta_arg_pr id="1602"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1613"/>
<meta_arg_pr id="1609"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1616"/>
<meta_arg_pr id="1612"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1619"/>
<meta_arg_pr id="1615"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1622"/>
<meta_arg_pr id="1618"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1625"/>
<meta_arg_pr id="1621"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1630"/>
<meta_arg_pr id="1626"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1637"/>
<meta_arg_pr id="1633"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1644"/>
<meta_arg_pr id="1640"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1662"/>
<meta_arg_pr id="1658"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1667"/>
<meta_arg_pr id="1663"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1670"/>
<meta_arg_pr id="1666"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1682"/>
<meta_arg_pr id="1678"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1685"/>
<meta_arg_pr id="1681"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1692"/>
<meta_arg_pr id="1688"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1697"/>
<meta_arg_pr id="1693"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1702"/>
<meta_arg_pr id="1698"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1703"/>
<meta_arg_pr id="1699"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1710"/>
<meta_arg_pr id="1706"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1723"/>
<meta_arg_pr id="1719"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1728"/>
<meta_arg_pr id="1724"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1929"/>
<meta_arg_pr id="1925"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1934"/>
<meta_arg_pr id="1930"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1939"/>
<meta_arg_pr id="1935"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1944"/>
<meta_arg_pr id="1940"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1949"/>
<meta_arg_pr id="1945"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1954"/>
<meta_arg_pr id="1950"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1959"/>
<meta_arg_pr id="1955"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1964"/>
<meta_arg_pr id="1960"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1969"/>
<meta_arg_pr id="1965"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1972"/>
<meta_arg_pr id="1968"/>
</meta>