Evgeniy Moiseenko

Hi @affeldt-aist, thank you for the quick response! > Note also that monae's master now uses Hierarchy Builder and this triggers a new set of dependencies that are here to...

> > What can I start from? > > I did a tentative split as PR #57 . > Dependencies on `classical_sets_ext.v` could be removed by PRing the needed lemmas...

> We've been using Z instead of ssrint because it is a bit easier to use (in particular, more people are familiar with it), > it lends itself to execution...

Hi, what is the status of this? Is somebody working on this currently? We need similar functionality (e.g. heterogeneous decidable relations, union, intersection, etc) in our project and for integration...

We will get back to this after #249

> why would a data structure launch a coroutine? I mentioned that this is unlikely case: > Currently, the primary use case of Lincheck is to test concurrent data structures...

I think we eventually should refactor `TestThreadExecutionGenerator`. See, e.g. this issue #196 Let's collect all the problems with current implementation that we want to solve with the refactoring.

Hi @ben-manes ! I was debugging your test and discovered a couple of suspicious things. First, I think there is a typo in the `merge` operation: ```java @Operation public Integer...

> I was wondering that too about containsValue, but then I was surprised it passed in prior releases? The number of invocations is relatively small (`1_000`). So yes, I guess...

New branch name for the strategy (after rebase to the new bytecode transformation): https://github.com/JetBrains/lincheck/tree/new-mc