Update kani-compiler/src/kani_middle/reachability.rs

model-checking · Dec 8, 2023 · 29ac962 · 29ac962
1 parent 5415041
commit 29ac962
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
@@ -153,7 +153,7 @@ impl<'tcx> MonoItemsCollector<'tcx> {
  /// instruction looking for the items that should be included in the compilation.
  fn reachable_items(&mut self) {
  while let Some(to_visit) = self.queue.pop() {
- if !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id()) {
+ if !self.collected.contains(&to_visit) {
  self.collected.insert(to_visit.clone());
  let next_items = match &to_visit {
  MonoItem::Fn(instance) => self.visit_fn(*instance),