kani-verifier 0.67.0: SMT-solver harness verifies SUCCESSFUL on aarch64 but emits CBMC ERROR (driver panic) on x86_64

[abishekk92]

The same #[kani::solver(z3)] harness produces a deterministic, architecture-dependent divergence between Linux x86_64 and Linux aarch64 on kani-verifier 0.67.0: aarch64 reports VERIFICATION:- SUCCESSFUL, x86_64 trips the cbmc_output_parser.rs:470 unwrap on an ERROR status. Likely related to #4519 / #4540, but with an extra twist: once #4540 ships, x86_64 will still diverge from aarch64, just as VERIFICATION: FAILED instead of a panic.

I tried this code:

The failing harness lives in solana-foundation/anchor#4424 at QEDGen:feat/v2-verification, commit 59a15f55. The single harness is pod::kani_proofs::adversarial::i32_rem_matches_native in lang-v2/src/pod.rs — a #[kani::proof] #[kani::solver(z3)] over i32 % i32 through a #[repr(transparent)] Pod wrapper. I can inline a minimal repro if it helps; starting with the repo link since the bug only manifests for a subset of harnesses inside the crate and I haven't reduced which one yet.

using the following command line invocation:

# Reproduces (exit 101)
docker run --rm --platform linux/amd64 -v $PWD:/repo -w /repo ubuntu:24.04 bash -c '
  apt-get update -qq && apt-get install -qq -y curl ca-certificates build-essential pkg-config libssl-dev git python3 >/dev/null
  curl -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile minimal >/dev/null 2>&1
  export PATH="/root/.cargo/bin:$PATH"
  cargo install --locked kani-verifier --version 0.67.0 >/dev/null 2>&1
  cargo kani setup >/dev/null 2>&1
  RUST_BACKTRACE=1 cargo kani -p anchor-lang-v2 --harness pod::kani_proofs::adversarial::i32_rem_matches_native
'

# Does NOT reproduce (exit 0): same script, --platform linux/arm64 (or omit on aarch64 host)

with Kani version: 0.67.0 (on both arches; cargo kani setup downloads the arch-appropriate bundle).

I expected to see this happen:

VERIFICATION:- SUCCESSFUL on both architectures — the harness is pure i32 % i32 in a #[repr(transparent)] newtype and has no reason to behave differently across arches. This is what aarch64 reports.

Instead, this happened on x86_64:

Checking harness pod::kani_proofs::adversarial::i32_rem_matches_native...

thread '<unnamed>' panicked at kani-driver/src/cbmc_output_parser.rs:470:25:
called `Result::unwrap()` on an `Err` value: Error("unknown variant `ERROR`, expected one of `FAILURE`, `COVERED`, `SATISFIED`, `SUCCESS`, `UNDETERMINED`, `UNKNOWN`, `UNREACHABLE`, `UNCOVERED`, `UNSATISFIABLE`", line: 16, column: 25)

(Happy to re-run with a fuller RUST_BACKTRACE=1 trace if useful — output above is the relevant tail; the rest of the suite's ~130 other harnesses before and after this one verify successfully.)

Questions for maintainers:

1. Is the CBMC+Z3 bundle shipped by cargo kani setup the same version across architectures? If not, the x86_64 vs aarch64 divergence likely lives in there rather than in kani-driver.
2. Is CBMC emitting ERROR on x86_64 for this harness a known CBMC/Z3-side issue?
3. Once Fix CBMC output parser panic when using SMT solvers #4540 reaches a release, x86_64 users will see VERIFICATION: FAILED (encountered a solver error) while aarch64 users see SUCCESSFUL on the same source. Should that second-order divergence also be tracked?

Happy to provide a reduced single-file repro, RUST_BACKTRACE=1 output, or CBMC/Z3 versions from the bundle if any of that would help.

[abishekk92]

Update after further testing — the bug is broader than the #[kani::solver(z3)] symbolic-rem pattern I originally reported.

I tried splitting the failing i32_rem_matches_native harness into per-concrete-divisor variants (symbolic dividend, concrete b ∈ {1, 2, 7, -1, -2, -7, i32::MAX, i32::MIN}), matching the pattern the codebase already uses for a similar previously-diagnosed x86_64 CBMC issue on symbolic usize × usize multiplication. On Linux x86_64 (Ubuntu 24.04 under Rosetta, kani-verifier 0.67.0) that split verifies cleanly — all 13 new harnesses report VERIFICATION:- SUCCESSFUL. So the x86_64 abort is specifically on symbolic-operand bitvector ops; concrete operands dodge it.

However, the same run surfaced two other harnesses in the same suite that trigger the identical panic:

TRIGGER: pod::kani_proofs::adversarial::u32_saturating_mul_max_matches_native
TRIGGER: pod::kani_proofs::wide_ops::pod_u128_roundtrip

The second one is surprising and strictly strengthens the bug report. Its body has zero arithmetic:

#[kani::proof]
#[kani::solver(z3)]
fn pod_u128_roundtrip() {
    let x: u128 = kani::any();
    assert!(PodU128::from(x).get() == x);
}

PodU128 is a #[repr(transparent)] newtype over u128; .get() reads it back. Purely a symbolic 128-bit roundtrip through a transparent wrapper, no +/*/%. Same panic:

thread '<unnamed>' panicked at kani-driver/src/cbmc_output_parser.rs:470:25:
called `Result::unwrap()` on an `Err` value: Error("unknown variant `ERROR`, ...")

Same architecture pattern: fails on Linux x86_64, passes on aarch64-linux and macOS aarch64.

Revised read:

• The abort isn't about symbolic arithmetic complexity — it fires on simple 128-bit symbolic values flowing through a #[repr(transparent)] wrapper.
• Whatever CBMC emits as ERROR during encoding on x86_64, it's happening upstream of solver dispatch. The #[kani::solver(z3)] annotation is consistently irrelevant — dropping it and letting the default solver handle the same harness also panics.

Happy to extract pod_u128_roundtrip into a standalone ~15-line single-file repro with no other dependencies if that'd help maintainers diagnose without cloning the full PR. Just say the word.