java-smt
java-smt copied to clipboard
CVC5: Crashes with segmentation fault in SolverConcurrencyTest
Hello everyone, while working on https://github.com/sosy-lab/java-smt/pull/345 I noticed that one of the concurrent tests seems to (occasionally) fail for CVC5. The test case is testBvConcurrencyWithConcurrentContext from SolverConcurrencyTest and you can find two examples here and here. I was able to replicate the issue on my own machine by running the test in a loop. After a few iterations the test will always fail, however, I get a segfault instead of the assertion error. The issue seems to equally affect testIntConcurrencyWithConcurrentContext and is different from https://github.com/sosy-lab/java-smt/issues/310. Has this already been looked into?
This is a bug in CVC5 and I reported it here