Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 0c3f68b5 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

example queens bv : added missing proof

parent 6c51b1e8
......@@ -106,7 +106,7 @@
<proof prover="6"><result status="valid" time="0.06"/></proof>
</goal>
</theory>
<theory name="NQueensBits" sum="9616dc000635808d847392b98246a13a">
<theory name="NQueensBits" sum="52654d3528256695406a132fccae498b">
<goal name="WP_parameter t" expl="VC for t">
<transf name="split_goal_wp">
<goal name="WP_parameter t.1" expl="1. assertion">
......@@ -129,19 +129,19 @@
<ip_library name="Unit"/>
<ip_qualid name="unit"/>
</ts_pos>
<ts_pos name="solution" arity="0" id="4009"
<ts_pos name="solution" arity="0" id="4008"
ip_theory="Solution">
<ip_qualid name="solution"/>
</ts_pos>
<ts_pos name="solutions" arity="0" id="4074"
<ts_pos name="solutions" arity="0" id="4073"
ip_theory="Solution">
<ip_qualid name="solutions"/>
</ts_pos>
<ts_pos name="t" arity="0" id="4107"
<ts_pos name="t" arity="0" id="4106"
ip_theory="BitsSpec">
<ip_qualid name="t"/>
</ts_pos>
<ts_pos name="ref" arity="1" id="4163"
<ts_pos name="ref" arity="1" id="4162"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="ref"/>
......@@ -152,1223 +152,1223 @@
<ip_library name="BuiltIn"/>
<ip_qualid name="infix ="/>
</ls_pos>
<ls_pos name="zero" id="1058"
<ls_pos name="zero" id="1057"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="one" id="1059"
<ls_pos name="one" id="1058"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="one"/>
</ls_pos>
<ls_pos name="infix &lt;" id="1060"
<ls_pos name="infix &lt;" id="1059"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &lt;"/>
</ls_pos>
<ls_pos name="infix +" id="2229"
<ls_pos name="infix +" id="2228"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix +"/>
</ls_pos>
<ls_pos name="prefix -" id="2230"
<ls_pos name="prefix -" id="2229"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="prefix -"/>
</ls_pos>
<ls_pos name="infix *" id="2231"
<ls_pos name="infix *" id="2230"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix *"/>
</ls_pos>
<ls_pos name="abs" id="2344"
<ls_pos name="abs" id="2343"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="abs"/>
</ls_pos>
<ls_pos name="div" id="2469"
<ls_pos name="div" id="2468"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="div"/>
</ls_pos>
<ls_pos name="mod" id="2472"
<ls_pos name="mod" id="2471"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="mod"/>
</ls_pos>
<ls_pos name="mem" id="3084"
<ls_pos name="mem" id="3083"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="mem"/>
</ls_pos>
<ls_pos name="infix ==" id="3087"
<ls_pos name="infix ==" id="3086"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="infix =="/>
</ls_pos>
<ls_pos name="subset" id="3105"
<ls_pos name="subset" id="3104"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="subset"/>
</ls_pos>
<ls_pos name="empty" id="3126"
<ls_pos name="empty" id="3125"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="empty"/>
</ls_pos>
<ls_pos name="add" id="3138"
<ls_pos name="add" id="3137"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="add"/>
</ls_pos>
<ls_pos name="singleton" id="3144"
<ls_pos name="singleton" id="3143"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="singleton"/>
</ls_pos>
<ls_pos name="remove" id="3149"
<ls_pos name="remove" id="3148"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="remove"/>
</ls_pos>
<ls_pos name="union" id="3167"
<ls_pos name="union" id="3166"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="union"/>
</ls_pos>
<ls_pos name="inter" id="3174"
<ls_pos name="inter" id="3173"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="inter"/>
</ls_pos>
<ls_pos name="diff" id="3181"
<ls_pos name="diff" id="3180"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="diff"/>
</ls_pos>
<ls_pos name="choose" id="3193"
<ls_pos name="choose" id="3192"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="choose"/>
</ls_pos>
<ls_pos name="cardinal" id="3197"
<ls_pos name="cardinal" id="3196"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="cardinal"/>
</ls_pos>
<ls_pos name="min_elt" id="3302"
<ls_pos name="min_elt" id="3301"
ip_theory="Fsetint">
<ip_library name="set"/>
<ip_qualid name="min_elt"/>
</ls_pos>
<ls_pos name="max_elt" id="3312"
<ls_pos name="max_elt" id="3311"
ip_theory="Fsetint">
<ip_library name="set"/>
<ip_qualid name="max_elt"/>
</ls_pos>
<ls_pos name="interval" id="3322"
<ls_pos name="interval" id="3321"
ip_theory="Fsetint">
<ip_library name="set"/>
<ip_qualid name="interval"/>
</ls_pos>
<ls_pos name="get" id="3407"
<ls_pos name="get" id="3406"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="3410"
<ls_pos name="set" id="3409"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="3430"
<ls_pos name="mixfix [&lt;-]" id="3429"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="andb" id="3834"
<ls_pos name="andb" id="3833"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="andb"/>
</ls_pos>
<ls_pos name="orb" id="3843"
<ls_pos name="orb" id="3842"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="orb"/>
</ls_pos>
<ls_pos name="notb" id="3852"
<ls_pos name="notb" id="3851"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="notb"/>
</ls_pos>
<ls_pos name="xorb" id="3857"
<ls_pos name="xorb" id="3856"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="xorb"/>
</ls_pos>
<ls_pos name="implb" id="3866"
<ls_pos name="implb" id="3865"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="implb"/>
</ls_pos>
<ls_pos name="succ" id="3993" ip_theory="S">
<ls_pos name="succ" id="3992" ip_theory="S">
<ip_qualid name="succ"/>
</ls_pos>
<ls_pos name="pred" id="4000" ip_theory="S">
<ls_pos name="pred" id="3999" ip_theory="S">
<ip_qualid name="pred"/>
</ls_pos>
<ls_pos name="n" id="4008" ip_theory="Solution">
<ls_pos name="n" id="4007" ip_theory="Solution">
<ip_qualid name="n"/>
</ls_pos>
<ls_pos name="eq_sol" id="4026"
<ls_pos name="eq_sol" id="4025"
ip_theory="Solution">
<ip_qualid name="eq_sol"/>
</ls_pos>
<ls_pos name="lt_sol" id="4062"
<ls_pos name="lt_sol" id="4061"
ip_theory="Solution">
<ip_qualid name="lt_sol"/>
</ls_pos>
<ls_pos name="sorted" id="4075"
<ls_pos name="sorted" id="4074"
ip_theory="Solution">
<ip_qualid name="sorted"/>
</ls_pos>
<ls_pos name="prefix !" id="4169"
<ls_pos name="prefix !" id="4168"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="prefix !"/>
</ls_pos>
<ls_pos name="pow2" id="4323"
<ls_pos name="pow2" id="4322"
ip_theory="Pow2int">
<ip_library name="bv"/>
<ip_qualid name="pow2"/>
</ls_pos>
<ls_pos name="size" id="5215"
<ls_pos name="size" id="5214"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="size"/>
</ls_pos>
<ls_pos name="nth" id="5220"
<ls_pos name="nth" id="5219"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="nth"/>
</ls_pos>
<ls_pos name="zero" id="5225"
<ls_pos name="zero" id="5224"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="ones" id="5228"
<ls_pos name="ones" id="5227"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="ones"/>
</ls_pos>
<ls_pos name="bw_and" id="5231"
<ls_pos name="bw_and" id="5230"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="bw_and"/>
</ls_pos>
<ls_pos name="bw_or" id="5238"
<ls_pos name="bw_or" id="5237"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="bw_or"/>
</ls_pos>
<ls_pos name="bw_xor" id="5245"
<ls_pos name="bw_xor" id="5244"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="bw_xor"/>
</ls_pos>
<ls_pos name="bw_not" id="5252"
<ls_pos name="bw_not" id="5251"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="bw_not"/>
</ls_pos>
<ls_pos name="lsr" id="5257"
<ls_pos name="lsr" id="5256"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="lsr"/>
</ls_pos>
<ls_pos name="asr" id="5271"
<ls_pos name="asr" id="5270"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="asr"/>
</ls_pos>
<ls_pos name="lsl" id="5285"
<ls_pos name="lsl" id="5284"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="lsl"/>
</ls_pos>
<ls_pos name="rotate_right" id="5299"
<ls_pos name="rotate_right" id="5298"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="rotate_right"/>
</ls_pos>
<ls_pos name="rotate_left" id="5305"
<ls_pos name="rotate_left" id="5304"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="rotate_left"/>
</ls_pos>
<ls_pos name="to_int" id="5313"
<ls_pos name="to_int" id="5312"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="to_int"/>
</ls_pos>
<ls_pos name="to_uint" id="5314"
<ls_pos name="to_uint" id="5313"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="to_uint"/>
</ls_pos>
<ls_pos name="of_int" id="5315"
<ls_pos name="of_int" id="5314"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="of_int"/>
</ls_pos>
<ls_pos name="size_bv" id="5336"
<ls_pos name="size_bv" id="5335"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="size_bv"/>
</ls_pos>
<ls_pos name="ugt" id="5363"
<ls_pos name="ugt" id="5362"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="ugt"/>
</ls_pos>
<ls_pos name="uge" id="5374"
<ls_pos name="uge" id="5373"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="uge"/>
</ls_pos>
<ls_pos name="sge" id="5418"
<ls_pos name="sge" id="5417"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="sge"/>
</ls_pos>
<ls_pos name="add" id="5427"
<ls_pos name="add" id="5426"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="add"/>
</ls_pos>
<ls_pos name="sub" id="5438"
<ls_pos name="sub" id="5437"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="sub"/>
</ls_pos>
<ls_pos name="neg" id="5449"
<ls_pos name="neg" id="5448"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="neg"/>
</ls_pos>
<ls_pos name="mul" id="5453"
<ls_pos name="mul" id="5452"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="mul"/>
</ls_pos>
<ls_pos name="udiv" id="5464"
<ls_pos name="udiv" id="5463"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="udiv"/>
</ls_pos>
<ls_pos name="urem" id="5470"
<ls_pos name="urem" id="5469"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="urem"/>
</ls_pos>
<ls_pos name="nth_bv" id="5476"
<ls_pos name="nth_bv" id="5475"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="nth_bv"/>
</ls_pos>
<ls_pos name="lsr_bv" id="5486"
<ls_pos name="lsr_bv" id="5485"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="lsr_bv"/>
</ls_pos>
<ls_pos name="asr_bv" id="5497"
<ls_pos name="asr_bv" id="5496"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="asr_bv"/>
</ls_pos>
<ls_pos name="lsl_bv" id="5503"
<ls_pos name="lsl_bv" id="5502"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="lsl_bv"/>
</ls_pos>
<ls_pos name="eq_sub_bv" id="5531"
<ls_pos name="eq_sub_bv" id="5530"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="eq_sub_bv"/>
</ls_pos>
<ls_pos name="eq_sub" id="5552"
<ls_pos name="eq_sub" id="5551"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="eq_sub"/>
</ls_pos>
<ls_pos name="eq" id="5582"
<ls_pos name="eq" id="5581"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="eq"/>
</ls_pos>
<pr_pos name="Assoc" id="2232"
<pr_pos name="Assoc" id="2231"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Unit_def_l" id="2239"
<pr_pos name="Unit_def_l" id="2238"
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="2242"
<pr_pos name="Unit_def_r" id="2241"
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="2245"
<pr_pos name="Inv_def_l" id="2244"
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="2248"
<pr_pos name="Inv_def_r" id="2247"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_r"/>
</pr_pos>
<pr_pos name="Comm" id="2251"
<pr_pos name="Comm" id="2250"
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="2256"
<pr_pos name="Assoc" id="2255"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Assoc"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Mul_distr_l" id="2263"
<pr_pos name="Mul_distr_l" id="2262"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_l"/>
</pr_pos>
<pr_pos name="Mul_distr_r" id="2270"
<pr_pos name="Mul_distr_r" id="2269"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_r"/>
</pr_pos>
<pr_pos name="Comm" id="2288"
<pr_pos name="Comm" id="2287"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Unitary" id="2293"
<pr_pos name="Unitary" id="2292"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Unitary"/>
</pr_pos>
<pr_pos name="NonTrivialRing" id="2296"
<pr_pos name="NonTrivialRing" id="2295"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="NonTrivialRing"/>
</pr_pos>
<pr_pos name="Refl" id="2308"
<pr_pos name="Refl" id="2307"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Refl"/>
</pr_pos>
<pr_pos name="Trans" id="2311"
<pr_pos name="Trans" id="2310"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Trans"/>
</pr_pos>
<pr_pos name="Antisymm" id="2318"
<pr_pos name="Antisymm" id="2317"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Antisymm"/>
</pr_pos>
<pr_pos name="Total" id="2323"
<pr_pos name="Total" id="2322"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Total"/>
</pr_pos>
<pr_pos name="ZeroLessOne" id="2328"
<pr_pos name="ZeroLessOne" id="2327"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="ZeroLessOne"/>
</pr_pos>
<pr_pos name="CompatOrderAdd" id="2329"
<pr_pos name="CompatOrderAdd" id="2328"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderAdd"/>
</pr_pos>
<pr_pos name="CompatOrderMult" id="2336"
<pr_pos name="CompatOrderMult" id="2335"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderMult"/>
</pr_pos>
<pr_pos name="Abs_le" id="2349"
<pr_pos name="Abs_le" id="2348"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="Abs_le"/>
</pr_pos>
<pr_pos name="Abs_pos" id="2354"
<pr_pos name="Abs_pos" id="2353"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="Abs_pos"/>
</pr_pos>
<pr_pos name="Div_mod" id="2475"
<pr_pos name="Div_mod" id="2474"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_mod"/>
</pr_pos>
<pr_pos name="Mod_bound" id="2480"
<pr_pos name="Mod_bound" id="2479"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_bound"/>
</pr_pos>
<pr_pos name="Div_unique" id="2485"
<pr_pos name="Div_unique" id="2484"
ip_theory="EuclideanDivision">
<ip_library name="int"/>