Description
SMT-Lib recursive function definitions are given semantics via quantified formulas for the defining equations. Hence, I'd expect:
(set-logic ALL)
(define-fun-rec f ((x Int)) Int (+ 1 (f x)))
(declare-fun y () Int)
(assert (distinct (f y) (+ 1 (f y))))
(check-sat)
(get-model)
(get-value (f))
to produce unsat since f is not satisfiable by any function Int -> Int. Indeed cvc5 produces unsat for this query. But z3 says:
sat
(
(define-fun y () Int
0)
)
((f (lambda ((x!1 Int)) (+ 2 (f x!1)))))
This model is bogus. Indeed:
$ z3 model_validate=true a.smt2
sat
... Loops forever ...
Surprisingly, if I replace define-fun-rec with:
(declare-fun f (Int) Int)
(assert (forall ((x Int)) (= (f x) (+ 1 (f x)))))
then z3 does say unsat correctly.
I understand that this is a bit of nit-picking. While z3 is not compliant to SMT-Lib spec in the above sense, I can also see that you forgo the undecidable termination checking and simply assume all recursive-equations are well-defined. But looks like you already have the mechanisms to at least "detect" such cases in certain circumstances, so I wonder why the discrepancy between define-fun-rec and the semantically equivalent forall variant. In particular, while looping-forever is never nice, it's better than having an unsound model returned; from the perspective of tools that use z3 as a backend.
I'm perfectly happy this being marked as "won't-fix", though perhaps it is worthy of a mention in the user-guide or documentation somewhere.