fix: if-then-else split + normalization issue

This PR fixes an issue in the `grind` tactic when case splitting on
if-then-else expressions.

It adds a new marker gadget that prevents `grind` for re-normalizing the condition `c` of an if-then-else
expression. Without this marker, the negated condition `¬c` might be rewritten into
an alternative form `c'`, which `grind` may not recognize as equivalent to `¬c`.
As a result, `grind` could fail to propagate that `if c then a else b` simplifies to `b`
in the `¬c` branch.
3 files changed