Feb 13, 2015 at 2:28 AM
Edited Feb 13, 2015 at 9:03 AM
Our software model checker generates a lot of SMT queries that contain formulas with quantifiers and arrays. The following two scripts each contain an example.
, we obtain the result UNKNOWN in less than a second. That answer is not perfect, but ok for our software model checker.
, we do not get an answer. I stopped Z3 after 20 minutes.
After 20 minutes I obtained some
and the following statistics.
Now, I am wondering why we do not get quickly the answer UNKNOWN also for the second script.
Is that a bug?
Is "getting UNKNOWN quickly for suspected SAT cases" a feature that I can switch on (via some parameter)?
Of course, I could use the timeout. However, our tool has a lot of queries to Z3. Some of them are important for the progress of our tool. Hence I do not want to set a very low timeout.
Mar 21, 2015 at 4:21 PM
I have a feeling I've answered this question elsewhere before, if not apologies for the delay.
There is no "quick unknown" feature, but we can disable MBQI. Roughly, e-matching is used to proof unsatisfiability and MBQI is used to show satisfiability. In this case, e-matching fails, which we can interpret as "suspected SAT", and MBQI
takes over, trying to build model functions. If you don't need any SAT answers at all, then you can just disable MBQI and Z3 will give up as soon as e-matching fails. To do that, we first have to disable auto-configuration, which may have other consequences,
but for a start try adding the following:
(set-option :auto_config false)
(set-option :smt.mbqi false)