diff --git a/Cargo.lock b/Cargo.lock
index f116c684b7a..89f56d16313 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -409,6 +409,16 @@ dependencies = [
  "rustc-demangle",
 ]
 
+[[package]]
+name = "backtrace-on-stack-overflow"
+version = "0.3.0"
+source = "git+https://github.com/Pistonight/backtrace-on-stack-overflow?branch=feature%2Flimit_stack_size#fa3874ecb04b3cb76a5a6563c620630dc5e15e7c"
+dependencies = [
+ "backtrace",
+ "libc",
+ "nix 0.23.2",
+]
+
 [[package]]
 name = "base64"
 version = "0.21.5"
@@ -1813,6 +1823,15 @@ version = "2.7.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3"
 
+[[package]]
+name = "memoffset"
+version = "0.6.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5aa361d4faea93603064a027415f07bd8e1d5c88c9fbf68bf56a285428fd79ce"
+dependencies = [
+ "autocfg",
+]
+
 [[package]]
 name = "memoffset"
 version = "0.7.1"
@@ -1917,6 +1936,19 @@ dependencies = [
  "tempfile",
 ]
 
+[[package]]
+name = "nix"
+version = "0.23.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8f3790c00a0150112de0f4cd161e3d7fc4b2d8a5542ffc35f099a2562aecb35c"
+dependencies = [
+ "bitflags 1.3.2",
+ "cc",
+ "cfg-if",
+ "libc",
+ "memoffset 0.6.5",
+]
+
 [[package]]
 name = "nix"
 version = "0.26.4"
@@ -1926,7 +1958,7 @@ dependencies = [
  "bitflags 1.3.2",
  "cfg-if",
  "libc",
- "memoffset",
+ "memoffset 0.7.1",
  "pin-utils",
 ]
 
@@ -2454,6 +2486,7 @@ dependencies = [
 name = "prusti-encoder"
 version = "0.1.0"
 dependencies = [
+ "backtrace-on-stack-overflow",
  "cfg-if",
  "pcg",
  "prusti-interface",
diff --git a/prusti-encoder/Cargo.toml b/prusti-encoder/Cargo.toml
index 1972541a4f0..9e344bdc13d 100644
--- a/prusti-encoder/Cargo.toml
+++ b/prusti-encoder/Cargo.toml
@@ -18,6 +18,8 @@ task-encoder = { path = "../task-encoder" }
 vir = { path = "../vir" }
 tracing = { path = "../tracing" }
 
+backtrace-on-stack-overflow = { git = "https://github.com/Pistonight/backtrace-on-stack-overflow", branch = "feature/limit_stack_size" }
+
 [package.metadata.rust-analyzer]
 # This crate uses #[feature(rustc_private)]
 rustc_private = true
diff --git a/prusti-encoder/src/lib.rs b/prusti-encoder/src/lib.rs
index 9a7dd8a1427..a4021a68889 100644
--- a/prusti-encoder/src/lib.rs
+++ b/prusti-encoder/src/lib.rs
@@ -27,6 +27,7 @@ pub fn test_entrypoint<'tcx>(
     def_spec: prusti_interface::specs::typed::DefSpecificationMap,
 ) -> request::RequestWithContext {
     vir::init_vcx(vir::VirCtxt::new(tcx, body, def_spec));
+    unsafe { backtrace_on_stack_overflow::enable() };
 
     // TODO: this should be a "crate" encoder, which will deps.require all the methods in the crate
 
diff --git a/prusti-tests/tests/harnesses/compiletest.rs b/prusti-tests/tests/harnesses/compiletest.rs
index f4f5976e690..f6f28e2efd9 100644
--- a/prusti-tests/tests/harnesses/compiletest.rs
+++ b/prusti-tests/tests/harnesses/compiletest.rs
@@ -78,6 +78,7 @@ fn run_prusti_tests(
         config
     };
 
+    /*
     // UI
     {
         let config = prusti_config(format!("tests/{group_name}/ui"));
@@ -94,6 +95,7 @@ fn run_prusti_tests(
         ));
         run_tests(config)?;
     }
+    */
 
     // pass
     {
@@ -176,10 +178,11 @@ pub(crate) fn run() {
     let server_address = spawn_server_thread();
     env::set_var("PRUSTI_SERVER_ADDRESS", server_address.to_string());
 
+    /*
     // Run (temporary) tests specific to Prusti v2.
     println!("[v2]");
     run_verification_no_overflow("v2");
-    /*
+
         let save_verification_cache =
             || match ureq::post(&format!("http://{server_address}/save")).call() {
                 Ok(response) => {
@@ -198,10 +201,13 @@ pub(crate) fn run() {
         // Test the type-checking of specifications. This doesn't run the verifier.
         println!("[typecheck]");
         run_no_verification("typecheck");
+    */
 
-        // Test the verifier.
-        println!("[verify]");
-        run_verification_no_overflow("verify");
+    // Test the verifier.
+    println!("[verify]");
+    run_verification_no_overflow("verify");
+
+    /*
         save_verification_cache();
 
         // Test the verifier with overflow checks enabled.
diff --git a/prusti/src/verifier.rs b/prusti/src/verifier.rs
index bf5e430303e..6e865f34b0b 100644
--- a/prusti/src/verifier.rs
+++ b/prusti/src/verifier.rs
@@ -89,6 +89,7 @@ pub fn verify(env: Environment<'_>, def_spec: typed::DefSpecificationMap) {
             //         || (config::skip_unsupported_features()
             //             && config::allow_unreachable_unsupported_code())
             // );
+            std::process::exit(1);
         }
 
         //let verification_result =