Unsound result with define-fun-rec and declare-const, reloaded

[Elarnon]

With the following query:

(declare-const W Int)
(declare-const x Int)
(define-fun-rec sat ((x Int)) Int (ite (< x W) x W))

(assert (not (= (sat x) (ite (< x W) x W))))
(assert (= W 10))

(check-sat)

Z3 (tested on 4.8.11 and on current master) answers sat and generates an invalid model (this is caught by model_validate).
If I either remove the assertion (= W 10) or use (define-const W Int 10) instead, Z3 correctly answers unsat.

This looks like a variation on #5305.

[Elarnon]

This doesn't happen with (check-sat-using smt), and I narrowed it down to the solve-eqs call used by the default tactic. It looks like that solve-eqs does not rewrite within the body of the recursive function (and macro-finder doesn't look like it does either).

Simplified example:

(declare-const W Int)
(declare-const x Int)
(define-fun-rec rW ((x Int)) Int W)
(assert (distinct (rW x) W))
(assert (= W 10))

(check-sat-using (then solve-eqs smt))

[Elarnon]

Thank you for the fix @NikolajBjorner; I can confirm the issue is no longer present with a constant + solve-eqs in the current master. However it is still present when using a function + macro-finder instead, see example below. I should have included it in the previous message.

(declare-fun W (Int) Int)
(declare-const x Int)
(define-fun-rec rW ((x Int)) Int (W x))
(assert (distinct (rW x) (W x)))
(assert (forall ((y Int)) (= (W y) 10)))

(check-sat-using (then macro-finder smt))

master (2c266a9) currently still answers sat for this problem.