From 61bc6d66eebfaa4649094b3ee8b2d5317d8f8346 Mon Sep 17 00:00:00 2001 From: acondolu Date: Fri, 14 Jul 2017 19:39:21 +0200 Subject: [PATCH] Failure in case of empty problem, to be fixed (cherry picked from commit 605ae9159149e42a17f044bbfad94f7dc2de79c2) --- ocaml/lambda4.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 4108ea5..a8899bc 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -757,14 +757,14 @@ let tmp (label, div, conv, nums, var_names) = (* TODO: *) (* replace div with bottom in problem??? *) - let special_k = - let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ nums @ conv in - compute_special_k (Listx.from_list (all_tms :> nf list)) in (* compute initial special K *) + let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ nums @ conv in + if all_tms = [] then failwith "FIXME: empty problem"; + let initialSpecialK = compute_special_k (Listx.from_list (all_tms :> nf list)) in let freshno = List.length var_names in let deltas = let dummy = `Var (max_int / 2, -666) in [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in - {freshno; div; conv; ps; sigma=[]; deltas; initialSpecialK=special_k; var_names; label} + {freshno; div; conv; ps; sigma=[]; deltas; initialSpecialK; var_names; label} ;; let problem_of ~div ~conv ~nums = -- 2.39.2