List.any l (fun x => x == k) is currently passed as-is to Z3, which struggles to reason about bound variables in lambda expressions and runs indefinitely on theorems involving this pattern.
A rewrite rule transforming this into List.elem k l before SMT translation would eliminate the bound variable. As a side effect, some theorems involving this pattern become provable in the optimization phase alone, without requiring Z3 at all.
List.any l (fun x => x == k)is currently passed as-is to Z3, which struggles to reason about bound variables in lambda expressions and runs indefinitely on theorems involving this pattern.A rewrite rule transforming this into
List.elem k lbefore SMT translation would eliminate the bound variable. As a side effect, some theorems involving this pattern become provable in the optimization phase alone, without requiring Z3 at all.