diff --git a/prusti-encoder/src/encoders/mir_fn/mod.rs b/prusti-encoder/src/encoders/mir_fn/mod.rs
index 149d344dcd2..6845e028027 100644
--- a/prusti-encoder/src/encoders/mir_fn/mod.rs
+++ b/prusti-encoder/src/encoders/mir_fn/mod.rs
@@ -39,9 +39,6 @@ pub fn encode_all_in_crate<'tcx>(tcx: ty::TyCtxt<'tcx>) {
         match kind {
             hir::def::DefKind::Fn | hir::def::DefKind::AssocFn => {
                 let def_id = def_id.to_def_id();
-                if prusti_interface::specs::is_spec_fn(tcx, def_id) {
-                    continue;
-                }
 
                 let (is_pure, is_trusted) = crate::encoders::with_proc_spec(
                     SpecQuery::GetProcKind(def_id, ty::List::identity_for_item(tcx, def_id)),
diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs
index 7aabddecd64..765bf18c4c3 100644
--- a/prusti/src/callbacks.rs
+++ b/prusti/src/callbacks.rs
@@ -4,7 +4,7 @@ use ide::{fake_error, IdeInfo};
 use prusti_interface::{
     data::VerificationTask,
     environment::{mir_storage, Environment},
-    specs::{self, cross_crate::CrossCrateSpecs, is_spec_fn},
+    specs::{self, cross_crate::CrossCrateSpecs},
     PrustiError,
 };
 use prusti_rustc_interface::{
@@ -39,7 +39,7 @@ fn mir_borrowck<'tcx>(tcx: TyCtxt<'tcx>, def_id: LocalDefId) -> MirBorrowck<'tcx
     // when calling `get_body_with_borrowck_facts`. TODO: figure out if we need
     // (anon) const bodies at all, and if so, how to get them?
     if !is_anon_const {
-        let consumer_opts = if is_spec_fn(tcx, def_id.to_def_id()) || config::no_verify() {
+        let consumer_opts = if config::no_verify() {
             consumers::ConsumerOptions::RegionInferenceContext
         } else {
             consumers::ConsumerOptions::PoloniusOutputFacts