diff --git a/compiler/rustc_smir/src/rustc_smir/convert/mir.rs b/compiler/rustc_smir/src/rustc_smir/convert/mir.rs
index 62a26bc089ad8..e9b835f90db24 100644
--- a/compiler/rustc_smir/src/rustc_smir/convert/mir.rs
+++ b/compiler/rustc_smir/src/rustc_smir/convert/mir.rs
@@ -578,13 +578,13 @@ impl<'tcx> Stable<'tcx> for mir::TerminatorKind<'tcx> {
             }
             mir::TerminatorKind::SwitchInt { discr, targets } => TerminatorKind::SwitchInt {
                 discr: discr.stable(tables),
-                targets: targets
-                    .iter()
-                    .map(|(value, target)| stable_mir::mir::SwitchTarget {
-                        value,
-                        target: target.as_usize(),
-                    })
-                    .collect(),
+                targets: {
+                    let (value_vec, mut target_vec): (Vec<_>, Vec<_>) =
+                        targets.iter().map(|(value, target)| (value, target.as_usize())).unzip();
+                    // We need to push otherwise as last element to ensure it's same as in MIR.
+                    target_vec.push(targets.otherwise().as_usize());
+                    stable_mir::mir::SwitchTargets { value: value_vec, targets: target_vec }
+                },
                 otherwise: targets.otherwise().as_usize(),
             },
             mir::TerminatorKind::UnwindResume => TerminatorKind::Resume,
diff --git a/compiler/stable_mir/src/lib.rs b/compiler/stable_mir/src/lib.rs
index 1f75dfb69cfd9..2099c485c6f8f 100644
--- a/compiler/stable_mir/src/lib.rs
+++ b/compiler/stable_mir/src/lib.rs
@@ -16,7 +16,7 @@
 //!
 //! The goal is to eventually be published on
 //! [crates.io](https://crates.io).
-
+#![feature(type_alias_impl_trait)]
 #[macro_use]
 extern crate scoped_tls;
 
@@ -184,7 +184,7 @@ impl std::fmt::Display for Opaque {
 
 impl std::fmt::Debug for Opaque {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(f, "{:?}", self.0)
+        write!(f, "{}", self.0)
     }
 }
 
diff --git a/compiler/stable_mir/src/mir/body.rs b/compiler/stable_mir/src/mir/body.rs
index 8d237fc9f1d95..02a2868767659 100644
--- a/compiler/stable_mir/src/mir/body.rs
+++ b/compiler/stable_mir/src/mir/body.rs
@@ -1,10 +1,9 @@
-use crate::mir::pretty::{function_body, pretty_statement};
+use crate::mir::pretty::{function_body, pretty_statement, pretty_terminator};
 use crate::ty::{
     AdtDef, ClosureDef, Const, CoroutineDef, GenericArgs, Movability, Region, RigidTy, Ty, TyKind,
 };
 use crate::{Error, Opaque, Span, Symbol};
-use std::io;
-
+use std::{io, slice};
 /// The SMIR representation of a single function.
 #[derive(Clone, Debug)]
 pub struct Body {
@@ -83,6 +82,8 @@ impl Body {
                         Ok(())
                     })
                     .collect::<Vec<_>>();
+                pretty_terminator(&block.terminator.kind, w)?;
+                writeln!(w, "").unwrap();
                 writeln!(w, "    }}").unwrap();
                 Ok(())
             })
@@ -100,7 +101,7 @@ pub struct LocalDecl {
     pub mutability: Mutability,
 }
 
-#[derive(Clone, Debug)]
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct BasicBlock {
     pub statements: Vec<Statement>,
     pub terminator: Terminator,
@@ -112,6 +113,14 @@ pub struct Terminator {
     pub span: Span,
 }
 
+impl Terminator {
+    pub fn successors(&self) -> Successors<'_> {
+        self.kind.successors()
+    }
+}
+
+pub type Successors<'a> = impl Iterator<Item = usize> + 'a;
+
 #[derive(Clone, Debug, Eq, PartialEq)]
 pub enum TerminatorKind {
     Goto {
@@ -119,7 +128,7 @@ pub enum TerminatorKind {
     },
     SwitchInt {
         discr: Operand,
-        targets: Vec<SwitchTarget>,
+        targets: SwitchTargets,
         otherwise: usize,
     },
     Resume,
@@ -156,6 +165,58 @@ pub enum TerminatorKind {
     },
 }
 
+impl TerminatorKind {
+    pub fn successors(&self) -> Successors<'_> {
+        use self::TerminatorKind::*;
+        match *self {
+            Call { target: Some(t), unwind: UnwindAction::Cleanup(ref u), .. }
+            | Drop { target: t, unwind: UnwindAction::Cleanup(ref u), .. }
+            | Assert { target: t, unwind: UnwindAction::Cleanup(ref u), .. }
+            | InlineAsm { destination: Some(t), unwind: UnwindAction::Cleanup(ref u), .. } => {
+                Some(t).into_iter().chain(slice::from_ref(u).into_iter().copied())
+            }
+            Goto { target: t }
+            | Call { target: None, unwind: UnwindAction::Cleanup(t), .. }
+            | Call { target: Some(t), unwind: _, .. }
+            | Drop { target: t, unwind: _, .. }
+            | Assert { target: t, unwind: _, .. }
+            | InlineAsm { destination: None, unwind: UnwindAction::Cleanup(t), .. }
+            | InlineAsm { destination: Some(t), unwind: _, .. } => {
+                Some(t).into_iter().chain((&[]).into_iter().copied())
+            }
+
+            CoroutineDrop
+            | Return
+            | Resume
+            | Abort
+            | Unreachable
+            | Call { target: None, unwind: _, .. }
+            | InlineAsm { destination: None, unwind: _, .. } => {
+                None.into_iter().chain((&[]).into_iter().copied())
+            }
+            SwitchInt { ref targets, .. } => {
+                None.into_iter().chain(targets.targets.iter().copied())
+            }
+        }
+    }
+
+    pub fn unwind(&self) -> Option<&UnwindAction> {
+        match *self {
+            TerminatorKind::Goto { .. }
+            | TerminatorKind::Return
+            | TerminatorKind::Unreachable
+            | TerminatorKind::CoroutineDrop
+            | TerminatorKind::Resume
+            | TerminatorKind::Abort
+            | TerminatorKind::SwitchInt { .. } => None,
+            TerminatorKind::Call { ref unwind, .. }
+            | TerminatorKind::Assert { ref unwind, .. }
+            | TerminatorKind::Drop { ref unwind, .. }
+            | TerminatorKind::InlineAsm { ref unwind, .. } => Some(unwind),
+        }
+    }
+}
+
 #[derive(Clone, Debug, Eq, PartialEq)]
 pub struct InlineAsmOperand {
     pub in_value: Option<Operand>,
@@ -602,9 +663,9 @@ pub struct Constant {
 }
 
 #[derive(Clone, Debug, Eq, PartialEq)]
-pub struct SwitchTarget {
-    pub value: u128,
-    pub target: usize,
+pub struct SwitchTargets {
+    pub value: Vec<u128>,
+    pub targets: Vec<usize>,
 }
 
 #[derive(Copy, Clone, Debug, Eq, PartialEq)]
diff --git a/compiler/stable_mir/src/mir/pretty.rs b/compiler/stable_mir/src/mir/pretty.rs
index e7bca295b5a04..759c3b148dfef 100644
--- a/compiler/stable_mir/src/mir/pretty.rs
+++ b/compiler/stable_mir/src/mir/pretty.rs
@@ -1,7 +1,11 @@
 use crate::crate_def::CrateDef;
-use crate::mir::{Operand, Rvalue, StatementKind};
+use crate::mir::{Operand, Rvalue, StatementKind, UnwindAction};
 use crate::ty::{DynKind, FloatTy, IntTy, RigidTy, TyKind, UintTy};
 use crate::{with, Body, CrateItem, Mutability};
+use std::io::Write;
+use std::{io, iter};
+
+use super::{AssertMessage, BinOp, TerminatorKind};
 
 pub fn function_name(item: CrateItem) -> String {
     let mut pretty_name = String::new();
@@ -70,6 +74,209 @@ pub fn pretty_statement(statement: &StatementKind) -> String {
     pretty
 }
 
+pub fn pretty_terminator<W: io::Write>(terminator: &TerminatorKind, w: &mut W) -> io::Result<()> {
+    write!(w, "{}", pretty_terminator_head(terminator))?;
+    let successor_count = terminator.successors().count();
+    let labels = pretty_successor_labels(terminator);
+
+    let show_unwind = !matches!(terminator.unwind(), None | Some(UnwindAction::Cleanup(_)));
+    let fmt_unwind = |fmt: &mut dyn Write| -> io::Result<()> {
+        write!(fmt, "unwind ")?;
+        match terminator.unwind() {
+            None | Some(UnwindAction::Cleanup(_)) => unreachable!(),
+            Some(UnwindAction::Continue) => write!(fmt, "continue"),
+            Some(UnwindAction::Unreachable) => write!(fmt, "unreachable"),
+            Some(UnwindAction::Terminate) => write!(fmt, "terminate"),
+        }
+    };
+
+    match (successor_count, show_unwind) {
+        (0, false) => Ok(()),
+        (0, true) => {
+            write!(w, " -> ")?;
+            fmt_unwind(w)?;
+            Ok(())
+        }
+        (1, false) => {
+            write!(w, " -> {:?}", terminator.successors().next().unwrap())?;
+            Ok(())
+        }
+        _ => {
+            write!(w, " -> [")?;
+            for (i, target) in terminator.successors().enumerate() {
+                if i > 0 {
+                    write!(w, ", ")?;
+                }
+                write!(w, "{}: bb{:?}", labels[i], target)?;
+            }
+            if show_unwind {
+                write!(w, ", ")?;
+                fmt_unwind(w)?;
+            }
+            write!(w, "]")
+        }
+    }?;
+
+    Ok(())
+}
+
+pub fn pretty_terminator_head(terminator: &TerminatorKind) -> String {
+    use self::TerminatorKind::*;
+    let mut pretty = String::new();
+    match terminator {
+        Goto { .. } => format!("        goto"),
+        SwitchInt { discr, .. } => {
+            format!("        switchInt(_{})", pretty_operand(discr))
+        }
+        Resume => format!("        resume"),
+        Abort => format!("        abort"),
+        Return => format!("        return"),
+        Unreachable => format!("        unreachable"),
+        Drop { place, .. } => format!("        drop(_{:?})", place.local),
+        Call { func, args, destination, .. } => {
+            pretty.push_str("        ");
+            pretty.push_str(format!("_{} = ", destination.local).as_str());
+            pretty.push_str(&pretty_operand(func));
+            pretty.push_str("(");
+            args.iter().enumerate().for_each(|(i, arg)| {
+                if i > 0 {
+                    pretty.push_str(", ");
+                }
+                pretty.push_str(&pretty_operand(arg));
+            });
+            pretty.push_str(")");
+            pretty
+        }
+        Assert { cond, expected, msg, target: _, unwind: _ } => {
+            pretty.push_str("        assert(");
+            if !expected {
+                pretty.push_str("!");
+            }
+            pretty.push_str(format!("{} bool),", &pretty_operand(cond)).as_str());
+            pretty.push_str(&pretty_assert_message(msg));
+            pretty.push_str(")");
+            pretty
+        }
+        CoroutineDrop => format!("        coroutine_drop"),
+        InlineAsm { .. } => todo!(),
+    }
+}
+
+pub fn pretty_successor_labels(terminator: &TerminatorKind) -> Vec<String> {
+    use self::TerminatorKind::*;
+    match terminator {
+        Resume | Abort | Return | Unreachable | CoroutineDrop => vec![],
+        Goto { .. } => vec!["".to_string()],
+        SwitchInt { targets, .. } => targets
+            .value
+            .iter()
+            .map(|target| format!("{}", target))
+            .chain(iter::once("otherwise".into()))
+            .collect(),
+        Drop { unwind: UnwindAction::Cleanup(_), .. } => vec!["return".into(), "unwind".into()],
+        Drop { unwind: _, .. } => vec!["return".into()],
+        Call { target: Some(_), unwind: UnwindAction::Cleanup(_), .. } => {
+            vec!["return".into(), "unwind".into()]
+        }
+        Call { target: Some(_), unwind: _, .. } => vec!["return".into()],
+        Call { target: None, unwind: UnwindAction::Cleanup(_), .. } => vec!["unwind".into()],
+        Call { target: None, unwind: _, .. } => vec![],
+        Assert { unwind: UnwindAction::Cleanup(_), .. } => {
+            vec!["success".into(), "unwind".into()]
+        }
+        Assert { unwind: _, .. } => vec!["success".into()],
+        InlineAsm { .. } => todo!(),
+    }
+}
+
+pub fn pretty_assert_message(msg: &AssertMessage) -> String {
+    let mut pretty = String::new();
+    match msg {
+        AssertMessage::BoundsCheck { len, index } => {
+            let pretty_len = pretty_operand(len);
+            let pretty_index = pretty_operand(index);
+            pretty.push_str(format!("\"index out of bounds: the length is {{}} but the index is {{}}\", {pretty_len}, {pretty_index}").as_str());
+            pretty
+        }
+        AssertMessage::Overflow(BinOp::Add, l, r) => {
+            let pretty_l = pretty_operand(l);
+            let pretty_r = pretty_operand(r);
+            pretty.push_str(format!("\"attempt to compute `{{}} + {{}}`, which would overflow\", {pretty_l}, {pretty_r}").as_str());
+            pretty
+        }
+        AssertMessage::Overflow(BinOp::Sub, l, r) => {
+            let pretty_l = pretty_operand(l);
+            let pretty_r = pretty_operand(r);
+            pretty.push_str(format!("\"attempt to compute `{{}} - {{}}`, which would overflow\", {pretty_l}, {pretty_r}").as_str());
+            pretty
+        }
+        AssertMessage::Overflow(BinOp::Mul, l, r) => {
+            let pretty_l = pretty_operand(l);
+            let pretty_r = pretty_operand(r);
+            pretty.push_str(format!("\"attempt to compute `{{}} * {{}}`, which would overflow\", {pretty_l}, {pretty_r}").as_str());
+            pretty
+        }
+        AssertMessage::Overflow(BinOp::Div, l, r) => {
+            let pretty_l = pretty_operand(l);
+            let pretty_r = pretty_operand(r);
+            pretty.push_str(format!("\"attempt to compute `{{}} / {{}}`, which would overflow\", {pretty_l}, {pretty_r}").as_str());
+            pretty
+        }
+        AssertMessage::Overflow(BinOp::Rem, l, r) => {
+            let pretty_l = pretty_operand(l);
+            let pretty_r = pretty_operand(r);
+            pretty.push_str(format!("\"attempt to compute `{{}} % {{}}`, which would overflow\", {pretty_l}, {pretty_r}").as_str());
+            pretty
+        }
+        AssertMessage::Overflow(BinOp::Shr, _, r) => {
+            let pretty_r = pretty_operand(r);
+            pretty.push_str(
+                format!("\"attempt to shift right by `{{}}`, which would overflow\", {pretty_r}")
+                    .as_str(),
+            );
+            pretty
+        }
+        AssertMessage::Overflow(BinOp::Shl, _, r) => {
+            let pretty_r = pretty_operand(r);
+            pretty.push_str(
+                format!("\"attempt to shift left by `{{}}`, which would overflow\", {pretty_r}")
+                    .as_str(),
+            );
+            pretty
+        }
+        AssertMessage::OverflowNeg(op) => {
+            let pretty_op = pretty_operand(op);
+            pretty.push_str(
+                format!("\"attempt to negate `{{}}`, which would overflow\", {pretty_op}").as_str(),
+            );
+            pretty
+        }
+        AssertMessage::DivisionByZero(op) => {
+            let pretty_op = pretty_operand(op);
+            pretty.push_str(format!("\"attempt to divide `{{}}` by zero\", {pretty_op}").as_str());
+            pretty
+        }
+        AssertMessage::RemainderByZero(op) => {
+            let pretty_op = pretty_operand(op);
+            pretty.push_str(
+                format!("\"attempt to calculate the remainder of `{{}}` with a divisor of zero\", {pretty_op}").as_str(),
+            );
+            pretty
+        }
+        AssertMessage::ResumedAfterReturn(_) => {
+            format!("attempt to resume a generator after completion")
+        }
+        AssertMessage::ResumedAfterPanic(_) => format!("attempt to resume a panicked generator"),
+        AssertMessage::MisalignedPointerDereference { required, found } => {
+            let pretty_required = pretty_operand(required);
+            let pretty_found = pretty_operand(found);
+            pretty.push_str(format!("\"misaligned pointer dereference: address must be a multiple of {{}} but is {{}}\",{pretty_required}, {pretty_found}").as_str());
+            pretty
+        }
+        _ => todo!(),
+    }
+}
+
 pub fn pretty_operand(operand: &Operand) -> String {
     let mut pretty = String::new();
     match operand {