Kani unwinds forever on semver-pubgrub

[zhassan-aws]

Steps to reproduce:

1. git clone https://github.com/pubgrub-rs/semver-pubgrub
2. cd semver-pubgrub
3. git reset --hard 2d8221eb8b00e3a72e107e384bec48b5dc048837
4. cd fuzz
5. Add the following harness at the end of fuzz_targets/contains.rs:

[kani::proof]

[kani::unwind(2)]

fn check_estimate_size() { use semver_pubgrub::SemverPubgrub; let ver = semver::Version { major: 0, minor: 0, patch: 0, pre: semver::Prerelease::EMPTY, build: semver::BuildMetadata::EMPTY, }; let op = if kani::any() { semver::Op::Exact } else { semver::Op::Less }; let req = semver::Comparator { op, major: 0, minor: Some(0), patch: Some(0), pre: semver::Prerelease::EMPTY, }; let req = semver::VersionReq { comparators: vec![req] }; let mat = req.matches(&ver);

let pver: SemverPubgrub = (&req).into(); // this line 

}

5. Run `cargo kani`

with Kani version: 0.44.0

Kani keeps unwinding for several minutes without converging.

[zhassan-aws]

If I remove the non-determinism by replacing this line:

    let op = if kani::any() { semver::Op::Exact } else { semver::Op::Less };

with:

    let op = semver::Op::Exact ;

Kani completes in ~13 seconds:

SUMMARY:
 ** 0 of 4986 failed (219 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 13.343105s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.