From 09203428d55ba79b5ddcf97eb92be9c5883414c5 Mon Sep 17 00:00:00 2001
From: Zekun Wang <41706692+fEst1ck@users.noreply.github.com>
Date: Mon, 29 Apr 2024 18:48:58 -0400
Subject: [PATCH] bug fix (#13117)

GitOrigin-RevId: 87a7f1d10d295a965634fe9abe2067535ab24aa8
---
 language/move-compiler-v2/src/unused_params_checker.rs | 4 +++-
 language/move-prover/src/lib.rs                        | 6 ++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/language/move-compiler-v2/src/unused_params_checker.rs b/language/move-compiler-v2/src/unused_params_checker.rs
index 10a32f49e4..276b8dc3d6 100644
--- a/language/move-compiler-v2/src/unused_params_checker.rs
+++ b/language/move-compiler-v2/src/unused_params_checker.rs
@@ -17,7 +17,9 @@ pub fn unused_params_checker(env: &GlobalEnv) {
     for module in env.get_modules() {
         if module.is_target() {
             for struct_env in module.get_structs() {
-                check_unused_params(&struct_env);
+                if !struct_env.is_ghost_memory() {
+                    check_unused_params(&struct_env);
+                }
             }
         }
     }
diff --git a/language/move-prover/src/lib.rs b/language/move-prover/src/lib.rs
index f5d5c00a79..b822dee5e0 100644
--- a/language/move-prover/src/lib.rs
+++ b/language/move-prover/src/lib.rs
@@ -85,8 +85,7 @@ pub fn run_move_prover_v2<W: WriteColor>(
         warn_unused: false,
         whole_program: false,
         compile_test_code: false,
-    }
-    .set_experiment(Experiment::UNUSED_STRUCT_PARAMS_CHECK, false);
+    };
 
     let mut env = move_compiler_v2::run_move_compiler_for_analysis(error_writer, compiler_options)?;
     run_move_prover_with_model_v2(&mut env, error_writer, options, now)
@@ -120,8 +119,7 @@ pub fn run_move_prover_with_model<W: WriteColor>(
     // Run the compiler v2 checking and rewriting pipeline
     let compiler_options = move_compiler_v2::Options::default()
         .set_experiment(Experiment::OPTIMIZE, false)
-        .set_experiment(Experiment::SPEC_REWRITE, true)
-        .set_experiment(Experiment::UNUSED_STRUCT_PARAMS_CHECK, false);
+        .set_experiment(Experiment::SPEC_REWRITE, true);
     env.set_extension(compiler_options.clone());
     let pipeline = move_compiler_v2::check_and_rewrite_pipeline(
         &compiler_options,