diff --git a/cargo-creusot/src/main.rs b/cargo-creusot/src/main.rs
index 0f024ebae3..71991952ca 100644
--- a/cargo-creusot/src/main.rs
+++ b/cargo-creusot/src/main.rs
@@ -137,6 +137,9 @@ fn invoke_cargo(args: &CreusotArgs, cargo_flags: Vec<String>) {
         .args(cargo_flags)
         .env("RUSTC", creusot_rustc_path)
         .env("CARGO_CREUSOT", "1");
+    // Incremental compilation causes Creusot to not see all of a crate's code
+    // (the `mir_borrowck` hook in `creusot/src/callbacks.rs` is not called on all closures).
+    cmd.env("CARGO_INCREMENTAL", "0");
 
     // Append flags to any pre-existing ones
     // CARGO_ENCODED_RUSTFLAGS contains options to pass to rustc, separated by '\x1f'.
diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma
index 8748b1839a..6b872e7e4e 100644
--- a/creusot/tests/creusot-contracts/creusot-contracts.coma
+++ b/creusot/tests/creusot-contracts/creusot-contracts.coma
@@ -6965,10 +6965,9 @@ module M_creusot_contracts__stdqy35z1__option__extern_spec_std_option_T_Option_T
   let%span sops5 = "../../../creusot-contracts/src/std/ops.rs" 152 0 174 1
   let%span soption6 = "../../../creusot-contracts/src/std/option.rs" 62 26 62 75
   let%span soption7 = "../../../creusot-contracts/src/std/option.rs" 64 20 65 100
-  let%span soption8 = "../../../creusot-contracts/src/std/option.rs" 31 0 423 1
-  let%span sresolve9 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sresolve10 = "../../../creusot-contracts/src/resolve.rs" 82 8 85 9
-  let%span sinvariant11 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
+  let%span sresolve8 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
+  let%span sresolve9 = "../../../creusot-contracts/src/resolve.rs" 82 8 85 9
+  let%span sinvariant10 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   
   type t_T'0
   
@@ -6992,14 +6991,14 @@ module M_creusot_contracts__stdqy35z1__option__extern_spec_std_option_T_Option_T
     
   
   predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 33 4 33 30] (self : borrowed t_T'0) =
-    [%#sinvariant11] inv'1 self.current /\ inv'1 self.final
+    [%#sinvariant10] inv'1 self.current /\ inv'1 self.final
   
   predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : borrowed t_T'0)
   
   axiom inv_axiom'0 [@rewrite] : forall x : borrowed t_T'0 [inv'2 x] . inv'2 x = invariant'0 x
   
   predicate resolve'4 [#"../../../creusot-contracts/src/resolve.rs" 53 4 53 28] (self : borrowed t_T'0) =
-    [%#sresolve9] self.final = self.current
+    [%#sresolve8] self.final = self.current
   
   predicate resolve'1 [#"../../../creusot-contracts/src/resolve.rs" 19 0 19 40] (_1 : borrowed t_T'0) =
     resolve'4 _1
@@ -7031,7 +7030,7 @@ module M_creusot_contracts__stdqy35z1__option__extern_spec_std_option_T_Option_T
   predicate resolve'7 [#"../../../creusot-contracts/src/resolve.rs" 19 0 19 40] (_1 : t_T'0)
   
   predicate resolve'5 [#"../../../creusot-contracts/src/resolve.rs" 81 4 81 28] (self : t_Option'0) =
-    [%#sresolve10] match self with
+    [%#sresolve9] match self with
       | C_Some'0 x -> resolve'7 x
       | C_None'0 -> true
       end
@@ -7040,7 +7039,7 @@ module M_creusot_contracts__stdqy35z1__option__extern_spec_std_option_T_Option_T
     resolve'5 _1
   
   predicate invariant'1 [#"../../../creusot-contracts/src/invariant.rs" 33 4 33 30] (self : borrowed (t_Option'0)) =
-    [%#sinvariant11] inv'3 self.current /\ inv'3 self.final
+    [%#sinvariant10] inv'3 self.current /\ inv'3 self.final
   
   predicate inv'4 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : borrowed (t_Option'0))
   
@@ -7069,11 +7068,11 @@ module M_creusot_contracts__stdqy35z1__option__extern_spec_std_option_T_Option_T
     
   
   let rec unwrap'0 (self:t_Option'1) (return'  (ret:borrowed t_T'0))= {[@expl:unwrap 'self' type invariant] inv'6 self}
-    {[@expl:unwrap requires] [%#soption8] self <> C_None'1}
-    any [ return' (result:borrowed t_T'0)-> {inv'2 result} {[%#soption8] C_Some'1 result = self} (! return' {result}) ] 
+    {[@expl:unwrap requires] [%#soption0] self <> C_None'1}
+    any [ return' (result:borrowed t_T'0)-> {inv'2 result} {[%#soption0] C_Some'1 result = self} (! return' {result}) ] 
   
   predicate resolve'6 [#"../../../creusot-contracts/src/resolve.rs" 53 4 53 28] (self : borrowed (t_Option'0)) =
-    [%#sresolve9] self.final = self.current
+    [%#sresolve8] self.final = self.current
   
   predicate resolve'3 [#"../../../creusot-contracts/src/resolve.rs" 19 0 19 40] (_1 : borrowed (t_Option'0)) =
     resolve'6 _1
@@ -7216,9 +7215,8 @@ module M_creusot_contracts__stdqy35z1__option__extern_spec_std_option_T_Option_T
   let%span soption3 = "../../../creusot-contracts/src/std/option.rs" 338 58 338 67
   let%span soption4 = "../../../creusot-contracts/src/std/option.rs" 328 26 337 17
   let%span sops5 = "../../../creusot-contracts/src/std/ops.rs" 152 0 174 1
-  let%span soption6 = "../../../creusot-contracts/src/std/option.rs" 31 0 423 1
-  let%span sresolve7 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sinvariant8 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
+  let%span sresolve6 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
+  let%span sinvariant7 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   
   type t_T'0
   
@@ -7240,7 +7238,7 @@ module M_creusot_contracts__stdqy35z1__option__extern_spec_std_option_T_Option_T
   predicate inv'4 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_P'0)
   
   predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 33 4 33 30] (self : borrowed t_T'0) =
-    [%#sinvariant8] inv'0 self.current /\ inv'0 self.final
+    [%#sinvariant7] inv'0 self.current /\ inv'0 self.final
   
   predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : borrowed t_T'0)
   
@@ -7268,7 +7266,7 @@ module M_creusot_contracts__stdqy35z1__option__extern_spec_std_option_T_Option_T
     
   
   predicate resolve'3 [#"../../../creusot-contracts/src/resolve.rs" 53 4 53 28] (self : borrowed t_T'0) =
-    [%#sresolve7] self.final = self.current
+    [%#sresolve6] self.final = self.current
   
   predicate resolve'0 [#"../../../creusot-contracts/src/resolve.rs" 19 0 19 40] (_1 : borrowed t_T'0) =
     resolve'3 _1
@@ -7282,7 +7280,7 @@ module M_creusot_contracts__stdqy35z1__option__extern_spec_std_option_T_Option_T
     end
   
   predicate invariant'1 [#"../../../creusot-contracts/src/invariant.rs" 33 4 33 30] (self : borrowed (t_Option'0)) =
-    [%#sinvariant8] inv'2 self.current /\ inv'2 self.final
+    [%#sinvariant7] inv'2 self.current /\ inv'2 self.final
   
   predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : borrowed (t_Option'0))
   
@@ -7291,12 +7289,12 @@ module M_creusot_contracts__stdqy35z1__option__extern_spec_std_option_T_Option_T
   let rec take'0 (self:borrowed (t_Option'0)) (return'  (ret:t_Option'0))= {[@expl:take 'self' type invariant] inv'3 self}
     any
     [ return' (result:t_Option'0)-> {inv'2 result}
-      {[%#soption6] result = self.current /\ self.final = C_None'0}
+      {[%#soption0] result = self.current /\ self.final = C_None'0}
       (! return' {result}) ]
     
   
   predicate resolve'4 [#"../../../creusot-contracts/src/resolve.rs" 53 4 53 28] (self : borrowed (t_Option'0)) =
-    [%#sresolve7] self.final = self.current
+    [%#sresolve6] self.final = self.current
   
   predicate resolve'1 [#"../../../creusot-contracts/src/resolve.rs" 19 0 19 40] (_1 : borrowed (t_Option'0)) =
     resolve'4 _1