From 1d1189092c18aae45400d40d0e32d53409440b86 Mon Sep 17 00:00:00 2001
From: Vytautas Astrauskas <vastrauskas@gmail.com>
Date: Wed, 19 Jul 2023 13:54:57 +0200
Subject: [PATCH] Disable recursive function call checking because it crashes.

---
 prusti-interface/src/environment/mod.rs | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs
index 7f1acf512fe..5af9b2b4dcb 100644
--- a/prusti-interface/src/environment/mod.rs
+++ b/prusti-interface/src/environment/mod.rs
@@ -150,8 +150,11 @@ impl<'tcx> Environment<'tcx> {
                 .resolve_instance(param_env.and((called_def_id, call_substs)))
                 .unwrap()
             {
-                self.tcx()
-                    .mir_callgraph_reachable((instance, caller_def_id.expect_local()))
+                // FIXME: This call panics due to stolen MIR. Therefore, we
+                // unsoundly assume that the callee is not reachable.
+                // self.tcx()
+                //     .mir_callgraph_reachable((instance, caller_def_id.expect_local()))
+                false
             } else {
                 true
             }