From 9ea9cc34b64ef41f134aa4630688f30ae8904e08 Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Fri, 25 May 2012 10:28:27 +0200
Subject: [PATCH] Bitvector example: more proofs

---
 examples/bitvectors/double/why3session.xml    |  36 +-
 .../bitvectors/neg_as_xor/why3session.xml     |  68 +--
 examples/bitvectors/power2/why3session.xml    | 452 +++++++++---------
 3 files changed, 278 insertions(+), 278 deletions(-)

diff --git a/examples/bitvectors/double/why3session.xml b/examples/bitvectors/double/why3session.xml
index 55df81019..410abac5c 100644
--- a/examples/bitvectors/double/why3session.xml
+++ b/examples/bitvectors/double/why3session.xml
@@ -47,7 +47,7 @@
     name="nth_one1"
     locfile="bitvectors/double/../double.why"
     loclnum="73" loccnumb="8" loccnume="16"
-    sum="d18ab08209f31f731dfd704613a2e30b"
+    sum="3848d3fd3fbc40c879e047aaab4a85a2"
     proved="true"
     expanded="false"
     shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c51Aainfix &lt;=c0V0F">
@@ -64,7 +64,7 @@
     name="nth_one2"
     locfile="bitvectors/double/../double.why"
     loclnum="74" loccnumb="8" loccnume="16"
-    sum="dbdf93155a985325f8f4fedd2cc1ce23"
+    sum="719c2d2317fadc995adafb386c90b2c5"
     proved="true"
     expanded="false"
     shape="ainfix =anthaoneV0aTrueIainfix &lt;=V0c61Aainfix &lt;=c52V0F">
@@ -74,14 +74,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.05"/>
+     <result status="valid" time="0.07"/>
     </proof>
    </goal>
    <goal
     name="nth_one3"
     locfile="bitvectors/double/../double.why"
     loclnum="75" loccnumb="8" loccnume="16"
-    sum="78dcef156ce4f14b8c06646563922753"
+    sum="6778125994116ef0019c84160a720db2"
     proved="true"
     expanded="false"
     shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c63Aainfix &lt;=c62V0F">
@@ -91,14 +91,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.06"/>
+     <result status="valid" time="0.07"/>
     </proof>
    </goal>
    <goal
     name="sign_one"
     locfile="bitvectors/double/../double.why"
     loclnum="77" loccnumb="8" loccnume="16"
-    sum="ff5eb7f2e82fa0653ea1884adaa61d9f"
+    sum="b70858eca86de90b74841ff3d76acfbc"
     proved="true"
     expanded="false"
     shape="ainfix =asignaoneaFalse">
@@ -108,7 +108,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.10"/>
+     <result status="valid" time="0.12"/>
     </proof>
     <proof
      prover="1"
@@ -124,7 +124,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.03"/>
     </proof>
     <proof
      prover="2"
@@ -132,7 +132,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.03"/>
     </proof>
     <proof
      prover="5"
@@ -140,14 +140,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.10"/>
+     <result status="valid" time="0.12"/>
     </proof>
    </goal>
    <goal
     name="exp_one"
     locfile="bitvectors/double/../double.why"
     loclnum="78" loccnumb="8" loccnume="15"
-    sum="08f27bcd545f7664746d5232bff96501"
+    sum="15a5f4ba0b6c6193db79d281053be198"
     proved="true"
     expanded="false"
     shape="ainfix =aexpaonec1023">
@@ -157,7 +157,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="4.87"/>
+     <result status="valid" time="0.58"/>
     </proof>
     <proof
      prover="3"
@@ -166,14 +166,14 @@
      edited="double_TestDouble_exp_one_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.60"/>
+     <result status="valid" time="0.66"/>
     </proof>
    </goal>
    <goal
     name="mantissa_one"
     locfile="bitvectors/double/../double.why"
     loclnum="79" loccnumb="8" loccnume="20"
-    sum="3916c94461ebce50b2aa55917a3011b8"
+    sum="d8d24976ea1004e5f2a002910f1f0307"
     proved="true"
     expanded="false"
     shape="ainfix =amantissaaonec0">
@@ -183,7 +183,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.67"/>
+     <result status="valid" time="0.77"/>
     </proof>
     <proof
      prover="0"
@@ -199,14 +199,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.98"/>
+     <result status="valid" time="3.21"/>
     </proof>
    </goal>
    <goal
     name="double_value_of_1"
     locfile="bitvectors/double/../double.why"
     loclnum="81" loccnumb="8" loccnume="25"
-    sum="d5d64f7ab2d369243a42739379eb07a9"
+    sum="fef95cf59dfcb5007abf14eb78393ff2"
     proved="true"
     expanded="false"
     shape="ainfix =adouble_of_bv64aonec1.0">
@@ -216,7 +216,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.03"/>
     </proof>
     <proof
      prover="0"
diff --git a/examples/bitvectors/neg_as_xor/why3session.xml b/examples/bitvectors/neg_as_xor/why3session.xml
index 064484d41..1b0fc27e5 100644
--- a/examples/bitvectors/neg_as_xor/why3session.xml
+++ b/examples/bitvectors/neg_as_xor/why3session.xml
@@ -32,7 +32,7 @@
     name="Nth_j"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="13" loccnumb="8" loccnume="13"
-    sum="abc7eaee768e35d633c1052837f84c8c"
+    sum="313f7cfd9cb238cefe6b30a61ef11c31"
     proved="true"
     expanded="false"
     shape="ainfix =anthajV0aFalseIainfix &lt;=V0c62Aainfix &lt;=c0V0F">
@@ -42,14 +42,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.08"/>
+     <result status="valid" time="0.09"/>
     </proof>
    </goal>
    <goal
     name="sign_of_j"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="15" loccnumb="8" loccnume="17"
-    sum="34eec7200ed8e48eaf94d3cc7620a3dc"
+    sum="1c5c190d58ac88ccf9f66a6e92798676"
     proved="true"
     expanded="false"
     shape="ainfix =asignajaTrue">
@@ -66,7 +66,7 @@
     name="mantissa_of_j"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="16" loccnumb="8" loccnume="21"
-    sum="6970305c1ef7a17012115ef268945552"
+    sum="522d8bafdca7f060bd6692b30a154154"
     proved="true"
     expanded="false"
     shape="ainfix =amantissaajc0">
@@ -76,7 +76,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.66"/>
+     <result status="valid" time="0.74"/>
     </proof>
     <proof
      prover="0"
@@ -84,7 +84,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.14"/>
+     <result status="valid" time="0.16"/>
     </proof>
     <proof
      prover="3"
@@ -92,14 +92,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="3.40"/>
+     <result status="valid" time="3.69"/>
     </proof>
    </goal>
    <goal
     name="exp_of_j"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="17" loccnumb="8" loccnume="16"
-    sum="8faf4117201f47f3d9a2bbedaae3c556"
+    sum="8124c943d92944659f01f19ed43f7c04"
     proved="true"
     expanded="false"
     shape="ainfix =aexpajc0">
@@ -109,7 +109,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.66"/>
+     <result status="valid" time="0.74"/>
     </proof>
     <proof
      prover="0"
@@ -117,7 +117,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.14"/>
+     <result status="valid" time="0.16"/>
     </proof>
     <proof
      prover="3"
@@ -125,14 +125,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="3.21"/>
+     <result status="valid" time="3.08"/>
     </proof>
    </goal>
    <goal
     name="int_of_bv"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="18" loccnumb="8" loccnume="17"
-    sum="aa658bdd2ce269f4bcf82983ea27b498"
+    sum="d341fed6fab8b02bd0bba58deeb31623"
     proved="true"
     expanded="false"
     shape="ainfix =adouble_of_bv64ajc0.0">
@@ -142,7 +142,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.11"/>
+     <result status="valid" time="0.12"/>
     </proof>
     <proof
      prover="0"
@@ -158,14 +158,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.10"/>
+     <result status="valid" time="0.12"/>
     </proof>
    </goal>
    <goal
     name="MainResultBits"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="20" loccnumb="8" loccnume="22"
-    sum="03bfc9513d319c9b73254a74d633013c"
+    sum="9ea8f95e8958d5af3426f01ba4e45dbf"
     proved="true"
     expanded="false"
     shape="ainfix =anthabw_xorV0ajV1anthV0V1Iainfix &lt;V1c63Aainfix &lt;=c0V1FF">
@@ -182,7 +182,7 @@
     name="MainResultSign"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="23" loccnumb="8" loccnume="22"
-    sum="4f563eb91bd49148fab0954a7ac4b7a8"
+    sum="9b95d73cc715f26a6e4a596ad40601a2"
     proved="true"
     expanded="false"
     shape="ainfix =anthabw_xorV0ajc63anotbanthV0c63F">
@@ -192,14 +192,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.03"/>
     </proof>
    </goal>
    <goal
     name="Sign_of_xor_j"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="25" loccnumb="8" loccnume="21"
-    sum="b19c46ce4058940cea14d79fc9d3d0c0"
+    sum="5c22f51afd72897f2722925bdf3ca2b0"
     proved="true"
     expanded="false"
     shape="ainfix =asignabw_xorV0ajanotbasignV0F">
@@ -232,7 +232,7 @@
     name="Exp_of_xor_j"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="27" loccnumb="8" loccnume="20"
-    sum="bf6f51fa79aaec331c331c4b0ebda5dd"
+    sum="ccbeb8d697184227f9f75d9bacb2a039"
     proved="true"
     expanded="false"
     shape="ainfix =aexpabw_xorV0ajaexpV0F">
@@ -242,7 +242,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.69"/>
+     <result status="valid" time="0.76"/>
     </proof>
     <proof
      prover="0"
@@ -250,7 +250,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.91"/>
+     <result status="valid" time="0.96"/>
     </proof>
     <proof
      prover="3"
@@ -258,14 +258,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="3.16"/>
+     <result status="valid" time="3.39"/>
     </proof>
    </goal>
    <goal
     name="Mantissa_of_xor_j"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="29" loccnumb="8" loccnume="25"
-    sum="5742f66ed818a0906e1a42f5abc3f359"
+    sum="14f714cc419ba2f8a7c89860ce5b945b"
     proved="true"
     expanded="false"
     shape="ainfix =amantissaabw_xorV0ajamantissaV0F">
@@ -275,7 +275,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.69"/>
+     <result status="valid" time="0.77"/>
     </proof>
     <proof
      prover="0"
@@ -283,7 +283,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.56"/>
+     <result status="valid" time="0.60"/>
     </proof>
     <proof
      prover="3"
@@ -291,14 +291,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="3.32"/>
+     <result status="valid" time="3.58"/>
     </proof>
    </goal>
    <goal
     name="MainResultZero"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="31" loccnumb="8" loccnume="22"
-    sum="921818a19cb7e0dd4adaa3784b678292"
+    sum="397e23c002ef82f6a4eace3139cc49c2"
     proved="true"
     expanded="false"
     shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix =amantissaV0c0Aainfix =c0aexpV0F">
@@ -308,7 +308,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.67"/>
+     <result status="valid" time="1.07"/>
     </proof>
     <proof
      prover="0"
@@ -316,7 +316,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.72"/>
+     <result status="valid" time="0.39"/>
     </proof>
     <proof
      prover="3"
@@ -324,14 +324,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="3.10"/>
+     <result status="valid" time="3.58"/>
     </proof>
    </goal>
    <goal
     name="sign_neg"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="34" loccnumb="8" loccnume="16"
-    sum="b54402c83b94259ef155185ddfdf1260"
+    sum="610aa54b635d7d1565a29d17127341ca"
     proved="true"
     expanded="false"
     shape="ainfix =asign_valueanotbasignV0aprefix -.asign_valueasignV0F">
@@ -341,14 +341,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.80"/>
+     <result status="valid" time="0.34"/>
     </proof>
    </goal>
    <goal
     name="MainResult"
     locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
     loclnum="36" loccnumb="8" loccnume="18"
-    sum="fa6f38fbf181f139fbf31b549f4e91ba"
+    sum="99f2c975165d320981338aa6c0532b76"
     proved="true"
     expanded="true"
     shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix &lt;aexpV0c2047Aainfix &lt;c0aexpV0F">
@@ -359,7 +359,7 @@
      edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.91"/>
+     <result status="valid" time="1.03"/>
     </proof>
    </goal>
   </theory>
diff --git a/examples/bitvectors/power2/why3session.xml b/examples/bitvectors/power2/why3session.xml
index 52ba486bd..f396d9d98 100644
--- a/examples/bitvectors/power2/why3session.xml
+++ b/examples/bitvectors/power2/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="power2/why3session.xml">
+ name="bitvectors/power2/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -36,13 +36,13 @@
   expanded="true">
   <theory
    name="Pow2int"
-   locfile="power2/../power2.why"
+   locfile="bitvectors/power2/../power2.why"
    loclnum="1" loccnumb="7" loccnume="14"
    verified="false"
    expanded="true">
    <goal
     name="Power_1"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="11" loccnumb="8" loccnume="15"
     sum="33bc32635e211600fb0149bbdc4cf0c0"
     proved="true"
@@ -70,7 +70,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
     <proof
      prover="2"
@@ -91,7 +91,7 @@
    </goal>
    <goal
     name="Power_sum"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="13" loccnumb="8" loccnume="17"
     sum="01d41b81dadfb478ff33dc9bdb7d39d1"
     proved="true"
@@ -104,12 +104,12 @@
      edited="power2_Pow2int_Power_sum_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.57"/>
+     <result status="valid" time="0.64"/>
     </proof>
    </goal>
    <goal
     name="pow2pos"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="16" loccnumb="8" loccnume="15"
     sum="b29b0d96b6d1c61cf88cd8d6542f22be"
     proved="true"
@@ -122,12 +122,12 @@
      edited="power2_Pow2int_pow2pos_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.55"/>
+     <result status="valid" time="0.61"/>
     </proof>
    </goal>
    <goal
     name="pow2_0"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="18" loccnumb="8" loccnume="14"
     sum="c994e6847b65cec02a9a67a7e1256098"
     proved="true"
@@ -184,7 +184,7 @@
    </goal>
    <goal
     name="pow2_1"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="19" loccnumb="8" loccnume="14"
     sum="0b0ec2b029c61974ce68d31d6f97a172"
     proved="true"
@@ -241,7 +241,7 @@
    </goal>
    <goal
     name="pow2_2"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="20" loccnumb="8" loccnume="14"
     sum="4f65b737ca06c7a2538ccc1a85cfc646"
     proved="true"
@@ -290,7 +290,7 @@
    </goal>
    <goal
     name="pow2_3"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="21" loccnumb="8" loccnume="14"
     sum="a4b54f2d0edef5ff1c8eed3b1f51abdf"
     proved="true"
@@ -318,7 +318,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="2"
@@ -339,7 +339,7 @@
    </goal>
    <goal
     name="pow2_4"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="22" loccnumb="8" loccnume="14"
     sum="bf783d4854f46bf58b30fa7956ffd130"
     proved="true"
@@ -388,7 +388,7 @@
    </goal>
    <goal
     name="pow2_5"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="23" loccnumb="8" loccnume="14"
     sum="43e68e6fad9b81b6d461bdffdfd4adb1"
     proved="true"
@@ -437,7 +437,7 @@
    </goal>
    <goal
     name="pow2_6"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="24" loccnumb="8" loccnume="14"
     sum="edc89c31e276d5ffaa0ff0cd08204f48"
     proved="true"
@@ -465,7 +465,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="2"
@@ -486,7 +486,7 @@
    </goal>
    <goal
     name="pow2_7"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="25" loccnumb="8" loccnume="14"
     sum="f83d53a4545b22268771697dc2c62487"
     proved="true"
@@ -514,7 +514,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
     <proof
      prover="2"
@@ -535,7 +535,7 @@
    </goal>
    <goal
     name="pow2_8"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="26" loccnumb="8" loccnume="14"
     sum="ea2922b4ffd5b891f1846a24141d0834"
     proved="true"
@@ -584,7 +584,7 @@
    </goal>
    <goal
     name="pow2_9"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="27" loccnumb="8" loccnume="14"
     sum="f2b729150337fdf74924ab9057b89793"
     proved="true"
@@ -633,7 +633,7 @@
    </goal>
    <goal
     name="pow2_10"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="28" loccnumb="8" loccnume="15"
     sum="9e79db755f052e76ecb4becea2b9845d"
     proved="true"
@@ -645,7 +645,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
     <proof
      prover="1"
@@ -682,7 +682,7 @@
    </goal>
    <goal
     name="pow2_11"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="29" loccnumb="8" loccnume="15"
     sum="3950419939a5e90300324e52aea6ef85"
     proved="true"
@@ -726,12 +726,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_12"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="30" loccnumb="8" loccnume="15"
     sum="c9ed517871342bec322595770124fe37"
     proved="true"
@@ -743,7 +743,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="1"
@@ -780,7 +780,7 @@
    </goal>
    <goal
     name="pow2_13"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="31" loccnumb="8" loccnume="15"
     sum="f7d72c29f3a98202b0a3be6da33033bf"
     proved="true"
@@ -829,7 +829,7 @@
    </goal>
    <goal
     name="pow2_14"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="32" loccnumb="8" loccnume="15"
     sum="e604c4ddf3db0c526a8db70bbeb7581d"
     proved="true"
@@ -841,7 +841,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.07"/>
+     <result status="valid" time="0.08"/>
     </proof>
     <proof
      prover="1"
@@ -878,7 +878,7 @@
    </goal>
    <goal
     name="pow2_15"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="33" loccnumb="8" loccnume="15"
     sum="399711f79855e75335e47faacc32f345"
     proved="true"
@@ -890,7 +890,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.08"/>
+     <result status="valid" time="0.10"/>
     </proof>
     <proof
      prover="1"
@@ -927,7 +927,7 @@
    </goal>
    <goal
     name="pow2_16"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="34" loccnumb="8" loccnume="15"
     sum="5b82174a654aa73e5fb688f529c0f7bf"
     proved="true"
@@ -939,7 +939,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.03"/>
     </proof>
     <proof
      prover="1"
@@ -976,7 +976,7 @@
    </goal>
    <goal
     name="pow2_17"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="35" loccnumb="8" loccnume="15"
     sum="ba6abc2aaab40b02122bd18370865673"
     proved="true"
@@ -988,7 +988,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.12"/>
+     <result status="valid" time="0.13"/>
     </proof>
     <proof
      prover="1"
@@ -1020,12 +1020,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.03"/>
     </proof>
    </goal>
    <goal
     name="pow2_18"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="36" loccnumb="8" loccnume="15"
     sum="2f3ddd1467a373a44e5f33345096d5d0"
     proved="true"
@@ -1037,7 +1037,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.13"/>
+     <result status="valid" time="0.14"/>
     </proof>
     <proof
      prover="1"
@@ -1053,7 +1053,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="2"
@@ -1069,12 +1069,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.03"/>
     </proof>
    </goal>
    <goal
     name="pow2_19"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="37" loccnumb="8" loccnume="15"
     sum="e757257a58f3bf3ea729c1b7492dd7ef"
     proved="true"
@@ -1123,7 +1123,7 @@
    </goal>
    <goal
     name="pow2_20"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="38" loccnumb="8" loccnume="15"
     sum="a387c15571e5972cda3e86f2ac723094"
     proved="true"
@@ -1135,7 +1135,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.17"/>
+     <result status="valid" time="0.18"/>
     </proof>
     <proof
      prover="1"
@@ -1159,7 +1159,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="6"
@@ -1167,12 +1167,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.04"/>
     </proof>
    </goal>
    <goal
     name="pow2_21"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="39" loccnumb="8" loccnume="15"
     sum="debddd70613cc7634397652622ecda4b"
     proved="true"
@@ -1184,7 +1184,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.19"/>
+     <result status="valid" time="0.21"/>
     </proof>
     <proof
      prover="1"
@@ -1200,7 +1200,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="2"
@@ -1221,7 +1221,7 @@
    </goal>
    <goal
     name="pow2_22"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="40" loccnumb="8" loccnume="15"
     sum="7045b8d62b5df621a36f590fe34facfe"
     proved="true"
@@ -1249,7 +1249,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="2"
@@ -1265,12 +1265,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.05"/>
     </proof>
    </goal>
    <goal
     name="pow2_23"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="41" loccnumb="8" loccnume="15"
     sum="6f6e42723d0b37b0b9a7300d5033c1f5"
     proved="true"
@@ -1282,7 +1282,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.22"/>
+     <result status="valid" time="0.25"/>
     </proof>
     <proof
      prover="1"
@@ -1298,7 +1298,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="2"
@@ -1314,12 +1314,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.06"/>
     </proof>
    </goal>
    <goal
     name="pow2_24"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="42" loccnumb="8" loccnume="15"
     sum="46c5ca50bcf19b2c6bae899c24cf9ff2"
     proved="true"
@@ -1331,7 +1331,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.05"/>
+     <result status="valid" time="0.06"/>
     </proof>
     <proof
      prover="1"
@@ -1347,7 +1347,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="2"
@@ -1363,12 +1363,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.05"/>
+     <result status="valid" time="0.06"/>
     </proof>
    </goal>
    <goal
     name="pow2_25"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="43" loccnumb="8" loccnume="15"
     sum="4b56b77a1203480aa720a9c28af57f5c"
     proved="true"
@@ -1380,7 +1380,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.27"/>
+     <result status="valid" time="0.32"/>
     </proof>
     <proof
      prover="1"
@@ -1412,12 +1412,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.05"/>
+     <result status="valid" time="0.07"/>
     </proof>
    </goal>
    <goal
     name="pow2_26"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="44" loccnumb="8" loccnume="15"
     sum="6b73dcf0eee1815c66e068cd4152cb4f"
     proved="true"
@@ -1429,7 +1429,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.06"/>
+     <result status="valid" time="0.08"/>
     </proof>
     <proof
      prover="1"
@@ -1445,7 +1445,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="2"
@@ -1453,7 +1453,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="6"
@@ -1466,7 +1466,7 @@
    </goal>
    <goal
     name="pow2_27"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="45" loccnumb="8" loccnume="15"
     sum="f5ac36dbd016fd8c8d009f71672d31f2"
     proved="true"
@@ -1478,7 +1478,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.32"/>
+     <result status="valid" time="0.38"/>
     </proof>
     <proof
      prover="1"
@@ -1494,7 +1494,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="2"
@@ -1510,12 +1510,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.06"/>
+     <result status="valid" time="0.07"/>
     </proof>
    </goal>
    <goal
     name="pow2_28"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="46" loccnumb="8" loccnume="15"
     sum="ad8665c7b3fd4da84624cd5690438a64"
     proved="true"
@@ -1527,7 +1527,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.08"/>
+     <result status="valid" time="0.09"/>
     </proof>
     <proof
      prover="1"
@@ -1551,7 +1551,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="6"
@@ -1559,12 +1559,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.07"/>
+     <result status="valid" time="0.08"/>
     </proof>
    </goal>
    <goal
     name="pow2_29"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="47" loccnumb="8" loccnume="15"
     sum="0cc89038ea8a0cadb76445ef3f9832f6"
     proved="true"
@@ -1576,7 +1576,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.08"/>
+     <result status="valid" time="0.09"/>
     </proof>
     <proof
      prover="1"
@@ -1613,7 +1613,7 @@
    </goal>
    <goal
     name="pow2_30"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="48" loccnumb="8" loccnume="15"
     sum="0eacc1ed9b4dcf0f14c3bf92babac3ab"
     proved="true"
@@ -1625,7 +1625,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.09"/>
+     <result status="valid" time="0.10"/>
     </proof>
     <proof
      prover="1"
@@ -1641,7 +1641,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="2"
@@ -1657,12 +1657,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.08"/>
+     <result status="valid" time="0.10"/>
     </proof>
    </goal>
    <goal
     name="pow2_31"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="49" loccnumb="8" loccnume="15"
     sum="789f3a0cdf976fcaea5bd9f68f905d43"
     proved="true"
@@ -1674,7 +1674,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.44"/>
+     <result status="valid" time="0.52"/>
     </proof>
     <proof
      prover="1"
@@ -1706,12 +1706,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.09"/>
+     <result status="valid" time="0.11"/>
     </proof>
    </goal>
    <goal
     name="pow2_32"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="50" loccnumb="8" loccnume="15"
     sum="5262eac4035547e7eb55ca457cbd7c7e"
     proved="true"
@@ -1723,7 +1723,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.48"/>
+     <result status="valid" time="0.57"/>
     </proof>
     <proof
      prover="1"
@@ -1755,12 +1755,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.51"/>
+     <result status="valid" time="0.57"/>
     </proof>
    </goal>
    <goal
     name="pow2_33"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="51" loccnumb="8" loccnume="15"
     sum="d845391a2c6a983a6621353e176b1ad3"
     proved="true"
@@ -1772,7 +1772,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.52"/>
+     <result status="valid" time="0.59"/>
     </proof>
     <proof
      prover="1"
@@ -1804,12 +1804,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.53"/>
+     <result status="valid" time="0.61"/>
     </proof>
    </goal>
    <goal
     name="pow2_34"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="52" loccnumb="8" loccnume="15"
     sum="142a6ab59a27d2c2317655b4c03e58b4"
     proved="true"
@@ -1821,7 +1821,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.59"/>
+     <result status="valid" time="0.65"/>
     </proof>
     <proof
      prover="1"
@@ -1837,7 +1837,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="2"
@@ -1853,12 +1853,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.57"/>
+     <result status="valid" time="0.65"/>
     </proof>
    </goal>
    <goal
     name="pow2_35"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="53" loccnumb="8" loccnume="15"
     sum="fbb033469a89ed98217a05bba3d74b32"
     proved="true"
@@ -1870,7 +1870,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.64"/>
+     <result status="valid" time="0.69"/>
     </proof>
     <proof
      prover="1"
@@ -1902,12 +1902,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.60"/>
+     <result status="valid" time="0.70"/>
     </proof>
    </goal>
    <goal
     name="pow2_36"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="54" loccnumb="8" loccnume="15"
     sum="92f43e03030de82dc9bf0d98e40cb3ad"
     proved="true"
@@ -1919,7 +1919,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.66"/>
+     <result status="valid" time="0.75"/>
     </proof>
     <proof
      prover="1"
@@ -1935,7 +1935,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="2"
@@ -1951,12 +1951,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.66"/>
+     <result status="valid" time="0.74"/>
     </proof>
    </goal>
    <goal
     name="pow2_37"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="55" loccnumb="8" loccnume="15"
     sum="5caf707cb46921197653d5c3b8eaff3d"
     proved="true"
@@ -1968,7 +1968,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.71"/>
+     <result status="valid" time="0.80"/>
     </proof>
     <proof
      prover="1"
@@ -2000,12 +2000,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.71"/>
+     <result status="valid" time="0.79"/>
     </proof>
    </goal>
    <goal
     name="pow2_38"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="56" loccnumb="8" loccnume="15"
     sum="c56f100f4f627a081f3e072965c8ad33"
     proved="true"
@@ -2017,7 +2017,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.78"/>
+     <result status="valid" time="0.85"/>
     </proof>
     <proof
      prover="1"
@@ -2049,12 +2049,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.74"/>
+     <result status="valid" time="0.84"/>
     </proof>
    </goal>
    <goal
     name="pow2_39"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="57" loccnumb="8" loccnume="15"
     sum="83793e44a36f197298a98c14723acafe"
     proved="true"
@@ -2066,7 +2066,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.81"/>
+     <result status="valid" time="0.91"/>
     </proof>
     <proof
      prover="1"
@@ -2098,12 +2098,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.82"/>
+     <result status="valid" time="0.93"/>
     </proof>
    </goal>
    <goal
     name="pow2_40"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="58" loccnumb="8" loccnume="15"
     sum="43358f583e28a318ace73e9a67c93d5f"
     proved="true"
@@ -2115,7 +2115,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.85"/>
+     <result status="valid" time="0.96"/>
     </proof>
     <proof
      prover="1"
@@ -2139,7 +2139,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="6"
@@ -2147,12 +2147,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.88"/>
+     <result status="valid" time="1.00"/>
     </proof>
    </goal>
    <goal
     name="pow2_41"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="59" loccnumb="8" loccnume="15"
     sum="8da953e11fe6fb80e047aaa8f6825519"
     proved="true"
@@ -2164,7 +2164,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.94"/>
+     <result status="valid" time="1.01"/>
     </proof>
     <proof
      prover="1"
@@ -2196,12 +2196,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.91"/>
+     <result status="valid" time="1.04"/>
     </proof>
    </goal>
    <goal
     name="pow2_42"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="60" loccnumb="8" loccnume="15"
     sum="03d89edee6599784dbc6edd582b98ad0"
     proved="true"
@@ -2213,7 +2213,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.96"/>
+     <result status="valid" time="1.11"/>
     </proof>
     <proof
      prover="1"
@@ -2245,12 +2245,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.01"/>
+     <result status="valid" time="1.10"/>
     </proof>
    </goal>
    <goal
     name="pow2_43"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="61" loccnumb="8" loccnume="15"
     sum="24b23bf8048a3af0567fc9a4f46b48c1"
     proved="true"
@@ -2262,7 +2262,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.01"/>
+     <result status="valid" time="1.13"/>
     </proof>
     <proof
      prover="1"
@@ -2294,12 +2294,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.08"/>
+     <result status="valid" time="1.23"/>
     </proof>
    </goal>
    <goal
     name="pow2_44"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="62" loccnumb="8" loccnume="15"
     sum="4ef8deca27b1026578401e9b975f01c2"
     proved="true"
@@ -2311,7 +2311,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.10"/>
+     <result status="valid" time="1.18"/>
     </proof>
     <proof
      prover="1"
@@ -2319,7 +2319,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="0"
@@ -2335,7 +2335,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.04"/>
     </proof>
     <proof
      prover="6"
@@ -2343,12 +2343,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.13"/>
+     <result status="valid" time="1.26"/>
     </proof>
    </goal>
    <goal
     name="pow2_45"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="63" loccnumb="8" loccnume="15"
     sum="15059037a55ca44268db07aba0fdd1ac"
     proved="true"
@@ -2360,7 +2360,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.14"/>
+     <result status="valid" time="1.30"/>
     </proof>
     <proof
      prover="1"
@@ -2376,7 +2376,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.03"/>
     </proof>
     <proof
      prover="2"
@@ -2392,12 +2392,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.28"/>
+     <result status="valid" time="1.39"/>
     </proof>
    </goal>
    <goal
     name="pow2_46"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="64" loccnumb="8" loccnume="15"
     sum="8ffabfeee5950833cf7a42871098d831"
     proved="true"
@@ -2409,7 +2409,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.17"/>
+     <result status="valid" time="1.32"/>
     </proof>
     <proof
      prover="1"
@@ -2425,7 +2425,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.03"/>
     </proof>
     <proof
      prover="2"
@@ -2433,7 +2433,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.04"/>
     </proof>
     <proof
      prover="6"
@@ -2441,12 +2441,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.41"/>
+     <result status="valid" time="1.58"/>
     </proof>
    </goal>
    <goal
     name="pow2_47"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="65" loccnumb="8" loccnume="15"
     sum="9e22735c31e26f8b90ba7d36b9615435"
     proved="true"
@@ -2458,7 +2458,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.29"/>
+     <result status="valid" time="1.38"/>
     </proof>
     <proof
      prover="1"
@@ -2474,7 +2474,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.03"/>
     </proof>
     <proof
      prover="2"
@@ -2490,12 +2490,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.47"/>
+     <result status="valid" time="1.64"/>
     </proof>
    </goal>
    <goal
     name="pow2_48"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="66" loccnumb="8" loccnume="15"
     sum="3d51e86d67da4c147d28f2263435125a"
     proved="true"
@@ -2507,7 +2507,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.32"/>
+     <result status="valid" time="1.45"/>
     </proof>
     <proof
      prover="1"
@@ -2539,12 +2539,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.68"/>
+     <result status="valid" time="1.89"/>
     </proof>
    </goal>
    <goal
     name="pow2_49"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="67" loccnumb="8" loccnume="15"
     sum="8153706358800abb69cf022dc2511fac"
     proved="true"
@@ -2556,7 +2556,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.36"/>
+     <result status="valid" time="1.53"/>
     </proof>
     <proof
      prover="1"
@@ -2572,7 +2572,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="2"
@@ -2588,12 +2588,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.82"/>
+     <result status="valid" time="1.99"/>
     </proof>
    </goal>
    <goal
     name="pow2_50"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="68" loccnumb="8" loccnume="15"
     sum="b8c783e12a9aedc6c4529eff27df5361"
     proved="true"
@@ -2605,7 +2605,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.44"/>
+     <result status="valid" time="1.68"/>
     </proof>
     <proof
      prover="1"
@@ -2613,7 +2613,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="0"
@@ -2621,7 +2621,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.03"/>
     </proof>
     <proof
      prover="2"
@@ -2637,12 +2637,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.04"/>
+     <result status="valid" time="2.18"/>
     </proof>
    </goal>
    <goal
     name="pow2_51"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="69" loccnumb="8" loccnume="15"
     sum="6ca479c9951f1be1a76f1cedfe677576"
     proved="true"
@@ -2654,7 +2654,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.56"/>
+     <result status="valid" time="1.72"/>
     </proof>
     <proof
      prover="1"
@@ -2686,12 +2686,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.22"/>
+     <result status="valid" time="2.47"/>
     </proof>
    </goal>
    <goal
     name="pow2_52"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="70" loccnumb="8" loccnume="15"
     sum="8cf76405019a5d4157fadf4fd40e872b"
     proved="true"
@@ -2703,7 +2703,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.65"/>
+     <result status="valid" time="1.79"/>
     </proof>
     <proof
      prover="1"
@@ -2735,12 +2735,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.47"/>
+     <result status="valid" time="2.66"/>
     </proof>
    </goal>
    <goal
     name="pow2_53"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="71" loccnumb="8" loccnume="15"
     sum="2190edd4ce45f9d8aadb602062b6623f"
     proved="true"
@@ -2752,7 +2752,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.67"/>
+     <result status="valid" time="1.94"/>
     </proof>
     <proof
      prover="1"
@@ -2784,12 +2784,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.58"/>
+     <result status="valid" time="2.75"/>
     </proof>
    </goal>
    <goal
     name="pow2_54"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="72" loccnumb="8" loccnume="15"
     sum="ec5a2418a7d2589c279a27618c1d8bd1"
     proved="true"
@@ -2801,7 +2801,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.72"/>
+     <result status="valid" time="1.94"/>
     </proof>
     <proof
      prover="1"
@@ -2809,7 +2809,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
     <proof
      prover="0"
@@ -2833,12 +2833,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.91"/>
+     <result status="valid" time="3.22"/>
     </proof>
    </goal>
    <goal
     name="pow2_55"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="73" loccnumb="8" loccnume="15"
     sum="b9cae9d85098806d1bd9c8ec9bc1e5c8"
     proved="true"
@@ -2850,7 +2850,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.80"/>
+     <result status="valid" time="2.04"/>
     </proof>
     <proof
      prover="1"
@@ -2882,12 +2882,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="3.45"/>
+     <result status="valid" time="3.63"/>
     </proof>
    </goal>
    <goal
     name="pow2_56"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="74" loccnumb="8" loccnume="15"
     sum="09192ac27836084833762b6987161110"
     proved="true"
@@ -2899,7 +2899,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.98"/>
+     <result status="valid" time="2.15"/>
     </proof>
     <proof
      prover="1"
@@ -2928,7 +2928,7 @@
    </goal>
    <goal
     name="pow2_57"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="75" loccnumb="8" loccnume="15"
     sum="6c19ec29a7a618342630609bbbc71bfc"
     proved="true"
@@ -2940,7 +2940,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.01"/>
+     <result status="valid" time="2.31"/>
     </proof>
     <proof
      prover="1"
@@ -2969,7 +2969,7 @@
    </goal>
    <goal
     name="pow2_58"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="76" loccnumb="8" loccnume="15"
     sum="68f01cfa95ee150b46feda968fd1f521"
     proved="true"
@@ -2981,7 +2981,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.15"/>
+     <result status="valid" time="2.36"/>
     </proof>
     <proof
      prover="1"
@@ -3005,12 +3005,12 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.05"/>
+     <result status="valid" time="0.06"/>
     </proof>
    </goal>
    <goal
     name="pow2_59"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="77" loccnumb="8" loccnume="15"
     sum="8fe8474981019e54fbeb558f5953a503"
     proved="true"
@@ -3022,7 +3022,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.17"/>
+     <result status="valid" time="2.45"/>
     </proof>
     <proof
      prover="1"
@@ -3038,7 +3038,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.04"/>
     </proof>
     <proof
      prover="2"
@@ -3051,7 +3051,7 @@
    </goal>
    <goal
     name="pow2_60"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="78" loccnumb="8" loccnume="15"
     sum="3bb4eb8c1f769e83909f33eade9990a9"
     proved="true"
@@ -3063,7 +3063,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.33"/>
+     <result status="valid" time="2.60"/>
     </proof>
     <proof
      prover="1"
@@ -3071,7 +3071,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
     <proof
      prover="0"
@@ -3092,7 +3092,7 @@
    </goal>
    <goal
     name="pow2_61"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="79" loccnumb="8" loccnume="15"
     sum="ef7f1ed42503b27b611496003d0e9d54"
     proved="true"
@@ -3104,7 +3104,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.38"/>
+     <result status="valid" time="2.78"/>
     </proof>
     <proof
      prover="1"
@@ -3133,7 +3133,7 @@
    </goal>
    <goal
     name="pow2_62"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="80" loccnumb="8" loccnume="15"
     sum="494f4da8ece0502d5cedc26fbbcfaf3e"
     proved="true"
@@ -3145,7 +3145,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.61"/>
+     <result status="valid" time="2.82"/>
     </proof>
     <proof
      prover="1"
@@ -3153,7 +3153,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="0"
@@ -3161,7 +3161,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.03"/>
     </proof>
     <proof
      prover="2"
@@ -3174,7 +3174,7 @@
    </goal>
    <goal
     name="pow2_63"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="81" loccnumb="8" loccnume="15"
     sum="a7b8962600d43f9512ef96485f59b8eb"
     proved="true"
@@ -3186,7 +3186,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.64"/>
+     <result status="valid" time="3.01"/>
     </proof>
     <proof
      prover="1"
@@ -3215,18 +3215,18 @@
    </goal>
    <goal
     name="Div_pow"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="86" loccnumb="8" loccnume="15"
-    sum="d22340cab632bc48b4a250f9506bda01"
+    sum="02d7ff6b872edf2c27a83ff9ccad2fd6"
     proved="false"
     expanded="false"
     shape="ainfix =adivV0apow2ainfix -V1c1c1Iainfix &lt;V0apow2V1Aainfix &lt;=apow2ainfix -V1c1V0F">
    </goal>
    <goal
     name="Div_pow2"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="89" loccnumb="8" loccnume="16"
-    sum="019bcafa5e45ebe975c2972ff04f880e"
+    sum="1063c2a5115bd783910baaec13bcb499"
     proved="false"
     expanded="false"
     shape="ainfix =adivV0apow2ainfix -V1c1aprefix -c2Iainfix &lt;V0aprefix -apow2ainfix -V1c1Aainfix &lt;=aprefix -apow2V1V0F">
@@ -3234,15 +3234,15 @@
   </theory>
   <theory
    name="Pow2real"
-   locfile="power2/../power2.why"
+   locfile="bitvectors/power2/../power2.why"
    loclnum="96" loccnumb="7" loccnume="15"
    verified="true"
    expanded="false">
    <goal
     name="Power_s_all"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="106" loccnumb="8" loccnume="19"
-    sum="6f696a9d2f07d6172a73d8dd30ac7b70"
+    sum="e6dd14fe3a5ba3283660945b0db58536"
     proved="true"
     expanded="false"
     shape="ainfix =apow2ainfix +V0c1ainfix *.c2.0apow2V0F">
@@ -3268,7 +3268,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="2"
@@ -3289,9 +3289,9 @@
    </goal>
    <goal
     name="Power_p_all"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="108" loccnumb="8" loccnume="19"
-    sum="ede41bed7ccb894e2af4fcf008dbd14f"
+    sum="8362ccd3afb76ed5964c12f93d13e691"
     proved="true"
     expanded="false"
     shape="ainfix =apow2ainfix -V0c1ainfix *.c0.5apow2V0F">
@@ -3338,9 +3338,9 @@
    </goal>
    <goal
     name="Power_1_2"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="110" loccnumb="8" loccnume="17"
-    sum="84a753b158c26d8042cfabd64c4737e0"
+    sum="c20c0af1b6667aaf5c9baccb088e0502"
     proved="true"
     expanded="false"
     shape="ainfix =c0.5ainfix /.c1.0c2.0">
@@ -3395,9 +3395,9 @@
    </goal>
    <goal
     name="Power_1"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="112" loccnumb="8" loccnume="15"
-    sum="14d8bd428d2a57bb612ee84ae54e1aba"
+    sum="1b6b426ee56137b8d3a4e16245cd1ca6"
     proved="true"
     expanded="false"
     shape="ainfix =apow2c1c2.0">
@@ -3444,9 +3444,9 @@
    </goal>
    <goal
     name="Power_neg1"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="114" loccnumb="8" loccnume="18"
-    sum="c7a57a300a9ae5d0db11a4a441d0e606"
+    sum="447b7e97b3415486c16cb85214eacf2c"
     proved="true"
     expanded="false"
     shape="ainfix =apow2aprefix -c1c0.5">
@@ -3493,9 +3493,9 @@
    </goal>
    <goal
     name="Power_non_null_aux"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="116" loccnumb="8" loccnume="26"
-    sum="742640b78c6f8972a42743290fdb56c5"
+    sum="102c0e4af3624557b64a4918155e323d"
     proved="true"
     expanded="false"
     shape="ainfix =apow2V0c0.0NIainfix &gt;=V0c0F">
@@ -3506,14 +3506,14 @@
      edited="power2_Pow2real_Power_non_null_aux_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.56"/>
+     <result status="valid" time="0.59"/>
     </proof>
    </goal>
    <goal
     name="Power_neg_aux"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="118" loccnumb="8" loccnume="21"
-    sum="2cbd515615e025e022da59b7fe3978d4"
+    sum="4fe88f543bd236e235693fcd0e29ce14"
     proved="true"
     expanded="false"
     shape="ainfix =apow2aprefix -V0ainfix /.c1.0apow2V0Iainfix &gt;=V0c0F">
@@ -3524,14 +3524,14 @@
      edited="power2_Pow2real_Power_neg_aux_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.81"/>
+     <result status="valid" time="0.76"/>
     </proof>
    </goal>
    <goal
     name="Power_non_null"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="120" loccnumb="8" loccnume="22"
-    sum="e76a0e7bb90eb5890c701551fc6bc41c"
+    sum="f1010eb45dc229fa0ed29876c36de6aa"
     proved="true"
     expanded="false"
     shape="ainfix =apow2V0c0.0NF">
@@ -3547,9 +3547,9 @@
    </goal>
    <goal
     name="Power_neg"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="122" loccnumb="8" loccnume="17"
-    sum="c98172b037771dc004f33a01af8dc28b"
+    sum="c59ddc59ba40d05be5cc98e0604d5fd6"
     proved="true"
     expanded="false"
     shape="ainfix =apow2aprefix -V0ainfix /.c1.0apow2V0F">
@@ -3559,7 +3559,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.12"/>
+     <result status="valid" time="1.16"/>
     </proof>
     <proof
      prover="0"
@@ -3572,9 +3572,9 @@
    </goal>
    <goal
     name="Power_sum_aux"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="124" loccnumb="8" loccnume="21"
-    sum="f172c7e0f52f667bb7b9c8653216ef40"
+    sum="82b2f0d764c0630aa1428b2f5f0db4c6"
     proved="true"
     expanded="false"
     shape="ainfix =apow2ainfix +V0V1ainfix *.apow2V0apow2V1Iainfix &gt;=V1c0F">
@@ -3590,9 +3590,9 @@
    </goal>
    <goal
     name="Power_sum"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="126" loccnumb="8" loccnume="17"
-    sum="763c6533a99370f6102384b6bb2768d3"
+    sum="3ea7fb43323bc703744d06e2925cbf06"
     proved="true"
     expanded="false"
     shape="ainfix =apow2ainfix +V0V1ainfix *.apow2V0apow2V1F">
@@ -3603,14 +3603,14 @@
      edited="power2_Pow2real_Power_sum_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.66"/>
+     <result status="valid" time="0.65"/>
     </proof>
    </goal>
    <goal
     name="Pow2_int_real"
-    locfile="power2/../power2.why"
+    locfile="bitvectors/power2/../power2.why"
     loclnum="131" loccnumb="8" loccnume="21"
-    sum="5e4ea430562958c674a50eadca768eb5"
+    sum="4ffe755bb774ce645e696cf2336b2531"
     proved="true"
     expanded="false"
     shape="ainfix =apow2V0afrom_intapow2V0Iainfix &gt;=V0c0F">
@@ -3621,7 +3621,7 @@
      edited="power2_Pow2real_Pow2_int_real_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.62"/>
+     <result status="valid" time="0.57"/>
     </proof>
    </goal>
   </theory>
-- 
GitLab