Skip to content

Commit 6a85ff1

Browse files
Small improvement to pruning datatypes when using spinoff_prover
1 parent f01fbda commit 6a85ff1

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

source/vir/src/prune.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -933,7 +933,7 @@ pub fn prune_krate_for_module_or_krate(
933933
}
934934
for d in &krate.datatypes {
935935
match &d.x.owning_module {
936-
Some(path) if is_root_module(path) => {
936+
Some(path) if is_root_module(path) && fun.is_none() => {
937937
// our datatype
938938
let t = ReachedType::Datatype(d.x.name.clone());
939939
reach(&mut state.reached_types, &mut state.worklist_types, &t);

0 commit comments

Comments
 (0)