I am studying decision procedures and, on the other hand, I am also studying Z3. Specifically, I am researching different decidable fragments of first-order theory of arrays.
For instance, paper [1] presents an ∃∗∀∗ fragment of arrays for which we can prove properties about: e.g., ∀i . 0 ≤ i < n → a[i+1] = a[i]−1. However, they establish decidability of this logic following an automata-theoretic approach, via definition of a new class of Büchi automata with counters. This sounds to me far from the classical quantifier eliminations that I understand SMT solvers have implemented as decision procedures for decidable theories with quantifiers.
Thus, my question is the following: if a theory is proven to be decidable like in paper [1], does Z3 (and other solvers) implement these decision procedures? In other words, is the ∀i . 0 ≤ i < n → a[i+1] = a[i]−1 query decided with a terminating decision procedure in Z3, or uses more-efficient-yet-semi-decidable heuristics? In case they use terminating procedures, how does Z3 (and the rest) identify the decidable fragment? Maybe with language-identification using formal grammars?
[1] What Else Is Decidable about Integer Arrays? https://hal.archives-ouvertes.fr/hal-01418914/document
Like any piece of large software, z3 is a collection of a bunch of algorithms implemented over the years. So, it can be hard to pin down exactly what algorithms are implemented and how they interact; especially given it's also being actively developed. So, to answer your question with any authority, you'd have to ask the actual developers. https://github.com/Z3Prover/z3/discussions is the best forum for that; stack-overflow will unlikely yield a satisfactory answer for you.
The other thing to do is to look at the source code itself. Since it's open source, you can see for yourself how it's constructed. While this is not for the casual end-users, sounds like your interest goes deeper; so you might as well get more familiar with how the whole thing is constructed.
My personal view is that it's like any other software project. The emphasis is on correctness, with a goal (but necessarily target) of completeness. Working well on practical problems that people in industry come across is more important than implementing a theoretical decision procedure that performs terribly in terms of performance. (So, this is where heuristics come into play. Recognizing and rewriting patterns with the hope that an unsat result might be reached. The bit-vector theory is a good example of this: It's easy to just bit-blast and toss it to the SAT solver, but z3 tries really hard to rewrite and do other "magic" so the computational complexity can be tamed; with varying degrees of success.) But all of this is the "kitchen" side of things. For precise answers, try the z3-discussions forum, and hopefully one of the actual developers will give you a more accurate answer.