first_order_matching may instantiate matching variables using bound variables
The routine first_order_matching within src/transform/reduction_engine.ml does not contains any checks to prevent the unification of a matching variable with a term containing a bound variable. As a consequence, we can prove false in the following module (using transformation compute_specified to prove the second goal):
module Soundness
use import int.Int
function f0 (x y z:int) : int = x * y + z
predicate p (f:int -> int) =
f (-1) = 0 && forall n:int. f n = f 0 + (f 1 - f 0) * n
lemma A : forall y z:int. p (fun x -> f0 x y z) <-> y = z
meta rewrite lemma A
lemma Fail : p (fun x -> f0 x x x)
lemma Absurd : false
end