Are there standard approaches to translate the semantics of for loops in imperative languages (say C or Java) to SMT-LIB? I was thinking of defining them as SMT-LIB axioms but it seems ad-hoc, and I understand that the translation will not always be decidable by solvers say z3.
The classic "trick" is to unroll your loops within a bound. This idea originates from the hardware community where bounded-proofs are much more common. But it also applies to software. CBMC (https://www.cprover.org/cbmc/) is a system that does this for C programs. Obviously this'll only provide "proof" for cases the unroll-number is sufficient.
Note that unrolling may not be practical as it can lead to code-explosion, in such cases, you can use the "uninterpreted-function" trick: i.e., you unroll a fixed number of times and then abstract over the remainder of the computation. This can lead to false-positives, i.e., the solver can return a bogus model. But this idea can be used in a CEGAR (counter-example-guided-abstraction-refinement) based system.
In general, loops imply invariants, and proofs for programs involving loops (or recursion) require figuring out what those invariants are and proving them by induction. SMT solvers don't do inductive proofs. For such problems, it's best to use a genuine theorem prover (Isabelle, HOL, HOL-Light, Coq, Agda, Lean; take your pick). Note that most of these systems these days can use an SMT-solver as an "oracle" to speed-up/discover proofs for subgoals, so in that sense, you get the best of both worlds. In particular, Lean comes from the z3 lineage and is definitely worth checking out: https://leanprover.github.io/