Addressing code review leftovers

cprover_bindings/src/goto_program/symbol.rs

@@ -386,7 +386,7 @@ impl Symbol {
  self
  }
 
- /// Set `is_property` to true.
+ /// Set `is_property`.
  pub fn with_is_property(mut self, v: bool) -> Self {
  self.is_property = v;
  self

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -256,6 +256,7 @@ impl<'tcx> GotocCtx<'tcx> {
  pub fn attach_contract(&mut self, instance: Instance<'tcx>, contract: Vec<Local>) {
  // This should be safe, since the contract is pretty much evaluated as
  // though it was the first (or last) assertion in the function.
+ assert!(self.current_fn.is_none());
  self.set_current_fn(instance);
  let goto_contract = self.as_goto_contract(contract);
  let name = self.current_fn().name();