strange Z3 model value

问题:

I'm using the latest Z3 version 3.2. I get an unexpected response from the "get-value" command. Here is the little script that I run in SMT-LIB2 compliant mode:

(set-option :produce-models true)
(declare-datatypes () ((Object o0 null)))
(declare-fun IF (Object) Int)
(declare-fun i2 () Int) 
(assert (= (IF o0) i2))
(assert (= (IF null) 0))
(check-sat)
(get-value (i2))

The response is:

((i2 (IF o0)))

I expect to get just "0" back. Is there any way to ask Z3 to evaluate the returned term to a universe constant?

Here is the full model:

(model 
;; universe for Object:
;;   Object!val!0 
;; -----------
;; definitions for universe elements:
(declare-fun Object!val!0 () Object)
;; cardinality constraint:
(forall ((x Object)) (= x Object!val!0))
;; -----------
(define-fun i2 () Int
(IF o0))
(define-fun IF ((x!1 Object)) Int
  (ite (= x!1 Object!val!0) 0
    0))
)

I'm also puzzled why o0 is not defined in the model.

回答1:

This has been fixed in Z3 4.0. Z3 4.0 will be released soon. In the meantime, you can use it online: http://rise4fun.com/Z3/75y

This link can be used to execute your example. Z3 4.0 produces the expected result.

Regarding the bug, the main problem is that Z3 is treating Object as an uninterpreted sort. In Z3 3.2, you can workaround this bug by including

(set-option :auto-config false)

in the beginning of your script.