fixes

src/core/InnerTerm.ml

@@ -48,6 +48,9 @@ let same_l l1 l2 = match l1, l2 with
   | [t1;u1], [t2;u2] -> equal t1 t2 && equal u1 u2
   | _ -> same_l_rec l1 l2
 
+let same_l_gen l1 l2 =
+  List.length l1 == List.length l2 && same_l l1 l2
+
 let _hash_ty t = match t.ty with
   | NoType -> 1
   | HasType ty -> Hash.combine2 2 ty.id

src/core/InnerTerm.mli

@@ -59,6 +59,11 @@ val hash_mod_alpha : t -> int
 val same_l : t list -> t list -> bool
 (** Physical equality on lists of terms, roughly the same as {!List.forall2 (==)} *)
 
+val same_l_gen : t list -> t list -> bool
+(** Physical equality on lists of terms, roughly the same as {!List.forall2 (==),
+    tolerates different lengths} *)
+
+
 val ho_weight : t -> int
 
 (** {3 Constructors}

src/core/Term.ml

@@ -57,6 +57,7 @@ let[@inline] ty t = match T.ty t with
 
 let hash_mod_alpha = T.hash_mod_alpha
 let same_l = T.same_l
+let same_l_gen = T.same_l_gen
 
 (* split list between types, terms.
    [ty] is the type of the function, [l] the arguments *)

src/core/Term.mli

@@ -72,6 +72,7 @@ val same_l : t list -> t list -> bool
     equal, [false] otherwise.
     Precondition: both lists have the same length
     @raise Assert_failure if lists have not the same length *)
+val same_l_gen : t list -> t list -> bool
 
 (** {2 Constructors} *)
 

src/prover/selection.ml

@@ -49,7 +49,7 @@ let can_select_lit ~ord (lits:Lits.t) (i:int) : bool =
         Lit.fold_terms ~vars:true ~ty_args:false ~which:`All ~subterms:true lits.(i)
         |> Iter.exists (fun (t,_) ->
             let t_head, t_args = T.as_app t in
-            vars_args |> CCList.exists (fun (head, args) -> head = t_head && t_args != args)
+            vars_args |> CCList.exists (fun (head, args) -> T.equal head t_head && not @@ T.same_l_gen t_args args)
           )
       in
     match !_ho_restriction with

src/prover_calculi/Higher_order.ml

@@ -689,7 +689,7 @@ module Make(E : Env.S) : S with module Env = E = struct
                            CCInt.to_string (CCRef.get_then_incr new_choice_counter) in
       let new_ch_id = ID.make choice_ty_name in
       let new_ch_const = T.const new_ch_id ~ty in
-      ignore(Signature.declare (C.Ctx.signature ()) new_ch_id ty);
+      Ctx.add_signature (Signature.declare (C.Ctx.signature ()) new_ch_id ty);
       Util.debugf 1 "new choice for type %a: %a(%a).\n" 
         (fun k -> k Type.pp ty T.pp new_ch_const Type.pp (T.ty new_ch_const));
       choice_ops := Term.Set.add new_ch_const !choice_ops;