[BUG] Failed to find assignments and symbolic transitions in InitPrimed

[romac]

Describe the bug

Running Apalache v0.7.3-SNAPSHOT (03fdeff) against the latest Tendermint light client specification results in the following error:

Assignment error: Failed to find assignments and symbolic transitions in InitPrimed E@15:05:27.381

To reproduce

1. Clone and build latest Apalache (currently 03fdeff)

$ git clone https://github.com/informalsystems/apalache/
$ cd apalache/
$ git checkout 03fdeff1af778172e8f9a8d344ac7d482a69c59b
$ mvn package

2. Clone the Tendermint specifications repository

$ git clone https://github.com/tendermint/spec/
$ cd spec/
$ git checkout 6abcb13dab6ef82f9ebf65b02ae7b861289d5742
$ cd rust-spec/lightclient/verification/

3. Run Apalache against MC4_3_correct.tla

$ /path/to/apalache-mc check --inv=CorrectnessInv --length=5 MC4_3_correct.tla

(the choice of the invariant and length does not matter)

4. Apalache exits with:

Assignment error: Failed to find assignments and symbolic transitions in InitPrimed E@15:05:27.381

Expected behavior
Apalache exits with EXITCODE: OK

Log files

• Tool output
• detailed.log

Desktop

• OS: macOS 10.15.7
• JDK version: OpenJDK 1.8.0_275 (OpenJDK Runtime Environment (AdoptOpenJDK)(build 1.8.0_275-b01))
• Version: 0.7.3-SNAPSHOT (03fdeff)

Additional context

@konnov pointed out that this is related to #338.

Temporary solution

@konnov suggests using Apalache at commit 014dd56 which does not exhibit this problem. I have confirmed this.

[konnov]

@Kukovec has fixed it.