Avoid name clashes in rule applyUpdateOnRigid

[tobias-rnh]

Fix #3254 To prevent name clashes with bound variables, the free variables in the update and the bound variables of a formula are compared. In case of a clash, the bound variable is renamed and a substitution is performed on the subterms of the formula automatically before applying the update.

now becomes

The new clash free name is created by appending a counter to the original name of the bound variable. However: as only the variables contained in the update and the formula the update is applied on are considered, the following situation is still possible:

still becomes

Currently, there is no way to get names on higher levels than the update. So if the different meanings of a1 in this situation are still of concern, it might be needed to find a solution on a higher level than ApplyUpdateOnRigidCondition, e.g. when parsing.

Tests for ApplyUpdateOnRigidCondition were also added.

[codecov[bot]]

Codecov Report

Attention: 1 lines in your changes are missing coverage. Please review.

Comparison is base (2d9f36c) 37.94% compared to head (778fd6a) 37.97%.

Files	Patch %	Lines
...y/rule/conditions/ApplyUpdateOnRigidCondition.java	98.27%	0 Missing and 1 partial :warning:

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #3355 +/- ## ============================================ + Coverage 37.94% 37.97% +0.03% - Complexity 17001 17018 +17 ============================================ Files 2059 2059 Lines 125973 126013 +40 Branches 21273 21281 +8 ============================================ + Hits 47797 47850 +53 + Misses 72293 72277 -16 - Partials 5883 5886 +3 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.