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