[Bug] [kprove] - Michelson Liquidity Baking ADDLIQUIDITY-POSITIVE Test Regression

[sskeirik]

Test Regression Information

The Michelson semantics has not been updated for a long time because some kprove tests would fail on newer versions of K.
In order to update the K submodule of K-Michelson, a few tests were disabled on CI.
We want to fix and re-enable these tests.
This issue contains information about how to run the tests (both the K versions and Michelson versions).

Here is the version information:

Prev K Submodule Commit/Version: bf17ff1 (v5.1.64)
Prev Michelson Commit (HEAD^): runtimeverification/michelson-semantics@ea0a99c

Curr K Submodule Commit/Version: b725ebd (v5.2.4)
Curr Michelson master Commit (HEAD): runtimeverification/michelson-semantics@d4b9cc89d

The test in question can be run on either Michelson commit by doing the following:

git clone https://github.com/runtimeverification/michelson-semantics/
cd michelson-semantics
git checkout <version-number>
git submodule update --init --recursive -- ext/k
make deps-k build-lb
make lb-prove_LIQUIDITY-BAKING-ADDLIQUIDITY-POSITIVE-SPEC

In order to more easily test K-Michelson against both versions of K, I recommend checking out the michelson-semantics repo into two separate git worktrees.

Additional Info

None

[ehildenb]

Closing as duplicate: #2326