CVC4 ignores its time limit
On the goal valuation_split
in file examples/multiprecision/valuation.mlw
, calling the prover cvc4 1.4 with timeout 1 second takes more than 10 seconds.
I reverted commit 2dd6af2e (which replaces all responses by timeouts if the time taken was over 90% of the limit) by hand, and it showed that CVC4 returns Unknown after 10 seconds. However, if I call cvc4 with timeout=20s, it does take the full 20 seconds before responding.
This behavior seems to originate from commit 54d4a2e7 (increase hard time limit for provers implementing a soft time limit).