Metitarski: more examples

examples/logic/my_cosine/why3session.xml

@@ -13,6 +13,10 @@
   id="2"
   name="Gappa"
   version="1.0.0"/>
+ <prover
+  id="3"
+  name="MetiTarski"
+  version="2.2"/>
  <file
   name="../my_cosine.why"
   verified="true"
@@ -40,6 +44,14 @@
      archived="false">
      <result status="valid" time="3.79"/>
     </proof>
+    <proof
+     prover="3"
+     timelimit="60"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="1.09"/>
+    </proof>
    </goal>
    <goal
     name="TotalErrorFullyExpanded"

examples/tests-provers/metitarski.why

@@ -34,5 +34,14 @@ theory P3
   goal cos_bound_harder :
     forall x:real. -0.7 <= x <= 0.7 -> 0.7 <= cos x <= 1.0
 
+
+  use import real.Abs
+
+  goal MethodErrorOK: forall x:real. abs x <= 0x1p-5 ->
+    abs (1.0 - 0.5 * (x * x) - cos x) <= 0x1p-24
+
+  goal MethodErrorWrong: forall x:real. abs x <= 0x1p-5 ->
+    abs (1.0 - 0.5 * (x * x) - cos x) <= 0x1p-25
+
 end
 

examples/tests-provers/metitarski/why3session.xml

@@ -115,6 +115,40 @@
      <result status="valid" time="0.94"/>
     </proof>
    </goal>
+   <goal
+    name="MethodErrorOK"
+    locfile="../metitarski.why"
+    loclnum="40" loccnumb="7" loccnume="20"
+    sum="27b7a4e648329fb8ba1034be92b6d410"
+    proved="true"
+    expanded="true"
+    shape="ainfix &lt;=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix &lt;=aabsV0c0x1.p-5F">
+    <proof
+     prover="0"
+     timelimit="60"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.72"/>
+    </proof>
+   </goal>
+   <goal
+    name="MethodErrorWrong"
+    locfile="../metitarski.why"
+    loclnum="43" loccnumb="7" loccnume="23"
+    sum="f4c30d39014556466d647e5f1aef352a"
+    proved="false"
+    expanded="true"
+    shape="ainfix &lt;=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-25Iainfix &lt;=aabsV0c0x1.p-5F">
+    <proof
+     prover="0"
+     timelimit="60"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="unknown" time="17.02"/>
+    </proof>
+   </goal>
   </theory>
  </file>
 </why3session>