diff --git a/bin/build.sh b/bin/build.sh
index ace18792f..85f096d48 100755
--- a/bin/build.sh
+++ b/bin/build.sh
@@ -387,8 +387,9 @@ if [ ${INSTALL_RUST} -eq 1 ] ; then
   ${WGET} https://static.rust-lang.org/dist/${RUST_VERSION}/rust-nightly-x86_64-unknown-linux-gnu.tar.gz -O rust.tar.gz
   tar xf rust.tar.gz
   cd rust-nightly-x86_64-unknown-linux-gnu
-  sudo ./install.sh
+  sudo ./install.sh --without=rust-docs
   cd ..
+  rm -r rust-nightly-x86_64-unknown-linux-gnu rust.tar.gz
   
   puts "Installed Rust"
 fi
diff --git a/bin/versions b/bin/versions
index 8a0b4afe2..f266b9df7 100644
--- a/bin/versions
+++ b/bin/versions
@@ -8,4 +8,4 @@ SYMBOOGLIX_COMMIT=7210e5d09b
 LOCKPWN_COMMIT=73eddf97bd
 LLVM_SHORT_VERSION=8
 LLVM_FULL_VERSION=8.0.1
-RUST_VERSION=2016-12-16
+RUST_VERSION=2019-07-16
diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp
index 89d28cf01..62120386b 100644
--- a/lib/smack/SmackInstGenerator.cpp
+++ b/lib/smack/SmackInstGenerator.cpp
@@ -646,10 +646,8 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) {
   } else if (name.find(Naming::RUST_ENTRY) != std::string::npos) {
     // Set the entry point for Rust programs
     auto castExpr = ci.getArgOperand(0);
-    if (auto CE = dyn_cast<const Constant>(castExpr)) {
-      auto mainFunc = CE->getOperand(0);
-      emit(Stmt::call(mainFunc->getName(), {}, {}));
-    }
+    auto mainFunction = cast<const Function>(castExpr);
+    emit(Stmt::call(mainFunction->getName(), {}, {}));
 
   } else if (name.find(Naming::RUST_PANIC1) != std::string::npos ||
              name.find(Naming::RUST_PANIC2) != std::string::npos) {
diff --git a/share/smack/frontend.py b/share/smack/frontend.py
index 9927fae10..222f234d8 100644
--- a/share/smack/frontend.py
+++ b/share/smack/frontend.py
@@ -220,7 +220,7 @@ def rust_frontend(input_file, args):
   """Generate Boogie code from Rust programming language source(s)."""
   compile_command = ['rustc', '-A', 'unused-imports', '-C', 'opt-level=0',
                      '-C', 'no-prepopulate-passes', '-g', '--emit=llvm-bc',
-                     '--cfg', 'verifier="smack"']
+                     '--cfg', 'verifier="smack"', '-C', 'passes=name-anon-globals']
   
   # This links in the Rust SMACK library. This is needed due to the way rustc
   # finds a programs libraries.