What is INST_GEN in z3

Question

Context: I do research on bounded java program verification using z3. I want to get an optimization model on a linearization problem. A standard approach could be incrementally search the model until find a unsat case. But the performance seems be a problem, and it destroys the code portability by introducing JNI, which intergrates z3 c/c++ api to my tool.

Now I want to add constraints on all inputs of a java method. I use quantity arrays (I use theory of array to model heaps). However, z3 always returns "unknown" immediately on a satisfiable problem. It seems that it is impossible to generate model. I notice that there is an option of z3, INST_GEN, then I am trying to understand it. I feed following formulas to z3.

(set-option :INST_GEN true)
(define-sort S () (_ BitVec 2))
(declare-fun s () S)
(assert (= s (_ bv0 2)))

(define-sort A () (Array S S))
(push) ;; 1st case    
(assert (forall ((a A)) (= (select a s) s)))
(check-sat)
(get-model)
(pop)

(push) ;; 2nd case
(declare-fun a () A)
(assert (forall ((t S)) (= (select a t) t)))
(check-sat)
(get-model)
(pop)

(push) ;; 3rd case
(check-sat)
(get-model)
(pop)

In both 1st and 2nd cases, z3 returns "segmentation fault" in Linux, while it crashes in windows 7. Both z3 are version 4.0, x64.

In 3rd case, it is quantify-free, and Z3 successfully generates model

sat 
(model (define-fun s () (_ BitVec 2) #b00) )

My first question is how this option works? Does it enumerate arrays?

Second question is, I notice that z3 could successfully return "unsat" on a unsatisfied problem with quantify arrays. Does z3 support some option or approach to generate a model in a satisfied problem with quantified arrays, with bounded indices and elements? e.g. using if-then-else clause.

Thank you for your reading and consideration! Any suggestions are greatly appreciated!

Answer 1

First, the option INST_GEN was part of an experiment. It should not have been exposed to external users. This options was not seriously tested. It will be hidden in future versions. Sorry about that.

Second, in general, Z3 will fail on satisfiable problems that quantify over arrays. The following tutorial (section Quantifiers) describes many fragments where Z3 is complete.

Finally, Z3 has many different engines/solvers. However, only one of them supports incremental solving. Whenever, push/pop commands are used, Z3 will automatically switch to this incremental solver. If we remove the push and pop commands, then Z3 can show the second problem to be satisfiable. Here is a link with the modified example: http://rise4fun.com/Z3/apcQ.