From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 24 Jul 2017 12:55:31 +0000 (+0200)
Subject: Fixed bug in computing special k
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cc1866c8e2ce19384d3ce5643cfb86ade7b8101f;p=fireball-separation.git

Fixed bug in computing special k
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 336f6b1..f26607b 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -59,7 +59,7 @@ let first bound p var f =
    with Backtrack s ->
 prerr_endline (">>>>>> BACKTRACK (reason: " ^ s ^") measure=$ ");
      List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ;
-prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int i);
+prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int (i+1));
      aux (i+1)
  in
   aux 1
@@ -557,7 +557,7 @@ let compute_special_k tms =
  | `Bottom
  | `Pacman
  | `Var _ -> 0 in
- Listx.max (Listx.map (fun t -> max (aux 0 t) (aux' true t)) tms)
+ Listx.max (Listx.map (aux 0) tms) + Listx.max (Listx.map (aux' true) tms)
 ;;
 
 let choose_step p =