java-smt icon indicating copy to clipboard operation
java-smt copied to clipboard

CVC5: Crashes with segmentation fault in SolverConcurrencyTest

Open daniel-raffler opened this issue 1 year ago • 1 comments

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?

daniel-raffler avatar Dec 20 '23 22:12 daniel-raffler

This is a bug in CVC5 and I reported it here

daniel-raffler avatar Dec 28 '23 22:12 daniel-raffler