Unsatisfiable recursion equations

[LeventErkok]

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.

[NikolajBjorner]

I am aware of this behavior. It is mentioned somewhere else before.
non-terminating recursive definitions -> unsound results.
Often unsoundness is the other way around: return unsat when the problem is sat.

Should z3 establish termination when it returns SAT?
Maybe. But currently, model-validation is naive and just loops.

A reason to not spending bandwidth on non-termination checking was to assume ITP or "auto-active" users handle this at their level: why replicate what first-class methods for termination and non-termination accomplish (some of which use z3 for solving sub-problems)?