Proxy simplifies the branching result from Kore and discovers that one of the branches is actually #Bottom. Proxy continues execution, effectively making a rewrite step. However, neither the depth is increased nor a rewrite step in recorded in the execution trace
This behavior is exposed in the test-issue3764-vacuous-branch integration test.
While working on https://github.com/runtimeverification/haskell-backend/pull/3960, I've discovered that we actually have a bug on
master
, which has to do with the process of pruning of vacuous branches.Scenario:
#Bottom
. Proxy continues execution, effectively making a rewrite step. However, neither the depth is increased nor a rewrite step in recorded in the execution traceThis behavior is exposed in the
test-issue3764-vacuous-branch
integration test.I'd expect he test-issue3764-vacuous-branch/response-branch-in-zero.json golden file to have
"depth": 3
and three rules in"logs"
, the first of which is the jumpi.true from kore-rpc, i.e.:But instead we get
"depth":2
and only the logs from Booster.