eliminate_if is not robust enough against if in triggers
When Gappa is called, its driver call the transformation inline_all
and later eliminate_if
.
module M
function f (x : int) : int = if x = 0 then x else x
predicate p (y : bool) = y
axiom x: forall x, y [f x]. p y -> x = f x
lemma l: forall y. p y
end
The combination of the two transformations fails on a such program and we get a message like:
internal failure: Failure in transformation eliminate_if
This expression isn't supported:
if x = 0 then x else x
cannot eliminate 'if-then-else' in trigger terms
As the transformation fails, it becomes impossible to use Gappa on any program that uses an axiom with a trigger like exposed in the example.
Wouldn't it be possible to remove the trigger in a such case if it is not possible to do something smarter?