If a theory is decidable in the existential fragment, does this mean that there is a (terminating) method to obtain witnesses of satisfaction?

I am concerned with whether there are algorithms (e.g., implemented in SMT solvers) that guarantee termination on the task of giving models of existential formulae; in the same way they guarantee termination for the satisfiability problem. Let me try to explain myself.

If a first-order theory T is decidable on its existential fragment, this means that there is a method (that guarantees termination) that solves the satisfiability problem for all existential formulae of T. Am I right?

My question is: does T being existential-decidable imply that we have a method (that guarantees termination) to obtain models of existential formulae within T? In other words, if we have a method to solve satisfiability on existential formulae of T, does this mean we also have a method to obtain models of such formulae (in satisfiable instances)?

For instance, consider the theory of linear integer arithmetic. We know there is a terminating algorithm (i.e., Cooper's method) that performs quantifier elimination (QE) yielding a decision procedure if all variables are bounded by the quantifiers. This means that Cooper can solve the satisfiability problem of linear arithmetic with a termination guarantee. And this also means that, if an SMT solver (say, Z3) implements Cooper for the satisfiability problem, then it (in theory) offers termination. Right?

However, what if we want to ask for a model? It is clear that, for this theory, it has not been necessary to compute a witness of satisfaction (it has been done using QE), so maybe there is no method to get this witness. In other words, we can e.g., decide satisfiability of ∃x,y. (x<y) using Cooper, but not get a witness!

So, is there a similar method that guarantees termination and offers a model? Maybe some modification of QE methods? I think it could be the case, because QE methods somehow compute test-points and maybe we can extract witnesses of such points...

Also, consider finite theories (e.g., naturals up to 100). Then, it is clear that, by enumeration, we can both have a method to decide satisfiability and return a witness. My concern is with respect to infinite theories. As we saw, QE does not imply witness obtention, but maybe there is some result out there that guarantees that if a theory is shown to be decidable with a QE method, then there is another method that computes witnesses.

In case of positive answer, do SMT solvers (any of them) implement these guarantee model-provision? If not, why is this so? Is there any information about this in the literature of SMT solvers?

If I understand your question correctly, you're asking if there are any scenarios where the SMT solver can say "yes this is SAT," but is unable to display a model for it.

This, by construction, doesn't happen in the typical DPLL(T) based SMT solving. The way such solvers work is by always finding a model in case of SAT. This does not mean that you can have some other algorithm to determine if something is SAT, but not be able to come up with a model. That's entirely possible in general theorem proving, but does not happen in what we usually consider under the purview of SMT solving. (Example from theorem proving: In a logic without excluded middle, you can establish something is false, yet not be able to show an instance. This is where the axiom-of-choice comes into play. But such techniques are way outside the realm of usual SMT solving.)

In the context of SMT solving, what we care about (usually) is finite-model finding. That is, can we demonstrate a small model? (This is very important in practice, as models are usually counter-examples, and the smaller the counter-example, the better.) If the model can only be infinite, you'll find that the SMT solvers usually won't terminate. There's a lot of research on this topic. This is a good paper to read: http://homepage.divms.uiowa.edu/~ajreynol/cav13.pdf