Dafny has the option to set {:induction false}. Also, as far as I know, whenever we use assertions in Dafny, what happens below it that it constructs proof obligations and then calculates on them using Z3.
However, I read Z3 does not support induction: e.g., ... however, any non-trivial property will require a proof by induction. Z3 currently does not support proofs by induction... (cross product in z3)
So my question is: whenever we set {:induction true}, how is this induction performed in Dafny if not using Z3? Are there different underlying solvers? Are there any kind of heuristics? This last one is suggested here (Z3 model for correct Dafny method).
However, which type of heuristics are we talking about?
Dafny is first a programming language, with built-in support for verification machinery of the programs you write. This machinery includes support for induction. Note that this has nothing to do with z3: It's something Dafny itself supports. So, to answer your question simply: Because Dafny's support for induction is not implemented by z3: It's implemented by Dafny itself. Compare this to the goal of z3: A push-button tool that understands SMTLib, excellent for applying decision procedures to (typically) quantifier-free subsets of first-order logic, algebraic data-types, reals, linear-integer arithmetic etc. In particular, z3 is not itself a programming language, nor it’s intended to be used in that way. This makes it suitable as a "backend" tool for custom tools like Dafny that focusses on specific programming styles.
The difficulty with induction is coming up with the inductive invariant. A good way to "guess" the invariant is to follow the structure of your program, which has been exploited to a great extent in the ACL2 theorem prover: The recursive nature of the program suggests an induction schema. Of course, this isn't always enough. The inductive hypothesis can be really difficult to come up with, and typically requires user guidance. This is the style used in most theorem provers, like HOL, Isabelle, Coq, Lean, and many others.
Looking back at Dafny, the need for induction typically comes from the loops in Dafny programs. (See: https://dafny.org/dafny/DafnyRef/DafnyRef#20141-loop-invariants-sec-loop-invariants). So, Dafny can construct the "inductive" proof by using the typical Hoare logic loop principle. (https://en.wikipedia.org/wiki/Hoare_logic) So, what Dafny does is takes your annotated program (and this is the key, you are expected to annotate loops with their invariants), sets up the inductive proof (i.e., the base-case and the inductive-step), and formulates those in terms of an SMTLib query and passes it to z3. (This is a simplified account, but it is roughly the strategy followed in similar tools like Why3 etc as well.) So, the "inductive" proof is done by Dafny, which keeps track of the proof status, how the subgoals for induction relate to each other and the overall goal etc., and z3 is merely used for establishing each of these individual goals that require no induction for their proofs.
A good paper to read on how Dafny works is Rustan's paper: Automating Theorem proving using SMT. This is a very good paper in the sense that it outlines how to build a theorem prover using SMT: While induction will be the main workhorse, there're many moving parts in such a system and Rustan gives a very nice overview of the techniques and challenges involved.
So, to summarize, Dafny supports induction because Dafny's verification system implements support for inductive proofs. z3 is simply a backend tool Dafny uses to discharge non-inductive goals; everything else is kept track of by Dafny itself.
Final note: Recent versions of SMTLib does include support for recursive-definitions, whose proofs will require induction. So, it is possible that SMT solvers will gain induction capabilities, and CVC5 already supports induction to some extent. (http://lara.epfl.ch/~reynolds/VMCAI2015-ind/smt-ind-RK.pdf). So, I'd expect more inductive capabilities to come to SMT-solvers in the upcoming years. However, tools like Dafny, ACL2, etc. will play a crucial role since coming up with inductive invariants is still an art more than engineering for most software applications; so user-intervention is still the name of the game. But it's reasonable to expect the automated systems to get better over time, as amply demonstrated by the last 50 years of theorem proving literature.