Kukovec

## Description See title. ## Input specification Any, where `Inv` has multiple counterexamples. ## The command line parameters used to run the tool `apalache-mc check --inv=Inv --max-error=10 MySpec.tla ` ##...

Currently, `INSTANCE`-`WITH` is resolved ad-hoc in the parser pass, and fails to account for naming collisions (see #2132). We should treat it as a `TlaDecl` and delay the instantiation until...

TLA+ spec of CCV

1

This PR ports and updates the previously created CCV TLA+ spec from https://github.com/cosmos/interchain-security/tree/jk/ISaudit. It includes additional modeling of provider-side timeout.

[FEATURE] Add CLI support for parameters tunable by the Apalache global configuration file

5

Title.

This is part of a broader set of efforts to modernize the solver core (see https://github.com/informalsystems/apalache/milestone/75). Since the new rules no longer use `SymbState`, we need to change the interface,...

This issue is meant to aggregate discussions regarding tests, which involve `Z3SolverContext` (or, more specifically, SMT constraints). In general, SMT constraints make unit testing difficult, because adding constraints mutates the...

See the TODO in `DelayedConstraintGenerator`.

Partially resolves #2339.

Not having access to all rewriting rules means we cannot write all of the meaningful test scenarios. Once we have all rules in place, we should go back and add...

Recent refactoring has uncovered that caches are often not being hit consistently. The reason for this is a type-tag check in the cache lookup, which often fails, as internally TLA...