NullPointerException in ForkJoinApplyAlgorithm
When running PJBDD on a machine with only 1 CPU[a], PJBDD will fail with a NullPointerException:
java.lang.NullPointerException: Cannot invoke "org.sosy_lab.pjbdd.util.threadpool.ParallelismManager.canFork(int)" because "this.parallelismManager" is null
at org.sosy_lab.pjbdd.bdd.algorithm.ForkJoinApplyAlgorithm.asyncShannonExpansion(ForkJoinApplyAlgorithm.java:87)
at org.sosy_lab.pjbdd.bdd.algorithm.ForkJoinApplyAlgorithm.lambda$makeOp$0(ForkJoinApplyAlgorithm.java:54)
at java.base/java.util.Optional.orElseGet(Optional.java:364)
at org.sosy_lab.pjbdd.bdd.algorithm.ForkJoinApplyAlgorithm.makeOp(ForkJoinApplyAlgorithm.java:54)
at org.sosy_lab.pjbdd.bdd.BDDCreator.makeOp(BDDCreator.java:123)
at org.sosy_lab.pjbdd.bdd.BDDCreator.makeAnd(BDDCreator.java:63)
You can emulate one core by passing the JVM flag -XX:ActiveProcessorCount=1
.
[a] Why would you run PJBDD on a machine with only one CPU? Well, it happened to us on a small virtual machine.
It would be great if this could be fixed. Happy to provide more information and/or test things.
Edited by Magnus Madsen