Fix simlpe havoc

model-checking · Nov 21, 2023 · 64f7e5f · 64f7e5f
1 parent b833438
commit 64f7e5f
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs
@@ -603,10 +603,10 @@ impl<'a> ContractConditionsHandler<'a> {
  )
  }
  ContractConditionsData::Modifies { attr } => {
- let args = make_wrapper_args(attr.len());
  quote!(
  let result = #call_to_prior;
- #(*#args = kani::any();)*
+ #(*#attr = kani::any();)*
+ result
  )
  }
  }