ini-option CASE_SPLIT produces strange model

Question

While working on my masters thesis with z3 I found something strange I can't understand. I hope you can help me. :)

The smt-file I wrote looks like this:

(set-logic QF_UF)
(set-info :smt-lib-version 2.0)

;Declare sort Node and its objects.
(declare-sort Node 0)
(declare-fun n0 () Node)
(declare-fun n1 () Node)

;Predicate
(declare-fun dead_0 (Node) Bool)
;Abbreviation
(declare-fun I () Bool)

;initial configuration
(assert(= I (and 
(not(= n0 n1))
(not(dead_0 n0))
(dead_0 n1))))

;Predicate
(declare-fun dead_1 (Node) Bool)
;variable
(declare-fun m0_1 () Node)

;Abbreviation for Transformation
(declare-fun TL1_1 () Bool)

;Transformation1neuerKnoten1
(assert(or (= m0_1 n0)(= m0_1 n1)))

;Is the whole formula satisfiable?
(assert(= (and I TL1_1) true))
(check-sat)
(get-model)

Everything works quite well while using z3 as a command line tool with default-options. The generated model contains:

;; universe for Node:
;;   Node!val!0 Node!val!1 
;; -----------

and

(define-fun n0 () Node
Node!val!0)
(define-fun n1 () Node
Node!val!1)
(define-fun m0_1 () Node
Node!val!0)

So my variable m0_1 is bound to the node n0.

Then I used z3 with an ini-file only containing CASE_SPLIT=5. The result was a strange model. In my opinion the difference is basically that my variable m0_1 is NOT bound to any of my nodes n0 or n1. The produced model contains:

;; universe for Node:
;;   Node!val!2 Node!val!0 Node!val!1 
;; -----------

and

(define-fun n0 () Node
Node!val!0)
(define-fun n1 () Node
Node!val!1)
(define-fun m0_1 () Node
Node!val!2)

So my question is this: why did z3 create another node (Node!val!2) and why is my variable m0_1 bound to this new node? I thought that one of my assertions ((assert(or (= m0_1 n0)(= m0_1 n1)))) would forbid this.

Thanks in advance! :)

Answer 1

Z3 has a feature called "relevancy propagation". This is feature is very effective for problems containing quantifiers, but it is usually overhead for quantifier free problems. The command line option RELEVANCY=0 disables relevancy propagation, and RELEVANCY=2 or RELEVANCY=1 enables it. The option CASE_SPLIT=5 assumes that relevancy propagation is enabled. If we provide CASE_SPLIT=5 RELEVANCY=0, then Z3 will generate a warning message

WARNING: relevacy must be enabled to use option CASE_SPLIT=3, 4 or 5

and, ignores the option.

Moreover, by default, Z3 uses a "automatic configuration" feature. This feature scans the input formula and adjusts the Z3 configuration for the given instance. So, in your example, the following happens:

1. You provide the option CASE_SPLIT=5
2. When Z3 validates the command line options, relevancy propagation is disabled, and no warning message is generated.
3. Z3 runs the auto configuration procedure, and since your example is quantifier free, it disables relevancy propagation RELEVANCY=0. Now, an inconsistent configuration is uses, and Z3 produces the wrong result.

To avoid this problem, if you use CASE_SPLIT=5, then you should also use AUTO_CONFIG=false (disables auto configuration) and RELEVANCY=2 (enables relevancy propagation). So, the command line should be:

z3 CASE_SPLIT=5 AUTO_CONFIG=false RELEVANCY=2 file.smt2

In the next release (Z3 4.2), I will make Z3 to display the warning message if the user tries to set CASE_SPLIT=5 when auto configuration is enabled.