Extra Symtabs leads to conflicting proof harnesses

[YoshikiTakashima]

I tried this code: cargo-kani/vecdeque-cve/

using the following command line invocation: ./scripts/kani-regressions.sh

with Kani version: git clone --branch 1478-bug-replication https://github.com/YoshikiTakashima/kani.git

I expected to see this happen: This test case to pass.

Instead, this happened: The test case fails b/c spurious warnings differ from expected output.

It seems he cause appears to be that passing extra symtabs in kani-driver/src/call_cargo.rs. If that is removed, then the warnings go away.

[celinval]

@YoshikiTakashima How did you conclude that the failure is due to the warnings? Looking at the CI failure here: https://github.com/YoshikiTakashima/kani/runs/7737696525

I see the following errors printed at the bottom:

Error: Conflicting proof harnesses named abstract_remove_maintains_invariant:
2022-08-09T01:54:13.8255351Z  abstract_vecdeque::verification::abstract_remove_maintains_invariant
2022-08-09T01:54:13.8255705Z  abstract_vecdeque::verification::abstract_remove_maintains_invariant
2022-08-09T01:54:13.8255898Z 

[YoshikiTakashima]

@celinval I think you're right. That's the actual cause.

It gave me a "unexpected output" as the message, so I wrongly assumed it was the different input.

[YoshikiTakashima]

More evidence for duplication: It seems proptests are actually running twice:

Checking harness sum_lower_than_2020...
Report written to: target/report-sum_lower_than_2020/html/index.html
Checking harness arbitrary_boolean::arbitrary_boolean...
Report written to: target/report-arbitrary_boolean-arbitrary_boolean/html/index.html
Checking harness proptest_library_is_linked::successfully_linked_proptest...
Report written to: target/report-proptest_library_is_linked-successfully_linked_proptest/html/index.html
Checking harness sum_lower_than_2020...
Report written to: target/report-sum_lower_than_2020/html/index.html
Checking harness arbitrary_boolean::arbitrary_boolean...
Report written to: target/report-arbitrary_boolean-arbitrary_boolean/html/index.html
Checking harness proptest_library_is_linked::successfully_linked_proptest...
Report written to: target/report-proptest_library_is_linked-successfully_linked_proptest/html/index.html

[YoshikiTakashima]

Due to changes in the way we integrate proptest, this issue is no longer blocking.

See the closing comment in #1435

[celinval]

This is a blocker for re-enabling the build cache.