Bug with recursive functions?

Question

I'm trying recursive functions in z3, and I'm curious if there's a bug with model construction. Consider:

(define-fun-rec f ((x Int)) Int
                  (ite (> x 1)
                       (f (- x 1))
                       1))
(check-sat)
(get-value ((f 0)))

Here f is actually the constant function 1, just defined in a silly way. For this input, z3 prints:

sat
(((f 0) 0))

This seems incorrect, since f 0 should equal 1.

What's interesting is if I assert what z3 proposes as the result, then I get the correct unsat answer:

(define-fun-rec f ((x Int)) Int
                  (ite (> x 1)
                       (f (- x 1))
                       1))
(assert (= (f 0) 0))
(check-sat)

I get:

unsat

So, it looks like z3 actually does now that f 0 cannot be 0; even though it produced that very model in the previous case.

Taking this one step further, if I issue:

(define-fun-rec f ((x Int)) Int
                  (ite (> x 1)
                       (f (- x 1))
                       1))
(assert (= (f 0) 1))
(check-sat)
(get-model)

Then z3 responds:

sat
(model
  (define-fun f ((x!0 Int)) Int
    1)
)

which is indeed a reasonable answer.

So, it seems perhaps there's a bug with recursive function models under certain conditions?

Answer 1

The models used not to reflect the graph of recursive function definitions. So when evaluating recursive functions on values that had not been seen during solving it could produce arbitrary results. This behavior is now changed as the recursive definitions are included in models.