diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml
index 4cca1ef48..4fe2d75a9 100644
--- a/charon-ml/src/CharonVersion.ml
+++ b/charon-ml/src/CharonVersion.ml
@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.1"
+let supported_charon_version = "0.1.2"
diff --git a/charon-ml/src/Expressions.ml b/charon-ml/src/Expressions.ml
index a95cb6bf4..d3d489fa2 100644
--- a/charon-ml/src/Expressions.ml
+++ b/charon-ml/src/Expressions.ml
@@ -101,6 +101,9 @@ type binop =
   | Add
   | Sub
   | Mul
+  | CheckedAdd
+  | CheckedSub
+  | CheckedMul
   | Shl
   | Shr
 [@@deriving show, ord]
diff --git a/charon-ml/src/ExpressionsUtils.ml b/charon-ml/src/ExpressionsUtils.ml
index a30b0e19f..a49da19b1 100644
--- a/charon-ml/src/ExpressionsUtils.ml
+++ b/charon-ml/src/ExpressionsUtils.ml
@@ -5,5 +5,7 @@ let unop_can_fail (unop : unop) : bool =
 
 let binop_can_fail (binop : binop) : bool =
   match binop with
-  | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false
+  | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt | CheckedAdd
+  | CheckedSub | CheckedMul ->
+      false
   | Div | Rem | Add | Sub | Mul | Shl | Shr -> true
diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml
index 961734410..c028dd17c 100644
--- a/charon-ml/src/GAstOfJson.ml
+++ b/charon-ml/src/GAstOfJson.ml
@@ -749,6 +749,9 @@ let binop_of_json (js : json) : (binop, string) result =
   | `String "Add" -> Ok Add
   | `String "Sub" -> Ok Sub
   | `String "Mul" -> Ok Mul
+  | `String "CheckedAdd" -> Ok CheckedAdd
+  | `String "CheckedSub" -> Ok CheckedSub
+  | `String "CheckedMul" -> Ok CheckedMul
   | `String "Shl" -> Ok Shl
   | `String "Shr" -> Ok Shr
   | _ -> Error ("binop_of_json failed on:" ^ show js)
diff --git a/charon-ml/src/PrintExpressions.ml b/charon-ml/src/PrintExpressions.ml
index cccca665d..a4b1b4096 100644
--- a/charon-ml/src/PrintExpressions.ml
+++ b/charon-ml/src/PrintExpressions.ml
@@ -82,6 +82,9 @@ let binop_to_string (binop : binop) : string =
   | Add -> "+"
   | Sub -> "-"
   | Mul -> "*"
+  | CheckedAdd -> "checked.+"
+  | CheckedSub -> "checked.-"
+  | CheckedMul -> "checked.*"
   | Shl -> "<<"
   | Shr -> ">>"
 
diff --git a/charon/Cargo.lock b/charon/Cargo.lock
index 940031b66..3bf7b8bcc 100644
--- a/charon/Cargo.lock
+++ b/charon/Cargo.lock
@@ -160,7 +160,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "charon"
-version = "0.1.1"
+version = "0.1.2"
 dependencies = [
  "anyhow",
  "assert_cmd",
diff --git a/charon/Cargo.toml b/charon/Cargo.toml
index f09d4c63c..8a24b06fd 100644
--- a/charon/Cargo.toml
+++ b/charon/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.1"
+version = "0.1.2"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 
diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs
index 021eb8bd2..adab5040f 100644
--- a/charon/src/ast/expressions.rs
+++ b/charon/src/ast/expressions.rs
@@ -140,19 +140,27 @@ pub enum BinOp {
     Ne,
     Ge,
     Gt,
-    /// Can fail if the divisor is 0.
+    /// Fails if the divisor is 0, or if the operation is `int::MIN / -1`.
     Div,
-    /// Can fail if the divisor is 0.
+    /// Fails if the divisor is 0, or if the operation is `int::MIN % -1`.
     Rem,
-    /// Can overflow
+    /// Fails on overflow.
     Add,
-    /// Can overflow
+    /// Fails on overflow.
     Sub,
-    /// Can overflow
+    /// Fails on overflow.
     Mul,
-    /// Can fail if the shift is too big
+    /// Returns `(result, did_overflow)`, where `result` is the result of the operation with
+    /// wrapping semantics, and `did_overflow` is a boolean that indicates whether the operation
+    /// overflowed. This operation does not fail.
+    CheckedAdd,
+    /// Like `CheckedAdd`.
+    CheckedSub,
+    /// Like `CheckedAdd`.
+    CheckedMul,
+    /// Fails if the shift is bigger than the bit-size of the type.
     Shl,
-    /// Can fail if the shift is too big
+    /// Fails if the shift is bigger than the bit-size of the type.
     Shr,
     // No Offset binary operation: this is an operation on raw pointers
 }
diff --git a/charon/src/driver.rs b/charon/src/driver.rs
index ba44d8ba0..c41593ebd 100644
--- a/charon/src/driver.rs
+++ b/charon/src/driver.rs
@@ -271,6 +271,15 @@ pub fn translate(
     // we simply apply some micro-passes to make the code cleaner, before
     // serializing the result.
 
+    // # Micro-pass: Remove overflow/div-by-zero/bounds checks since they are already part of the
+    // arithmetic/array operation in the semantics of (U)LLBC.
+    // **WARNING**: this pass uses the fact that the dynamic checks introduced by Rustc use a
+    // special "assert" construct. Because of this, it must happen *before* the
+    // [reconstruct_asserts] pass. See the comments in [crate::remove_dynamic_checks].
+    // **WARNING**: this pass relies on a precise structure of the MIR statements. Because of this,
+    // it must happen before passes that insert statements like [simplify_constants].
+    remove_dynamic_checks::transform(&mut ctx);
+
     // # Micro-pass: desugar the constants to other values/operands as much
     // as possible.
     simplify_constants::transform(&mut ctx);
@@ -304,14 +313,6 @@ pub fn translate(
         // which ignores this first variable. This micro-pass updates this.
         update_closure_signatures::transform(&ctx, &mut llbc_funs);
 
-        // # Micro-pass: remove the dynamic checks for array/slice bounds
-        // and division by zero.
-        // **WARNING**: this pass uses the fact that the dynamic checks
-        // introduced by Rustc use a special "assert" construct. Because of
-        // this, it must happen *before* the [reconstruct_asserts] pass.
-        // See the comments in [crate::remove_dynamic_checks].
-        remove_dynamic_checks::transform(&mut ctx, &mut llbc_funs, &mut llbc_globals);
-
         // # Micro-pass: reconstruct the asserts
         reconstruct_asserts::transform(&mut ctx, &mut llbc_funs, &mut llbc_globals);
 
diff --git a/charon/src/lib.rs b/charon/src/lib.rs
index 66989aedb..61936bab3 100644
--- a/charon/src/lib.rs
+++ b/charon/src/lib.rs
@@ -17,6 +17,7 @@
 #![recursion_limit = "256"]
 #![feature(trait_alias)]
 #![feature(let_chains)]
+#![feature(if_let_guard)]
 #![feature(iterator_try_collect)]
 
 extern crate rustc_ast;
diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs
index f339c5549..2c9cfb160 100644
--- a/charon/src/pretty/fmt_with_ctx.rs
+++ b/charon/src/pretty/fmt_with_ctx.rs
@@ -1486,6 +1486,9 @@ impl std::fmt::Display for BinOp {
             BinOp::Add => write!(f, "+"),
             BinOp::Sub => write!(f, "-"),
             BinOp::Mul => write!(f, "*"),
+            BinOp::CheckedAdd => write!(f, "checked.+"),
+            BinOp::CheckedSub => write!(f, "checked.-"),
+            BinOp::CheckedMul => write!(f, "checked.*"),
             BinOp::Shl => write!(f, "<<"),
             BinOp::Shr => write!(f, ">>"),
         }
diff --git a/charon/src/transform/remove_dynamic_checks.rs b/charon/src/transform/remove_dynamic_checks.rs
index f5f885637..79e1289b6 100644
--- a/charon/src/transform/remove_dynamic_checks.rs
+++ b/charon/src/transform/remove_dynamic_checks.rs
@@ -1,346 +1,167 @@
-//! # Micro-pass: remove the dynamic checks for array/slice bounds and division by zero.
+//! # Micro-pass: remove the dynamic checks for array/slice bounds, overflow, and division by zero.
 //! Note that from a semantic point of view, an out-of-bound access or a division by zero
 //! must lead to a panic in Rust (which is why those checks are always present, even when
 //! compiling for release). In our case, we take this into account in the semantics of our
 //! array/slice manipulation and arithmetic functions, on the verification side.
-use crate::formatter::{Formatter, IntoFormatter};
-use crate::llbc_ast::*;
-use crate::translate_ctx::{error_assert_then, TransCtx};
-use crate::types::*;
-use crate::values::*;
-use take_mut::take;
 
-struct RemoveDynChecks<'tcx, 'ctx, 'a> {
-    /// We use the context for debugging and error reporting
-    ctx: &'a mut TransCtx<'tcx, 'ctx>,
-}
+use crate::formatter::{Formatter, IntoFormatter};
+use crate::llbc_ast::{BinOp, FieldProjKind, Operand, ProjectionElem, Rvalue};
+use crate::translate_ctx::{register_error_or_panic, TransCtx};
+use crate::ullbc_ast::{BlockData, RawStatement, RawTerminator, Statement};
 
-impl<'tcx, 'ctx, 'a> MutTypeVisitor for RemoveDynChecks<'tcx, 'ctx, 'a> {}
-impl<'tcx, 'ctx, 'a> MutExprVisitor for RemoveDynChecks<'tcx, 'ctx, 'a> {}
+/// Rustc inserts dybnamic checks during MIR lowering. They all end in an `Assert` terminator (and
+/// this is the only use of this terminator).
+fn remove_dynamic_checks(ctx: &mut TransCtx, block: &mut BlockData) {
+    let RawTerminator::Assert {
+        cond: Operand::Move(cond),
+        expected,
+        target,
+    } = &block.terminator.content else { return };
 
-/// Check that a statement is exactly:
-/// ```text
-/// assert(move p == expected)
-/// ```
-fn is_assert_move(p: &Place, s: &Statement, expected: bool) -> bool {
-    if let RawStatement::Assert(Assert {
-        cond: Operand::Move(ap),
-        expected: aexpected,
-    }) = &s.content
-    {
-        return ap == p && *aexpected == expected;
-    }
-    // Default
-    false
-}
+    // We return the statements we want to keep, which must be a prefix of `block.statements`.
+    let statements_to_keep = match block.statements.as_mut_slice() {
+        // Bounds checks for arrays/slices. They look like:
+        //   l := len(a)
+        //   b := copy x < copy l
+        //   assert(move b == true)
+        [rest @ .., Statement {
+            content: RawStatement::Assign(len, Rvalue::Len(..)),
+            ..
+        }, Statement {
+            content:
+                RawStatement::Assign(
+                    is_in_bounds,
+                    Rvalue::BinaryOp(BinOp::Lt, _, Operand::Copy(lt_op2)),
+                ),
+            ..
+        }] if lt_op2 == len && cond == is_in_bounds && *expected == true => rest,
 
-impl<'tcx, 'ctx, 'a> RemoveDynChecks<'tcx, 'ctx, 'a> {
-    /// Return [true] if we simplified the statements, [false] otherwise.
-    /// TODO: we need a way of simplifying all this...
-    ///
-    /// We simply detect sequences of the following shapes, and remove them:
-    /// # 1. Division/remainder/multiplication
-    /// ======================================
-    /// ```text
-    /// b := copy x == const 0
-    /// assert(move b == false)
-    /// ```
-    ///
-    /// **Special case**: division/remainder for signed integers. Rust checks
-    /// that we don't have, for instance: `i32::min / (-1)`:
-    /// ```text
-    /// b_y := y == const (-1)
-    /// b_x := x == const INT::min
-    /// b := move (b_y) & move (b_x)
-    /// assert(move b == false)
-    /// z := x / y
-    /// ```
-    ///
-    /// # 2. Addition/substraction/multiplication.
-    /// ==========================================
-    /// In release mode, the rust compiler inserts assertions only inside the
-    /// body of global constants.
-    /// ```text
-    /// r := x + y;
-    /// assert(move r.1 == false);
-    /// z := move r.0;
-    /// ```
-    ///
-    /// # 3. Arrays/slices
-    /// ==================
-    /// ```text
-    /// l := len(a)
-    /// b := copy x < copy l
-    /// assert(move b == true)
-    /// ```
-    ///
-    /// # Shifts
-    /// ========
-    /// ```text
-    /// x := ...;
-    /// b := move x < const 32; // or another constant
-    /// assert(move b == true);
-    /// ```
-    fn simplify(&mut self, s: &mut Statement) -> bool {
-        if let RawStatement::Sequence(s0, s1) = &s.content {
-            if let RawStatement::Sequence(s1, s2) = &s1.content {
-                // Arrays/Slices
-                if let (
-                    // s0 should be: `l := len(a)`
-                    RawStatement::Assign(dest_l_p, Rvalue::Len(..)),
-                    // s1 should be: `b := copy x < copy l`
-                    RawStatement::Assign(
-                        dest_b_p,
-                        Rvalue::BinaryOp(BinOp::Lt, _, Operand::Copy(l_op_place)),
-                    ),
-                    // s2
-                    RawStatement::Sequence(s2, _),
-                ) = (&s0.content, &s1.content, &s2.content)
-                {
-                    // s2 should be: `assert(move b == true)`
-                    if dest_l_p == l_op_place && is_assert_move(dest_b_p, s2, true) {
-                        // Eliminate the first three statements
-                        take(s, |s| {
-                            let (_, s1) = s.content.to_sequence();
-                            let (_, s2) = s1.content.to_sequence();
-                            let (_, s3) = s2.content.to_sequence();
-                            *s3
-                        });
-                        // A simplification happened
-                        return true;
-                    }
-                }
-                // Shift left
-                else if let (
-                    // s0 should be an assignment
-                    RawStatement::Assign(dest_x_p, _),
-                    // s1 should be: `b := copy x < const ...`
-                    RawStatement::Assign(
-                        dest_b_p,
-                        Rvalue::BinaryOp(BinOp::Lt, Operand::Move(x_place), Operand::Const(..)),
-                    ),
-                    RawStatement::Sequence(s2, _),
-                ) = (&s0.content, &s1.content, &s2.content)
-                {
-                    // s2 should be: `assert(move b == true)`
-                    if dest_x_p == x_place && is_assert_move(dest_b_p, s2, true) {
-                        // Eliminate the first three statements
-                        take(s, |s| {
-                            let (_, s1) = s.content.to_sequence();
-                            let (_, s2) = s1.content.to_sequence();
-                            let (_, s3) = s2.content.to_sequence();
-                            *s3
-                        });
-                        // A simplification happened
-                        return true;
-                    }
-                }
-                // Overflow checks for signed division and remainder. They look like:
-                //   is_neg_1 := y == (-1)
-                //   is_min := x == INT::min
-                //   has_overflow := move (is_neg_1) & move (is_min)
-                //   assert(move has_overflow == false)
-                // TODO: check `_minus_1` and `_min_op`.
-                else if let (
-                    // is_neg_1 := y == -1
-                    RawStatement::Assign(
-                        is_neg_1,
-                        Rvalue::BinaryOp(
-                            BinOp::Eq,
-                            _y_op,
-                            Operand::Const(ConstantExpr {
-                                value: RawConstantExpr::Literal(Literal::Scalar(_minus_1)),
-                                ty: _,
-                            }),
-                        ),
-                    ),
-                    // is_min := x == INT::min
-                    RawStatement::Assign(is_min, Rvalue::BinaryOp(BinOp::Eq, _x_op, _min_op)),
-                    // s2
-                    // s3
-                    RawStatement::Sequence(s2, s3),
-                ) = (&s0.content, &s1.content, &s2.content)
-                {
-                    if let RawStatement::Sequence(s3, _) = &s3.content {
-                        if let (
-                            // has_overflow := move (is_neg_1) & move (is_min)
-                            RawStatement::Assign(
-                                has_overflow,
-                                Rvalue::BinaryOp(
-                                    BinOp::BitAnd,
-                                    Operand::Move(has_overflow_op_1),
-                                    Operand::Move(has_overflow_op_2),
-                                ),
-                            ),
-                            // assert(move b == false)
-                            RawStatement::Assert(Assert {
-                                cond: Operand::Move(asserted),
-                                expected: false,
-                            }),
-                        ) = (&s2.content, &s3.content)
-                        {
-                            if is_neg_1 == has_overflow_op_1
-                                && is_min == has_overflow_op_2
-                                && asserted == has_overflow
-                            {
-                                // Eliminate the first 4 statements
-                                take(s, |s| {
-                                    let (_, s1) = s.content.to_sequence();
-                                    let (_, s2) = s1.content.to_sequence();
-                                    let (_, s3) = s2.content.to_sequence();
-                                    let (_, s4) = s3.content.to_sequence();
-                                    *s4
-                                });
-                                return true;
-                            }
-                        }
-                    }
-                }
-                // Division/remainder/addition/etc.
-                else if let RawStatement::Assign(dest_p, Rvalue::BinaryOp(binop, _, _)) =
-                    &s0.content
-                {
-                    // We don't check that the second operand is 0 in
-                    // case we are in the division/remainder case
-                    if matches!(binop, BinOp::Eq | BinOp::BitAnd)
-                        && is_assert_move(dest_p, s1, false)
-                    {
-                        // This should be the division/remainder case
-                        // Eliminate the first two statements
-                        take(s, |s| {
-                            let (_, s1) = s.content.to_sequence();
-                            let (_, s2) = s1.content.to_sequence();
-                            *s2
-                        });
-                        // We performed a change
-                        return true;
-                    } else if let (
-                        RawStatement::Assert(Assert {
-                            cond: Operand::Move(move_p),
-                            ..
-                        }),
-                        RawStatement::Sequence(s2, _),
-                    ) = (&s1.content, &s2.content)
-                    {
-                        // TODO: the last statement is not necessarily a sequence
-                        // This should be the addition/subtraction/etc. case
-                        error_assert_then!(
-                            self.ctx,
-                            s0.meta.span,
-                            matches!(binop, BinOp::Add | BinOp::Sub | BinOp::Mul),
-                            // TODO: we could replace the whole statement with an "ERROR" statement
-                            // A simplification should have happened but was missed:
-                            // stop the simplification here.
-                            return true,
-                            format!(
-                                "Unexpected binop while removing dynamic checks: {:?}",
-                                binop
-                            )
-                        );
+        // Zero checks for division and remainder. They look like:
+        //   b := copy x == const 0
+        //   assert(move b == false)
+        [rest @ .., Statement {
+            content: RawStatement::Assign(is_zero, Rvalue::BinaryOp(BinOp::Eq, _, Operand::Const(_zero))),
+            ..
+        }] if cond == is_zero && *expected == false => rest,
 
-                        if let RawStatement::Assign(_, Rvalue::Use(Operand::Move(move_p1))) =
-                            &s2.content
-                        {
-                            // move_p should be: r.1
-                            // move_p1 should be: r.0
-                            if move_p.var_id == move_p1.var_id
-                                && move_p.projection.len() == 1
-                                && move_p1.projection.len() == 1
-                            {
-                                if let (
-                                    ProjectionElem::Field(FieldProjKind::Tuple(..), fid0),
-                                    ProjectionElem::Field(FieldProjKind::Tuple(..), fid1),
-                                ) = (&move_p.projection[0], &move_p1.projection[0])
-                                {
-                                    if fid0.index() == 1 && fid1.index() == 0 {
-                                        // Collapse into one assignment
-                                        take(s, |s| {
-                                            let (s0, s1) = s.content.to_sequence();
-                                            let (_, s2) = s1.content.to_sequence();
-                                            let (s2, s3) = s2.content.to_sequence();
-                                            let (_, op) = s0.content.to_assign();
-                                            let (dest, _) = s2.content.to_assign();
-                                            let meta0 = s0.meta;
-                                            let s0 = RawStatement::Assign(dest, op);
-                                            let s0 = Statement {
-                                                meta: meta0,
-                                                content: s0,
-                                            };
-                                            Statement {
-                                                meta: s2.meta,
-                                                content: RawStatement::Sequence(Box::new(s0), s3),
-                                            }
-                                        });
-                                        // A simplification happened
-                                        return true;
-                                    }
-                                }
-                            }
-                        }
-                    }
-                }
-            }
-        };
-
-        // No simplification
-        false
-    }
-}
+        // Overflow checks for signed division and remainder. They look like:
+        //   is_neg_1 := y == (-1)
+        //   is_min := x == INT::min
+        //   has_overflow := move (is_neg_1) & move (is_min)
+        //   assert(move has_overflow == false)
+        [rest @ .., Statement {
+            content: RawStatement::Assign(is_neg_1, Rvalue::BinaryOp(BinOp::Eq, _y_op, _minus_1)),
+            ..
+        }, Statement {
+            content: RawStatement::Assign(is_min, Rvalue::BinaryOp(BinOp::Eq, _x_op, _int_min)),
+            ..
+        }, Statement {
+            content:
+                RawStatement::Assign(
+                    has_overflow,
+                    Rvalue::BinaryOp(BinOp::BitAnd, Operand::Move(and_op1), Operand::Move(and_op2)),
+                ),
+            ..
+        }] if and_op1 == is_neg_1
+            && and_op2 == is_min
+            && cond == has_overflow
+            && *expected == false =>
+        {
+            rest
+        }
 
-impl<'tcx, 'ctx, 'a> MutAstVisitor for RemoveDynChecks<'tcx, 'ctx, 'a> {
-    fn spawn(&mut self, visitor: &mut dyn FnMut(&mut Self)) {
-        visitor(self)
-    }
+        // Overflow checks for right/left shift. They can look like:
+        //   x := ...;
+        //   b := move x < const 32; // or another constant
+        //   assert(move b == true);
+        [rest @ .., Statement {
+            content: RawStatement::Assign(x, _),
+            ..
+        }, Statement {
+            content:
+                RawStatement::Assign(
+                    has_overflow,
+                    Rvalue::BinaryOp(BinOp::Lt, Operand::Move(lt_op2), Operand::Const(..)),
+                ),
+            ..
+        }] if lt_op2 == x && cond == has_overflow && *expected == true => rest,
+        // They can also look like:
+        //   b := const c < const 32; // or another constant
+        //   assert(move b == true);
+        [rest @ .., Statement {
+            content:
+                RawStatement::Assign(
+                    has_overflow,
+                    Rvalue::BinaryOp(BinOp::Lt, Operand::Const(..), Operand::Const(..)),
+                ),
+            ..
+        }] if cond == has_overflow && *expected == true => rest,
 
-    fn merge(&mut self) {}
+        // Overflow checks for addition/subtraction/multiplication. They look like:
+        //   r := x checked.+ y;
+        //   assert(move r.1 == false);
+        // They only happen in constants because we compile with `-C opt-level=3`. They're tricky
+        // to remove so we leave them for now.
+        [.., Statement {
+            content:
+                RawStatement::Assign(result, Rvalue::BinaryOp(BinOp::CheckedAdd | BinOp::CheckedSub | BinOp::CheckedMul, ..)),
+            ..
+        }] if cond.var_id == result.var_id
+            && result.projection.is_empty()
+            && let [ProjectionElem::Field(FieldProjKind::Tuple(2), p_id)] = cond.projection.as_slice()
+            && p_id.index() == 1
+            && *expected == false =>
+        {
+            // We leave this assert intact.
+            return
+        }
 
-    fn visit_statement(&mut self, s: &mut Statement) {
-        // Simplify
-        if self.simplify(s) {
-            // A simplification happened: visit again the updated statement
-            self.visit_statement(s)
-        } else {
-            // No simplification: dive in.
-            // Make sure we eliminated all the asserts and all the `len`
-            error_assert_then!(
-                self.ctx,
-                s.meta.span,
-                !s.content.is_assert(),
-                // Return so as to stop the exploration
-                return,
-                "Found an assert which was not simplified"
+        _ => {
+            // This can happen for the dynamic checks we don't handle, corresponding to the
+            // `rustc_middle::mir::AssertKind` variants `ResumedAfterReturn`, `ResumedAfterPanic`
+            // and `MisalignedPointerDereference`.
+            let fmt_ctx = ctx.into_fmt();
+            let msg = format!("Found an `assert` we don't recognize:\n{}", block.fmt_with_ctx("", &fmt_ctx));
+            register_error_or_panic!(
+                ctx,
+                block.terminator.meta.span,
+                msg
             );
-            if s.content.is_assign() {
-                let (_, rv) = s.content.as_assign();
-                error_assert_then!(
-                    self.ctx,
-                    s.meta.span,
-                    !rv.is_len(),
-                    // Return so as to stop the exploration
-                    return,
-                    "Found an occurrence of Len which was not simplified"
-                );
-            }
-            self.default_visit_raw_statement(&mut s.content);
+            return
         }
-    }
+    };
+
+    // Remove the statements and replace the assert with a goto.
+    let len = statements_to_keep.len();
+    block.statements.truncate(len);
+    block.terminator.content = RawTerminator::Goto { target: *target };
 }
 
-pub fn transform(ctx: &mut TransCtx, funs: &mut FunDecls, globals: &mut GlobalDecls) {
-    ctx.iter_bodies(funs, globals, |ctx, name, b| {
+pub fn transform(ctx: &mut TransCtx) {
+    // Slightly annoying: we have to clone because of borrowing issues
+    let mut fun_decls = ctx.fun_decls.clone();
+    let mut global_decls = ctx.global_decls.clone();
+
+    ctx.iter_bodies(&mut fun_decls, &mut global_decls, |ctx, name, b| {
         let fmt_ctx = ctx.into_fmt();
         trace!(
             "# About to remove the dynamic checks: {}:\n{}",
             name.fmt_with_ctx(&fmt_ctx),
             fmt_ctx.format_object(&*b)
         );
-        let mut visitor = RemoveDynChecks { ctx };
-        visitor.visit_statement(&mut b.body);
+
+        for block in b.body.iter_mut() {
+            remove_dynamic_checks(ctx, block);
+        }
+
         let fmt_ctx = ctx.into_fmt();
         trace!(
             "# After we removed the dynamic checks: {}:\n{}",
             name.fmt_with_ctx(&fmt_ctx),
             fmt_ctx.format_object(&*b)
         );
-    })
+    });
+
+    ctx.fun_decls = fun_decls;
+    ctx.global_decls = global_decls;
 }
diff --git a/charon/src/translate/translate_ctx.rs b/charon/src/translate/translate_ctx.rs
index 27a0902dd..73f60cde4 100644
--- a/charon/src/translate/translate_ctx.rs
+++ b/charon/src/translate/translate_ctx.rs
@@ -65,24 +65,6 @@ macro_rules! error_assert {
 }
 pub(crate) use error_assert;
 
-/// Custom assert to either panic or return an error
-macro_rules! error_assert_then {
-    ($ctx:expr, $span: expr, $b: expr, $then: expr) => {
-        if !$b {
-            let msg = format!("assertion failure: {:?}", stringify!($b));
-            $crate::translate_ctx::register_error_or_panic!($ctx, $span, msg);
-            $then;
-        }
-    };
-    ($ctx:expr, $span: expr, $b: expr, $then: expr, $msg:expr) => {
-        if !$b {
-            $crate::translate_ctx::register_error_or_panic!($ctx, $span, $msg);
-            $then;
-        }
-    };
-}
-pub(crate) use error_assert_then;
-
 /// We use this to save the origin of an id. This is useful for the external
 /// dependencies, especially if some external dependencies don't extract:
 /// we use this information to tell the user what is the code which
diff --git a/charon/src/translate/translate_functions_to_ullbc.rs b/charon/src/translate/translate_functions_to_ullbc.rs
index d08fe7027..7b67cb584 100644
--- a/charon/src/translate/translate_functions_to_ullbc.rs
+++ b/charon/src/translate/translate_functions_to_ullbc.rs
@@ -685,9 +685,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     }
                 }
             }
-            hax::Rvalue::BinaryOp(binop, operands)
-            | hax::Rvalue::CheckedBinaryOp(binop, operands) => {
-                // We merge checked and unchecked binary operations
+            hax::Rvalue::BinaryOp(binop, operands) => {
                 let (left, right) = operands.deref();
                 Ok(Rvalue::BinaryOp(
                     self.t_ctx.translate_binaryop_kind(span, *binop)?,
@@ -695,6 +693,22 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     self.translate_operand(span, right)?,
                 ))
             }
+            hax::Rvalue::CheckedBinaryOp(binop, operands) => {
+                let binop = match binop {
+                    hax::BinOp::Add => BinOp::CheckedAdd,
+                    hax::BinOp::Sub => BinOp::CheckedSub,
+                    hax::BinOp::Mul => BinOp::CheckedMul,
+                    _ => {
+                        error_or_panic!(self, span, "Only Add, Sub and Mul are supported as checked binary operations, found {binop:?}");
+                    }
+                };
+                let (left, right) = operands.deref();
+                Ok(Rvalue::BinaryOp(
+                    binop,
+                    self.translate_operand(span, left)?,
+                    self.translate_operand(span, right)?,
+                ))
+            }
             hax::Rvalue::NullaryOp(nullop, _ty) => {
                 trace!("NullOp: {:?}", nullop);
                 // Nullary operations are very low-level and shouldn't be necessary
diff --git a/charon/tests/ui/binop-simplifications.out b/charon/tests/ui/remove-dynamic-checks.out
similarity index 69%
rename from charon/tests/ui/binop-simplifications.out
rename to charon/tests/ui/remove-dynamic-checks.out
index daf4afb95..babd9b942 100644
--- a/charon/tests/ui/binop-simplifications.out
+++ b/charon/tests/ui/remove-dynamic-checks.out
@@ -28,6 +28,19 @@ fn test_crate::add_u32(@1: u32, @2: u32) -> u32
     return
 }
 
+fn test_crate::incr<'_0>(@1: &'_0 mut (u32))
+{
+    let @0: (); // return
+    let x@1: &'_ mut (u32); // arg #1
+    let @2: (); // anonymous local
+
+    *(x@1) := copy (*(x@1)) + const (1 : u32)
+    @2 := ()
+    @0 := move (@2)
+    @0 := ()
+    return
+}
+
 fn test_crate::subs_u32(@1: u32, @2: u32) -> u32
 {
     let @0: u32; // return
@@ -326,17 +339,179 @@ fn test_crate::mix_arith_i32(@1: i32, @2: i32, @3: i32) -> i32
     return
 }
 
-global test_crate::CONST0  {
-    let @0: usize; // return
+fn test_crate::shl(@1: u32, @2: u32) -> u32
+{
+    let @0: u32; // return
+    let x@1: u32; // arg #1
+    let y@2: u32; // arg #2
+    let @3: u32; // anonymous local
+    let @4: u32; // anonymous local
+
+    @3 := copy (x@1)
+    @4 := copy (y@2)
+    @0 := move (@3) << move (@4)
+    drop @4
+    drop @3
+    return
+}
+
+fn test_crate::shr(@1: u32, @2: u32) -> u32
+{
+    let @0: u32; // return
+    let x@1: u32; // arg #1
+    let y@2: u32; // arg #2
+    let @3: u32; // anonymous local
+    let @4: u32; // anonymous local
+
+    @3 := copy (x@1)
+    @4 := copy (y@2)
+    @0 := move (@3) >> move (@4)
+    drop @4
+    drop @3
+    return
+}
+
+global test_crate::_  {
+    let @0: isize; // return
+    let @1: (isize, bool); // anonymous local
+
+    @1 := const (1 : isize) checked.+ const (1 : isize)
+    assert(move ((@1).1) == false)
+    @0 := move ((@1).0)
+    return
+}
+
+global test_crate::_#1  {
+    let @0: isize; // return
+    let @1: (isize, bool); // anonymous local
+
+    @1 := const (1 : isize) checked.- const (1 : isize)
+    assert(move ((@1).1) == false)
+    @0 := move ((@1).0)
+    return
+}
+
+global test_crate::_#2  {
+    let @0: isize; // return
+
+    @0 := const (-1 : isize)
+    return
+}
+
+global test_crate::_#3  {
+    let @0: isize; // return
+    let @1: (isize, bool); // anonymous local
+
+    @1 := const (2 : isize) checked.* const (2 : isize)
+    assert(move ((@1).1) == false)
+    @0 := move ((@1).0)
+    return
+}
+
+global test_crate::_#4  {
+    let @0: isize; // return
+
+    @0 := const (2 : isize) >> const (2 : i32)
+    return
+}
+
+global test_crate::_#5  {
+    let @0: isize; // return
+
+    @0 := const (2 : isize) << const (2 : i32)
+    return
+}
+
+global test_crate::_#6  {
+    let @0: isize; // return
+
+    @0 := const (2 : isize) % const (2 : isize)
+    return
+}
+
+global test_crate::_#7  {
+    let @0: isize; // return
+
+    @0 := const (2 : isize) / const (2 : isize)
+    return
+}
+
+global test_crate::FOO  {
+    let @0: u32; // return
+
+    @0 := const (10 : u32)
+    return
+}
+
+global test_crate::_#8  {
+    let @0: u32; // return
+    let @1: (u32, bool); // anonymous local
+    let @2: u32; // anonymous local
+
+    @2 := test_crate::FOO
+    @1 := const (1 : u32) checked.+ move (@2)
+    assert(move ((@1).1) == false)
+    @0 := move ((@1).0)
+    return
+}
+
+global test_crate::_#9  {
+    let @0: u32; // return
+    let @1: (u32, bool); // anonymous local
+    let @2: u32; // anonymous local
+
+    @2 := test_crate::FOO
+    @1 := const (1 : u32) checked.- move (@2)
+    assert(move ((@1).1) == false)
+    @0 := move ((@1).0)
+    return
+}
+
+global test_crate::_#10  {
+    let @0: u32; // return
+    let @1: (u32, bool); // anonymous local
+    let @2: u32; // anonymous local
+
+    @2 := test_crate::FOO
+    @1 := const (2 : u32) checked.* move (@2)
+    assert(move ((@1).1) == false)
+    @0 := move ((@1).0)
+    return
+}
+
+global test_crate::_#11  {
+    let @0: u32; // return
+    let @1: u32; // anonymous local
 
-    @0 := const (1 : usize) + const (1 : usize)
+    @1 := test_crate::FOO
+    @0 := const (2 : u32) >> move (@1)
     return
 }
 
-global test_crate::CONST1  {
-    let @0: usize; // return
+global test_crate::_#12  {
+    let @0: u32; // return
+    let @1: u32; // anonymous local
 
-    @0 := const (2 : usize) * const (2 : usize)
+    @1 := test_crate::FOO
+    @0 := const (2 : u32) << move (@1)
+    return
+}
+
+global test_crate::_#13  {
+    let @0: u32; // return
+    let @1: u32; // anonymous local
+
+    @1 := test_crate::FOO
+    @0 := const (2 : u32) % move (@1)
+    return
+}
+
+global test_crate::_#14  {
+    let @0: u32; // return
+    let @1: u32; // anonymous local
+
+    @1 := test_crate::FOO
+    @0 := const (2 : u32) / move (@1)
     return
 }
 
@@ -350,16 +525,10 @@ global test_crate::div_signed_with_constant::FOO  {
 fn test_crate::div_signed_with_constant() -> i32
 {
     let @0: i32; // return
-    let @1: bool; // anonymous local
-    let @2: bool; // anonymous local
-    let @3: i32; // anonymous local
-    let @4: i32; // anonymous local
+    let @1: i32; // anonymous local
 
-    @1 := const (2 : i32) == const (-1 : i32)
-    @3 := test_crate::div_signed_with_constant::FOO
-    @2 := move (@3) == const (-2147483648 : i32)
-    @4 := test_crate::div_signed_with_constant::FOO
-    @0 := move (@4) / const (2 : i32)
+    @1 := test_crate::div_signed_with_constant::FOO
+    @0 := move (@1) / const (2 : i32)
     return
 }
 
diff --git a/charon/tests/ui/binop-simplifications.rs b/charon/tests/ui/remove-dynamic-checks.rs
similarity index 67%
rename from charon/tests/ui/binop-simplifications.rs
rename to charon/tests/ui/remove-dynamic-checks.rs
index a031a2777..5ae953cfb 100644
--- a/charon/tests/ui/binop-simplifications.rs
+++ b/charon/tests/ui/remove-dynamic-checks.rs
@@ -12,6 +12,10 @@ pub fn add_u32(x: u32, y: u32) -> u32 {
     x + y
 }
 
+pub fn incr(x: &mut u32) {
+    *x += 1;
+}
+
 /// Testing binop simplification
 /// In debug mode, rust inserts an assertion after the substraction
 pub fn subs_u32(x: u32, y: u32) -> u32 {
@@ -74,13 +78,35 @@ pub fn mix_arith_i32(x: i32, y: i32, z: i32) -> i32 {
     ((x + y) * (x / y) + (x - (z % y))) % (x + y + z)
 }
 
-/* Checking the simplification of binop operations *inside* global constants.
+fn shl(x: u32, y: u32) -> u32 {
+    x << y
+}
+
+fn shr(x: u32, y: u32) -> u32 {
+    x >> y
+}
+
+// Checking the simplification of binop operations *inside* global constants.
+// Even in release mode, rustc inserts additional checks inside constant bodies.
+pub const _: isize = 1 + 1;
+pub const _: isize = 1 - 1;
+pub const _: isize = -1;
+pub const _: isize = 2 * 2;
+pub const _: isize = 2 >> 2;
+pub const _: isize = 2 << 2;
+pub const _: isize = 2 % 2;
+pub const _: isize = 2 / 2;
 
-   In release mode, the Rust compiler inserts additional checks inside constant
-   bodies.
-*/
-pub const CONST0: usize = 1 + 1;
-pub const CONST1: usize = 2 * 2;
+// When the operand is a bare const it sometimes gets inlined, which trips up our simplification
+// pass. I used `u32` here because other types use a `cast` and thus aren't inlined.
+pub const FOO: u32 = 10;
+pub const _: u32 = 1 + FOO;
+pub const _: u32 = 1 - FOO;
+pub const _: u32 = 2 * FOO;
+pub const _: u32 = 2 >> FOO;
+pub const _: u32 = 2 << FOO;
+pub const _: u32 = 2 % FOO;
+pub const _: u32 = 2 / FOO;
 
 fn div_signed_with_constant() -> i32 {
     const FOO: i32 = 42;
diff --git a/charon/tests/ui/unsupported/foreign-constant-aux.rs b/charon/tests/ui/unsupported/foreign-constant-aux.rs
new file mode 100644
index 000000000..cc81d65ec
--- /dev/null
+++ b/charon/tests/ui/unsupported/foreign-constant-aux.rs
@@ -0,0 +1,2 @@
+//@ skip
+pub const CONSTANT: u8 = 16;
diff --git a/charon/tests/ui/unsupported/foreign-constant.out b/charon/tests/ui/unsupported/foreign-constant.out
new file mode 100644
index 000000000..a8db4b184
--- /dev/null
+++ b/charon/tests/ui/unsupported/foreign-constant.out
@@ -0,0 +1,11 @@
+thread 'rustc' panicked at 'foreign_constant_aux does not have a "explicit_predicates_of"', compiler/rustc_metadata/src/rmeta/decoder/cstore_impl.rs:205:1
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+error: Thread panicked when extracting body.
+ --> tests/ui/unsupported/foreign-constant.rs:4:1
+  |
+4 | const _: i32 = 1 << CONSTANT;
+  | ^^^^^^^^^^^^
+
+error: aborting due to previous error
+
+[ ERROR charon_driver:200] The extraction encountered 1 errors
diff --git a/charon/tests/ui/unsupported/foreign-constant.rs b/charon/tests/ui/unsupported/foreign-constant.rs
new file mode 100644
index 000000000..6b2543517
--- /dev/null
+++ b/charon/tests/ui/unsupported/foreign-constant.rs
@@ -0,0 +1,4 @@
+//@ known-failure
+//@ aux-crate=foreign-constant-aux.rs
+use foreign_constant_aux::CONSTANT;
+const _: i32 = 1 << CONSTANT;
diff --git a/charon/tests/version/example.out b/charon/tests/version/example.out
index 6c5bc532c..4821ff9ee 100644
--- a/charon/tests/version/example.out
+++ b/charon/tests/version/example.out
@@ -1 +1 @@
-{"charon_version":"0.1.1","name":"example","id_to_file":[[{"LocalId":0},{"Local":"tests/version/example.rs"}],[{"VirtualId":0},{"Virtual":"/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/clone.rs"}],[{"VirtualId":1},{"Virtual":"/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/default.rs"}],[{"VirtualId":2},{"Virtual":"/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs"}],[{"VirtualId":3},{"Virtual":"/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/str/mod.rs"}],[{"VirtualId":4},{"Virtual":"/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs"}]],"declarations":[{"Type":{"NonRec":0}},{"TraitDecl":{"NonRec":1}},{"TraitDecl":{"NonRec":0}},{"Fun":{"NonRec":0}},{"TraitImpl":{"NonRec":1}},{"TraitImpl":{"NonRec":0}},{"TraitDecl":{"NonRec":3}},{"TraitDecl":{"NonRec":2}},{"Fun":{"NonRec":6}},{"TraitImpl":{"NonRec":3}},{"Fun":{"NonRec":1}},{"TraitImpl":{"NonRec":2}},{"Global":{"NonRec":0}},{"Global":{"NonRec":1}},{"Type":{"NonRec":1}},{"Fun":{"NonRec":3}},{"Fun":{"NonRec":2}},{"Fun":{"NonRec":4}},{"Fun":{"NonRec":5}}],"types":[{"def_id":0,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":4,"col":0},"end":{"line":4,"col":8}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"is_local":true,"name":[{"Ident":["example",0]},{"Ident":["Foo",0]}],"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Enum":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":5,"col":4},"end":{"line":5,"col":5}},"generated_from_span":null},"name":"A","fields":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":5,"col":6},"end":{"line":5,"col":9}},"generated_from_span":null},"name":null,"ty":{"Literal":{"Integer":"U32"}}}],"discriminant":{"Isize":"0"}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":6,"col":4},"end":{"line":6,"col":5}},"generated_from_span":null},"name":"B","fields":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":6,"col":8},"end":{"line":6,"col":19}},"generated_from_span":null},"name":"field","ty":{"Literal":"Bool"}}],"discriminant":{"Isize":"1"}}]}},{"def_id":1,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":4},"beg":{"line":563,"col":0},"end":{"line":563,"col":18}},"generated_from_span":null},"attributes":[],"inline":null,"public":true},"is_local":false,"name":[{"Ident":["core",0]},{"Ident":["option",0]},{"Ident":["Option",0]}],"generics":{"regions":[],"types":[{"index":0,"name":"T"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Enum":[{"meta":{"span":{"file_id":{"VirtualId":4},"beg":{"line":567,"col":4},"end":{"line":567,"col":8}},"generated_from_span":null},"name":"None","fields":[],"discriminant":{"Isize":"0"}},{"meta":{"span":{"file_id":{"VirtualId":4},"beg":{"line":571,"col":4},"end":{"line":571,"col":8}},"generated_from_span":null},"name":"Some","fields":[{"meta":{"span":{"file_id":{"VirtualId":4},"beg":{"line":571,"col":55},"end":{"line":571,"col":56}},"generated_from_span":null},"name":null,"ty":{"TypeVar":0}}],"discriminant":{"Isize":"1"}}]}}],"functions":[{"def_id":0,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":15},"end":{"line":3,"col":20}},"generated_from_span":null},"attributes":["inline"],"inline":"Hint","public":true},"is_local":true,"name":[{"Ident":["example",0]},{"Impl":{"disambiguator":2,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":1,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}}},{"Ident":["clone",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[{"index":0,"name":null}],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":{"num_region_params":0,"num_type_params":0,"num_const_generic_params":0,"num_trait_clauses":0,"num_regions_outlive":0,"num_types_outlive":0,"num_trait_type_constraints":0},"inputs":[{"Ref":[{"BVar":[0,0]},{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}],"output":{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},"kind":{"TraitItemImpl":{"impl_id":1,"trait_id":1,"item_name":"clone","provided":false}},"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":15},"end":{"line":3,"col":20}},"generated_from_span":null},"arg_count":1,"locals":[{"index":0,"name":null,"ty":{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},{"index":1,"name":"self","ty":{"Ref":["Erased",{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}}],"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":15},"end":{"line":3,"col":20}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":15},"end":{"line":3,"col":20}},"generated_from_span":null},"content":{"Assign":[{"var_id":0,"projection":[]},{"Use":{"Copy":{"var_id":1,"projection":["Deref"]}}}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":15},"end":{"line":3,"col":20}},"generated_from_span":null},"content":"Return"}]}}}},{"def_id":1,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":18,"col":4},"end":{"line":18,"col":23}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"is_local":true,"name":[{"Ident":["example",0]},{"Impl":{"disambiguator":0,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":2,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}}},{"Ident":["method",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":{"num_region_params":0,"num_type_params":0,"num_const_generic_params":0,"num_trait_clauses":0,"num_regions_outlive":0,"num_types_outlive":0,"num_trait_type_constraints":0},"inputs":[],"output":{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},"kind":{"TraitItemImpl":{"impl_id":2,"trait_id":2,"item_name":"method","provided":false}},"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":18,"col":4},"end":{"line":20,"col":5}},"generated_from_span":null},"arg_count":0,"locals":[{"index":0,"name":null,"ty":{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}}],"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":18,"col":4},"end":{"line":20,"col":5}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":18,"col":4},"end":{"line":20,"col":5}},"generated_from_span":null},"content":{"Assign":[{"var_id":0,"projection":[]},{"Aggregate":[{"Adt":[{"Adt":0},0,{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},[{"Const":{"value":{"Literal":{"Scalar":{"U32":"42"}}},"ty":{"Literal":{"Integer":"U32"}}}}]]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":18,"col":4},"end":{"line":20,"col":5}},"generated_from_span":null},"content":"Return"}]}}}},{"def_id":2,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":27,"col":9}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"is_local":true,"name":[{"Ident":["example",0]},{"Ident":["main",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":null,"inputs":[],"output":{"Adt":["Tuple",{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},"kind":"Regular","body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"arg_count":0,"locals":[{"index":0,"name":null,"ty":{"Adt":["Tuple",{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},{"index":1,"name":"foo","ty":{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},{"index":2,"name":null,"ty":{"Adt":[{"Adt":1},{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}]}},{"index":3,"name":null,"ty":{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},{"index":4,"name":null,"ty":{"Adt":["Tuple",{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}}],"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Call":{"func":{"Regular":{"func":{"Trait":[{"trait_id":{"TraitImpl":2},"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"trait_decl_ref":{"trait_id":2,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}},"method",3]},"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}}},"args":[],"dest":{"var_id":1,"projection":[]}}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"FakeRead":{"var_id":1,"projection":[]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Assign":[{"var_id":3,"projection":[]},{"Use":{"Copy":{"var_id":1,"projection":[]}}}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Assign":[{"var_id":2,"projection":[]},{"Aggregate":[{"Adt":[{"Adt":1},1,{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}]},[{"Move":{"var_id":3,"projection":[]}}]]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Drop":{"var_id":3,"projection":[]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"FakeRead":{"var_id":2,"projection":[]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Switch":{"Match":[{"var_id":2,"projection":[]},[[[1],{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Switch":{"Match":[{"var_id":2,"projection":[{"Field":[{"ProjAdt":[1,1]},0]}]},[[[1],{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Switch":{"If":[{"Copy":{"var_id":2,"projection":[{"Field":[{"ProjAdt":[1,1]},0]},{"Field":[{"ProjAdt":[0,1]},0]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Assign":[{"var_id":4,"projection":[]},{"Aggregate":[{"Adt":["Tuple",null,{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},[]]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Assign":[{"var_id":0,"projection":[]},{"Use":{"Move":{"var_id":4,"projection":[]}}}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Drop":{"var_id":1,"projection":[]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Drop":{"var_id":2,"projection":[]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Assign":[{"var_id":0,"projection":[]},{"Aggregate":[{"Adt":["Tuple",null,{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},[]]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":"Return"}]}}]}}]}}]}}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":"Nop"}]}}}]],{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":"Nop"}]}}}]],{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":"Nop"}]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":"Panic"}]}}]}}]}}]}}]}}]}}]}}}},{"def_id":3,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":13,"col":4},"end":{"line":13,"col":24}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"is_local":true,"name":[{"Ident":["example",0]},{"Ident":["Trait",0]},{"Ident":["method",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":{"num_region_params":0,"num_type_params":1,"num_const_generic_params":0,"num_trait_clauses":0,"num_regions_outlive":0,"num_types_outlive":0,"num_trait_type_constraints":0},"inputs":[],"output":{"TypeVar":0}},"kind":{"TraitItemDecl":[2,"method"]},"body":null},{"def_id":4,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":0},"beg":{"line":120,"col":4},"end":{"line":120,"col":28}},"generated_from_span":null},"attributes":[],"inline":null,"public":true},"is_local":false,"name":[{"Ident":["core",0]},{"Ident":["clone",0]},{"Ident":["Clone",0]},{"Ident":["clone",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[{"index":0,"name":null}],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":{"num_region_params":0,"num_type_params":1,"num_const_generic_params":0,"num_trait_clauses":0,"num_regions_outlive":0,"num_types_outlive":0,"num_trait_type_constraints":0},"inputs":[{"Ref":[{"BVar":[0,0]},{"TypeVar":0},"Shared"]}],"output":{"TypeVar":0}},"kind":{"TraitItemDecl":[1,"clone"]},"body":null},{"def_id":5,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":1},"beg":{"line":133,"col":4},"end":{"line":133,"col":25}},"generated_from_span":null},"attributes":[],"inline":null,"public":true},"is_local":false,"name":[{"Ident":["core",0]},{"Ident":["default",0]},{"Ident":["Default",0]},{"Ident":["default",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":{"num_region_params":0,"num_type_params":1,"num_const_generic_params":0,"num_trait_clauses":0,"num_regions_outlive":0,"num_types_outlive":0,"num_trait_type_constraints":0},"inputs":[],"output":{"TypeVar":0}},"kind":{"TraitItemDecl":[3,"default"]},"body":null},{"def_id":6,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":3},"beg":{"line":2592,"col":4},"end":{"line":2592,"col":24}},"generated_from_span":null},"attributes":[],"inline":"Hint","public":true},"is_local":false,"name":[{"Ident":["core",0]},{"Ident":["str",0]},{"Impl":{"disambiguator":2,"generics":{"regions":[{"index":0,"name":null}],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":3,"generics":{"regions":[],"types":[{"Ref":[{"BVar":[0,0]},{"Adt":[{"Assumed":"Str"},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}],"const_generics":[],"trait_refs":[]}}}}},{"Ident":["default",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[{"index":0,"name":null}],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":{"num_region_params":1,"num_type_params":0,"num_const_generic_params":0,"num_trait_clauses":0,"num_regions_outlive":0,"num_types_outlive":0,"num_trait_type_constraints":0},"inputs":[],"output":{"Ref":[{"BVar":[0,0]},{"Adt":[{"Assumed":"Str"},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}},"kind":{"TraitItemImpl":{"impl_id":3,"trait_id":3,"item_name":"default","provided":false}},"body":null}],"globals":[{"def_id":0,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":23,"col":0},"end":{"line":23,"col":18}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"is_local":true,"name":[{"Ident":["example",0]},{"Ident":["CONST",0]}],"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"ty":{"Literal":{"Integer":"Isize"}},"kind":"Regular","body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":23,"col":0},"end":{"line":23,"col":25}},"generated_from_span":null},"arg_count":0,"locals":[{"index":0,"name":null,"ty":{"Literal":{"Integer":"Isize"}}}],"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":23,"col":0},"end":{"line":23,"col":25}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":23,"col":0},"end":{"line":23,"col":25}},"generated_from_span":null},"content":{"Assign":[{"var_id":0,"projection":[]},{"Use":{"Const":{"value":{"Literal":{"Scalar":{"Isize":"128"}}},"ty":{"Literal":{"Integer":"Isize"}}}}}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":23,"col":0},"end":{"line":23,"col":25}},"generated_from_span":null},"content":"Return"}]}}}},{"def_id":1,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":28}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"is_local":true,"name":[{"Ident":["example",0]},{"Ident":["STATIC",0]}],"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"ty":{"Ref":["Static",{"Literal":"Bool"},"Shared"]},"kind":"Regular","body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"arg_count":0,"locals":[{"index":0,"name":null,"ty":{"Ref":["Erased",{"Literal":"Bool"},"Shared"]}},{"index":1,"name":null,"ty":{"Ref":["Erased",{"Literal":"Bool"},"Shared"]}},{"index":2,"name":null,"ty":{"Literal":"Bool"}}],"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Assign":[{"var_id":2,"projection":[]},{"Use":{"Const":{"value":{"Literal":{"Bool":false}},"ty":{"Literal":"Bool"}}}}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Assign":[{"var_id":1,"projection":[]},{"Ref":[{"var_id":2,"projection":[]},"Shared"]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Assign":[{"var_id":0,"projection":[]},{"Ref":[{"var_id":1,"projection":["Deref"]},"Shared"]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Drop":{"var_id":1,"projection":[]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":"Return"}]}}]}}]}}]}}}}],"trait_decls":[{"def_id":0,"is_local":false,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":2},"beg":{"line":450,"col":0},"end":{"line":450,"col":21}},"generated_from_span":null},"attributes":[],"inline":null,"public":true},"name":[{"Ident":["core",0]},{"Ident":["marker",0]},{"Ident":["Copy",0]}],"generics":{"regions":[],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_clauses":[{"clause_id":0,"meta":{"span":{"file_id":{"VirtualId":2},"beg":{"line":450,"col":16},"end":{"line":450,"col":21}},"generated_from_span":null},"trait_id":1,"generics":{"regions":[],"types":[{"TypeVar":0}],"const_generics":[],"trait_refs":[]}}],"consts":[],"types":[],"required_methods":[],"provided_methods":[]},{"def_id":1,"is_local":false,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":0},"beg":{"line":107,"col":0},"end":{"line":107,"col":22}},"generated_from_span":null},"attributes":[],"inline":null,"public":true},"name":[{"Ident":["core",0]},{"Ident":["clone",0]},{"Ident":["Clone",0]}],"generics":{"regions":[],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_clauses":[],"consts":[],"types":[],"required_methods":[["clone",4]],"provided_methods":[["clone_from",null]]},{"def_id":2,"is_local":true,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":11,"col":0},"end":{"line":11,"col":17}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"name":[{"Ident":["example",0]},{"Ident":["Trait",0]}],"generics":{"regions":[],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_clauses":[{"clause_id":0,"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":11,"col":13},"end":{"line":11,"col":17}},"generated_from_span":null},"trait_id":0,"generics":{"regions":[],"types":[{"TypeVar":0}],"const_generics":[],"trait_refs":[]}}],"consts":[],"types":[["AssocType",[[{"clause_id":0,"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":1,"col":0},"end":{"line":1,"col":0}},"generated_from_span":null},"trait_id":3,"generics":{"regions":[],"types":[{"TraitType":[{"trait_id":"SelfId","generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"trait_decl_ref":{"trait_id":2,"generics":{"regions":[],"types":[{"TypeVar":0}],"const_generics":[],"trait_refs":[]}}},"AssocType"]}],"const_generics":[],"trait_refs":[]}}],null]]],"required_methods":[["method",3]],"provided_methods":[]},{"def_id":3,"is_local":false,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":1},"beg":{"line":102,"col":0},"end":{"line":102,"col":24}},"generated_from_span":null},"attributes":[],"inline":null,"public":true},"name":[{"Ident":["core",0]},{"Ident":["default",0]},{"Ident":["Default",0]}],"generics":{"regions":[],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_clauses":[],"consts":[],"types":[],"required_methods":[["default",5]],"provided_methods":[]}],"trait_impls":[{"def_id":0,"is_local":true,"name":[{"Ident":["example",0]},{"Impl":{"disambiguator":1,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":0,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}}}],"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":9},"end":{"line":3,"col":13}},"generated_from_span":null},"attributes":["automatically_derived"],"inline":null,"public":false},"impl_trait":{"trait_id":0,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_trait_refs":[{"trait_id":{"TraitImpl":1},"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"trait_decl_ref":{"trait_id":1,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}],"consts":[],"types":[],"required_methods":[],"provided_methods":[]},{"def_id":1,"is_local":true,"name":[{"Ident":["example",0]},{"Impl":{"disambiguator":2,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":1,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}}}],"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":15},"end":{"line":3,"col":20}},"generated_from_span":null},"attributes":["automatically_derived"],"inline":null,"public":false},"impl_trait":{"trait_id":1,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_trait_refs":[],"consts":[],"types":[],"required_methods":[["clone",0]],"provided_methods":[]},{"def_id":2,"is_local":true,"name":[{"Ident":["example",0]},{"Impl":{"disambiguator":0,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":2,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}}}],"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":16,"col":0},"end":{"line":16,"col":18}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"impl_trait":{"trait_id":2,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_trait_refs":[{"trait_id":{"TraitImpl":0},"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"trait_decl_ref":{"trait_id":0,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}],"consts":[],"types":[["AssocType",[[{"trait_id":{"TraitImpl":3},"generics":{"regions":["Erased"],"types":[],"const_generics":[],"trait_refs":[]},"trait_decl_ref":{"trait_id":3,"generics":{"regions":[],"types":[{"Ref":["Erased",{"Adt":[{"Assumed":"Str"},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}],"const_generics":[],"trait_refs":[]}}}],{"Ref":["Static",{"Adt":[{"Assumed":"Str"},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}]]],"required_methods":[["method",1]],"provided_methods":[]},{"def_id":3,"is_local":false,"name":[{"Ident":["core",0]},{"Ident":["str",0]},{"Impl":{"disambiguator":2,"generics":{"regions":[{"index":0,"name":null}],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":3,"generics":{"regions":[],"types":[{"Ref":[{"BVar":[0,0]},{"Adt":[{"Assumed":"Str"},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}],"const_generics":[],"trait_refs":[]}}}}}],"item_meta":{"meta":{"span":{"file_id":{"VirtualId":3},"beg":{"line":2589,"col":0},"end":{"line":2589,"col":21}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"impl_trait":{"trait_id":3,"generics":{"regions":[],"types":[{"Ref":[{"BVar":[0,0]},{"Adt":[{"Assumed":"Str"},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}],"const_generics":[],"trait_refs":[]}},"generics":{"regions":[{"index":0,"name":null}],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_trait_refs":[],"consts":[],"types":[],"required_methods":[["default",6]],"provided_methods":[]}]}
\ No newline at end of file
+{"charon_version":"0.1.2","name":"example","id_to_file":[[{"LocalId":0},{"Local":"tests/version/example.rs"}],[{"VirtualId":0},{"Virtual":"/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/clone.rs"}],[{"VirtualId":1},{"Virtual":"/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/default.rs"}],[{"VirtualId":2},{"Virtual":"/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs"}],[{"VirtualId":3},{"Virtual":"/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/str/mod.rs"}],[{"VirtualId":4},{"Virtual":"/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs"}]],"declarations":[{"Type":{"NonRec":0}},{"TraitDecl":{"NonRec":1}},{"TraitDecl":{"NonRec":0}},{"Fun":{"NonRec":0}},{"TraitImpl":{"NonRec":1}},{"TraitImpl":{"NonRec":0}},{"TraitDecl":{"NonRec":3}},{"TraitDecl":{"NonRec":2}},{"Fun":{"NonRec":6}},{"TraitImpl":{"NonRec":3}},{"Fun":{"NonRec":1}},{"TraitImpl":{"NonRec":2}},{"Global":{"NonRec":0}},{"Global":{"NonRec":1}},{"Type":{"NonRec":1}},{"Fun":{"NonRec":3}},{"Fun":{"NonRec":2}},{"Fun":{"NonRec":4}},{"Fun":{"NonRec":5}}],"types":[{"def_id":0,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":4,"col":0},"end":{"line":4,"col":8}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"is_local":true,"name":[{"Ident":["example",0]},{"Ident":["Foo",0]}],"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Enum":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":5,"col":4},"end":{"line":5,"col":5}},"generated_from_span":null},"name":"A","fields":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":5,"col":6},"end":{"line":5,"col":9}},"generated_from_span":null},"name":null,"ty":{"Literal":{"Integer":"U32"}}}],"discriminant":{"Isize":"0"}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":6,"col":4},"end":{"line":6,"col":5}},"generated_from_span":null},"name":"B","fields":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":6,"col":8},"end":{"line":6,"col":19}},"generated_from_span":null},"name":"field","ty":{"Literal":"Bool"}}],"discriminant":{"Isize":"1"}}]}},{"def_id":1,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":4},"beg":{"line":563,"col":0},"end":{"line":563,"col":18}},"generated_from_span":null},"attributes":[],"inline":null,"public":true},"is_local":false,"name":[{"Ident":["core",0]},{"Ident":["option",0]},{"Ident":["Option",0]}],"generics":{"regions":[],"types":[{"index":0,"name":"T"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Enum":[{"meta":{"span":{"file_id":{"VirtualId":4},"beg":{"line":567,"col":4},"end":{"line":567,"col":8}},"generated_from_span":null},"name":"None","fields":[],"discriminant":{"Isize":"0"}},{"meta":{"span":{"file_id":{"VirtualId":4},"beg":{"line":571,"col":4},"end":{"line":571,"col":8}},"generated_from_span":null},"name":"Some","fields":[{"meta":{"span":{"file_id":{"VirtualId":4},"beg":{"line":571,"col":55},"end":{"line":571,"col":56}},"generated_from_span":null},"name":null,"ty":{"TypeVar":0}}],"discriminant":{"Isize":"1"}}]}}],"functions":[{"def_id":0,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":15},"end":{"line":3,"col":20}},"generated_from_span":null},"attributes":["inline"],"inline":"Hint","public":true},"is_local":true,"name":[{"Ident":["example",0]},{"Impl":{"disambiguator":2,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":1,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}}},{"Ident":["clone",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[{"index":0,"name":null}],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":{"num_region_params":0,"num_type_params":0,"num_const_generic_params":0,"num_trait_clauses":0,"num_regions_outlive":0,"num_types_outlive":0,"num_trait_type_constraints":0},"inputs":[{"Ref":[{"BVar":[0,0]},{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}],"output":{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},"kind":{"TraitItemImpl":{"impl_id":1,"trait_id":1,"item_name":"clone","provided":false}},"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":15},"end":{"line":3,"col":20}},"generated_from_span":null},"arg_count":1,"locals":[{"index":0,"name":null,"ty":{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},{"index":1,"name":"self","ty":{"Ref":["Erased",{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}}],"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":15},"end":{"line":3,"col":20}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":15},"end":{"line":3,"col":20}},"generated_from_span":null},"content":{"Assign":[{"var_id":0,"projection":[]},{"Use":{"Copy":{"var_id":1,"projection":["Deref"]}}}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":15},"end":{"line":3,"col":20}},"generated_from_span":null},"content":"Return"}]}}}},{"def_id":1,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":18,"col":4},"end":{"line":18,"col":23}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"is_local":true,"name":[{"Ident":["example",0]},{"Impl":{"disambiguator":0,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":2,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}}},{"Ident":["method",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":{"num_region_params":0,"num_type_params":0,"num_const_generic_params":0,"num_trait_clauses":0,"num_regions_outlive":0,"num_types_outlive":0,"num_trait_type_constraints":0},"inputs":[],"output":{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},"kind":{"TraitItemImpl":{"impl_id":2,"trait_id":2,"item_name":"method","provided":false}},"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":18,"col":4},"end":{"line":20,"col":5}},"generated_from_span":null},"arg_count":0,"locals":[{"index":0,"name":null,"ty":{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}}],"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":18,"col":4},"end":{"line":20,"col":5}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":18,"col":4},"end":{"line":20,"col":5}},"generated_from_span":null},"content":{"Assign":[{"var_id":0,"projection":[]},{"Aggregate":[{"Adt":[{"Adt":0},0,{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},[{"Const":{"value":{"Literal":{"Scalar":{"U32":"42"}}},"ty":{"Literal":{"Integer":"U32"}}}}]]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":18,"col":4},"end":{"line":20,"col":5}},"generated_from_span":null},"content":"Return"}]}}}},{"def_id":2,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":27,"col":9}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"is_local":true,"name":[{"Ident":["example",0]},{"Ident":["main",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":null,"inputs":[],"output":{"Adt":["Tuple",{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},"kind":"Regular","body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"arg_count":0,"locals":[{"index":0,"name":null,"ty":{"Adt":["Tuple",{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},{"index":1,"name":"foo","ty":{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},{"index":2,"name":null,"ty":{"Adt":[{"Adt":1},{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}]}},{"index":3,"name":null,"ty":{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}},{"index":4,"name":null,"ty":{"Adt":["Tuple",{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}}],"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Call":{"func":{"Regular":{"func":{"Trait":[{"trait_id":{"TraitImpl":2},"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"trait_decl_ref":{"trait_id":2,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}},"method",3]},"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}}},"args":[],"dest":{"var_id":1,"projection":[]}}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"FakeRead":{"var_id":1,"projection":[]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Assign":[{"var_id":3,"projection":[]},{"Use":{"Copy":{"var_id":1,"projection":[]}}}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Assign":[{"var_id":2,"projection":[]},{"Aggregate":[{"Adt":[{"Adt":1},1,{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}]},[{"Move":{"var_id":3,"projection":[]}}]]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Drop":{"var_id":3,"projection":[]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"FakeRead":{"var_id":2,"projection":[]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Switch":{"Match":[{"var_id":2,"projection":[]},[[[1],{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Switch":{"Match":[{"var_id":2,"projection":[{"Field":[{"ProjAdt":[1,1]},0]}]},[[[1],{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Switch":{"If":[{"Copy":{"var_id":2,"projection":[{"Field":[{"ProjAdt":[1,1]},0]},{"Field":[{"ProjAdt":[0,1]},0]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Assign":[{"var_id":4,"projection":[]},{"Aggregate":[{"Adt":["Tuple",null,{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},[]]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Assign":[{"var_id":0,"projection":[]},{"Use":{"Move":{"var_id":4,"projection":[]}}}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Drop":{"var_id":1,"projection":[]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Drop":{"var_id":2,"projection":[]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":{"Assign":[{"var_id":0,"projection":[]},{"Aggregate":[{"Adt":["Tuple",null,{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},[]]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":27,"col":0},"end":{"line":33,"col":1}},"generated_from_span":null},"content":"Return"}]}}]}}]}}]}}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":"Nop"}]}}}]],{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":"Nop"}]}}}]],{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":"Nop"}]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":28,"col":4},"end":{"line":33,"col":1}},"generated_from_span":null},"content":"Panic"}]}}]}}]}}]}}]}}]}}]}}}},{"def_id":3,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":13,"col":4},"end":{"line":13,"col":24}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"is_local":true,"name":[{"Ident":["example",0]},{"Ident":["Trait",0]},{"Ident":["method",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":{"num_region_params":0,"num_type_params":1,"num_const_generic_params":0,"num_trait_clauses":0,"num_regions_outlive":0,"num_types_outlive":0,"num_trait_type_constraints":0},"inputs":[],"output":{"TypeVar":0}},"kind":{"TraitItemDecl":[2,"method"]},"body":null},{"def_id":4,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":0},"beg":{"line":120,"col":4},"end":{"line":120,"col":28}},"generated_from_span":null},"attributes":[],"inline":null,"public":true},"is_local":false,"name":[{"Ident":["core",0]},{"Ident":["clone",0]},{"Ident":["Clone",0]},{"Ident":["clone",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[{"index":0,"name":null}],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":{"num_region_params":0,"num_type_params":1,"num_const_generic_params":0,"num_trait_clauses":0,"num_regions_outlive":0,"num_types_outlive":0,"num_trait_type_constraints":0},"inputs":[{"Ref":[{"BVar":[0,0]},{"TypeVar":0},"Shared"]}],"output":{"TypeVar":0}},"kind":{"TraitItemDecl":[1,"clone"]},"body":null},{"def_id":5,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":1},"beg":{"line":133,"col":4},"end":{"line":133,"col":25}},"generated_from_span":null},"attributes":[],"inline":null,"public":true},"is_local":false,"name":[{"Ident":["core",0]},{"Ident":["default",0]},{"Ident":["Default",0]},{"Ident":["default",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":{"num_region_params":0,"num_type_params":1,"num_const_generic_params":0,"num_trait_clauses":0,"num_regions_outlive":0,"num_types_outlive":0,"num_trait_type_constraints":0},"inputs":[],"output":{"TypeVar":0}},"kind":{"TraitItemDecl":[3,"default"]},"body":null},{"def_id":6,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":3},"beg":{"line":2592,"col":4},"end":{"line":2592,"col":24}},"generated_from_span":null},"attributes":[],"inline":"Hint","public":true},"is_local":false,"name":[{"Ident":["core",0]},{"Ident":["str",0]},{"Impl":{"disambiguator":2,"generics":{"regions":[{"index":0,"name":null}],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":3,"generics":{"regions":[],"types":[{"Ref":[{"BVar":[0,0]},{"Adt":[{"Assumed":"Str"},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}],"const_generics":[],"trait_refs":[]}}}}},{"Ident":["default",0]}],"signature":{"is_unsafe":false,"is_closure":false,"closure_info":null,"generics":{"regions":[{"index":0,"name":null}],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_params_info":{"num_region_params":1,"num_type_params":0,"num_const_generic_params":0,"num_trait_clauses":0,"num_regions_outlive":0,"num_types_outlive":0,"num_trait_type_constraints":0},"inputs":[],"output":{"Ref":[{"BVar":[0,0]},{"Adt":[{"Assumed":"Str"},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}},"kind":{"TraitItemImpl":{"impl_id":3,"trait_id":3,"item_name":"default","provided":false}},"body":null}],"globals":[{"def_id":0,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":23,"col":0},"end":{"line":23,"col":18}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"is_local":true,"name":[{"Ident":["example",0]},{"Ident":["CONST",0]}],"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"ty":{"Literal":{"Integer":"Isize"}},"kind":"Regular","body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":23,"col":0},"end":{"line":23,"col":25}},"generated_from_span":null},"arg_count":0,"locals":[{"index":0,"name":null,"ty":{"Literal":{"Integer":"Isize"}}}],"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":23,"col":0},"end":{"line":23,"col":25}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":23,"col":0},"end":{"line":23,"col":25}},"generated_from_span":null},"content":{"Assign":[{"var_id":0,"projection":[]},{"Use":{"Const":{"value":{"Literal":{"Scalar":{"Isize":"128"}}},"ty":{"Literal":{"Integer":"Isize"}}}}}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":23,"col":0},"end":{"line":23,"col":25}},"generated_from_span":null},"content":"Return"}]}}}},{"def_id":1,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":28}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"is_local":true,"name":[{"Ident":["example",0]},{"Ident":["STATIC",0]}],"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"ty":{"Ref":["Static",{"Literal":"Bool"},"Shared"]},"kind":"Regular","body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"arg_count":0,"locals":[{"index":0,"name":null,"ty":{"Ref":["Erased",{"Literal":"Bool"},"Shared"]}},{"index":1,"name":null,"ty":{"Ref":["Erased",{"Literal":"Bool"},"Shared"]}},{"index":2,"name":null,"ty":{"Literal":"Bool"}}],"body":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Assign":[{"var_id":2,"projection":[]},{"Use":{"Const":{"value":{"Literal":{"Bool":false}},"ty":{"Literal":"Bool"}}}}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Assign":[{"var_id":1,"projection":[]},{"Ref":[{"var_id":2,"projection":[]},"Shared"]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Assign":[{"var_id":0,"projection":[]},{"Ref":[{"var_id":1,"projection":["Deref"]},"Shared"]}]}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Sequence":[{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":{"Drop":{"var_id":1,"projection":[]}}},{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":25,"col":0},"end":{"line":25,"col":38}},"generated_from_span":null},"content":"Return"}]}}]}}]}}]}}}}],"trait_decls":[{"def_id":0,"is_local":false,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":2},"beg":{"line":450,"col":0},"end":{"line":450,"col":21}},"generated_from_span":null},"attributes":[],"inline":null,"public":true},"name":[{"Ident":["core",0]},{"Ident":["marker",0]},{"Ident":["Copy",0]}],"generics":{"regions":[],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_clauses":[{"clause_id":0,"meta":{"span":{"file_id":{"VirtualId":2},"beg":{"line":450,"col":16},"end":{"line":450,"col":21}},"generated_from_span":null},"trait_id":1,"generics":{"regions":[],"types":[{"TypeVar":0}],"const_generics":[],"trait_refs":[]}}],"consts":[],"types":[],"required_methods":[],"provided_methods":[]},{"def_id":1,"is_local":false,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":0},"beg":{"line":107,"col":0},"end":{"line":107,"col":22}},"generated_from_span":null},"attributes":[],"inline":null,"public":true},"name":[{"Ident":["core",0]},{"Ident":["clone",0]},{"Ident":["Clone",0]}],"generics":{"regions":[],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_clauses":[],"consts":[],"types":[],"required_methods":[["clone",4]],"provided_methods":[["clone_from",null]]},{"def_id":2,"is_local":true,"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":11,"col":0},"end":{"line":11,"col":17}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"name":[{"Ident":["example",0]},{"Ident":["Trait",0]}],"generics":{"regions":[],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_clauses":[{"clause_id":0,"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":11,"col":13},"end":{"line":11,"col":17}},"generated_from_span":null},"trait_id":0,"generics":{"regions":[],"types":[{"TypeVar":0}],"const_generics":[],"trait_refs":[]}}],"consts":[],"types":[["AssocType",[[{"clause_id":0,"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":1,"col":0},"end":{"line":1,"col":0}},"generated_from_span":null},"trait_id":3,"generics":{"regions":[],"types":[{"TraitType":[{"trait_id":"SelfId","generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"trait_decl_ref":{"trait_id":2,"generics":{"regions":[],"types":[{"TypeVar":0}],"const_generics":[],"trait_refs":[]}}},"AssocType"]}],"const_generics":[],"trait_refs":[]}}],null]]],"required_methods":[["method",3]],"provided_methods":[]},{"def_id":3,"is_local":false,"item_meta":{"meta":{"span":{"file_id":{"VirtualId":1},"beg":{"line":102,"col":0},"end":{"line":102,"col":24}},"generated_from_span":null},"attributes":[],"inline":null,"public":true},"name":[{"Ident":["core",0]},{"Ident":["default",0]},{"Ident":["Default",0]}],"generics":{"regions":[],"types":[{"index":0,"name":"Self"}],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_clauses":[],"consts":[],"types":[],"required_methods":[["default",5]],"provided_methods":[]}],"trait_impls":[{"def_id":0,"is_local":true,"name":[{"Ident":["example",0]},{"Impl":{"disambiguator":1,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":0,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}}}],"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":9},"end":{"line":3,"col":13}},"generated_from_span":null},"attributes":["automatically_derived"],"inline":null,"public":false},"impl_trait":{"trait_id":0,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_trait_refs":[{"trait_id":{"TraitImpl":1},"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"trait_decl_ref":{"trait_id":1,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}],"consts":[],"types":[],"required_methods":[],"provided_methods":[]},{"def_id":1,"is_local":true,"name":[{"Ident":["example",0]},{"Impl":{"disambiguator":2,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":1,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}}}],"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":3,"col":15},"end":{"line":3,"col":20}},"generated_from_span":null},"attributes":["automatically_derived"],"inline":null,"public":false},"impl_trait":{"trait_id":1,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_trait_refs":[],"consts":[],"types":[],"required_methods":[["clone",0]],"provided_methods":[]},{"def_id":2,"is_local":true,"name":[{"Ident":["example",0]},{"Impl":{"disambiguator":0,"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":2,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}}}],"item_meta":{"meta":{"span":{"file_id":{"LocalId":0},"beg":{"line":16,"col":0},"end":{"line":16,"col":18}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"impl_trait":{"trait_id":2,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_trait_refs":[{"trait_id":{"TraitImpl":0},"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"trait_decl_ref":{"trait_id":0,"generics":{"regions":[],"types":[{"Adt":[{"Adt":0},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]}],"const_generics":[],"trait_refs":[]}}}],"consts":[],"types":[["AssocType",[[{"trait_id":{"TraitImpl":3},"generics":{"regions":["Erased"],"types":[],"const_generics":[],"trait_refs":[]},"trait_decl_ref":{"trait_id":3,"generics":{"regions":[],"types":[{"Ref":["Erased",{"Adt":[{"Assumed":"Str"},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}],"const_generics":[],"trait_refs":[]}}}],{"Ref":["Static",{"Adt":[{"Assumed":"Str"},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}]]],"required_methods":[["method",1]],"provided_methods":[]},{"def_id":3,"is_local":false,"name":[{"Ident":["core",0]},{"Ident":["str",0]},{"Impl":{"disambiguator":2,"generics":{"regions":[{"index":0,"name":null}],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"kind":{"Trait":{"trait_id":3,"generics":{"regions":[],"types":[{"Ref":[{"BVar":[0,0]},{"Adt":[{"Assumed":"Str"},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}],"const_generics":[],"trait_refs":[]}}}}}],"item_meta":{"meta":{"span":{"file_id":{"VirtualId":3},"beg":{"line":2589,"col":0},"end":{"line":2589,"col":21}},"generated_from_span":null},"attributes":[],"inline":null,"public":false},"impl_trait":{"trait_id":3,"generics":{"regions":[],"types":[{"Ref":[{"BVar":[0,0]},{"Adt":[{"Assumed":"Str"},{"regions":[],"types":[],"const_generics":[],"trait_refs":[]}]},"Shared"]}],"const_generics":[],"trait_refs":[]}},"generics":{"regions":[{"index":0,"name":null}],"types":[],"const_generics":[],"trait_clauses":[]},"preds":{"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"parent_trait_refs":[],"consts":[],"types":[],"required_methods":[["default",6]],"provided_methods":[]}]}
\ No newline at end of file