Use new define-fun-rec

    instantiate more rapidly reccursive definition.

src_colibri2/tests/solve/all/unsat/dune.inc

@@ -20,6 +20,9 @@
 --dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:union-Union-is_singletonqtvc_2.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_2.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:union-Union-is_singletonqtvc_5.psmt2})))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_5.psmt2})))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 

src_colibri2/tests/solve/all/unsat/union-Union-is_singletonqtvc_2.psmt2

+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;;; SMT-LIB2: integer arithmetic
+;;; SMT-LIB2: real arithmetic
+
+(declare-sort t 0)
+
+(declare-fun make (Int Int) t)
+
+(declare-datatypes ((t2 0))
+(((Strict) (Large))))
+(declare-datatypes ((t0 0))
+(((Singleton (Singleton_proj_1 t)(Singleton_proj_2 t0))
+ (Inter
+ (Inter_proj_1 t)(Inter_proj_2 t2)(Inter_proj_3 t)(Inter_proj_4 t2)(Inter_proj_5 t0))
+ (FiniteInf (FiniteInf_proj_1 t)(FiniteInf_proj_2 t2)) (End))))
+(declare-datatypes ((t3 0))
+(((InfFinite (InfFinite_proj_1 t)(InfFinite_proj_2 t2)(InfFinite_proj_3 t0))
+ (Finite (Finite_proj_1 t0)) (Inf))))
+
+(define-fun-rec nth0 ((i Int)
+  (l t0)) t (ite ((_ is Singleton) l) (let ((x2 (Singleton_proj_1 l))
+                                      (x3 (Singleton_proj_2 l))) (ite (= i 0)
+                                                                 x2
+                                                                 (nth0
+                                                                 (- i 1) x3))) 
+            (ite ((_ is Inter) l) (let ((x4 (Inter_proj_1 l)) 
+                                  (x5 (Inter_proj_3 l)) 
+                                  (x6 (Inter_proj_5 l))) (ite (= i 0) x4
+                                                         (ite (= i 1) x5
+                                                         (nth0 (- i 2) x6)))) 
+            (ite ((_ is FiniteInf) l) (let ((x7 (FiniteInf_proj_1 l))
+                                      ) (ite (= i 0) x7 (make 0 1))) 
+            (make 0 1)))))
+
+(define-fun-rec nth ((i Int)
+  (l t3)) t (ite ((_ is InfFinite) l) (let ((x10 (InfFinite_proj_1 l)) 
+                                      (x11 (InfFinite_proj_3 l))) (ite (= i 0)
+                                                                  x10
+                                                                  (nth0
+                                                                  (- i 1)
+                                                                  x11))) 
+            (ite ((_ is Finite) l) (let ((x12 (Finite_proj_1 l))) (nth0 i
+                                                                  x12)) 
+            (make 0 1))))
+(declare-sort tqt 0)
+
+(declare-fun a12 (tqt) t3)
+
+(declare-fun u () tqt)
+
+(declare-fun x28 () t)
+
+(declare-fun x29 () t2)
+
+(declare-fun x30 () t)
+
+(declare-fun x31 () t2)
+
+(declare-fun x32 () t0)
+
+;; H
+  (assert
+  (= (a12 u) (Finite (Singleton x28 (Inter (nth 1 (a12 u)) x29 x30 x31 x32)))))
+
+(assert
+;; is_singletonqtvc
+ ;; File "src_common/union.mlw", line 126, characters 8-20
+  (not (= (nth 2 (a12 u)) x30)))
+(check-sat)

src_common/union/why3session.xml

@@ -12,7 +12,7 @@
  <goal name="t&#39;&#39;vc" expl="VC for t&#39;" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="t&#39;&#39;vc.0" expl="type invariant" proved="true">
-  <proof prover="3"><result status="valid" time="0.03"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="t&#39;&#39;vc.1" expl="type invariant" proved="true">
   <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -20,58 +20,42 @@
  </transf>
  </goal>
  <goal name="singleton&#39;vc" expl="VC for singleton" proved="true">
- <proof prover="3"><result status="valid" time="0.80"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="is_singleton&#39;vc" expl="VC for is_singleton" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="is_singleton&#39;vc.0" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="0.23"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.1" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="1.59"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.2" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="0.94"/></proof>
+  <proof prover="3"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.3" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="0.54"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.4" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="2.23"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.5" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="1.39"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.6" expl="unreachable point" proved="true">
-  <proof prover="3"><result status="valid" time="0.03"/></proof>
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.7" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="0.22"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.8" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="0.88"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.9" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="0.55"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.10" expl="postcondition" proved="true">
-  <transf name="split_vc" proved="true" >
-   <goal name="is_singleton&#39;vc.10.0" expl="postcondition" proved="true">
-   <proof prover="3"><result status="valid" time="0.28"/></proof>
-   </goal>
-   <goal name="is_singleton&#39;vc.10.1" expl="postcondition" proved="true">
-   <proof prover="3"><result status="valid" time="0.08"/></proof>
-   </goal>
-   <goal name="is_singleton&#39;vc.10.2" expl="postcondition" proved="true">
-   <proof prover="3"><result status="valid" time="0.05"/></proof>
-   </goal>
-   <goal name="is_singleton&#39;vc.10.3" expl="postcondition" proved="true">
-   <proof prover="3"><result status="valid" time="3.05"/></proof>
-   </goal>
-   <goal name="is_singleton&#39;vc.10.4" expl="postcondition" proved="true">
-   <proof prover="3"><result status="valid" time="3.28"/></proof>
-   </goal>
-  </transf>
+  <proof prover="3"><result status="valid" time="0.89"/></proof>
   </goal>
  </transf>
  </goal>