Expression sharing via (uninterpreted) functions

[ThomasHaas]

Background: I have a BMC tool that finds bugs in C-code. One of its preprocessing steps is inlining of functions calls.
Now suppose there is a function f(x) = some complex expression in x and there are multiple calls to this function in the code, let's say,

a := f(r);
b := f(s);
c := f(t);

Inlining the function calls and then translating this code into SMT (+ some assertions of course) will cause the resulting formula to contain the complex expression 3 times (for r, s, and t), which I think may cause the solver to do redundant reasoning.

Now my question is this: If I introduce an uninterpreted function symbol f, add the assertion assert forall x: f(x) = complex expression in x and then reuse this function symbol in the actual SMT-query, will this help the solver in some way or does it rather hurt the solver because of the new forall quantifier? Will the solver perhaps just instantiate the definition of f 3 times and essentially produce the identical query as the original one?

Is there a maybe another trick to maximize sharing of expressions and minimize redundant reasoning for the solver?

[NikolajBjorner]

You can define f as a recursive function. While z3 detects that f isn't recursive and has special unfolding for it, the unfolding semantics is delayed.

[ThomasHaas]

As far as I understand this only delays the unfolding, so if the constraints involving the function are guaranteed to be relevant for satisfiability, then eventually everything will get unfolded and I'm back to the original query, right?
In my use-case, the expressions are guaranteed to be necessary so I feel like this shouldn't help at all then.

Let me ask a similar question then: If I know that the range of possible values for r, s, and t is quite small (lets say 0<=r,s,t<=5), would it be beneficial to precompute the values of f for those values to assert them expliticity (i.e. assert f(0)=... and f(1)=... and ...), and then avoid the complex expression altogether?
Basically I'm trying to get to know if there are general SMT-modeling techniques that can be exploited to ease the problem for the SMT-solver.

[NikolajBjorner]

It is often (in various contexts) observed that in-lining quantifier instantiation by the
application can be better than using the quantifier engine lazily instantiate them.
There is a limit to this, of course.

[ThomasHaas]

Okay, thank you. Then I will likely keep the inlining as is and see if I can find more promising areas where I can optimize the encoding.