  We consider the decidability of the verification problem of programs
\emph{modulo axioms} --- that is, verifying whether programs satisfy their
assertions, when the functions and relations it uses are assumed to interpreted
by arbitrary functions and relations that satisfy a set of first-order axioms.
Unfortunately, verification of entirely uninterpreted programs (with the empty
set of axioms) is already undecidable. A recent work introduced a subclass of
\emph{coherent} uninterpreted programs, and showed that they admit decidable
verification \cite{coherence2019}. We undertake a systematic study of various
natural axioms for relations and functions, and study the decidability of the
coherent verification problem. Axioms include relations being reflexive,
symmetric, transitive, or total order relations, %and their combinations,
functions restricted to being associative, idempotent or commutative, and
combinations of such axioms as well. Our comprehensive results unearth a rich
landscape that shows that though several axiom classes admit decidability for
coherent programs, coherence is not a panacea as several others continue to be
undecidable.
