Dat3M icon indicating copy to clipboard operation
Dat3M copied to clipboard

Published 20 hours ago • verified publisher icon hernanponcedeleon

Performance of Incremental and Assume Solver

Open hernanponcedeleon opened this issue 3 years ago • 2 comments

Under Power, the TwoSolvers can easily handle the test /litmus/PPC/Dart-ctrl-two-regs.litmus. However both IncrementalSolver and AssumeSolver get stuck. The problem happens in the javasmt branch and it is not reproducible in master. Thus the problem is probably in the JavaSMT library.

hernanponcedeleon avatar Aug 03 '21 07:08 hernanponcedeleon

This seems to also affect refinement (which inherently uses the incremental solver for the outer iteration): when running refinement tests on the litmus tests, we get problems in these benchmarks (the mentioned one + those with similar names + 2 in Linux)

hernanponcedeleon avatar Sep 08 '21 11:09 hernanponcedeleon

I tried disabling the usePhantomReferences option and the problem remains.

hernanponcedeleon avatar Sep 08 '21 12:09 hernanponcedeleon

This issue is not reproducible anymore.

hernanponcedeleon avatar Jan 29 '23 18:01 hernanponcedeleon