SMTChecker：the description of model-checker-timeout does not match the actual behavior.

[Subway2023]

The model-checker-timeout does not match the description. If I set it to 5 seconds, the actual program runtime could be 10 seconds.

test.sol

contract BugDetection {
    struct Data {
        uint256 value;
    }
    Data private data;
    function initialize(uint256 initialValue) public {
        data = Data(initialValue);
        checkLiveness();
    }
    function checkLiveness() private view {
        assert(data.value > 0 || data.value < 0); // Contradictory assertion
    }
    function modifyValue(uint256 newValue) public {
        data.value = newValue;
        bitwiseOperationCheck();
    }
    function bitwiseOperationCheck() internal view {
        uint256 calculatedValue = data.value & 0xffffffffffffffffffffffffffffffff; // Intentionally incorrect bitwise operation
        assert(calculatedValue == data.value);
    }
}

test.py

import time
import subprocess

start_time = time.time()
command="solc-0828 test.sol --model-checker-timeout 5000 --model-checker-ext-calls trusted --model-checker-engine bmc --model-checker-bmc-loop-iterations 1 --model-checker-solvers z3"
output = subprocess.check_output(command,shell=True)
end_time = time.time() 
execution_time = end_time - start_time  # Calculate the time difference
print(f"smtchecker:  {execution_time:.4f} seconds")

Warning: BMC: 2 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.

smtchecker:  10.1223 seconds