diff --git a/.travis.yml b/.travis.yml
index ca5c28e3..fe3621c3 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -4,7 +4,7 @@ os:
   # - windows
 language: rust
 rust:
-- nightly-2021-01-01
+- nightly-2021-02-09
 
 before_install:
 - if [ ${TRAVIS_OS_NAME} == "osx" ]; then curl -L https://github.com/mozilla/grcov/releases/download/v0.5.9/grcov-osx-x86_64.tar.bz2 | tar jxf -; fi
diff --git a/Cargo.lock b/Cargo.lock
index 8328b3c1..71fbf82f 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -200,7 +200,7 @@ checksum = "1d34cfa13a63ae058bfa601fe9e313bbdb3746427c1459185464ce0fcf62e1e8"
 dependencies = [
  "cfg-if",
  "libc",
- "redox_syscall 0.2.4",
+ "redox_syscall",
  "winapi",
 ]
 
@@ -364,7 +364,7 @@ dependencies = [
 
 [[package]]
 name = "mirai-annotations"
-version = "1.10.1"
+version = "1.11.0"
 
 [[package]]
 name = "mirai-standard-contracts"
@@ -392,14 +392,14 @@ dependencies = [
 
 [[package]]
 name = "parking_lot_core"
-version = "0.8.2"
+version = "0.8.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9ccb628cad4f84851442432c60ad8e1f607e29752d0bf072cbd0baf28aa34272"
+checksum = "fa7a782938e745763fe6907fc6ba86946d72f49fe7e21de074e08128a99fb018"
 dependencies = [
  "cfg-if",
  "instant",
  "libc",
- "redox_syscall 0.1.57",
+ "redox_syscall",
  "smallvec",
  "winapi",
 ]
@@ -421,9 +421,9 @@ dependencies = [
 
 [[package]]
 name = "quote"
-version = "1.0.8"
+version = "1.0.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "991431c3519a3f36861882da93630ce66b52918dcf1b8e2fd66b397fc96f28df"
+checksum = "c3d0b9745dc2debf507c8422de05d7226cc1f0644216dfdfead988f9b1ab32a7"
 dependencies = [
  "proc-macro2",
 ]
@@ -468,12 +468,6 @@ dependencies = [
  "rand_core",
 ]
 
-[[package]]
-name = "redox_syscall"
-version = "0.1.57"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41cc0f7e4d5d4544e8861606a285bb08d3e70712ccc7d2b84d7c0ccfaf4b05ce"
-
 [[package]]
 name = "redox_syscall"
 version = "0.2.4"
@@ -658,7 +652,7 @@ dependencies = [
  "cfg-if",
  "libc",
  "rand",
- "redox_syscall 0.2.4",
+ "redox_syscall",
  "remove_dir_all",
  "winapi",
 ]
diff --git a/annotations/Cargo.toml b/annotations/Cargo.toml
index f98220fd..1b192538 100644
--- a/annotations/Cargo.toml
+++ b/annotations/Cargo.toml
@@ -1,7 +1,7 @@
 [package]
 
 name = "mirai-annotations"
-version = "1.10.1"
+version = "1.11.0"
 authors = ["Herman Venter <hermanv@fb.com>"]
 description = "Macros that provide source code annotations for MIRAI"
 repository = "https://github.com/facebookexperimental/MIRAI"
diff --git a/annotations/README.md b/annotations/README.md
index c6d55729..ceb42ca3 100644
--- a/annotations/README.md
+++ b/annotations/README.md
@@ -37,7 +37,9 @@ Additionally we also have:
 
 This crate also provides macros for describing and constraining abstract state that only has meaning to MIRAI. These are:
 * abstract_value!
+* add_tag!
 * get_model_field!
+* has_tag!  
 * result!
 * set_model_field!
 
diff --git a/annotations/src/lib.rs b/annotations/src/lib.rs
index dcbe705e..c22ecfab 100644
--- a/annotations/src/lib.rs
+++ b/annotations/src/lib.rs
@@ -64,6 +64,7 @@ pub enum TagPropagation {
     Sub,
     SubComponent,
     SubOverflows,
+    Transmute,
     UninterpretedCall,
 }
 
diff --git a/binaries/summary_store.tar b/binaries/summary_store.tar
index db4dfa3b..73a4475d 100644
Binary files a/binaries/summary_store.tar and b/binaries/summary_store.tar differ
diff --git a/checker/src/abstract_value.rs b/checker/src/abstract_value.rs
index 6c81b10b..3e8ac613 100644
--- a/checker/src/abstract_value.rs
+++ b/checker/src/abstract_value.rs
@@ -194,11 +194,11 @@ impl AbstractValue {
             // The overall expression is going to overflow, so pre-compute the simpler domains from
             // the larger expression and then replace its expression with TOP.
             if left.expression_size < right.expression_size {
-                info!("binary expression right operand abstracted");
+                debug!("binary expression right operand abstracted");
                 right = AbstractValue::make_from(right.expression.clone(), u64::MAX);
                 expression_size = left.expression_size + 1;
             } else {
-                info!("binary expression left operand abstracted");
+                debug!("binary expression left operand abstracted");
                 left = AbstractValue::make_from(left.expression.clone(), u64::MAX);
                 expression_size = right.expression_size + 1;
             }
@@ -310,7 +310,7 @@ impl AbstractValue {
         if expression_size > k_limits::MAX_EXPRESSION_SIZE {
             if expression_size < u64::MAX {
                 trace!("expression {:?}", expression);
-                info!("expression abstracted");
+                debug!("expression abstracted");
             }
             // If the expression gets too large, refining it gets expensive and composing it
             // into other expressions leads to exponential growth. We therefore need to abstract
@@ -484,6 +484,7 @@ pub trait AbstractValueTrait: Sized {
         fresh: usize,
     ) -> Self;
     fn refine_with(&self, path_condition: &Self, depth: usize) -> Self;
+    fn replace_embedded_path_root(&self, old_root: &Rc<Path>, new_root: Rc<Path>) -> Self;
     fn transmute(&self, target_type: ExpressionType) -> Self;
     fn try_resolve_as_byte_array(&self, _environment: &Environment) -> Option<Vec<u8>>;
     fn try_resolve_as_ref_to_str(&self, environment: &Environment) -> Option<Rc<str>>;
@@ -965,7 +966,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                 if let Some(trimmed) = self
                     .trim_prefix_conjuncts(k_limits::MAX_EXPRESSION_SIZE - other.expression_size)
                 {
-                    info!("and expression prefix trimmed");
+                    debug!("and expression prefix trimmed");
                     trimmed_self = trimmed;
                 } else {
                     return other;
@@ -1538,7 +1539,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                 .expression_size
                 .saturating_add(consequent.expression_size);
             if condition_plus_consequent < k_limits::MAX_EXPRESSION_SIZE - 1 {
-                info!("alternate abstracted");
+                debug!("alternate abstracted");
                 alternate = AbstractValue::make_from(alternate.expression.clone(), u64::MAX);
                 expression_size = condition_plus_consequent + 1;
             } else {
@@ -1546,7 +1547,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                     .expression_size
                     .saturating_add(alternate.expression_size);
                 if condition_plus_alternate < k_limits::MAX_EXPRESSION_SIZE - 1 {
-                    info!("consequent abstracted");
+                    debug!("consequent abstracted");
                     consequent = AbstractValue::make_from(consequent.expression.clone(), u64::MAX);
                     expression_size = condition_plus_alternate + 1;
                 } else {
@@ -1554,7 +1555,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                         .expression_size
                         .saturating_add(alternate.expression_size);
                     if consequent_plus_alternate < k_limits::MAX_EXPRESSION_SIZE - 1 {
-                        info!("condition abstracted");
+                        debug!("condition abstracted");
                         condition =
                             AbstractValue::make_from(condition.expression.clone(), u64::MAX);
                         expression_size = consequent_plus_alternate + 1;
@@ -2613,6 +2614,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
         match &self.expression {
             Expression::Cast { operand, .. }
             | Expression::TaggedExpression { operand, .. }
+            | Expression::Transmute { operand, .. }
             | Expression::UnknownTagCheck { operand, .. } => {
                 operand.might_benefit_from_refinement()
             }
@@ -3990,7 +3992,8 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             | Expression::IntrinsicBitVectorUnary { operand, .. }
             | Expression::IntrinsicFloatingPointUnary { operand, .. }
             | Expression::LogicalNot { operand, .. }
-            | Expression::Neg { operand, .. } => {
+            | Expression::Neg { operand, .. }
+            | Expression::Transmute { operand, .. } => {
                 operand.get_cached_tags().propagate_through(exp_tag_prop)
             }
 
@@ -4061,6 +4064,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             | Expression::Neg { operand }
             | Expression::LogicalNot { operand }
             | Expression::TaggedExpression { operand, .. }
+            | Expression::Transmute { operand, .. }
             | Expression::UnknownTagCheck { operand, .. } => {
                 operand.get_widened_subexpression(path)
             }
@@ -4435,6 +4439,12 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             Expression::TaggedExpression { operand, tag } => operand
                 .refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
                 .add_tag(*tag),
+            Expression::Transmute {
+                operand,
+                target_type,
+            } => operand
+                .refine_parameters_and_paths(args, result, pre_env, post_env, fresh)
+                .transmute(target_type.clone()),
             Expression::UninterpretedCall {
                 callee,
                 arguments,
@@ -4562,7 +4572,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
         //do not use false path conditions to refine things
         checked_precondition!(path_condition.as_bool_if_known().is_none());
         if depth >= k_limits::MAX_REFINE_DEPTH {
-            info!("max refine depth exceeded during refine_with");
+            debug!("max refine depth exceeded during refine_with");
             //todo: perhaps this should go away.
             // right now it deals with the situation where some large expressions have sizes
             // that are not accurately tracked. These really should get fixed.
@@ -4821,6 +4831,12 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             Expression::TaggedExpression { operand, tag } => {
                 operand.refine_with(path_condition, depth + 1).add_tag(*tag)
             }
+            Expression::Transmute {
+                operand,
+                target_type,
+            } => operand
+                .refine_with(path_condition, depth + 1)
+                .transmute(target_type.clone()),
             Expression::UninterpretedCall {
                 callee,
                 arguments,
@@ -4863,6 +4879,55 @@ impl AbstractValueTrait for Rc<AbstractValue> {
         }
     }
 
+    /// Given a left-hand expression that occurs in a Path that is in a root position, look for an embedded
+    /// path that is rooted in old_root and replace the path with one that is rooted in new_root.
+    #[logfn_inputs(TRACE)]
+    fn replace_embedded_path_root(
+        &self,
+        old_root: &Rc<Path>,
+        new_root: Rc<Path>,
+    ) -> Rc<AbstractValue> {
+        match &self.expression {
+            Expression::ConditionalExpression {
+                condition,
+                consequent,
+                alternate,
+            } => {
+                let replaced_consequent =
+                    consequent.replace_embedded_path_root(old_root, new_root.clone());
+                let replaced_alternate = alternate.replace_embedded_path_root(old_root, new_root);
+                condition.conditional_expression(replaced_consequent, replaced_alternate)
+            }
+            Expression::InitialParameterValue { path, var_type } => {
+                AbstractValue::make_initial_parameter_value(
+                    var_type.clone(),
+                    path.replace_root(old_root, new_root),
+                )
+            }
+            Expression::Reference(path) => {
+                AbstractValue::make_reference(path.replace_root(old_root, new_root))
+            }
+            Expression::Variable { path, var_type } => AbstractValue::make_typed_unknown(
+                var_type.clone(),
+                path.replace_root(old_root, new_root),
+            ),
+            Expression::WidenedJoin { path, operand } => {
+                operand.widen(&path.replace_root(old_root, new_root))
+            }
+            _ => {
+                if self.is_top() || self.is_bottom() {
+                    return self.clone();
+                }
+                unimplemented!(
+                    "replacing embedded path root of {:?}, old_root {:?}, new_root {:?}",
+                    self,
+                    old_root,
+                    new_root
+                );
+            }
+        }
+    }
+
     /// A cast that re-interprets existing bits rather than doing conversions.
     /// When the source type and target types differ in length, bits are truncated
     /// or zero filled as appropriate.
@@ -4870,15 +4935,19 @@ impl AbstractValueTrait for Rc<AbstractValue> {
     fn transmute(&self, target_type: ExpressionType) -> Rc<AbstractValue> {
         if let Expression::CompileTimeConstant(c) = &self.expression {
             Rc::new(c.transmute(target_type).into())
-        } else if target_type.is_integer() {
+        } else if target_type.is_integer() && self.expression.infer_type().is_integer() {
             self.unsigned_modulo(target_type.bit_length())
                 .cast(target_type)
         } else if target_type == ExpressionType::Bool {
             self.unsigned_modulo(target_type.bit_length())
                 .not_equals(Rc::new(ConstantDomain::U128(0).into()))
         } else {
-            // todo: add an expression case that will delay transmutation until the operand refines to a constant
-            AbstractValue::make_typed_unknown(target_type, Path::get_as_path(self.clone()))
+            AbstractValue::make_typed_unary(self.clone(), target_type, |operand, target_type| {
+                Expression::Transmute {
+                    operand,
+                    target_type,
+                }
+            })
         }
     }
 
@@ -5038,6 +5107,7 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             | Expression::Neg { operand }
             | Expression::LogicalNot { operand }
             | Expression::TaggedExpression { operand, .. }
+            | Expression::Transmute { operand, .. }
             | Expression::UnknownTagCheck { operand, .. } => operand.uses(variables),
             Expression::CompileTimeConstant(..) => false,
             Expression::ConditionalExpression {
diff --git a/checker/src/block_visitor.rs b/checker/src/block_visitor.rs
index 0c97d530..5120aa8e 100644
--- a/checker/src/block_visitor.rs
+++ b/checker/src/block_visitor.rs
@@ -124,7 +124,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
     /// Write the RHS Rvalue to the LHS Place.
     #[logfn_inputs(TRACE)]
     fn visit_assign(&mut self, place: &mir::Place<'tcx>, rvalue: &mir::Rvalue<'tcx>) {
-        let mut path = self.visit_place_defer_refinement(place);
+        let mut path = self.visit_lh_place(place);
         match &path.value {
             PathEnum::PhantomData => {
                 // No need to track this data
@@ -147,7 +147,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
         place: &mir::Place<'tcx>,
         variant_index: rustc_target::abi::VariantIdx,
     ) {
-        let target_path = Path::new_discriminant(self.visit_place(place));
+        let target_path = Path::new_discriminant(self.visit_rh_place(place));
         let ty = self
             .bv
             .type_visitor
@@ -453,8 +453,8 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
                     .clone();
                 let func_to_call = Rc::new(func_const.clone().into());
                 let destination = Some((*place, target));
-                let path = self.visit_place(place);
-                let val = self.bv.lookup_path_and_refine_result(path.clone(), ty);
+                let path = self.visit_rh_place(place);
+                let ref_to_path_value = AbstractValue::make_reference(path);
                 let mut call_visitor = CallVisitor::new(
                     self,
                     destructor.did,
@@ -463,7 +463,10 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
                     self.bv.current_environment.clone(),
                     func_const,
                 );
-                call_visitor.actual_args = vec![(path, val)];
+                call_visitor.actual_args = vec![(
+                    Path::new_computed(ref_to_path_value.clone()),
+                    ref_to_path_value,
+                )];
                 call_visitor.actual_argument_types = actual_argument_types;
                 call_visitor.cleanup = unwind;
                 call_visitor.destination = destination;
@@ -1396,7 +1399,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
     /// with place.
     #[logfn_inputs(TRACE)]
     fn visit_used_copy(&mut self, target_path: Rc<Path>, place: &mir::Place<'tcx>) {
-        let rpath = self.visit_place(place);
+        let rpath = self.visit_rh_place(place);
         let rtype = self
             .bv
             .type_visitor
@@ -1410,7 +1413,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
     /// with place, and also remove the (path', value) pair from the environment.
     #[logfn_inputs(TRACE)]
     fn visit_used_move(&mut self, target_path: Rc<Path>, place: &mir::Place<'tcx>) {
-        let rpath = self.visit_place(place);
+        let rpath = self.visit_rh_place(place);
         let rtype = self
             .bv
             .type_visitor
@@ -1441,7 +1444,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
             .bv
             .type_visitor
             .get_path_rustc_type(&path, self.bv.current_span);
-        let value_path = self.visit_place_defer_refinement(place);
+        let value_path = self.visit_lh_place(place);
         let value = match &value_path.value {
             PathEnum::QualifiedPath {
                 qualifier,
@@ -1563,7 +1566,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
             // With more optimization the len instruction becomes a constant.
             self.visit_constant(None, &len)
         } else {
-            let mut value_path = self.visit_place_defer_refinement(place);
+            let mut value_path = self.visit_lh_place(place);
             if let PathEnum::QualifiedPath {
                 qualifier,
                 selector,
@@ -1626,7 +1629,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
                         return;
                     }
                 };
-                let source_path = self.visit_place(place);
+                let source_path = self.visit_rh_place(place);
                 let source_type = self.get_operand_rustc_type(operand);
                 if let PointerCast::Unsize = pointer_cast {
                     // Unsize a pointer/reference value, e.g., `&[T; n]` to`&[T]`.
@@ -1639,7 +1642,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
                             .starts_with_slice_pointer(source_type.kind())
                         {
                             // Need to upgrade the thin pointer to a fat pointer
-                            let target_thin_pointer_path =
+                            let (target_thin_pointer_path, _) =
                                 Path::get_path_to_thin_pointer_at_offset_0(
                                     self.bv.tcx,
                                     &self.bv.current_environment,
@@ -1647,7 +1650,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
                                     ty,
                                 )
                                 .expect("there to be such path because ty starts with it");
-                            let source_thin_pointer_path =
+                            let (source_thin_pointer_path, thin_ptr_type) =
                                 Path::get_path_to_thin_pointer_at_offset_0(
                                     self.bv.tcx,
                                     &self.bv.current_environment,
@@ -1657,10 +1660,6 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
                                 .expect(
                                     "there to be such a path because source_type can cast to target type",
                                 );
-                            let thin_ptr_type = self.bv.type_visitor.get_path_rustc_type(
-                                &source_thin_pointer_path,
-                                self.bv.current_span,
-                            );
                             let target_type = type_visitor::get_target_type(thin_ptr_type);
                             self.bv.copy_or_move_elements(
                                 target_thin_pointer_path.clone(),
@@ -1698,7 +1697,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
                     .visit_operand(operand)
                     .cast(ExpressionType::from(ty.kind()));
                 if let mir::Operand::Move(place) = operand {
-                    let source_path = self.visit_place(place);
+                    let source_path = self.visit_rh_place(place);
                     self.bv.current_environment.value_map =
                         self.bv.current_environment.value_map.remove(&source_path);
                 }
@@ -1866,7 +1865,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
     /// Read the discriminant of an enum and assign to path.
     #[logfn_inputs(TRACE)]
     fn visit_discriminant(&mut self, path: Rc<Path>, place: &mir::Place<'tcx>) {
-        let discriminant_path = Path::new_discriminant(self.visit_place(place));
+        let discriminant_path = Path::new_discriminant(self.visit_rh_place(place));
         let discriminant_value = self
             .bv
             .lookup_path_and_refine_result(discriminant_path, self.bv.tcx.types.u128);
@@ -1927,7 +1926,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
     #[logfn_inputs(TRACE)]
     fn get_operand_path(&mut self, operand: &mir::Operand<'tcx>) -> Rc<Path> {
         match operand {
-            mir::Operand::Copy(place) | mir::Operand::Move(place) => self.visit_place(place),
+            mir::Operand::Copy(place) | mir::Operand::Move(place) => self.visit_rh_place(place),
             mir::Operand::Constant(..) => Path::new_computed(self.visit_operand(operand)),
         }
     }
@@ -1969,7 +1968,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
     /// by construction during build, but also checked by the MIR type checker.
     #[logfn_inputs(TRACE)]
     fn visit_copy(&mut self, place: &mir::Place<'tcx>) -> Rc<AbstractValue> {
-        let path = self.visit_place(place);
+        let path = self.visit_rh_place(place);
         let rust_place_type = self
             .bv
             .type_visitor
@@ -1984,7 +1983,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
     /// `Copy` may be converted to `Move` to enable "last-use" optimizations.
     #[logfn_inputs(TRACE)]
     fn visit_move(&mut self, place: &mir::Place<'tcx>) -> Rc<AbstractValue> {
-        let path = self.visit_place(place);
+        let path = self.visit_rh_place(place);
         let rust_place_type = self
             .bv
             .type_visitor
@@ -2777,7 +2776,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
     /// Returns a normalized Path instance that is the essentially the same as the Place instance, but which
     /// can be serialized and used as a cache key. Also caches the place type with the path as key.
     #[logfn_inputs(TRACE)]
-    pub fn visit_place(&mut self, place: &mir::Place<'tcx>) -> Rc<Path> {
+    pub fn visit_rh_place(&mut self, place: &mir::Place<'tcx>) -> Rc<Path> {
         let place_path = self.get_path_for_place(place);
         let mut path = place_path.canonicalize(&self.bv.current_environment);
         match &place_path.value {
@@ -2843,13 +2842,13 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
         path
     }
 
-    /// Returns a Path instance that is the essentially the same as the Place instance, but which
+    /// Returns a Path instance that is essentially the same as the Place instance, but which
     /// can be serialized and used as a cache key. Also caches the place type with the path as key.
     /// The path is not normalized so deref selectors are left in place until it is determined if
     /// the fat pointer is being dereferenced to get at its target value, or dereferenced to make
     /// a copy of it.
     #[logfn_inputs(TRACE)]
-    pub fn visit_place_defer_refinement(&mut self, place: &mir::Place<'tcx>) -> Rc<Path> {
+    pub fn visit_lh_place(&mut self, place: &mir::Place<'tcx>) -> Rc<Path> {
         self.get_path_for_place(place)
     }
 
@@ -2935,16 +2934,14 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
             let selector = self.visit_projection_elem(ty, elem);
             match elem {
                 mir::ProjectionElem::Deref => {
-                    if let Some(thin_pointer_path) = Path::get_path_to_thin_pointer_at_offset_0(
-                        self.bv.tcx,
-                        &self.bv.current_environment,
-                        &result,
-                        ty,
-                    ) {
-                        let thin_ptr_type = self
-                            .bv
-                            .type_visitor
-                            .get_path_rustc_type(&thin_pointer_path, self.bv.current_span);
+                    if let Some((thin_pointer_path, thin_ptr_type)) =
+                        Path::get_path_to_thin_pointer_at_offset_0(
+                            self.bv.tcx,
+                            &self.bv.current_environment,
+                            &result,
+                            ty,
+                        )
+                    {
                         ty = type_visitor::get_target_type(thin_ptr_type);
                         let deref_path =
                             Path::new_deref(thin_pointer_path, ExpressionType::from(ty.kind()));
@@ -2952,7 +2949,12 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
                             .type_visitor
                             .path_ty_cache
                             .insert(deref_path.clone(), ty);
-                        prev_result = Some(result);
+                        let fat_pointer_target_type = type_visitor::get_target_type(ty);
+                        let fat_pointer_path = Path::new_deref(
+                            result,
+                            ExpressionType::from(fat_pointer_target_type.kind()),
+                        );
+                        prev_result = Some(fat_pointer_path);
                         result = deref_path;
                         continue;
                     }
@@ -2960,6 +2962,13 @@ impl<'block, 'analysis, 'compilation, 'tcx, E>
                 }
                 mir::ProjectionElem::Field(_, field_ty) => {
                     if let Some(prev) = prev_result {
+                        //todo: Actually, field 0 of fat pointer path does not have to mean
+                        //the thin pointer. It looks like we might have to unroll the qualifier
+                        //if the field type is not an actual raw pointer. Perhaps only well known
+                        //types behave like fat pointers. Perhaps also, we might be better off to
+                        // normalize fields into (typed) offsets. At any rate, the code below is wrong.
+                        // Make some test cases.
+
                         // The previous selector was a deref of a fat pointer, which in MIR seems
                         // to be any struct that has a field 0 that is a thin or fat pointer.
                         // When such a path is used as is, or as the qualifier of an index or slice
diff --git a/checker/src/body_visitor.rs b/checker/src/body_visitor.rs
index d64a6deb..b3e700dc 100644
--- a/checker/src/body_visitor.rs
+++ b/checker/src/body_visitor.rs
@@ -29,7 +29,7 @@ use rpds::HashTrieMap;
 use rustc_errors::DiagnosticBuilder;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
-use rustc_middle::ty::{Ty, TyCtxt, TyKind};
+use rustc_middle::ty::{Ty, TyCtxt, TyKind, UintTy};
 use std::collections::{HashMap, HashSet};
 use std::convert::TryFrom;
 use std::fmt::{Debug, Formatter, Result};
@@ -93,7 +93,9 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx
             .summary_cache
             .get_summary_key_for(def_id)
             .clone();
-        let mir = crate_visitor.tcx.optimized_mir(def_id);
+        let id = rustc_middle::ty::WithOptConstParam::unknown(def_id);
+        let def = rustc_middle::ty::InstanceDef::Item(id);
+        let mir = crate_visitor.tcx.instance_mir(def);
         let tcx = crate_visitor.tcx;
         BodyVisitor {
             cv: crate_visitor,
@@ -161,8 +163,8 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx
         function_constant_args: &[(Rc<Path>, Rc<AbstractValue>)],
         parameter_types: &[Ty<'tcx>],
     ) -> Summary {
-        if cfg!(DEBUG) {
-            let mut stdout = std::io::stdout();
+        if !cfg!(DEBUG) {
+            let mut stdout = std::io::sink();
             stdout.write_fmt(format_args!("{:?}", self.def_id)).unwrap();
             rustc_mir::util::write_mir_pretty(self.tcx, Some(self.def_id), &mut stdout).unwrap();
             info!("{:?}", stdout.flush());
@@ -783,6 +785,13 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx
     #[logfn_inputs(TRACE)]
     fn promote_constants(&mut self) -> Environment {
         let mut environment = Environment::default();
+        if matches!(
+            self.tcx.def_kind(self.def_id),
+            rustc_hir::def::DefKind::Variant
+        ) {
+            return environment;
+        }
+        trace!("def_id {:?}", self.tcx.def_kind(self.def_id));
         let saved_mir = self.mir;
         for (ordinal, constant_mir) in self.tcx.promoted_mir(self.def_id).iter().enumerate() {
             self.mir = constant_mir;
@@ -1166,7 +1175,9 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx
                         } = &tpath.value
                         {
                             match selector.as_ref() {
-                                PathSelector::Field(0) | PathSelector::UnionField { .. } => {
+                                PathSelector::Field(0)
+                                | PathSelector::Slice(..)
+                                | PathSelector::UnionField { .. } => {
                                     // assign the pointer field of the slice pointer to the unqualified target
                                     tpath = qualifier.clone();
                                 }
@@ -1174,7 +1185,7 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx
                                     // drop the assignment of the length field
                                     continue;
                                 }
-                                _ => assume_unreachable!("something went wrong here"),
+                                _ => assume_unreachable!("something went wrong here: {:?}", tpath),
                             }
                         }
                     }
@@ -2003,15 +2014,6 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx
         // be saddled with removing it. This case corresponds to no_children being true.
         if val_type == ExpressionType::NonPrimitive || val_type == ExpressionType::Function {
             // First look at paths that are rooted in rpath.
-            // Remove an explicit deref from source_path to make it a valid root.
-            let source_path = match &source_path.value {
-                PathEnum::QualifiedPath {
-                    qualifier,
-                    selector,
-                    ..
-                } if **selector == PathSelector::Deref => qualifier.clone(),
-                _ => source_path,
-            };
             let value_map = self.current_environment.value_map.clone();
             for (path, value) in value_map
                 .iter()
@@ -2064,7 +2066,7 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx
                 // The value is a string literal. See if the target will treat it as &[u8].
                 if let TyKind::Ref(_, ty, _) = root_rustc_type.kind() {
                     if let TyKind::Slice(elem_ty) = ty.kind() {
-                        if let TyKind::Uint(rustc_ast::ast::UintTy::U8) = elem_ty.kind() {
+                        if let TyKind::Uint(UintTy::U8) = elem_ty.kind() {
                             self.expand_aliased_string_literals_if_appropriate(
                                 &target_path,
                                 &value,
@@ -2511,8 +2513,14 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx
     ) -> (Rc<Path>, Rc<AbstractValue>) {
         precondition!(!root_rustc_type.is_scalar());
 
-        let tag_field_path =
-            Path::new_tag_field(qualifier.clone()).canonicalize(&self.current_environment);
+        let target_type = type_visitor::get_target_type(root_rustc_type);
+        let tag_field_path = if target_type != root_rustc_type {
+            let target_type = ExpressionType::from(target_type.kind());
+            Path::new_tag_field(Path::new_deref(qualifier.clone(), target_type))
+                .canonicalize(&self.current_environment)
+        } else {
+            Path::new_tag_field(qualifier.clone()).canonicalize(&self.current_environment)
+        };
         let mut tag_field_value = self.lookup_path_and_refine_result(
             tag_field_path.clone(),
             self.type_visitor.dummy_untagged_value_type,
diff --git a/checker/src/call_visitor.rs b/checker/src/call_visitor.rs
index b7fb3f0c..d8a8d88b 100644
--- a/checker/src/call_visitor.rs
+++ b/checker/src/call_visitor.rs
@@ -5,11 +5,10 @@
 
 use log_derive::*;
 use mirai_annotations::*;
-use rustc_ast::ast;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
 use rustc_middle::ty::subst::{GenericArg, GenericArgKind, SubstsRef};
-use rustc_middle::ty::{AdtDef, Ty, TyCtxt, TyKind};
+use rustc_middle::ty::{AdtDef, Ty, TyCtxt, TyKind, UintTy};
 use std::collections::HashMap;
 use std::fmt::{Debug, Formatter, Result};
 use std::rc::Rc;
@@ -338,7 +337,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
                 .bv
                 .type_visitor
                 .get_rustc_place_type(place, self.block_visitor.bv.current_span);
-            let target_path = self.block_visitor.visit_place(place);
+            let target_path = self.block_visitor.visit_rh_place(place);
             if !summary.is_computed {
                 self.deal_with_missing_summary();
                 // Now just do a deep copy and carry on.
@@ -450,7 +449,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
             }
             KnownNames::MiraiResult => {
                 if let Some((place, _)) = &self.destination {
-                    let target_path = self.block_visitor.visit_place(place);
+                    let target_path = self.block_visitor.visit_rh_place(place);
                     let target_rustc_type = self
                         .block_visitor
                         .bv
@@ -547,7 +546,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
                 let result = self.try_to_inline_special_function();
                 if !result.is_bottom() {
                     if let Some((place, _)) = &self.destination {
-                        let target_path = self.block_visitor.visit_place(place);
+                        let target_path = self.block_visitor.visit_rh_place(place);
                         self.block_visitor
                             .bv
                             .current_environment
@@ -1014,7 +1013,15 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
         let mut argument_map = self.callee_generic_argument_map.clone();
         if closure_ty.is_closure() {
             if self.callee_known_name != KnownNames::StdSyncOnceCallOnce {
-                actual_args.insert(0, self.actual_args[0].clone());
+                let closure_path = self.actual_args[0].0.clone();
+                let closure_reference = AbstractValue::make_reference(closure_path);
+                actual_args.insert(
+                    0,
+                    (
+                        Path::get_as_path(closure_reference.clone()),
+                        closure_reference,
+                    ),
+                );
                 actual_argument_types.insert(0, closure_ref_ty);
             }
             //todo: could this be a generator?
@@ -1092,7 +1099,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
     #[logfn_inputs(TRACE)]
     fn handle_abstract_value(&mut self) {
         if let Some((place, target)) = &self.destination {
-            let path = self.block_visitor.visit_place(place);
+            let path = self.block_visitor.visit_rh_place(place);
             let expression_type = self
                 .block_visitor
                 .bv
@@ -1131,13 +1138,13 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
             let target_type = ExpressionType::from(
                 type_visitor::get_target_type(self.actual_argument_types[0]).kind(),
             );
-            let source_thin_pointer_path = Path::get_path_to_thin_pointer_at_offset_0(
+            let (source_thin_pointer_path, _) = Path::get_path_to_thin_pointer_at_offset_0(
                 self.block_visitor.bv.tcx,
                 &self.block_visitor.bv.current_environment,
                 &source_pointer_path,
                 source_pointer_rustc_type,
             )
-            .unwrap_or(source_pointer_path);
+            .unwrap_or((source_pointer_path, source_pointer_rustc_type));
             let source_path = Path::new_deref(source_thin_pointer_path, target_type)
                 .canonicalize(&self.block_visitor.bv.current_environment);
             trace!("MiraiAddTag: tagging {:?} with {:?}", tag, source_path);
@@ -1219,13 +1226,13 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
             let target_type = ExpressionType::from(
                 type_visitor::get_target_type(self.actual_argument_types[0]).kind(),
             );
-            let source_thin_pointer_path = Path::get_path_to_thin_pointer_at_offset_0(
+            let (source_thin_pointer_path, _) = Path::get_path_to_thin_pointer_at_offset_0(
                 self.block_visitor.bv.tcx,
                 &self.block_visitor.bv.current_environment,
                 &source_pointer_path,
                 source_pointer_rustc_type,
             )
-            .unwrap_or(source_pointer_path);
+            .unwrap_or((source_pointer_path, source_pointer_rustc_type));
             let source_path = Path::new_deref(source_thin_pointer_path, target_type)
                 .canonicalize(&self.block_visitor.bv.current_environment);
             trace!(
@@ -1338,7 +1345,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
         // Return the abstract result and update exit conditions.
         let destination = &self.destination;
         if let Some((place, _)) = destination {
-            let target_path = self.block_visitor.visit_place(place);
+            let target_path = self.block_visitor.visit_rh_place(place);
             self.block_visitor.bv.current_environment.update_value_at(
                 target_path.clone(),
                 result.unwrap_or_else(|| {
@@ -1378,7 +1385,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
             let source_path = Path::new_model_field(qualifier, field_name)
                 .canonicalize(&self.block_visitor.bv.current_environment);
 
-            let target_path = self.block_visitor.visit_place(place);
+            let target_path = self.block_visitor.visit_rh_place(place);
             if self
                 .block_visitor
                 .bv
@@ -1655,7 +1662,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
                     }
                 }
             }
-            let target_path = self.block_visitor.visit_place(place);
+            let target_path = self.block_visitor.visit_rh_place(place);
             self.block_visitor
                 .bv
                 .current_environment
@@ -1797,7 +1804,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
                 KnownNames::StdIntrinsicsMulWithOverflow => mir::BinOp::Mul,
                 _ => assume_unreachable!(),
             };
-            let target_path = self.block_visitor.visit_place(target_place);
+            let target_path = self.block_visitor.visit_rh_place(target_place);
             let path0 = Path::new_field(target_path.clone(), 0);
             let path1 = Path::new_field(target_path.clone(), 1);
             let target_type = self
@@ -1880,7 +1887,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
         .canonicalize(&self.block_visitor.bv.current_environment);
         let source_path = &Path::get_as_path(self.actual_args[1].1.clone());
         if let Some((place, _)) = &self.destination {
-            let target_path = self.block_visitor.visit_place(place);
+            let target_path = self.block_visitor.visit_rh_place(place);
             let root_rustc_type = self
                 .block_visitor
                 .bv
@@ -1920,7 +1927,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
                 return Rc::new((ty_and_layout.layout.size.bytes() as u128).into());
             }
         }
-        let path = self.block_visitor.visit_place(
+        let path = self.block_visitor.visit_rh_place(
             &self
                 .destination
                 .expect("std::intrinsics::size_of should have a destination")
@@ -1948,12 +1955,12 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
     fn handle_min_align_of_val(&mut self) -> Rc<AbstractValue> {
         let param_env = self.block_visitor.bv.tcx.param_env(self.callee_def_id);
         checked_assume!(self.actual_argument_types.len() == 1);
-        let t = self.actual_argument_types[0];
+        let t = type_visitor::get_target_type(self.actual_argument_types[0]);
         if let Ok(ty_and_layout) = self.block_visitor.bv.tcx.layout_of(param_env.and(t)) {
             return Rc::new((ty_and_layout.layout.align.abi.bytes() as u128).into());
         }
         // todo: need an expression that resolves to the value size once the value is known (typically after call site refinement).
-        let path = self.block_visitor.visit_place(
+        let path = self.block_visitor.visit_rh_place(
             &self
                 .destination
                 .expect("std::intrinsics::min_align_of_val should have a destination")
@@ -2013,7 +2020,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
             }
         }
         // todo: need an expression that resolves to the value size once the value is known (typically after call site refinement).
-        let path = self.block_visitor.visit_place(
+        let path = self.block_visitor.visit_rh_place(
             &self
                 .destination
                 .expect("std::intrinsics::size_of_value should have a destination")
@@ -2042,7 +2049,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
             .expect("rustc type error")
             .expect_ty();
         if let Some((place, _)) = &self.destination {
-            let mut target_path = self.block_visitor.visit_place(place);
+            let mut target_path = self.block_visitor.visit_rh_place(place);
             let target_rustc_type = self
                 .block_visitor
                 .bv
@@ -2056,7 +2063,8 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
                     &source_path,
                     source_rustc_type,
                 )
-                .unwrap_or(source_path);
+                .unwrap_or((source_path, target_rustc_type))
+                .0;
             } else if type_visitor::is_thin_pointer(&source_rustc_type.kind()) {
                 target_path = Path::get_path_to_thin_pointer_at_offset_0(
                     self.block_visitor.bv.tcx,
@@ -2064,7 +2072,8 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
                     &target_path,
                     target_rustc_type,
                 )
-                .unwrap_or(target_path);
+                .unwrap_or((target_path, source_rustc_type))
+                .0;
             }
 
             fn add_leaf_fields_for<'a>(
@@ -2109,6 +2118,20 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
                     );
                     self.copy_field_bits(source_fields, target_fields);
                 }
+                (TyKind::Float(..), TyKind::Uint(..))
+                | (TyKind::Float(..), TyKind::Int(..))
+                | (TyKind::Uint(..), TyKind::Float(..))
+                | (TyKind::Int(..), TyKind::Float(..)) => {
+                    let val = self
+                        .block_visitor
+                        .bv
+                        .lookup_path_and_refine_result(source_path, source_rustc_type);
+                    let target_expression_type = ExpressionType::from(target_rustc_type.kind());
+                    self.block_visitor
+                        .bv
+                        .current_environment
+                        .update_value_at(target_path, val.transmute(target_expression_type));
+                }
                 _ => {
                     self.block_visitor.bv.copy_or_move_elements(
                         target_path,
@@ -2525,7 +2548,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
         let destination = self.destination;
         if let Some((place, _)) = &destination {
             // Assign function result to place
-            let target_path = self.block_visitor.visit_place(place);
+            let target_path = self.block_visitor.visit_rh_place(place);
             let result_path = &Some(target_path.clone());
             let return_value_path = Path::new_result();
 
@@ -2611,7 +2634,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
     pub fn add_post_condition_to_exit_conditions(&mut self, function_summary: &Summary) {
         let destination = self.destination;
         if let Some((place, target)) = &destination {
-            let target_path = self.block_visitor.visit_place(place);
+            let target_path = self.block_visitor.visit_rh_place(place);
             let result_path = &Some(target_path);
             let mut exit_condition = self
                 .block_visitor
@@ -2783,7 +2806,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E>
                 let tag_propagation_set_rustc_const;
                 match tag_substs_ref[0].unpack() {
                     GenericArgKind::Const(rustc_const)
-                        if *rustc_const.ty.kind() == TyKind::Uint(ast::UintTy::U128) =>
+                        if *rustc_const.ty.kind() == TyKind::Uint(UintTy::U128) =>
                     {
                         tag_propagation_set_rustc_const = rustc_const
                     }
diff --git a/checker/src/callbacks.rs b/checker/src/callbacks.rs
index 374b9260..8f06fa40 100644
--- a/checker/src/callbacks.rs
+++ b/checker/src/callbacks.rs
@@ -139,33 +139,14 @@ impl MiraiCallbacks {
     }
 
     fn is_excluded(file_name: &str) -> bool {
-        file_name.contains("common/logger/src")
-        || file_name.contains("config/src")    
-        || file_name.contains("config/management/src")    
-        || file_name.contains("config/management/operational/src")
-        || file_name.contains("config/management/genesis/src")
-        || file_name.contains("language/bytecode-verifier/src")
-        || file_name.contains("language/compiler/src")
-        || file_name.contains("language/compiler/ir-to-bytecode/src")
-        || file_name.contains("language/compiler/ir-to-bytecode/syntax/src")
-        || file_name.contains("language/diem-tools/diem-events-fetcher/src")
-        || file_name.contains("language/diem-vm/src")
-        || file_name.contains("language/move-lang/src")
-        || file_name.contains("language/move-model/src")
-        || file_name.contains("language/move-prover/src") // compiler panic
-        || file_name.contains("language/move-prover/bytecode/src")
-        || file_name.contains("language/move-prover/abigen/src")
-        || file_name.contains("language/move-prover/docgen/src")
-        || file_name.contains("language/move-prover/spec-lang/src") // compiler panic
-        || file_name.contains("language/move-vm/test-utils/src")
-        || file_name.contains("language/stdlib/src")
-        || file_name.contains("language/tools/move-cli/src")
-        || file_name.contains("language/tools/move-coverage/src")
-        || file_name.contains("language/libra-tools/transaction-replay/src")
-        || file_name.contains("language/vm/src")
-        || file_name.contains("secure/push-metrics/src")
-        || file_name.contains("state-synchronizer/src") // Z3 encoding error 
-        || file_name.contains("storage/diemdb/src")
+        file_name.contains("config/management/src") // too slow
+        || file_name.contains("language/bytecode-verifier/src") // too slow
+        || file_name.contains("language/move-lang/src") // probably does not terminate
+        || file_name.contains("language/move-model/src") // too slow
+        || file_name.contains("language/move-prover/bytecode/src") // too slow
+        || file_name.contains("language/tools/move-coverage/src") /* probably does not terminate */
+        || file_name.contains("language/vm/src") // too slow
+        || file_name.contains("types/src") // too slow
     }
 
     /// Analyze the crate currently being compiled, using the information given in compiler and tcx.
diff --git a/checker/src/expression.rs b/checker/src/expression.rs
index 69a0c5f6..242a4b93 100644
--- a/checker/src/expression.rs
+++ b/checker/src/expression.rs
@@ -12,8 +12,7 @@ use crate::type_visitor;
 
 use log_derive::*;
 use mirai_annotations::*;
-use rustc_ast::ast;
-use rustc_middle::ty::{Ty, TyCtxt, TyKind};
+use rustc_middle::ty::{FloatTy, IntTy, Ty, TyCtxt, TyKind, UintTy};
 use serde::{Deserialize, Serialize};
 use std::collections::HashSet;
 use std::fmt::{Debug, Formatter, Result};
@@ -363,6 +362,12 @@ pub enum Expression {
         tag: Tag,
     },
 
+    /// An expression that interprets the bits of operand as being a value of the target type
+    Transmute {
+        operand: Rc<AbstractValue>,
+        target_type: ExpressionType,
+    },
+
     /// An expression that represents the result of calling an unknown function.
     /// Typically this will be a trait method, function parameter, or an intrinsic/foreign function.
     /// In the case of a trait method or a function parameter, the caller might be able to refine
@@ -591,6 +596,10 @@ impl Debug for Expression {
             Expression::TaggedExpression { operand, tag } => {
                 f.write_fmt(format_args!("{:?} tagged with {:?}", operand, tag))
             }
+            Expression::Transmute {
+                operand,
+                target_type,
+            } => f.write_fmt(format_args!("transmute({:?}, {:?})", operand, target_type)),
             Expression::UninterpretedCall {
                 callee,
                 arguments,
@@ -667,9 +676,8 @@ impl Expression {
             | Expression::Cast { operand, .. }
             | Expression::IntrinsicBitVectorUnary { operand, .. }
             | Expression::IntrinsicFloatingPointUnary { operand, .. }
-            | Expression::TaggedExpression { operand, .. } => {
-                operand.expression.contains_local_variable()
-            }
+            | Expression::TaggedExpression { operand, .. }
+            | Expression::Transmute { operand, .. } => operand.expression.contains_local_variable(),
             Expression::Bottom => true,
 
             Expression::CompileTimeConstant(..) => false,
@@ -767,9 +775,8 @@ impl Expression {
             | Expression::Cast { operand, .. }
             | Expression::IntrinsicBitVectorUnary { operand, .. }
             | Expression::IntrinsicFloatingPointUnary { operand, .. }
-            | Expression::TaggedExpression { operand, .. } => {
-                operand.expression.contains_parameter()
-            }
+            | Expression::TaggedExpression { operand, .. }
+            | Expression::Transmute { operand, .. } => operand.expression.contains_parameter(),
             Expression::Bottom => true,
 
             Expression::CompileTimeConstant(..) => false,
@@ -864,9 +871,8 @@ impl Expression {
             | Expression::Cast { operand, .. }
             | Expression::IntrinsicBitVectorUnary { operand, .. }
             | Expression::IntrinsicFloatingPointUnary { operand, .. }
-            | Expression::TaggedExpression { operand, .. } => {
-                operand.expression.contains_widened_join()
-            }
+            | Expression::TaggedExpression { operand, .. }
+            | Expression::Transmute { operand, .. } => operand.expression.contains_widened_join(),
             Expression::Bottom => false,
 
             Expression::CompileTimeConstant(..) => false,
@@ -981,6 +987,7 @@ impl Expression {
             Expression::SubOverflows { .. } => Some(TagPropagation::SubOverflows),
             Expression::Switch { .. } => None,
             Expression::TaggedExpression { .. } => None,
+            Expression::Transmute { .. } => Some(TagPropagation::Transmute),
             Expression::UninterpretedCall { .. } => Some(TagPropagation::UninterpretedCall),
             Expression::UnknownModelField { .. } => None,
             Expression::UnknownTagCheck { .. } => None,
@@ -1122,6 +1129,7 @@ impl Expression {
             Expression::SubOverflows { .. } => Bool,
             Expression::Switch { default, .. } => default.expression.infer_type(),
             Expression::TaggedExpression { operand, .. } => operand.expression.infer_type(),
+            Expression::Transmute { target_type, .. } => target_type.clone(),
             Expression::UninterpretedCall { result_type, .. } => result_type.clone(),
             Expression::UnknownModelField { default, .. } => default.expression.infer_type(),
             Expression::UnknownTagCheck { .. } => Bool,
@@ -1212,6 +1220,7 @@ impl Expression {
             | Expression::Neg { operand }
             | Expression::LogicalNot { operand }
             | Expression::TaggedExpression { operand, .. }
+            | Expression::Transmute { operand, .. }
             | Expression::UnknownTagCheck { operand, .. } => {
                 operand.expression.record_heap_blocks_and_strings(result);
             }
@@ -1341,20 +1350,20 @@ impl<'a> From<&TyKind<'a>> for ExpressionType {
         match ty_kind {
             TyKind::Bool => ExpressionType::Bool,
             TyKind::Char => ExpressionType::Char,
-            TyKind::Int(ast::IntTy::Isize) => ExpressionType::Isize,
-            TyKind::Int(ast::IntTy::I8) => ExpressionType::I8,
-            TyKind::Int(ast::IntTy::I16) => ExpressionType::I16,
-            TyKind::Int(ast::IntTy::I32) => ExpressionType::I32,
-            TyKind::Int(ast::IntTy::I64) => ExpressionType::I64,
-            TyKind::Int(ast::IntTy::I128) => ExpressionType::I128,
-            TyKind::Uint(ast::UintTy::Usize) => ExpressionType::Usize,
-            TyKind::Uint(ast::UintTy::U8) => ExpressionType::U8,
-            TyKind::Uint(ast::UintTy::U16) => ExpressionType::U16,
-            TyKind::Uint(ast::UintTy::U32) => ExpressionType::U32,
-            TyKind::Uint(ast::UintTy::U64) => ExpressionType::U64,
-            TyKind::Uint(ast::UintTy::U128) => ExpressionType::U128,
-            TyKind::Float(ast::FloatTy::F32) => ExpressionType::F32,
-            TyKind::Float(ast::FloatTy::F64) => ExpressionType::F64,
+            TyKind::Int(IntTy::Isize) => ExpressionType::Isize,
+            TyKind::Int(IntTy::I8) => ExpressionType::I8,
+            TyKind::Int(IntTy::I16) => ExpressionType::I16,
+            TyKind::Int(IntTy::I32) => ExpressionType::I32,
+            TyKind::Int(IntTy::I64) => ExpressionType::I64,
+            TyKind::Int(IntTy::I128) => ExpressionType::I128,
+            TyKind::Uint(UintTy::Usize) => ExpressionType::Usize,
+            TyKind::Uint(UintTy::U8) => ExpressionType::U8,
+            TyKind::Uint(UintTy::U16) => ExpressionType::U16,
+            TyKind::Uint(UintTy::U32) => ExpressionType::U32,
+            TyKind::Uint(UintTy::U64) => ExpressionType::U64,
+            TyKind::Uint(UintTy::U128) => ExpressionType::U128,
+            TyKind::Float(FloatTy::F32) => ExpressionType::F32,
+            TyKind::Float(FloatTy::F64) => ExpressionType::F64,
             TyKind::Dynamic(..)
             | TyKind::Foreign(..)
             | TyKind::FnDef(..)
diff --git a/checker/src/lib.rs b/checker/src/lib.rs
index 02bf1103..13aa1fad 100644
--- a/checker/src/lib.rs
+++ b/checker/src/lib.rs
@@ -16,7 +16,6 @@
 #![feature(box_patterns)]
 #![feature(box_syntax)]
 #![feature(core_intrinsics)]
-#![feature(vec_remove_item)]
 
 extern crate rustc_ast;
 extern crate rustc_data_structures;
diff --git a/checker/src/path.rs b/checker/src/path.rs
index 2e8c804c..291732cf 100644
--- a/checker/src/path.rs
+++ b/checker/src/path.rs
@@ -92,7 +92,7 @@ impl Path {
     /// When splitting paths while doing weak updates, it is important to not refine paths because
     /// they are already canonical and because doing so can lead to recursive loops as refined paths
     /// re-introduce joined paths that have been split earlier.
-    /// A split path, however, can be serve as the qualifier of a newly constructed qualified path
+    /// A split path, however, can serve as the qualifier of a newly constructed qualified path
     /// and the qualified path might not be canonical. This routine tries to remove the two sources of
     /// de-canonicalization that are currently know. Essentially: when a path that binds to a value
     /// that is a reference is implicitly dereferenced by the selector, the canonical path will
@@ -103,7 +103,7 @@ impl Path {
     /// If the function returns a re-canonicalized path, which is used as the qualifier of a newly
     /// constructed qualified path, the caller of this function should check if the selector of the
     /// qualified path is `PathSelector::Deref`. If so, the deref selector should also be removed.
-    #[logfn_inputs(DEBUG)]
+    #[logfn_inputs(TRACE)]
     pub fn try_to_dereference(path: &Rc<Path>, environment: &Environment) -> Option<Rc<Path>> {
         if let PathEnum::Computed { value } = &path.value {
             if let Expression::Reference(path) = &value.expression {
@@ -373,7 +373,7 @@ impl Path {
         environment: &Environment,
         path: &Rc<Path>,
         path_rustc_type: Ty<'tcx>,
-    ) -> Option<Rc<Path>> {
+    ) -> Option<(Rc<Path>, Ty<'tcx>)> {
         trace!(
             "get_path_to_thin_pointer_at_offset_0 {:?} {:?}",
             path,
@@ -382,12 +382,20 @@ impl Path {
         match path_rustc_type.kind() {
             TyKind::Ref(..) | TyKind::RawPtr(..) => {
                 if type_visitor::is_slice_pointer(path_rustc_type.kind()) {
-                    Some(Path::new_field(path.clone(), 0))
+                    let elem_t = type_visitor::get_element_type(path_rustc_type);
+                    let ft = tcx.mk_ptr(rustc_middle::ty::TypeAndMut {
+                        ty: elem_t,
+                        mutbl: rustc_hir::Mutability::Not,
+                    });
+                    Some((Path::new_field(path.clone(), 0), ft))
                 } else {
-                    Some(path.clone())
+                    Some((path.clone(), path_rustc_type))
                 }
             }
             TyKind::Adt(def, substs) => {
+                if def.is_enum() {
+                    return None;
+                }
                 let path0 = Path::new_field(path.clone(), 0);
                 for v in def.variants.iter() {
                     if let Some(field0) = v.fields.get(0) {
@@ -631,17 +639,6 @@ impl Path {
     #[logfn_inputs(TRACE)]
     pub fn new_discriminant(enum_path: Rc<Path>) -> Rc<Path> {
         let selector = Rc::new(PathSelector::Discriminant);
-        if let PathEnum::QualifiedPath {
-            qualifier: base_qualifier,
-            selector: base_selector,
-            ..
-        } = &enum_path.value
-        {
-            if *base_selector.as_ref() == PathSelector::Deref {
-                // no need for an explicit deref in a qualifier
-                return Path::new_qualified(base_qualifier.clone(), selector);
-            }
-        }
         Self::new_qualified(enum_path, selector)
     }
 
@@ -649,17 +646,6 @@ impl Path {
     #[logfn_inputs(TRACE)]
     pub fn new_field(qualifier: Rc<Path>, field_index: usize) -> Rc<Path> {
         let selector = Rc::new(PathSelector::Field(field_index));
-        if let PathEnum::QualifiedPath {
-            qualifier: base_qualifier,
-            selector: base_selector,
-            ..
-        } = &qualifier.value
-        {
-            if *base_selector.as_ref() == PathSelector::Deref {
-                // no need for an explicit deref in a qualifier
-                return Path::new_qualified(base_qualifier.clone(), selector);
-            }
-        }
         Self::new_qualified(qualifier, selector)
     }
 
@@ -677,17 +663,6 @@ impl Path {
     #[logfn_inputs(TRACE)]
     pub fn new_index(collection_path: Rc<Path>, index_value: Rc<AbstractValue>) -> Rc<Path> {
         let selector = Rc::new(PathSelector::Index(index_value));
-        if let PathEnum::QualifiedPath {
-            qualifier: base_qualifier,
-            selector: base_selector,
-            ..
-        } = &collection_path.value
-        {
-            if *base_selector.as_ref() == PathSelector::Deref {
-                // no need for an explicit deref in a qualifier
-                return Path::new_qualified(base_qualifier.clone(), selector);
-            }
-        }
         Self::new_qualified(collection_path, selector)
     }
 
@@ -753,17 +728,6 @@ impl Path {
     #[logfn_inputs(TRACE)]
     pub fn new_length(array_path: Rc<Path>) -> Rc<Path> {
         let selector = Rc::new(PathSelector::Field(1));
-        if let PathEnum::QualifiedPath {
-            qualifier: base_qualifier,
-            selector: base_selector,
-            ..
-        } = &array_path.value
-        {
-            if *base_selector.as_ref() == PathSelector::Deref {
-                // no need for an explicit deref in a qualifier
-                return Path::new_qualified(base_qualifier.clone(), selector);
-            }
-        }
         Self::new_qualified(array_path, selector)
     }
 
@@ -978,18 +942,6 @@ impl PathRefinement for Rc<Path> {
         } = &self.value
         {
             let canonical_qualifier = qualifier.canonicalize(environment);
-            // (*p).q is equivalent to p.q, etc.
-            if let PathEnum::QualifiedPath {
-                qualifier: base_qualifier,
-                selector: base_selector,
-                ..
-            } = &canonical_qualifier.value
-            {
-                if *base_selector.as_ref() == PathSelector::Deref {
-                    // no need for an explicit deref in a qualifier
-                    return Path::new_qualified(base_qualifier.clone(), selector.clone());
-                }
-            }
             // If the canonical qualifier binds to a special value, we may need to deconstruct that
             // value before constructing the qualified path.
             let qualifier_as_value =
@@ -1006,18 +958,13 @@ impl PathRefinement for Rc<Path> {
                     // address of the parameter, which is the same in the pre and post state,
                     // but is it true in other cases?
                     Expression::InitialParameterValue { path, .. } => {
-                        if let PathEnum::QualifiedPath {
-                            qualifier,
-                            selector: qs,
-                            ..
-                        } = &path.value
-                        {
+                        if let PathEnum::QualifiedPath { selector: qs, .. } = &path.value {
                             if *qs.as_ref() == PathSelector::Deref {
-                                // old(q.deref).s => old(q.s)
+                                // old(q.deref).s => old(q.deref.s)
                                 return Path::new_computed(
                                     AbstractValue::make_initial_parameter_value(
                                         ExpressionType::ThinPointer,
-                                        Path::new_qualified(qualifier.clone(), selector.clone()),
+                                        Path::new_qualified(path.clone(), selector.clone()),
                                     ),
                                 );
                             }
@@ -1037,6 +984,9 @@ impl PathRefinement for Rc<Path> {
                         return Path::new_qualified(p.clone(), selector.clone())
                             .canonicalize(environment);
                     }
+                    Expression::Variable { path, .. } => {
+                        return Path::new_qualified(path.clone(), selector.clone());
+                    }
                     _ => {}
                 }
             }
@@ -1103,59 +1053,18 @@ impl PathRefinement for Rc<Path> {
             return new_root;
         }
         match &self.value {
-            PathEnum::Computed { value } => match &value.expression {
-                Expression::InitialParameterValue { path, .. } => {
-                    path.replace_root(old_root, new_root)
-                }
-                Expression::Reference(path) => Path::new_computed(AbstractValue::make_reference(
-                    path.replace_root(old_root, new_root),
-                )),
-                Expression::Variable { path, var_type } => {
-                    Path::new_computed(AbstractValue::make_typed_unknown(
-                        var_type.clone(),
-                        path.replace_root(old_root, new_root),
-                    ))
-                }
-                _ => {
-                    if value.is_top() || value.is_bottom() {
-                        return self.clone();
-                    }
-                    unimplemented!(
-                        "replacing root of {:?}, old_root {:?}, new_root {:?}",
-                        self,
-                        old_root,
-                        new_root
-                    );
-                }
-            },
+            PathEnum::Computed { value } => {
+                Path::new_computed(value.replace_embedded_path_root(old_root, new_root))
+            }
             PathEnum::Offset { value } => {
                 if let Expression::Offset { left, right } = &value.expression {
-                    match &left.expression {
-                        Expression::InitialParameterValue { path, var_type }
-                        | Expression::Variable { path, var_type } => {
-                            let replaced_left = AbstractValue::make_typed_unknown(
-                                var_type.clone(),
-                                path.replace_root(old_root, new_root),
-                            );
-                            let replaced_offset = replaced_left.offset(right.clone());
-                            return Path::get_as_path(replaced_offset);
-                        }
-                        Expression::Reference(path) => {
-                            let replaced_left = AbstractValue::make_reference(
-                                path.replace_root(old_root, new_root),
-                            );
-                            let replaced_offset = replaced_left.offset(right.clone());
-                            return Path::get_as_path(replaced_offset);
-                        }
-                        _ => {}
-                    }
+                    let replaced_left = left.replace_embedded_path_root(old_root, new_root);
+                    Path::get_as_path(replaced_left.offset(right.clone()))
+                } else {
+                    assume_unreachable!(
+                        "PathEnum::Offset has value that is not Expression::Offset"
+                    );
                 }
-                unimplemented!(
-                    "replacing root of {:?}, old_root {:?}, new_root {:?}",
-                    self,
-                    old_root,
-                    new_root
-                );
             }
             PathEnum::QualifiedPath {
                 qualifier,
diff --git a/checker/src/type_visitor.rs b/checker/src/type_visitor.rs
index 127f0966..bbaddb3c 100644
--- a/checker/src/type_visitor.rs
+++ b/checker/src/type_visitor.rs
@@ -76,14 +76,20 @@ impl<'analysis, 'compilation, 'tcx> TypeVisitor<'tcx> {
         path: &Rc<Path>,
         first_state: &mut Environment,
     ) {
+        let mut is_ref = false;
         if let TyKind::Ref(_, t, _) = path_ty.kind() {
+            is_ref = true;
             path_ty = t;
         }
         match path_ty.kind() {
             TyKind::Closure(_, substs) => {
                 for (i, ty) in substs.as_closure().upvar_tys().enumerate() {
                     let var_type: ExpressionType = ty.kind().into();
-                    let closure_field_path = Path::new_field(path.clone(), i);
+                    let mut qualifier = path.clone();
+                    if is_ref {
+                        qualifier = Path::new_deref(path.clone(), ExpressionType::NonPrimitive)
+                    }
+                    let closure_field_path = Path::new_field(qualifier, i);
                     self.path_ty_cache.insert(closure_field_path.clone(), ty);
                     let closure_field_val =
                         AbstractValue::make_typed_unknown(var_type, closure_field_path.clone());
@@ -92,8 +98,11 @@ impl<'analysis, 'compilation, 'tcx> TypeVisitor<'tcx> {
                         .insert_mut(closure_field_path, closure_field_val);
                 }
             }
-            TyKind::Opaque(def_id, ..) => {
-                self.add_any_closure_fields_for(self.tcx.type_of(*def_id), path, first_state);
+            TyKind::Opaque(def_id, substs) => {
+                let map = self.get_generic_arguments_map(*def_id, substs, &[]);
+                let path_ty =
+                    self.specialize_generic_argument_type(self.tcx.type_of(*def_id), &map);
+                self.add_any_closure_fields_for(path_ty, path, first_state);
             }
             TyKind::FnDef(..) | TyKind::FnPtr(..) => {}
             _ => {
diff --git a/checker/src/utils.rs b/checker/src/utils.rs
index 3b14e0ba..4a6e14bd 100644
--- a/checker/src/utils.rs
+++ b/checker/src/utils.rs
@@ -13,7 +13,7 @@ use rustc_hir::{ItemKind, Node};
 use rustc_middle::ty;
 use rustc_middle::ty::print::{FmtPrinter, Printer};
 use rustc_middle::ty::subst::{GenericArgKind, SubstsRef};
-use rustc_middle::ty::{DefIdTree, ProjectionTy, Ty, TyCtxt, TyKind};
+use rustc_middle::ty::{DefIdTree, FloatTy, IntTy, ProjectionTy, Ty, TyCtxt, TyKind, UintTy};
 use std::rc::Rc;
 
 /// Returns the location of the rust system binaries that are associated with this build of Mirai.
@@ -97,35 +97,34 @@ pub fn argument_types_key_str<'tcx>(
 /// generic trait methods).
 fn append_mangled_type<'tcx>(str: &mut String, ty: Ty<'tcx>, tcx: TyCtxt<'tcx>) {
     trace!("append_mangled_type {:?} to {}", ty.kind(), str);
-    use rustc_ast::ast;
     use TyKind::*;
     match ty.kind() {
         Bool => str.push_str("bool"),
         Char => str.push_str("char"),
         Int(int_ty) => {
             str.push_str(match int_ty {
-                ast::IntTy::Isize => "isize",
-                ast::IntTy::I8 => "i8",
-                ast::IntTy::I16 => "i16",
-                ast::IntTy::I32 => "i32",
-                ast::IntTy::I64 => "i64",
-                ast::IntTy::I128 => "i128",
+                IntTy::Isize => "isize",
+                IntTy::I8 => "i8",
+                IntTy::I16 => "i16",
+                IntTy::I32 => "i32",
+                IntTy::I64 => "i64",
+                IntTy::I128 => "i128",
             });
         }
         Uint(uint_ty) => {
             str.push_str(match uint_ty {
-                ast::UintTy::Usize => "usize",
-                ast::UintTy::U8 => "u8",
-                ast::UintTy::U16 => "u16",
-                ast::UintTy::U32 => "u32",
-                ast::UintTy::U64 => "u64",
-                ast::UintTy::U128 => "u128",
+                UintTy::Usize => "usize",
+                UintTy::U8 => "u8",
+                UintTy::U16 => "u16",
+                UintTy::U32 => "u32",
+                UintTy::U64 => "u64",
+                UintTy::U128 => "u128",
             });
         }
         Float(float_ty) => {
             str.push_str(match float_ty {
-                ast::FloatTy::F32 => "f32",
-                ast::FloatTy::F64 => "f64",
+                FloatTy::F32 => "f32",
+                FloatTy::F64 => "f64",
             });
         }
         Adt(def, subs) => {
diff --git a/checker/src/z3_solver.rs b/checker/src/z3_solver.rs
index 087bff01..dd7e5844 100644
--- a/checker/src/z3_solver.rs
+++ b/checker/src/z3_solver.rs
@@ -808,13 +808,15 @@ impl Z3Solver {
                 | Expression::IntrinsicBitVectorUnary { operand, .. }
                 | Expression::IntrinsicFloatingPointUnary { operand, .. }
                 | Expression::LogicalNot { operand, .. }
-                | Expression::Neg { operand, .. } => self.general_has_tag(&operand.expression, tag),
+                | Expression::Neg { operand, .. }
+                | Expression::Transmute { operand, .. } => {
+                    self.general_has_tag(&operand.expression, tag)
+                }
 
                 Expression::UninterpretedCall {
                     callee, arguments, ..
                 } => {
-                    let mut checks = Vec::new();
-                    checks.push(self.general_has_tag(&callee.expression, tag));
+                    let mut checks = vec![self.general_has_tag(&callee.expression, tag)];
                     for argument in arguments {
                         checks.push(self.general_has_tag(&argument.expression, tag));
                     }
@@ -1071,6 +1073,17 @@ impl Z3Solver {
             Expression::TaggedExpression { operand, .. } => {
                 self.get_as_numeric_z3_ast(&operand.expression)
             }
+            Expression::Transmute { target_type, .. } => unsafe {
+                if target_type.is_floating_point_number() {
+                    let sort = self.get_sort_for(target_type);
+                    (
+                        true,
+                        z3_sys::Z3_mk_fresh_const(self.z3_context, self.empty_str, sort),
+                    )
+                } else {
+                    self.numeric_fresh_const()
+                }
+            },
             Expression::Top | Expression::Bottom => self.numeric_fresh_const(),
             Expression::UninterpretedCall {
                 result_type: var_type,
diff --git a/checker/tests/run-pass/to_bits.rs b/checker/tests/run-pass/to_bits.rs
new file mode 100644
index 00000000..2109c715
--- /dev/null
+++ b/checker/tests/run-pass/to_bits.rs
@@ -0,0 +1,14 @@
+// Copyright (c) Facebook, Inc. and its affiliates.
+//
+// This source code is licensed under the MIT license found in the
+// LICENSE file in the root directory of this source tree.
+
+// A test for transmutation of floating point numbers to integers
+
+use mirai_annotations::*;
+
+pub fn t1() {
+    verify!((12.5f64).to_bits() == 0x4029000000000000);
+}
+
+pub fn main() {}
diff --git a/checker/tests/run-pass/vec_dealloc.rs b/checker/tests/run-pass/vec_dealloc.rs
new file mode 100644
index 00000000..f90f2c7a
--- /dev/null
+++ b/checker/tests/run-pass/vec_dealloc.rs
@@ -0,0 +1,23 @@
+// Copyright (c) Facebook, Inc. and its affiliates.
+//
+// This source code is licensed under the MIT license found in the
+// LICENSE file in the root directory of this source tree.
+//
+
+// A test that checks layout consistency for vec alloc/dealloc
+
+fn might_be_none(i: u8) -> Option<u8> {
+    if i > 0 {
+        Some(i)
+    } else {
+        None
+    }
+}
+
+pub fn encode_key(i: u8) -> std::io::Result<Vec<u8>> {
+    Ok(vec![
+        might_be_none(i).ok_or(std::io::ErrorKind::InvalidInput)?
+    ])
+}
+
+pub fn main() {}
diff --git a/rebuild_std.sh b/rebuild_std.sh
index 88a7623c..bb441951 100755
--- a/rebuild_std.sh
+++ b/rebuild_std.sh
@@ -9,16 +9,13 @@
 # Exit immediately if a command exits with a non-zero status.
 set -e
 
-# start clean
-cargo clean
-
-#install mirai into cargo (use --debug because it is quicker to build and build is currently the long pole)
-cargo uninstall -q mirai || true
-cargo install --debug --path ./checker
+cargo build
 
 # build the mirai-standard-contracts crate
 touch standard_contracts/src/lib.rs
-RUSTFLAGS="-Z force-overflow-checks=off" RUSTC_WRAPPER=mirai RUST_BACKTRACE=1 MIRAI_LOG=warn MIRAI_START_FRESH=true MIRAI_SHARE_PERSISTENT_STORE=true MIRAI_FLAGS="--diag=paranoid" cargo build --lib -p mirai-standard-contracts
+RUSTFLAGS="-Z force-overflow-checks=off" cargo build --lib -p mirai-standard-contracts
+touch standard_contracts/src/lib.rs
+RUSTFLAGS="-Z force-overflow-checks=off" RUSTC_WRAPPER=target/debug/mirai RUST_BACKTRACE=1 MIRAI_LOG=warn MIRAI_START_FRESH=true MIRAI_SHARE_PERSISTENT_STORE=true MIRAI_FlAGS="--diag=paranoid" cargo build --lib -p mirai-standard-contracts
 
 # collect the summary store into a tar file
 cd target/debug/deps
diff --git a/rust-toolchain b/rust-toolchain
index a2b82fb1..e500a60d 100644
--- a/rust-toolchain
+++ b/rust-toolchain
@@ -1 +1 @@
-nightly-2021-01-01
+nightly-2021-02-12
diff --git a/setup.sh b/setup.sh
index b80e9ff3..7f996976 100755
--- a/setup.sh
+++ b/setup.sh
@@ -19,3 +19,5 @@ rustup "+$TOOLCHAIN" component add rustc-dev
 rustup "+$TOOLCHAIN" component add llvm-tools-preview
 # install audit
 cargo "+$TOOLCHAIN" install cargo-audit
+# override tool chain
+rustup override set $TOOLCHAIN
diff --git a/standard_contracts/src/foreign_contracts.rs b/standard_contracts/src/foreign_contracts.rs
index 89dade1d..0f9876df 100644
--- a/standard_contracts/src/foreign_contracts.rs
+++ b/standard_contracts/src/foreign_contracts.rs
@@ -3774,6 +3774,10 @@ pub mod std {
                 _self
             }
         }
+
+        default_contract!(read);
+        default_contract!(read_to_string);
+        default_contract!(write);
     }
 
     pub mod io {
@@ -3884,6 +3888,7 @@ pub mod std {
             }
 
             default_contract!(_join);
+            default_contract!(to_str);
         }
 
         pub mod implement_std_path_PathBuf {