--numberOfParallelVerifiers 0 causes NPE
alexanderjsummers opened this issue · 1 comments
The documentation of this command-line option says that the number of Z3 instances run by silicon is this number plus 1. So, to get sequential verification, I assume we should set it to 0. However, this causes a crash. Running with 1 seems to work fine (but I'm not sure this is sequential).
Maybe we could eventually have a simpler option to specify sequential verification (for reproducibility: the reason I wanted to set this up was for a non-deterministic behaviour I was debugging). But we should fix the crash anyway, I think.
For the record, yes, setting it to 1 will cause sequential verification. The reason it's plus 1 is that there is always an additional Z3 instance used to verify functions (sequentially, before method verification happens). But obviously the documentation should be clear about this and Silicon shouldn't crash.