From 02e33276cc27bc027d79779205d63d0ed6285241 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
Date: Fri, 12 Jul 2024 15:05:44 -0400
Subject: [PATCH] Upgrade toolchain to 7/12 (#3337)

Upgrade toolchain to 7/12

Relevant PRs: https://github.com/rust-lang/rust/pull/127176/
and
https://github.com/rust-lang/rust/pull/125507


Resolves #3319

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs   | 2 +-
 rust-toolchain.toml                                      | 2 +-
 tests/expected/function-contract/const_fn_with_effect.rs | 2 ++
 tools/compiletest/src/json.rs                            | 1 +
 4 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 6e6547295ff9..1703335dda51 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -574,7 +574,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Ref(_, t, _) | ty::RawPtr(t, _) => self.codegen_ty_ref(*t),
             ty::FnDef(def_id, args) => {
                 let instance =
-                    Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
+                    Instance::try_resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
                         .unwrap()
                         .unwrap();
                 self.codegen_fndef_type(instance)
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index dfe3febbb927..f2e8fede457c 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-07-01"
+channel = "nightly-2024-07-12"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/expected/function-contract/const_fn_with_effect.rs b/tests/expected/function-contract/const_fn_with_effect.rs
index d57c1f42fe16..070c44482a80 100644
--- a/tests/expected/function-contract/const_fn_with_effect.rs
+++ b/tests/expected/function-contract/const_fn_with_effect.rs
@@ -1,11 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts -Zmem-predicates
+// compile-flags: -Znext-solver
 
 //! Check that Kani contract can be applied to a constant function.
 //! <https://github.com/model-checking/kani/issues/3258>
 
 #![feature(effects)]
+#![allow(incomplete_features)]
 
 #[kani::requires(kani::mem::can_dereference(arg))]
 const unsafe fn dummy<T>(arg: *const T) -> T {
diff --git a/tools/compiletest/src/json.rs b/tools/compiletest/src/json.rs
index c46c3b3225e8..89c733abc59a 100644
--- a/tools/compiletest/src/json.rs
+++ b/tools/compiletest/src/json.rs
@@ -35,6 +35,7 @@ struct FutureBreakageItem {
 }
 
 #[derive(Deserialize, Clone)]
+#[allow(dead_code)]
 struct DiagnosticSpanMacroExpansion {
     /// name of macro that was applied (e.g., "foo!" or "#[derive(Eq)]")
     _macro_decl_name: String,