diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
index 41120b34d7..2aaa1e80ef 100644
--- a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
+++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
@@ -8,15 +8,19 @@ pub use once_cell::unsync::Lazy;
 use std::{
     any::Any,
     borrow::Borrow,
+    boxed::Box,
     cell::{RefCell, UnsafeCell},
+    clone::Clone,
     cmp::Ordering,
     collections::{HashMap, HashSet},
+    convert::From,
     fmt::{Debug, Display, Formatter},
     hash::{Hash, Hasher},
     ptr::NonNull,
     mem,
-    ops::{Add, Deref, Div, Mul, Neg, Rem, Sub},
+    ops::{Add, Deref, Div, Fn, Mul, Neg, Rem, Sub},
     rc::{Rc, Weak},
+    vec::Vec,
 };
 
 pub use system::*;
@@ -71,11 +75,11 @@ pub mod dafny_runtime_conversions {
         pub type DafnyArray2<T> = crate::Object<crate::Array2<T>>;
         pub type DafnyArray3<T> = crate::Object<crate::Array3<T>>;
         // Conversion to and from Dafny reference-counted classes. All these methods take ownership of the class.
-        pub unsafe fn dafny_class_to_struct<T: Clone>(ptr: DafnyClass<T>) -> T {
+        pub fn dafny_class_to_struct<T: Clone>(ptr: DafnyClass<T>) -> T {
             let t: &T = crate::rd!(ptr);
             t.clone()
         }
-        pub unsafe fn dafny_class_to_boxed_struct<T: Clone>(ptr: DafnyClass<T>) -> Box<T> {
+        pub fn dafny_class_to_boxed_struct<T: Clone>(ptr: DafnyClass<T>) -> Box<T> {
             Box::new(dafny_class_to_struct(ptr))
         }
         pub unsafe fn dafny_class_to_rc_struct<T: Clone + ?Sized>(ptr: DafnyClass<T>) -> ::std::rc::Rc<T> {
@@ -87,7 +91,7 @@ pub mod dafny_runtime_conversions {
         pub fn boxed_struct_to_dafny_class<T>(t: Box<T>) -> DafnyClass<T> {
             struct_to_dafny_class(*t)
         }
-        pub unsafe fn rc_struct_to_dafny_class<T>(t: ::std::rc::Rc<T>) -> DafnyClass<T> {
+        pub unsafe fn rc_struct_to_dafny_class<T: ?Sized>(t: ::std::rc::Rc<T>) -> DafnyClass<T> {
             crate::Object::from_rc(t)
         }
         // Conversions to and from Dafny arrays. They all take ownership
@@ -590,14 +594,14 @@ impl DafnyInt {
 macro_rules! impl_dafnyint_from {
     () => {};
     ($type:ident) => {
-        impl From<$type> for DafnyInt {
+        impl $crate::From<$type> for $crate::DafnyInt {
             fn from(n: $type) -> Self {
-                DafnyInt {
-                    data: Rc::new(n.into()),
+                $crate::DafnyInt {
+                    data: $crate::Rc::new(n.into()),
                 }
             }
         }
-        impl DafnyUsize for $type {
+        impl $crate::DafnyUsize for $type {
             fn into_usize(self) -> usize {
                 self as usize
             }
@@ -1986,8 +1990,8 @@ impl<A: DafnyPrint> DafnyPrint for LazyFieldWrapper<A> {
 // Convert the DafnyPrint above into a macro so that we can create it for functions of any input arity
 macro_rules! dafny_print_function {
     ($($n:tt)*) => {
-        impl <B, $($n),*> DafnyPrint for Rc<dyn Fn($($n),*) -> B> {
-            fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
+        impl <B, $($n),*> $crate::DafnyPrint for $crate::Rc<dyn $crate::Fn($($n),*) -> B> {
+            fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result {
                 write!(f, "<function>")
             }
         }
@@ -2060,9 +2064,9 @@ impl<T> DafnyPrint for *const T {
 
 macro_rules! impl_print_display {
     ($name:ty) => {
-        impl DafnyPrint for $name {
-            fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
-                std::fmt::Display::fmt(&self, f)
+        impl $crate::DafnyPrint for $name {
+            fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result {
+                ::std::fmt::Display::fmt(&self, f)
             }
         }
     };
@@ -2407,12 +2411,12 @@ pub fn string_utf16_of(s: &str) -> DafnyStringUTF16 {
 
 macro_rules! impl_tuple_print {
     ($($items:ident)*) => {
-        impl <$($items,)*> DafnyPrint for ($($items,)*)
+        impl <$($items,)*> $crate::DafnyPrint for ($($items,)*)
         where
-            $($items: DafnyPrint,)*
+            $($items: $crate::DafnyPrint,)*
         {
             #[allow(unused_assignments)]
-            fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
+            fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result {
                 #[allow(non_snake_case)]
                 let ($($items,)*) = self;
 
@@ -2527,8 +2531,8 @@ macro_rules! int {
 macro_rules! ARRAY_GETTER_LENGTH0 {
     () => {
         #[inline]
-        pub fn length0(&self) -> DafnyInt {
-            DafnyInt::from(self.length0_usize())
+        pub fn length0(&self) -> $crate::DafnyInt {
+            $crate::DafnyInt::from(self.length0_usize())
         }
         #[inline]
         pub fn length0_usize(&self) -> usize {
@@ -2539,7 +2543,7 @@ macro_rules! ARRAY_GETTER_LENGTH0 {
 macro_rules! ARRAY_GETTER_LENGTH {
     ($field: ident, $field_usize: ident) => {
         #[inline]
-        pub fn $field(&self) -> DafnyInt {
+        pub fn $field(&self) -> $crate::DafnyInt {
             $crate::DafnyInt::from(self.$field_usize())
         }
         #[inline]
@@ -2553,14 +2557,14 @@ macro_rules! ARRAY_GETTER_LENGTH {
 #[macro_export]
 macro_rules! array {
     ($($x:expr), *) => {
-        array::from_native(Box::new([$($x), *]))
+        $crate::array::from_native($crate::Box::new([$($x), *]))
     }
 }
 
 macro_rules! ARRAY_INIT {
     {$length: ident, $inner: expr} => {
         $crate::array::initialize_box_usize($length, {
-            Rc::new(move |_| { $inner })
+            $crate::Rc::new(move |_| { $inner })
         })
     }
 }
@@ -2575,10 +2579,10 @@ macro_rules! ARRAY_INIT_INNER {
 // Box<[Box<[Box<[T]>]>]>
 macro_rules! ARRAY_DATA_TYPE {
     ($length:ident) => {
-        Box<[T]>
+        $crate::Box<[T]>
     };
     ($length:ident, $($rest_length:ident),+) => {
-        Box<[ARRAY_DATA_TYPE!($($rest_length),+)]>
+        $crate::Box<[ARRAY_DATA_TYPE!($($rest_length),+)]>
     };
 }
 
@@ -2602,18 +2606,18 @@ macro_rules! ARRAY_METHODS {
         pub fn placebos_box_usize(
             $length0: usize,
             $($length: usize),+
-        ) -> Box<$ArrayType<$crate::MaybeUninit<T>>> {
-            Box::new($ArrayType {
+        ) -> $crate::Box<$ArrayType<$crate::MaybeUninit<T>>> {
+            $crate::Box::new($ArrayType {
                 $($length: $length),+,
                 data: INIT_ARRAY_DATA!($ArrayType, $length0, $($length),+),
             })
         }
-        
+
         pub fn placebos_usize(
             $length0: usize,
             $($length: usize),+
-        ) -> Ptr<$ArrayType<$crate::MaybeUninit<T>>> {
-            Ptr::from_box(Self::placebos_box_usize(
+        ) -> $crate::Ptr<$ArrayType<$crate::MaybeUninit<T>>> {
+            $crate::Ptr::from_box(Self::placebos_box_usize(
                 $length0,
                 $($length),+
             ))
@@ -2633,7 +2637,7 @@ macro_rules! ARRAY_METHODS {
         pub fn placebos(
             $length0: &$crate::DafnyInt,
             $($length: &$crate::DafnyInt),+
-        ) -> Ptr<$ArrayType<$crate::MaybeUninit<T>>> {
+        ) -> $crate::Ptr<$ArrayType<$crate::MaybeUninit<T>>> {
             Self::placebos_usize(
                 $length0.as_usize(),
                 $($length.as_usize()),+
@@ -2641,11 +2645,11 @@ macro_rules! ARRAY_METHODS {
         }
 
         // Once all the elements have been initialized, transform the signature of the pointer
-        pub fn construct(p: Ptr<$ArrayType<$crate::MaybeUninit<T>>>) -> Ptr<$ArrayType<T>> {
+        pub fn construct(p: $crate::Ptr<$ArrayType<$crate::MaybeUninit<T>>>) -> $crate::Ptr<$ArrayType<T>> {
             unsafe { std::mem::transmute(p) }
         }
         // Once all the elements have been initialized, transform the signature of the pointer
-        pub fn construct_object(p: $crate::Object<$ArrayType<MaybeUninit<T>>>) -> Object<$ArrayType<T>> {
+        pub fn construct_object(p: $crate::Object<$ArrayType<$crate::MaybeUninit<T>>>) -> $crate::Object<$ArrayType<T>> {
             unsafe { std::mem::transmute(p) }
         }
     };
@@ -2672,15 +2676,15 @@ macro_rules! ARRAY_TO_VEC_LOOP {
     };
     (@inner $self: ident, $outerTmp: ident, $data: expr $(, $rest_length_usize: ident)*) => {
         {
-            let mut tmp = Vec::new();
+            let mut tmp = $crate::Vec::new();
             ARRAY_TO_VEC_LOOP!(@for $self, tmp, $data $(, $rest_length_usize)*);
             $outerTmp.push(tmp);
         }
     };
-    
+
     ($self: ident, $data: expr $(, $rest_length_usize: ident)*) => {
         {
-            let mut tmp = Vec::new();
+            let mut tmp = $crate::Vec::new();
             ARRAY_TO_VEC_LOOP!(@for $self, tmp, $data $(, $rest_length_usize)*);
             tmp
         }
@@ -2689,10 +2693,10 @@ macro_rules! ARRAY_TO_VEC_LOOP {
 
 macro_rules! ARRAY_TO_VEC_TYPE {
     ($length0: ident) => {
-        Vec<T>
+        $crate::Vec<T>
     };
     ($length0: ident $(, $res_length: ident)*) => {
-        Vec<ARRAY_TO_VEC_TYPE!($($res_length), *)>
+        $crate::Vec<ARRAY_TO_VEC_TYPE!($($res_length), *)>
     }
 }
 
@@ -2747,7 +2751,7 @@ macro_rules! ARRAY_DEF {
                 $(($length, $length_usize)), +
             }
         }
-        impl<T: Clone> $ArrayType<T> {
+        impl<T: $crate::Clone> $ArrayType<T> {
             ARRAY_TO_VEC_WRAPPER!{
                 $(($length, $length_usize)), +
             }
@@ -2757,12 +2761,12 @@ macro_rules! ARRAY_DEF {
 
 // Array2 to Array16
 
-ARRAY_DEF!{Array2, 
+ARRAY_DEF!{Array2,
     (length0, length0_usize),
     (length1, length1_usize)
 }
 
-ARRAY_DEF!{Array3, 
+ARRAY_DEF!{Array3,
     (length0, length0_usize),
     (length1, length1_usize),
     (length2, length2_usize)
@@ -3107,7 +3111,7 @@ macro_rules! is_object {
 #[macro_export]
 macro_rules! cast_any {
     ($raw:expr) => {
-        $crate::Upcast::<dyn Any>::upcast($crate::read!($raw))
+        $crate::Upcast::<dyn $crate::Any>::upcast($crate::read!($raw))
     };
 }
 // cast_any_object is meant to be used on references only, to convert any references (classes or traits)*
@@ -3115,7 +3119,7 @@ macro_rules! cast_any {
 #[macro_export]
 macro_rules! cast_any_object {
     ($obj:expr) => {
-        $crate::UpcastObject::<dyn Any>::upcast($crate::md!($obj))
+        $crate::UpcastObject::<dyn $crate::Any>::upcast($crate::md!($obj))
     };
 }
 
@@ -3551,7 +3555,7 @@ macro_rules! rd {
 #[macro_export]
 macro_rules! refcount {
     ($x:expr) => {
-        Rc::strong_count(unsafe { rcmut::as_rc($x.0.as_ref().unwrap()) })
+        $crate::Rc::strong_count(unsafe { $crate::rcmut::as_rc($x.0.as_ref().unwrap()) })
     };
 }
 
@@ -3835,10 +3839,10 @@ macro_rules! UpcastDef {
             $crate::UpcastFn!($B);
         }
     };
-    
+
     ($A:ty, $B:ty, $($C: ty),*) => {
-        UpcastDef!($A, $B);
-        UpcastDef!($A, $($C),*);
+        $crate::UpcastDef!($A, $B);
+        $crate::UpcastDef!($A, $($C),*);
     }
 }
 
@@ -3849,10 +3853,10 @@ macro_rules! UpcastDefObject {
             $crate::UpcastObjectFn!($B);
         }
     };
-    
+
     ($A:ty, $B:ty, $($C: ty),*) => {
-        UpcastDefObject!($A, $B);
-        UpcastDefObject!($A, $($C),*);
+        $crate::UpcastDefObject!($A, $B);
+        $crate::UpcastDefObject!($A, $($C),*);
     }
 }