Autoharness --constructor-args: mined-invariant filtering of types with their own Arbitrary is not marked "(ctor)" #4995

With --constructor-args, the automatic harness assumes a type's mined invariants for every generated struct or enum value, including values of types that already implement Arbitrary (AutomaticHarnessPass in kani-compiler/src/kani_middle/transform/automatic.rs). The "(ctor)" marker, however, is decided by uses_ctor_generation in kani-compiler/src/kani_middle/mod.rs, which returns false as soon as the type implements Arbitrary directly. A harness whose inputs were narrowed by mined invariants can therefore report Success without the "(ctor)" marker or the note after the summary table, so the user is not told that the result only covers the filtered values.

Reproducer:

pub struct Level {
    v: u8,
}

impl Level {
    pub fn first(&self) -> u8 {
        assert!(self.v >= 1);
        self.v
    }
    pub fn second(&self) -> u8 {
        assert!(self.v >= 1);
        self.v - 1
    }
}

#[cfg(kani)]
impl kani::Arbitrary for Level {
    fn any() -> Self {
        Level { v: kani::any() }
    }
}

pub fn check_level(l: Level) {
    assert!(l.v != 0, "zero level");
}

1. cargo kani autoharness -Z autoharness --include-pattern 'check_level$' reports Failure ("zero level"), since the hand-written Arbitrary can produce v == 0.
2. The same command with --constructor-args reports Success for check_level, with kind #[kani::proof]: no "(ctor)" marker and no note after the table. The mined condition self.v >= 1 was assumed for the generated value.
3. For comparison, an identical type without the hand-written Arbitrary impl gets #[kani::proof] (ctor) under --constructor-args.

This is related to #4763: the mined-invariant filter is heuristic, and the "(ctor)" marker is how users learn that a result only covers filtered values. Until this is resolved, the autoharness reference page will describe this case among the soundness caveats (#4991).

Tested with Kani 0.68.0 and CBMC 6.11.0.