add node merging heuristic
test-update for KCFGSemantics Modification

…for booster (#4533)

The previous change #4522 was insufficient to make the equations usable
in `booster`. Matches with literal `Int` constants will still be
indeterminate, so this PR removes the literals from the rule LHSs.

* Use `0 ==Int I` instead of a syntactic _match_ in the equation for
argument `0`. This enables evaluating terms with `I ==Int 0` in the path
condition.
* Remove equation with literal `-1` and widen requires in equation for
negative arguments (previously `I <Int -1`, now `I <Int 0`). The result
is the same as before with no extra equation required.

Fixes #4543

Co-authored-by: devops <devops@runtimeverification.com>

Add an `install-build-deps` script to replace the manual commands in the
README. See commit message(s) for details.

__WARNING:__ This commit is based on the commit in #4054; if you merge
this it will merge that one too. (The script includes the
`libunwind-dev` package added in that commit.)

You'll probably want to do a quick check that this works on MacOS and
update the commit message appropriately.

Co-authored-by: devops <devops@runtimeverification.com>

add node merging heuristic
test-update for KCFGSemantics Modification

…into merge-node