I am reading the following paper, On the Combination of the Bernays–Schönfinkel–Ramsey Fragment with Simple Linear Integer Arithmetic: https://arxiv.org/pdf/1705.08792.pdf
In the introduction it states the following: The Bernays-Schönfinkel-Ramsey (BSR) fragment comprises exactly the first-order logic prenex sentences with the $\exists^*\forall^*$ quantifier prefix, resulting in a CNF where all occurring function symbols are constants. Formulas may contain equality. Satisfiability of the BSR fragment is decidable and NExpTime-complete. Its extension with linear arithmetic is undecidable.
However, as far as I knew:
- From (https://en.wikipedia.org/wiki/Bernays%E2%80%93Sch%C3%B6nfinkel_class): BSR It is the set of sentences that, when written in prenex normal form, have an $\exists^*\forall^*$ quantifier prefix and do not contain any function symbols.
- Linear integer arithmetic (LIA) and linear real arithmetic (LRA) are both decidable. Thus, the whole first-order theory of linear arithmetics is decidable.
So I am not understanding something: in my opinion, BSR modulo LIA/LRA should be decidable.
My reasoning is that, since LIA/LRA is decidable (i.e., not matters the quantifier alternation, it is decidable), then the LIA/LRA restricted to BSR fragment (equivalently, BSR modulo LIA/LRA) should be decidable. I mean, decidability implies $\exists^*\forall^*$-decidability, am I right?
I am sure I am the one that is missing something, so can anyone help me out?