Merge branch 'tallying-debug' of https://git.cduce.org/cduce into tallying-debug

types/types.ml

@@ -2952,9 +2952,9 @@ module Tallying = struct
         let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in
         let acc = aux single_chars normchars acc (BoolChars.get t.chars) in
         let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in
-        let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
         let acc = aux single_times normpair acc (BoolPair.get t.times) in
         let acc = aux single_xml normpair acc (BoolPair.get t.xml) in
+        let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
 
         (* XXX normrec is not tested at all !!! *)
         aux single_record normrec acc (BoolRec.get t.record)
@@ -3148,9 +3148,10 @@ module Tallying = struct
       let d = diff s t in
       if is_empty d then CS.sat else
         if no_var d then CS.unsat else
-          CS.prod acc (norm d)) CS.sat l in
+          CS.prod acc (norm d)) CS.sat l
+    in
 (*    Format.printf "Norm : %a\n" CS.pp_s n;*)
-    if CS.S.is_empty n then raise Step1Fail else
+    if Pervasives.(n = CS.unsat) then raise Step1Fail else
     let m = CS.S.fold (fun c acc -> try CS.ES.union (solve (merge c)) acc with UnSatConstr _ -> acc) n CS.ES.empty in
 (*    Format.printf "Union/Merge : %a \n" CS.ES.print m;*)
     if CS.ES.is_empty m then raise Step2Fail else
@@ -3182,7 +3183,9 @@ let apply_raw s t =
   let gamma = var (Var.mk "Gamma") in
   let rec aux (i,acc1) (j,acc2) t1 t2 () =
     let acc1 = Lazy.force acc1 and acc2 = Lazy.force acc2 in
-    try (Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]) , (acc1, acc2)
+    try
+      (Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]),
+      (acc1, acc2)
     with
     |Tallying.Step1Fail -> raise (Tallying.UnSatConstr "apply_raw step1")
     |Tallying.Step2Fail -> begin