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 9dcb39cb authored by Martin Clochard's avatar Martin Clochard
Browse files
parents f3067abc b66bc4a5
......@@ -6,7 +6,7 @@ printer "smtv2"
filename "%f-%t-%g.smt2"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
outofmemory "^(error \".*out of memory\")\\|Cannot allocate memory"
fail "^(error \"\\(.*\\)\")" "Error: \1"
fail "^(error \"\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\)\\(.*\\)\")" "Error: \1"
timeout "interrupted by timeout"
time "why3cpulimit time : %s s"
valid "^unsat"
......@@ -394,3 +394,84 @@ theory bv.BVConverter_8_16
remove prop back_from_bigBV
end
theory bitvec.Pow2int
remove prop Power_0
remove prop Power_s
remove prop Power_1
remove prop Power_sum
remove prop pow2pos
remove prop Div_mult_inst
remove prop Div_double
remove prop Div_pow
remove prop Div_double_neg
remove prop Div_pow2
remove prop Div_div_pow
remove prop Mod_pow2_gen
remove prop pow2_0
remove prop pow2_1
remove prop pow2_2
remove prop pow2_3
remove prop pow2_4
remove prop pow2_5
remove prop pow2_6
remove prop pow2_7
remove prop pow2_8
remove prop pow2_9
remove prop pow2_10
remove prop pow2_11
remove prop pow2_12
remove prop pow2_13
remove prop pow2_14
remove prop pow2_15
remove prop pow2_16
remove prop pow2_17
remove prop pow2_18
remove prop pow2_19
remove prop pow2_20
remove prop pow2_21
remove prop pow2_22
remove prop pow2_23
remove prop pow2_24
remove prop pow2_25
remove prop pow2_26
remove prop pow2_27
remove prop pow2_28
remove prop pow2_29
remove prop pow2_30
remove prop pow2_31
remove prop pow2_32
remove prop pow2_33
remove prop pow2_34
remove prop pow2_35
remove prop pow2_36
remove prop pow2_37
remove prop pow2_38
remove prop pow2_39
remove prop pow2_40
remove prop pow2_41
remove prop pow2_42
remove prop pow2_43
remove prop pow2_44
remove prop pow2_45
remove prop pow2_46
remove prop pow2_47
remove prop pow2_48
remove prop pow2_49
remove prop pow2_50
remove prop pow2_51
remove prop pow2_52
remove prop pow2_53
remove prop pow2_54
remove prop pow2_55
remove prop pow2_56
remove prop pow2_57
remove prop pow2_58
remove prop pow2_59
remove prop pow2_60
remove prop pow2_61
remove prop pow2_62
remove prop pow2_63
remove prop pow2_64
end
......@@ -56,7 +56,7 @@ theory bitvec.BitVector64
syntax function lsr "(bvlshr %1 %2)"
syntax function lsl "(bvshl %1 %2)"
syntax function asr "(bvashr %1 %2)"
syntax converter of_int "(_ bv%1 64)"
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_int "(bv2int %1)"
remove prop to_int_of_int
remove prop to_int_extensionality
......@@ -121,7 +121,7 @@ theory bitvec.BitVector32
syntax function lsr "(bvlshr %1 %2)"
syntax function lsl "(bvshl %1 %2)"
syntax function asr "(bvashr %1 %2)"
syntax converter of_int "(_ bv%1 32)"
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_int "(bv2int %1)"
remove prop to_int_of_int
remove prop to_int_extensionality
......@@ -186,7 +186,7 @@ theory bitvec.BitVector16
syntax function lsr "(bvlshr %1 %2)"
syntax function lsl "(bvshl %1 %2)"
syntax function asr "(bvashr %1 %2)"
syntax converter of_int "(_ bv%1 16)"
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_int "(bv2int %1)"
remove prop to_int_of_int
remove prop to_int_extensionality
......@@ -251,7 +251,7 @@ theory bitvec.BitVector8
syntax function lsr "(bvlshr %1 %2)"
syntax function lsl "(bvshl %1 %2)"
syntax function asr "(bvashr %1 %2)"
syntax converter of_int "(_ bv%1 8)"
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_int "(bv2int %1)"
remove prop to_int_of_int
remove prop to_int_extensionality
......
......@@ -173,55 +173,55 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="trap">
<goal name="trap" expanded="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="smoke1">
<proof prover="0"><result status="timeout" time="4.80"/></proof>
<proof prover="1"><result status="timeout" time="4.96"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke2">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="4.99"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke3">
<proof prover="0"><result status="timeout" time="4.21"/></proof>
<proof prover="1"><result status="timeout" time="4.96"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke4">
<proof prover="0"><result status="timeout" time="4.74"/></proof>
<proof prover="1"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.95"/></proof>
</goal>
<goal name="smoke5">
<proof prover="0"><result status="timeout" time="4.96"/></proof>
<proof prover="1"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke6">
<proof prover="0"><result status="timeout" time="4.97"/></proof>
<proof prover="1"><result status="timeout" time="4.93"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke7">
<proof prover="0"><result status="timeout" time="4.80"/></proof>
<proof prover="1"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="smoke8">
<proof prover="0"><result status="timeout" time="4.79"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="6.01"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="4.98"/></proof>
</goal>
<goal name="g1">
......@@ -231,7 +231,7 @@
<goal name="f1">
<proof prover="0"><result status="timeout" time="4.98"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
</goal>
<goal name="g2">
......@@ -241,7 +241,7 @@
<goal name="f2">
<proof prover="0"><result status="timeout" time="4.78"/></proof>
<proof prover="1"><result status="timeout" time="4.96"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
</goal>
<goal name="g3">
......@@ -263,7 +263,7 @@
<goal name="f3">
<proof prover="0"><result status="timeout" time="4.98"/></proof>
<proof prover="1"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="4.93"/></proof>
</goal>
<goal name="g4a">
......@@ -295,7 +295,7 @@
<goal name="f7">
<proof prover="0"><result status="timeout" time="4.95"/></proof>
<proof prover="1"><result status="timeout" time="4.99"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="g8a">
......@@ -531,49 +531,49 @@
<goal name="smoke1" expanded="true">
<proof prover="0"><result status="timeout" time="4.98"/></proof>
<proof prover="1"><result status="timeout" time="4.97"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="smoke2" expanded="true">
<proof prover="0"><result status="timeout" time="4.84"/></proof>
<proof prover="1"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke3" expanded="true">
<proof prover="0"><result status="timeout" time="4.81"/></proof>
<proof prover="1"><result status="timeout" time="4.96"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke4" expanded="true">
<proof prover="0"><result status="timeout" time="4.85"/></proof>
<proof prover="1"><result status="timeout" time="4.96"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke5" expanded="true">
<proof prover="0"><result status="timeout" time="4.96"/></proof>
<proof prover="1"><result status="timeout" time="4.99"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.03"/></proof>
</goal>
<goal name="smoke6" expanded="true">
<proof prover="0"><result status="timeout" time="4.95"/></proof>
<proof prover="1"><result status="timeout" time="4.99"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="smoke7" expanded="true">
<proof prover="0"><result status="timeout" time="4.78"/></proof>
<proof prover="1"><result status="timeout" time="4.94"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
</goal>
<goal name="smoke8" expanded="true">
<proof prover="0"><result status="timeout" time="4.97"/></proof>
<proof prover="1"><result status="timeout" time="4.99"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="4.97"/></proof>
</goal>
</theory>
......@@ -750,49 +750,49 @@
<goal name="smoke1" expanded="true">
<proof prover="0"><result status="timeout" time="4.90"/></proof>
<proof prover="1"><result status="timeout" time="4.95"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
</goal>
<goal name="smoke2" expanded="true">
<proof prover="0"><result status="timeout" time="4.96"/></proof>
<proof prover="1"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.02"/></proof>
</goal>
<goal name="smoke3" expanded="true">
<proof prover="0"><result status="timeout" time="4.79"/></proof>
<proof prover="1"><result status="timeout" time="4.94"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
</goal>
<goal name="smoke4" expanded="true">
<proof prover="0"><result status="timeout" time="4.78"/></proof>
<proof prover="1"><result status="timeout" time="4.97"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke5" expanded="true">
<proof prover="0"><result status="timeout" time="4.96"/></proof>
<proof prover="1"><result status="timeout" time="4.97"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
</goal>
<goal name="smoke6" expanded="true">
<proof prover="0"><result status="timeout" time="4.90"/></proof>
<proof prover="1"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="smoke7" expanded="true">
<proof prover="0"><result status="timeout" time="4.33"/></proof>
<proof prover="1"><result status="timeout" time="4.97"/></proof>
<proof prover="2"><result status="timeout" time="5.96"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="smoke8" expanded="true">
<proof prover="0"><result status="timeout" time="4.95"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="4.98"/></proof>
</goal>
</theory>
......@@ -969,49 +969,49 @@
<goal name="smoke1" expanded="true">
<proof prover="0"><result status="timeout" time="4.98"/></proof>
<proof prover="1"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="5.02"/></proof>
</goal>
<goal name="smoke2" expanded="true">
<proof prover="0"><result status="timeout" time="4.64"/></proof>
<proof prover="1"><result status="timeout" time="4.97"/></proof>
<proof prover="2"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.97"/></proof>
</goal>
<goal name="smoke3" expanded="true">
<proof prover="0"><result status="timeout" time="4.99"/></proof>
<proof prover="1"><result status="timeout" time="5.01"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.98"/></proof>
</goal>
<goal name="smoke4" expanded="true">
<proof prover="0"><result status="timeout" time="4.99"/></proof>
<proof prover="1"><result status="timeout" time="4.99"/></proof>
<proof prover="2"><result status="timeout" time="5.97"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="smoke5" expanded="true">
<proof prover="0"><result status="timeout" time="4.99"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="smoke6" expanded="true">
<proof prover="0"><result status="timeout" time="4.87"/></proof>
<proof prover="1"><result status="timeout" time="4.97"/></proof>
<proof prover="2"><result status="timeout" time="5.99"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
</goal>
<goal name="smoke7" expanded="true">
<proof prover="0"><result status="timeout" time="4.59"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.98"/></proof>
</goal>
<goal name="smoke8" expanded="true">
<proof prover="0"><result status="timeout" time="4.99"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.98"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.98"/></proof>
</goal>
</theory>
......
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