we catch the refiner errors in the critical step and fall back to the non-criticall...

[helm.git] / helm / software / components / acic_procedural / proceduralOptimizer.ml

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index a397de41e8fa3b8b82b930968a1ef1251d45baec..8a7e5bea5047cd0e3bcdddc9b9d50e130834751d 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -211,8 +211,13 @@ and opt_mutcase_critical g st es c uri tyno outty arg cases =
    in
    let lifted_cases = List.map2 map2 cases constructors in
    let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
-   let x = H.refine c (C.Appl args) in
-   opt_proof g (info st "Optimizer: remove 3") es c x
+   try 
+      let x = H.refine c (C.Appl args) in
+      opt_proof g (info st "Optimizer: remove 3") es c x        
+   with e ->
+(* FG: the transformation is not possible, we fall back into the plain case *)
+      let st = info st ("Optimizer: refine_error: " ^ Printexc.to_string e) in
+      opt_mutcase_plain g st es c uri tyno outty arg cases
 
 and opt_mutcase_plain g st es c uri tyno outty arg cases =
    let g st v =