Getting UNKNOWN quickly for suspected SAT cases

Feb 13, 2015 at 3:28 AM
Edited Feb 13, 2015 at 10: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.
For the first script, we obtain the result UNKNOWN in less than a second. That answer is not perfect, but ok for our software model checker.
For the second script, we do not get an answer. I stopped Z3 after 20 minutes.
After 20 minutes I obtained some verbose output and the following statistics.
(:added-eqs 100444610
:array-ax1 219605
:array-ax2 67917179
:array-exp-ax2 98784
:array-ext-ax 184337
:conflicts 33551
:decisions 1112541
:del-clause 323814764
:final-checks 108
:max-generation 10
:memory 603.02
:minimized-lits 26209
:mk-clause 324073401
:num-checks 1
:propagations 114823967
:quant-instantiations 54223
:restarts 161
:time 1211.33
:total-time 1211.33)
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 5: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)