[Predicate unfolding] Fix off-by-one error when unfolding ite-rules

src/SL/InductiveDefinition.ml

@@ -114,8 +114,13 @@ let map_cases fn id =
 let is_finite id = List.is_empty id.inductive_cases
 
 let unfold_finite id xs : SL.t =
-  let phi = SL.mk_or id.base_cases in
-  SL.substitute_list phi ~vars:id.header ~by:xs
+  let unfolding = match id.base_cases with
+    | [] ->
+      let aux = SL.mk_or id.inductive_cases in
+      SL.map_view (fun (Predicate _) -> SL.ff) aux (* Needed for rules with if-then-else *)
+    | bs -> SL.mk_or bs
+  in
+  SL.substitute_list unfolding ~vars:id.header ~by:xs
 
 module ID_map = Stdlib.Map.Make(String)
 
@@ -136,16 +141,3 @@ let rec unfold_guided id_map id g xs n =
       let id' = ID_map.find name' id_map in
       unfold_guided id_map id' g ys (n-1)
   ) (instantiate ~refresh:true id xs)
-
-
-
-
-
-
-
-
-
-
-
-
-

src/preprocessing/UnfoldIDs.ml

@@ -1,7 +1,7 @@
 module Logger = Logger.Make(struct let name = "unfolder" let level = 1 end)
 
 let unfold_predicate_lhs name xs =
-  let bound = 1 + SID.unfolding_depth name in (* TODO: fix in predicate! *)
+  let bound = SID.unfolding_depth name in
   Logger.debug "Unfolding predicate %s(%s) up to depth %d\n"
     name (SL.Term.show_list xs) bound;
   SID.unfold name xs bound