search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
302 stars 52 forks source link

use atomic instead of mutex to allow multiple calls to disableLimitEnforcement #622

Closed MichaelRawson closed 20 hours ago

MichaelRawson commented 1 week ago

In #577 I failed to notice that FMB calls Timer::disableLimitEnforcement more than once for some reason. This causes FMB to hang on success (!). Oops.

Fix that by using an atomic flag rather than a mutex. This also seems more intuitive to me in retrospect.

MichaelRawson commented 20 hours ago

After discussion with @quickbeam123 , probably std::mutex::try_lock is a better option. (or std::recursive_mutex)