Clean smtv2 output for bitvectors.

drivers/smt-libv2.drv

@@ -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

examples/tests-provers/bv/why3session.xml

@@ -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>