diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml index ed3ea87c763b8537b00c38a674182d3195925d29..a499059856b701b290f23e7f36dc25a781d03b87 100644 --- a/src_colibri2/theories/quantifier/InvertedPath.ml +++ b/src_colibri2/theories/quantifier/InvertedPath.ml @@ -179,12 +179,7 @@ let insert_pattern d (trigger : Trigger.t) = | Pattern.Var v -> let pairs = Expr.Term.Var.M.find_def [] v.var pp_vars in let pairs = - List.filter - (fun pp -> - (* improvement: possible to limit to just parent1 since only one - path is needed by pairs *) - F_Pos.equal fp pp.PP.parent1 || F_Pos.equal fp pp.PP.parent2) - pairs + List.filter (fun pp -> F_Pos.equal fp pp.PP.parent1) pairs in let ips = List.map (fun pp -> HPP.find pp_ips d pp) pairs in let ip = create (Egraph.context d) in