Are there terminating methods to provide models of first-order theory formulae?

Question

If a first-order theory is decidable on its existential fragment, does this imply that we have a method (that guarantees termination) to obtain models of existentially quantified formulae within this theory?

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 it can solve the satisfiability problem. But what if we want to ask for a model? Is there a similar procedure that guarantees termination and offers a model? Maybe some modification of Cooper's method?

Generally, I am interested in the following. Consider we have a formula with the shape ∃∀.φ and φ is in theory T; then, I wonder whether there are T such that (one option or the other):

1. T admits QE and, if we perform elimination of ∀ in ∃∀.φ and get ∃.φ'; then, T has a terminating method that guarantees providing models of ∃.φ'?

2. T is decidable, but does not admit QE (this seems to hold for naturals; e.g., Showing the natural numbers $(\Bbb{N},<)$ do not admit quantifier elimination); however, T has a terminating method that guarantees providing models of ∃∀.φ?

I know there are SMT solvers, but I am rather interested in procedural methods of classic literature (e.g., Cooper, Ferrante-Rackoff etc). The question may be obvious; in such case, I am happy to just receive witnesses of those terminating algorithms that produce models in T.

PS: I am not sure if I should ask this question here or in the Computer Science Stack, sorry for the inconvenience in advance.