Fix perfomance regression

model-checking · Dec 20, 2023 · 6f3dfb6 · 6f3dfb6
1 parent f7e2d82
commit 6f3dfb6
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -230,7 +230,7 @@ impl CodegenBackend for GotocCodegenBackend {
                     let mut items: HashSet<_> = HashSet::with_capacity(harnesses.len());
                     items.extend(harnesses);
                     let harnesses = filter_crate_items(tcx, |_, instance| {
-                        items.contains(&instance.name().intern())
+                        items.contains(&instance.mangled_name().intern())
                     });
                     for harness in harnesses {
                         let model_path = queries.harness_model_path(&harness.name()).unwrap();

diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs
@@ -285,7 +285,7 @@ impl KaniCompiler {
             let all_harnesses = harnesses
                 .into_iter()
                 .map(|harness| {
-                    let def_path = harness.name().intern();
+                    let def_path = harness.mangled_name().intern();
                     let metadata = gen_proof_metadata(tcx, harness, &base_filename);
                     let stub_map = harness_stub_map(tcx, harness, &metadata);
                     (def_path, HarnessInfo { metadata, stub_map })