diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs
index 787c368f7e7..3b940d66483 100644
--- a/prusti-utils/src/config.rs
+++ b/prusti-utils/src/config.rs
@@ -69,7 +69,7 @@ lazy_static::lazy_static! {
 
         // 0. Default values
         settings.set_default("be_rustc", false).unwrap();
-        settings.set_default("viper_backend", "Lithium").unwrap();
+        settings.set_default("viper_backend", "Silicon").unwrap();
         settings.set_default::<Option<String>>("smt_solver_path", env::var("Z3_EXE").ok()).unwrap();
         settings.set_default::<Option<String>>("smt_solver_wrapper_path", None).unwrap();
         settings.set_default::<Option<String>>("boogie_path", env::var("BOOGIE_EXE").ok()).unwrap();
@@ -81,7 +81,7 @@ lazy_static::lazy_static! {
         settings.set_default("check_overflows", true).unwrap();
         settings.set_default("check_panics", true).unwrap();
         settings.set_default("encode_unsigned_num_constraint", true).unwrap();
-        settings.set_default("encode_bitvectors", true).unwrap();
+        settings.set_default("encode_bitvectors", false).unwrap();
         settings.set_default("simplify_encoding", true).unwrap();
         settings.set_default("log", "").unwrap();
         settings.set_default("log_style", "auto").unwrap();
@@ -92,7 +92,7 @@ lazy_static::lazy_static! {
         settings.set_default("dump_debug_info_during_fold", false).unwrap();
         settings.set_default("dump_nll_facts", false).unwrap();
         settings.set_default("ignore_regions", false).unwrap();
-        settings.set_default("max_log_file_name_length", 240).unwrap();
+        settings.set_default("max_log_file_name_length", 60).unwrap();
         settings.set_default("dump_path_ctxt_in_debug_info", false).unwrap();
         settings.set_default("dump_reborrowing_dag_in_debug_info", false).unwrap();
         settings.set_default("dump_borrowck_info", false).unwrap();
@@ -104,7 +104,7 @@ lazy_static::lazy_static! {
         settings.set_default("assert_timeout", 10_000).unwrap();
         settings.set_default("smt_qi_eager_threshold", 1000).unwrap();
         settings.set_default("use_more_complete_exhale", true).unwrap();
-        settings.set_default("skip_unsupported_features", true).unwrap();
+        settings.set_default("skip_unsupported_features", false).unwrap();
         settings.set_default("internal_errors_as_warnings", false).unwrap();
         settings.set_default("allow_unreachable_unsupported_code", false).unwrap();
         settings.set_default("no_verify", false).unwrap();
@@ -114,16 +114,16 @@ lazy_static::lazy_static! {
         settings.set_default("json_communication", false).unwrap();
         settings.set_default("optimizations", "all").unwrap();
         settings.set_default("intern_names", true).unwrap();
-        settings.set_default("enable_purification_optimization", true).unwrap();
+        settings.set_default("enable_purification_optimization", false).unwrap();
         // settings.set_default("enable_manual_axiomatization", false).unwrap();
-        settings.set_default("unsafe_core_proof", true).unwrap();
-        settings.set_default("verify_core_proof", false).unwrap();
+        settings.set_default("unsafe_core_proof", false).unwrap();
+        settings.set_default("verify_core_proof", true).unwrap();
         settings.set_default("verify_specifications", true).unwrap();
         settings.set_default("verify_types", false).unwrap();
         settings.set_default("verify_specifications_with_core_proof", false).unwrap();
-        settings.set_default("verify_specifications_backend", "Lithium").unwrap();
+        settings.set_default("verify_specifications_backend", "Silicon").unwrap();
         settings.set_default("use_eval_axioms", true).unwrap();
-        settings.set_default("inline_caller_for", true).unwrap();
+        settings.set_default("inline_caller_for", false).unwrap();
         settings.set_default("check_no_drops", false).unwrap();
         settings.set_default("enable_type_invariants", false).unwrap();
         settings.set_default("use_new_encoder", true).unwrap();
diff --git a/prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs b/prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs
index e12dadbae49..01938a7dc88 100644
--- a/prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs
+++ b/prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs
@@ -218,7 +218,6 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
         state.check_consistency();
         let actions = ensure_required_permissions(self, state, consumed_permissions.clone())?;
         self.process_actions(actions)?;
-        // TODO: Remove permission reasoning
         state.remove_permissions(&consumed_permissions)?;
         state.insert_permissions(produced_permissions)?;
         match &statement {
diff --git a/prusti-viper/src/encoder/places.rs b/prusti-viper/src/encoder/places.rs
index 75833c3f456..508f4b324ae 100644
--- a/prusti-viper/src/encoder/places.rs
+++ b/prusti-viper/src/encoder/places.rs
@@ -5,7 +5,7 @@
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 use prusti_rustc_interface::{
-    index::vec::{Idx, IndexVec},
+    index::{Idx, IndexVec},
     middle::{mir, ty::Ty},
 };
 use std::iter;
diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index dee9fdf71fd..655edd5dc97 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -70,7 +70,7 @@ use prusti_rustc_interface::{
     middle::{
         mir,
         mir::{Mutability, TerminatorKind},
-        ty::{self, subst::SubstsRef},
+        ty::{self, GenericArgsRef},
     },
     span::Span,
     target::abi::{FieldIdx, Integer},
@@ -1051,12 +1051,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             Some((mid_g, mid_b1))
         } else {
             // Cannot add loop guard to loop invariant
-            let fn_names: Vec<_> = preconds.iter().filter_map(|(name, _)| name.as_ref()).map(|name| {
-                if let Some(rust_name) = name.strip_prefix("f_") {
-                    return rust_name
-                };
-                name.strip_prefix("m_").unwrap_or(name)
-            }).collect();
+            let fn_names: Vec<_> = preconds
+                .iter()
+                .filter_map(|(name, _)| name.as_ref())
+                .map(|name| {
+                    if let Some(rust_name) = name.strip_prefix("f_") {
+                        return rust_name;
+                    };
+                    name.strip_prefix("m_").unwrap_or(name)
+                })
+                .collect();
             let warning_msg = if fn_names.is_empty() {
                 "the loop guard was not automatically added as a `body_invariant!(...)`, consider doing this manually".to_string()
             } else {
@@ -1640,9 +1644,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     times,
                     ty,
                     location,
-                )?
-            }
-            mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), ref operand, cast_ty) => {
+                )?,
+            mir::Rvalue::Cast(
+                mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
+                ref operand,
+                cast_ty,
+            ) => {
                 let rhs_ty = self.mir_encoder.get_operand_ty(operand);
                 if rhs_ty.is_array_ref() && cast_ty.is_slice_ref() {
                     trace!("slice: operand={:?}, ty={:?}", operand, cast_ty);
@@ -1654,8 +1661,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     ));
                 }
             }
-            mir::Rvalue::Cast(mir::CastKind::PointerCoercion(_), _, _) |
-            mir::Rvalue::Cast(mir::CastKind::DynStar, _, _) => {
+            mir::Rvalue::Cast(mir::CastKind::PointerCoercion(_), _, _)
+            | mir::Rvalue::Cast(mir::CastKind::DynStar, _, _) => {
                 return Err(SpannedEncodingError::unsupported(
                     "raw pointers are not supported",
                     span,
@@ -1830,7 +1837,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 (expiring, Some(restored), false, stmts)
             }
 
-            mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), ref operand, ty) => {
+            mir::Rvalue::Cast(
+                mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
+                ref operand,
+                ty,
+            ) => {
                 trace!("cast: operand={:?}, ty={:?}", operand, ty);
                 let place = match *operand {
                     mir::Operand::Move(place) => place,
@@ -1923,11 +1934,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         if let Some(stmt) = self.polonius_info().get_assignment_for_loan(loan)? {
             Ok(match stmt.kind {
                 mir::StatementKind::Assign(box (_, ref rhs)) => match rhs {
-                    &mir::Rvalue::Ref(_, mir::BorrowKind::Shared, _) |
-                    &mir::Rvalue::Use(mir::Operand::Copy(_)) => false,
-                    &mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, _) |
-                    &mir::Rvalue::Use(mir::Operand::Move(_)) => true,
-                    &mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), _, _ty) => false,
+                    &mir::Rvalue::Ref(_, mir::BorrowKind::Shared, _)
+                    | &mir::Rvalue::Use(mir::Operand::Copy(_)) => false,
+                    &mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, _)
+                    | &mir::Rvalue::Use(mir::Operand::Move(_)) => true,
+                    &mir::Rvalue::Cast(
+                        mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
+                        _,
+                        _ty,
+                    ) => false,
                     &mir::Rvalue::Use(mir::Operand::Constant(_)) => false,
                     x => unreachable!("{:?}", x),
                 },
@@ -3381,7 +3396,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
             // TODO: weird fix for closure call substitutions, we need to
             // prepend the identity substs of the containing method ...
-            substs = self.encoder.env().tcx().mk_args_from_iter(self.substs.iter().chain(substs));
+            substs = self
+                .encoder
+                .env()
+                .tcx()
+                .mk_args_from_iter(self.substs.iter().chain(substs));
         } else {
             for (arg, encoded_operand) in mir_args.iter().zip(encoded_operands.iter_mut()) {
                 let arg_ty = self.mir_encoder.get_operand_ty(arg);
@@ -3990,13 +4009,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         &self,
         contract: &ProcedureContract<'tcx>,
         substs: GenericArgsRef<'tcx>,
-        override_spans: FxHashMap<Local, Span> // spans for fake locals
-    ) -> SpannedEncodingResult<(
-        vir::Expr,
-        Vec<vir::Expr>,
-        vir::Expr,
-        vir::Expr,
-    )> {
+        override_spans: FxHashMap<Local, Span>, // spans for fake locals
+    ) -> SpannedEncodingResult<(vir::Expr, Vec<vir::Expr>, vir::Expr, vir::Expr)> {
         let borrow_infos = &contract.borrow_infos;
         let maybe_blocked_paths = if !borrow_infos.is_empty() {
             assert_eq!(
diff --git a/prusti-viper/src/utils/type_visitor.rs b/prusti-viper/src/utils/type_visitor.rs
index d1cddaa60b3..72faa5eec33 100644
--- a/prusti-viper/src/utils/type_visitor.rs
+++ b/prusti-viper/src/utils/type_visitor.rs
@@ -4,10 +4,13 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use prusti_rustc_interface::hir::Mutability;
-use prusti_rustc_interface::middle::ty::{
-    AdtDef, FieldDef, List, ParamTy, Region, AliasKind, AliasTy, Ty, TyCtxt,
-    TypeFlags, TyKind, IntTy, UintTy, FloatTy, VariantDef, GenericArgsRef, Const
+use prusti_rustc_interface::{
+    hir::Mutability,
+    middle::ty::{
+        AdtDef, AliasKind, AliasTy, Const, FieldDef, FloatTy, GenericArgsRef, IntTy, List, ParamTy,
+        Region, Ty, TyCtxt, TyKind, TypeFlags, UintTy, VariantDef,
+    },
+    span::def_id::DefId,
 };
 
 pub trait TypeVisitor<'tcx>: Sized {
@@ -87,7 +90,7 @@ pub trait TypeVisitor<'tcx>: Sized {
     fn visit_adt(
         &mut self,
         adt_def: AdtDef<'tcx>,
-        substs: GenericArgsRef<'tcx>
+        substs: GenericArgsRef<'tcx>,
     ) -> Result<(), Self::Error> {
         walk_adt(self, adt_def, substs)
     }
@@ -99,7 +102,7 @@ pub trait TypeVisitor<'tcx>: Sized {
         idx: prusti_rustc_interface::target::abi::VariantIdx,
         variant: &VariantDef,
         substs: GenericArgsRef<'tcx>,
-    )  -> Result<(), Self::Error> {
+    ) -> Result<(), Self::Error> {
         walk_adt_variant(self, variant, substs)
     }
 
@@ -143,7 +146,7 @@ pub trait TypeVisitor<'tcx>: Sized {
     fn visit_closure(
         &mut self,
         def_id: DefId,
-        substs: GenericArgsRef<'tcx>
+        substs: GenericArgsRef<'tcx>,
     ) -> Result<(), Self::Error> {
         walk_closure(self, def_id, substs)
     }
@@ -152,7 +155,7 @@ pub trait TypeVisitor<'tcx>: Sized {
     fn visit_fndef(
         &mut self,
         def_id: DefId,
-        substs: GenericArgsRef<'tcx>
+        substs: GenericArgsRef<'tcx>,
     ) -> Result<(), Self::Error> {
         walk_fndef(self, def_id, substs)
     }
@@ -232,7 +235,7 @@ pub fn walk_raw_ptr<'tcx, E, V: TypeVisitor<'tcx, Error = E>>(
 pub fn walk_closure<'tcx, E, V: TypeVisitor<'tcx, Error = E>>(
     visitor: &mut V,
     _def_id: DefId,
-    substs: GenericArgsRef<'tcx>
+    substs: GenericArgsRef<'tcx>,
 ) -> Result<(), E> {
     let cl_substs = substs.as_closure();
     // TODO: when are there bound typevars? can type visitor deal with generics?
@@ -248,7 +251,7 @@ pub fn walk_closure<'tcx, E, V: TypeVisitor<'tcx, Error = E>>(
 pub fn walk_fndef<'tcx, E, V: TypeVisitor<'tcx, Error = E>>(
     visitor: &mut V,
     _def_id: DefId,
-    substs: GenericArgsRef<'tcx>
+    substs: GenericArgsRef<'tcx>,
 ) -> Result<(), E> {
     for ty in substs.types() {
         visitor.visit_ty(ty)?;