search

hernanponcedeleon / Dat3M

A verification tool for many memory models
MIT License
77 stars 29 forks source link

Refinement getting stuck on qspinlock with Z3 in CI/UnitTests #378

Closed ThomasHaas closed 1 year ago

ThomasHaas commented 1 year ago

Refinement sometimes gets stuck on the qspinlock unit tests. This is because the Z3 solver doesn't return from its first isUnsat call. If I forcefully terminate the solver, I get the exception

org.sosy_lab.java_smt.solvers.z3.Z3SolverException: Solver returned 'unknown' status, reason: (incomplete (theory arithmetic))

I assume this is because qspinlock needs BV theory but we use IA theory by default. This theory mixing can cause Z3 to get stuck. It does not seem to happen with the other solvers (assume/incremental), likely because the Wmm constraints prohibit the smt solver to even get into the incomplete situation.

As long as we cannot configure individual tests to use different ARCH_PRECISION, I think we need to remove this unit test.

ThomasHaas commented 1 year ago

The preoblematic unit test was removed in #386