Shon Feder

I think the easy path to this would proceed as follows: - [ ] Factor the current integration tests into separate files - [ ] Add a makefile pattern target...

Many thanks for this deep and thoughtful feedback, @hwayne! From my preliminary skim here, it seems to offer many critical insights on how we can improve -- not just this...

afaik, we've never supported integration with existing z3 installations. Instead, it was previously required to build z3 from source as part of the build for this project. We might target...

We've also just discussed internally about the possibility of adding an option to our build configuration that would allow using the system Z3 instead of z3-turnkey. I'll plan to investigate.

Yes! That will be much better :)

I don't think I would be in favor of any changes that reduced the quality of our linting or static analysis for the sake of making links in the API...

Thanks for the report! This is maybe a duplicate of #943, but that has an even broader scope, so we can keep this open as sub issue for now. It...

The problem @thpani identified should be fixed by https://github.com/informalsystems/apalache/pull/2041

Motivated by #1794, in our meeting today we discussed whether or not this functionality is actually used and useful. I think a good way forward here is to either document...

> This should motivate us to periodically run a large set of benchmarks in the CI. /cc @shonfeder Low hanging fruit is to set up a CI job in this...