Booster's simplifier is unable to prune a #Bottom state

[geo2a]

The integration test test-issue3764-vacuous-branch isolates a case where Booster's simplifier is unable to prune a bottom state.

When sent given the state-branch-in-zero.send request, booster-dev (and kore-rpc-booster --no-post-exec-simplify) returns a Branchingresponse, whilekore-rpc-boosterreturnsDepthBound, making two steps. This happens because kore-rpc-booster` will call Kore's simplify endpoint, which is more powerful (but much slower).

The other request, state-branch-after-one.send, is basically the same, but the state is from one step before. booster-dev branches after 1 step and kore-rpc-booster makes 3 steps.

We need to figure out exactly what allows the Kore's simplifier to prune the state. An important details is that the pruning happens not in Kore's rule unification algorithm, i.e. Kore returns Branching too. It is the simplify request that produces #Bottom in the end.

Note that #4020 (checking input pattern's conditions with SMT in Booster) is also not enough, i.e. even with that code Booster is unable to derive a contradiction.

To observe the relevant logs, run the following from the following from the repo root:

SERVER=$(cabal list-bin kore-rpc-booster) SERVER_OPTS="--log-context \"*>proxy>*\"" CLIENT=$(cabal list-bin kore-rpc-client) ./booster/test/rpc-integration/runDirectoryTest.sh booster/test/rpc-integration/test-issue3764-vacuous-branch 

[jberthold]

A similar phenomenon was observed in the wild on an engagement proof.
An execute request was erroneously branching because the branching condition could not be evaluated to False by the SMT solver. Due to a bug (fixed in #4078 ) this led to infinite branching in the proof. One of the branches can be simplified to #Bottom by the legacy backend but not by booster, it's unclear why.
Discussed here with some artefacts.