Failure to prune branch due to removal of exists in side condition

[virgil-serbanuta]

See the info for reproducing this issue at the end.

As far as I can tell, what happens is that in a certain case, the backend rewrites config1(X) and not exists y . X == stuff(Y) to config2(stuff(Z)) and not stuff(Z) == stuff(Y), completely dropping the exists y quantifier. With the quantifier, most likely the backend would have been able to evaluate exists y . stuff(Z) == stuff(Y) to top, which would have pruned the branch.

report.tar.gz

$ kompile --version
K version:    v5.6.122-0-g77b76f004a-dirty
Build date:   Thu Jun 08 22:29:39 EEST 2023
$ kore-rpc --version
Kore version 0.60.0.0
Git:
  revision:	f7a90ba41aa98d79f400099e2a27156e07543540
  branch:	HEAD
  last commit:	Fri May 5 08:23:49 2023 -0600

[virgil-serbanuta]

FWIW, this happens when applying these three rules twice for the same ADDR value (though the report may have only two of the rules):
https://github.com/runtimeverification/elrond-semantics/blob/master/elrond-config.md?plain=1#L197-L225

The first time each rule is applied properly, and the configuration is split into three. On the owise branch, when attempting to apply again these rules, the configuration is still split into three, and the thing mentioned in the first issue comment happens.

[goodlyrottenapple]

^ should be https://github.com/runtimeverification/elrond-semantics/blob/31b905283fa24834d3bc6939c60d767e0a9cee93/elrond-config.md?plain=1#L197-L225

[goodlyrottenapple]

related to #3605