Updated sessions after setting poly-detection on Z3 4.3.2

drivers/cvc4_14.drv

@@ -62,18 +62,4 @@ theory int.EuclideanDivision
 end
 *)
 
-theory map.Map
-  meta "encoding:ignore_polymorphism_ts" type map
-  meta "encoding:ignore_polymorphism_ls" function get
-  meta "encoding:ignore_polymorphism_ls" function ([])
-  meta "encoding:ignore_polymorphism_ls" function set
-  meta "encoding:ignore_polymorphism_ls" function ([<-])
-  meta "encoding:ignore_polymorphism_pr" prop Select_eq
-  meta "encoding:ignore_polymorphism_pr" prop Select_neq
-
-  remove prop Select_eq
-  remove prop Select_neq
-end
-
-
 import "cvc4_bv.gen"

drivers/smt-libv2.drv

@@ -142,11 +142,21 @@ end
 
 theory map.Map
   syntax type map "(Array %1 %2)"
-  meta "encoding : lskept" function get
-  meta "encoding : lskept" function set
+  meta "encoding:ignore_polymorphism_ts" type map
 
   syntax function get   "(select %1 %2)"
   syntax function set   "(store %1 %2 %3)"
+  meta "encoding : lskept" function get
+  meta "encoding : lskept" function set
+  meta "encoding:ignore_polymorphism_ls" function get
+  meta "encoding:ignore_polymorphism_ls" function ([])
+  meta "encoding:ignore_polymorphism_ls" function set
+  meta "encoding:ignore_polymorphism_ls" function ([<-])
+
+  meta "encoding:ignore_polymorphism_pr" prop Select_eq
+  meta "encoding:ignore_polymorphism_pr" prop Select_neq
+  remove prop Select_eq
+  remove prop Select_neq
 end
 
 theory map.Const

examples/bts/fsetint/why3session.xml

@@ -8,7 +8,7 @@
 <prover id="3" name="CVC3" version="2.2" timelimit="3" memlimit="1000"/>
 <prover id="4" name="Z3" version="3.2" timelimit="3" memlimit="1000"/>
 <file name="../fsetint.why" expanded="true">
-<theory name="Th1" sum="100b2d71a5c0f4e1d40045332eacef33" expanded="true">
+<theory name="Th1" sum="ef22ff2d63b0de72f33a0af8c29d811b" expanded="true">
  <goal name="l_false" expanded="true">
  <proof prover="0"><result status="timeout" time="3.01"/></proof>
  <proof prover="1" timelimit="5"><result status="unknown" time="0.01"/></proof>
@@ -17,7 +17,7 @@
  <proof prover="4"><result status="timeout" time="3.01"/></proof>
  </goal>
 </theory>
-<theory name="Th2" sum="0fbe57945be00b85b8cc0510a867e5a4" expanded="true">
+<theory name="Th2" sum="53142f5d6cc187e6f3955620e5ff5704" expanded="true">
  <goal name="mem_integer" expanded="true">
  <proof prover="0"><result status="timeout" time="3.11"/></proof>
  <proof prover="1"><result status="unknown" time="0.00"/></proof>

examples/coincidence_count/why3session.xml

@@ -5,15 +5,15 @@
 <prover id="0" name="Z3" version="4.3.1" timelimit="10" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
 <file name="../coincidence_count.mlw" expanded="true">
-<theory name="CoincidenceCount" sum="bb91af34e3378d77979707fd55da2144" expanded="true">
+<theory name="CoincidenceCount" sum="c8fb7856ca9e35d98067c6b03ff5c8e4" expanded="true">
  <goal name="drop_left" expanded="true">
- <proof prover="1"><result status="valid" time="0.31" steps="515"/></proof>
+ <proof prover="1"><result status="valid" time="0.80" steps="1147"/></proof>
  </goal>
  <goal name="not_mem_inter_r" expanded="true">
- <proof prover="1"><result status="valid" time="2.28" steps="468"/></proof>
+ <proof prover="1"><result status="valid" time="1.02" steps="585"/></proof>
  </goal>
  <goal name="not_mem_inter_l" expanded="true">
- <proof prover="1"><result status="valid" time="2.19" steps="468"/></proof>
+ <proof prover="1"><result status="valid" time="1.01" steps="585"/></proof>
  </goal>
  <goal name="WP_parameter coincidence_count" expl="VC for coincidence_count" expanded="true">
  <transf name="split_goal_wp" expanded="true">
@@ -79,7 +79,7 @@
   <proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>
   </goal>
   <goal name="WP_parameter coincidence_count.20" expl="20. loop invariant preservation" expanded="true">
-  <proof prover="1"><result status="valid" time="0.70" steps="136"/></proof>
+  <proof prover="1"><result status="valid" time="0.70" steps="167"/></proof>
   </goal>
   <goal name="WP_parameter coincidence_count.21" expl="21. loop variant decrease" expanded="true">
   <proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>

examples/dijkstra/why3session.xml

@@ -11,7 +11,7 @@
 <prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
 <prover id="7" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
 <file name="../dijkstra.mlw" expanded="true">
-<theory name="DijkstraShortestPath" sum="220377be65b752bd52f4a72d4566760e" expanded="true">
+<theory name="DijkstraShortestPath" sum="64b694a314ef1dbe118406287800fba2" expanded="true">
  <goal name="WP_parameter relax" expl="VC for relax">
  <transf name="split_goal_wp">
   <goal name="WP_parameter relax.1" expl="1. postcondition">
@@ -79,7 +79,7 @@
   <proof prover="2"><result status="valid" time="0.07"/></proof>
   <proof prover="3" timelimit="15"><result status="valid" time="0.05" steps="59"/></proof>
   <proof prover="4"><result status="valid" time="0.03"/></proof>
-  <proof prover="5" timelimit="15"><result status="valid" time="9.97"/></proof>
+  <proof prover="5" timelimit="15"><result status="valid" time="15.85"/></proof>
   </goal>
   <goal name="WP_parameter shortest_path_code.6" expl="6. loop invariant init">
   <proof prover="3"><result status="valid" time="0.00" steps="17"/></proof>
@@ -137,13 +137,13 @@
     <proof prover="3"><result status="valid" time="0.44" steps="97"/></proof>
     </goal>
     <goal name="WP_parameter shortest_path_code.12.1.2" expl="2. VC for shortest_path_code">
-    <proof prover="2" timelimit="10"><result status="valid" time="0.28"/></proof>
+    <proof prover="2" timelimit="10"><result status="valid" time="1.06"/></proof>
     </goal>
     <goal name="WP_parameter shortest_path_code.12.1.3" expl="3. VC for shortest_path_code">
     <proof prover="3"><result status="valid" time="0.03" steps="25"/></proof>
     </goal>
     <goal name="WP_parameter shortest_path_code.12.1.4" expl="4. VC for shortest_path_code">
-    <proof prover="2" timelimit="10"><result status="valid" time="1.53"/></proof>
+    <proof prover="2" timelimit="10"><result status="valid" time="2.78"/></proof>
     </goal>
     <goal name="WP_parameter shortest_path_code.12.1.5" expl="5. VC for shortest_path_code">
     <proof prover="3"><result status="valid" time="1.84" steps="316"/></proof>
@@ -169,7 +169,7 @@
      <proof prover="5"><result status="valid" time="2.08"/></proof>
      </goal>
      <goal name="WP_parameter shortest_path_code.13.1.1.2" expl="2. loop invariant preservation">
-     <proof prover="2"><result status="valid" time="0.39"/></proof>
+     <proof prover="2"><result status="valid" time="0.79"/></proof>
      </goal>
     </transf>
     </goal>

examples/finite_tarski/why3session.xml

@@ -6,12 +6,12 @@
 <file name="../finite_tarski.mlw" expanded="true">
 <theory name="Tarski" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
 </theory>
-<theory name="Tarski_rec" sum="20d20c3410f1ee7ca702ab8a5ddc114b" expanded="true">
+<theory name="Tarski_rec" sum="7660d2907cfd8e511a220f73e34092e0" expanded="true">
  <goal name="WP_parameter least_fix_point" expl="VC for least_fix_point" expanded="true">
  <proof prover="0"><result status="valid" time="0.15"/></proof>
  </goal>
 </theory>
-<theory name="Tarski_while" sum="c37e9e467a99afa7706f40c48683b43f" expanded="true">
+<theory name="Tarski_while" sum="42ef6eac87005fde946d13637ce98a08" expanded="true">
  <goal name="WP_parameter least_fix_point" expl="VC for least_fix_point" expanded="true">
  <proof prover="0"><result status="valid" time="0.19"/></proof>
  </goal>

examples/isqrt.mlw

@@ -42,12 +42,12 @@ module NewtonMethod
     let y = ref x in
     let z = ref (div (x+1) 2) in
     while !z < !y do
-      invariant { !z > 0
-               /\ !y > 0
-               /\ !z = div (div x !y + !y) 2
-               /\ x < (!y + 1) * (!y + 1)
-               /\ x < (!z + 1) * (!z + 1) }
       variant { !y }
+      invariant { !z > 0 }
+      invariant { !y > 0 }
+      invariant { !z = div (div x !y + !y) 2 }
+      invariant { x < (!y + 1) * (!y + 1) }
+      invariant { x < (!z + 1) * (!z + 1) }
       y := !z;
       z := div (div x !z + !z) 2
     done;

examples/isqrt/why3session.xml

@@ -2,11 +2,15 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
+<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="20" memlimit="0"/>
 <prover id="1" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
 <prover id="2" name="CVC3" version="2.2" timelimit="10" memlimit="0"/>
 <prover id="3" name="Z3" version="4.3.1" timelimit="5" memlimit="4000"/>
 <prover id="4" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
+<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
+<prover id="6" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
+<prover id="7" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
+<prover id="8" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
 <file name="../isqrt.mlw" expanded="true">
 <theory name="Simple" sum="37986e654f2b5693ba9c6ee771a12da0" expanded="true">
  <goal name="WP_parameter isqrt" expl="VC for isqrt">
@@ -19,90 +23,68 @@
  <proof prover="3"><result status="valid" time="0.02"/></proof>
  </goal>
 </theory>
-<theory name="NewtonMethod" sum="2f024f674d36e207994d5a608f1eab47" expanded="true">
+<theory name="NewtonMethod" sum="b7341e429ac65ad70fa88e1a89ae7e56" expanded="true">
  <goal name="WP_parameter sqrt" expl="VC for sqrt" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="WP_parameter sqrt.1" expl="1. postcondition">
-  <proof prover="0" timelimit="20"><result status="valid" time="0.02"/></proof>
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
   <proof prover="1"><result status="valid" time="0.02"/></proof>
   <proof prover="2"><result status="valid" time="0.00"/></proof>
   <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="WP_parameter sqrt.2" expl="2. postcondition">
-  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  <proof prover="0" timelimit="10"><result status="valid" time="0.02"/></proof>
   <proof prover="1"><result status="valid" time="0.02"/></proof>
   <proof prover="2"><result status="valid" time="0.00"/></proof>
   <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="WP_parameter sqrt.3" expl="3. loop invariant init">
+  <proof prover="5"><result status="valid" time="0.03" steps="8"/></proof>
+  </goal>
+  <goal name="WP_parameter sqrt.4" expl="4. loop invariant init">
+  <proof prover="5"><result status="valid" time="0.01" steps="3"/></proof>
+  </goal>
+  <goal name="WP_parameter sqrt.5" expl="5. loop invariant init">
+  <proof prover="5"><result status="timeout" time="5.00"/></proof>
+  <proof prover="6"><result status="valid" time="0.03"/></proof>
+  <proof prover="7"><result status="unknown" time="0.01"/></proof>
+  <proof prover="8"><result status="timeout" time="4.99"/></proof>
+  </goal>
+  <goal name="WP_parameter sqrt.6" expl="6. loop invariant init">
+  <proof prover="5"><result status="valid" time="0.00" steps="3"/></proof>
+  </goal>
+  <goal name="WP_parameter sqrt.7" expl="7. loop invariant init">
   <transf name="split_goal_wp">
-   <goal name="WP_parameter sqrt.3.1" expl="1. VC for sqrt">
-   <proof prover="0"><result status="valid" time="0.02"/></proof>
-   <proof prover="1"><result status="valid" time="0.02"/></proof>
-   <proof prover="2"><result status="valid" time="0.01"/></proof>
-   <proof prover="3"><result status="valid" time="0.02"/></proof>
-   </goal>
-   <goal name="WP_parameter sqrt.3.2" expl="2. VC for sqrt">
-   <proof prover="0"><result status="valid" time="0.01"/></proof>
-   <proof prover="1"><result status="valid" time="0.02"/></proof>
-   <proof prover="2"><result status="valid" time="0.00"/></proof>
-   <proof prover="3"><result status="valid" time="0.02"/></proof>
-   </goal>
-   <goal name="WP_parameter sqrt.3.3" expl="3. VC for sqrt">
-   <proof prover="2"><result status="valid" time="0.03"/></proof>
-   <proof prover="3"><result status="timeout" time="5.05"/></proof>
-   </goal>
-   <goal name="WP_parameter sqrt.3.4" expl="4. VC for sqrt">
-   <proof prover="0"><result status="valid" time="0.01"/></proof>
-   <proof prover="1"><result status="valid" time="0.02"/></proof>
-   <proof prover="2"><result status="valid" time="0.00"/></proof>
-   <proof prover="3"><result status="valid" time="0.02"/></proof>
-   </goal>
-   <goal name="WP_parameter sqrt.3.5" expl="5. VC for sqrt">
-   <proof prover="0"><result status="valid" time="0.02"/></proof>
+   <goal name="WP_parameter sqrt.7.1" expl="1. loop invariant init">
+   <proof prover="0" timelimit="10"><result status="valid" time="0.02"/></proof>
    <proof prover="1"><result status="valid" time="0.02"/></proof>
    <proof prover="2"><result status="valid" time="0.02"/></proof>
    <proof prover="3"><result status="valid" time="0.02"/></proof>
    </goal>
   </transf>
   </goal>
-  <goal name="WP_parameter sqrt.4" expl="4. loop invariant preservation" expanded="true">
-  <transf name="split_goal_wp" expanded="true">
-   <goal name="WP_parameter sqrt.4.1" expl="1. VC for sqrt">
-   <proof prover="0"><result status="valid" time="3.53"/></proof>
-   <proof prover="1"><result status="valid" time="0.02"/></proof>
-   <proof prover="2"><result status="valid" time="0.07"/></proof>
-   <proof prover="3"><result status="valid" time="0.03"/></proof>
-   </goal>
-   <goal name="WP_parameter sqrt.4.2" expl="2. VC for sqrt">
-   <proof prover="0"><result status="valid" time="0.01"/></proof>
-   <proof prover="1"><result status="valid" time="0.01"/></proof>
-   <proof prover="2"><result status="valid" time="0.01"/></proof>
-   <proof prover="3"><result status="valid" time="0.02"/></proof>
-   </goal>
-   <goal name="WP_parameter sqrt.4.3" expl="3. VC for sqrt">
-   <proof prover="0"><result status="valid" time="0.00"/></proof>
-   <proof prover="1"><result status="valid" time="0.01"/></proof>
-   <proof prover="2"><result status="valid" time="0.01"/></proof>
-   <proof prover="3"><result status="valid" time="0.02"/></proof>
-   </goal>
-   <goal name="WP_parameter sqrt.4.4" expl="4. VC for sqrt">
-   <proof prover="0"><result status="valid" time="0.00"/></proof>
-   <proof prover="2"><result status="valid" time="0.01"/></proof>
-   <proof prover="3"><result status="timeout" time="5.05"/></proof>
-   </goal>
-   <goal name="WP_parameter sqrt.4.5" expl="5. VC for sqrt" expanded="true">
-   </goal>
-  </transf>
+  <goal name="WP_parameter sqrt.8" expl="8. loop invariant preservation">
+  <proof prover="5"><result status="valid" time="4.08" steps="51"/></proof>
+  </goal>
+  <goal name="WP_parameter sqrt.9" expl="9. loop invariant preservation">
+  <proof prover="5"><result status="valid" time="0.01" steps="11"/></proof>
+  </goal>
+  <goal name="WP_parameter sqrt.10" expl="10. loop invariant preservation">
+  <proof prover="5"><result status="valid" time="0.01" steps="11"/></proof>
+  </goal>
+  <goal name="WP_parameter sqrt.11" expl="11. loop invariant preservation">
+  <proof prover="5"><result status="valid" time="0.01" steps="11"/></proof>
+  </goal>
+  <goal name="WP_parameter sqrt.12" expl="12. loop invariant preservation" expanded="true">
   </goal>
-  <goal name="WP_parameter sqrt.5" expl="5. loop variant decrease">
-  <proof prover="0" timelimit="20"><result status="valid" time="0.00"/></proof>
+  <goal name="WP_parameter sqrt.13" expl="13. loop variant decrease">
+  <proof prover="0"><result status="valid" time="0.00"/></proof>
   <proof prover="1"><result status="valid" time="0.01"/></proof>
   <proof prover="2"><result status="valid" time="0.01"/></proof>
   <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="WP_parameter sqrt.6" expl="6. postcondition" expanded="true">
-  <proof prover="0" timelimit="20"><result status="valid" time="0.68"/></proof>
+  <goal name="WP_parameter sqrt.14" expl="14. postcondition">
+  <proof prover="0"><result status="valid" time="0.68"/></proof>
   <proof prover="4"><result status="valid" time="0.14"/></proof>
   </goal>
  </transf>

examples/pigeonhole/why3session.xml

@@ -5,7 +5,7 @@
 <prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
 <prover id="6" name="Alt-Ergo" version="0.95.1" timelimit="6" memlimit="1000"/>
 <file name="../pigeonhole.mlw" expanded="true">
-<theory name="Pigeonhole" sum="8ee565a294b83da869ffcfd8fb11b973" expanded="true">
+<theory name="Pigeonhole" sum="8113cf408735303d4f558f38156b7683" expanded="true">
  <goal name="WP_parameter below" expl="VC for below" expanded="true">
  <proof prover="6"><result status="valid" time="0.01" steps="75"/></proof>
  </goal>

examples/schorr_waite/why3session.xml

@@ -7,7 +7,7 @@
 <prover id="2" name="CVC4" version="1.4" timelimit="60" memlimit="3000"/>
 <prover id="4" name="Z3" version="4.3.2" timelimit="5" memlimit="3500"/>
 <file name="../schorr_waite.mlw">
-<theory name="SchorrWaite" sum="5d0d6bc869b127a8e754b9fc7b20ba16">
+<theory name="SchorrWaite" sum="2f05802da1ae46ff6a13a12a02cb4b75">
  <goal name="WP_parameter tl_stackNodes" expl="VC for tl_stackNodes">
  <transf name="split_goal_wp">
   <goal name="WP_parameter tl_stackNodes.1" expl="1. postcondition">
@@ -106,7 +106,7 @@
   <proof prover="2" timelimit="5"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.12" expl="12. loop invariant init">
-  <proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
   <proof prover="2" timelimit="5"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.13" expl="13. loop invariant init">
@@ -508,7 +508,7 @@
   </goal>
   <goal name="WP_parameter schorr_waite.130" expl="130. loop invariant preservation">
   <proof prover="0"><result status="valid" time="0.04" steps="165"/></proof>
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.17"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.131" expl="131. loop invariant preservation">
   <proof prover="2"><result status="valid" time="0.03"/></proof>
@@ -523,7 +523,7 @@
   <proof prover="2"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.135" expl="135. loop invariant preservation">
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.18"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.136" expl="136. loop invariant preservation">
   <proof prover="2"><result status="valid" time="0.04"/></proof>
@@ -568,7 +568,7 @@
   </transf>
   </goal>
   <goal name="WP_parameter schorr_waite.146" expl="146. loop invariant preservation">
-  <proof prover="2"><result status="valid" time="0.29"/></proof>
+  <proof prover="2"><result status="valid" time="0.60"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.147" expl="147. loop variant decrease">
   <proof prover="2"><result status="valid" time="0.04"/></proof>

examples/sudoku.mlw

@@ -491,6 +491,7 @@ this is true but with 2 different possible reasons:
 
 end
 
+(*
 module RandomSolver
 
   (* a variant: solve using a random order of cells *)
@@ -602,6 +603,7 @@ module RandomSolver
     if check_valid s g then solve s g else raise NoSolution
 
 end
+*)
 
 
 (** {2 Some Tests} *)

examples/topological_sorting/why3session.xml

@@ -6,7 +6,7 @@
 <file name="../topological_sorting.mlw">
 <theory name="Graph" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="Static" sum="ecc79d2004b6ad13a63bc04f0513df28">
+<theory name="Static" sum="1ac582433a951fb0ad7d44fd441d2b4c">
  <goal name="WP_parameter dfs" expl="VC for dfs">
  <transf name="split_goal_wp">
   <goal name="WP_parameter dfs.1" expl="1. loop invariant init">
@@ -158,7 +158,7 @@
 </theory>
 <theory name="Online_graph" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="Online_Basic" sum="c73a75ca9cb00e8ef9fa1d731bbfff78">
+<theory name="Online_Basic" sum="5c47f08d628fd9c20aab38d65ad9609b">
  <goal name="WP_parameter create" expl="VC for create">
  <transf name="split_goal_wp">
   <goal name="WP_parameter create.1" expl="1. postcondition">
@@ -214,7 +214,7 @@
   <proof prover="0"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="WP_parameter dfs.16" expl="16. postcondition">
-  <proof prover="0"><result status="valid" time="0.10"/></proof>
+  <proof prover="0"><result status="valid" time="0.78"/></proof>
   </goal>
   <goal name="WP_parameter dfs.17" expl="17. postcondition">
   <proof prover="0"><result status="valid" time="0.04"/></proof>