All issues

Search results

Spurious counterexample: second i128 struct field reported as possibly-modified after an Err early-return (cross-crate), while the first field verifies

Status: Open.

#108 In Certora/CertoraProver;

· mshakeg opened on Jul 22, 2026

sub: unsound rewrite

Status: Open.

#107 In Certora/CertoraProver;

· intrigus-lgtm opened on Jul 21, 2026

sqrtByDiv3: incorrect rewrite

Status: Open.

#106 In Certora/CertoraProver;

· intrigus-lgtm opened on Jul 21, 2026

negation: incorrect rewrite leading to missing revert

Status: Open.

#105 In Certora/CertoraProver;

· intrigus-lgtm opened on Jul 21, 2026

division-comparison: incorrect rewrite for negative dividend

Status: Open.

#104 In Certora/CertoraProver;

· intrigus-lgtm opened on Jul 21, 2026

const-prop: wrong rewrite for x / x -> 1

Status: Open.

#103 In Certora/CertoraProver;

· intrigus-lgtm opened on Jul 21, 2026

const-prop: wrong rewrite for 1 %n -> 1

Status: Open.

#102 In Certora/CertoraProver;

· intrigus-lgtm opened on Jul 21, 2026

bipropagation: missing guard for mod

Status: Open.

#101 In Certora/CertoraProver;

· intrigus-lgtm opened on Jul 21, 2026

smod: incorrect rewrite for SMod(x, y) -> x due to missing magnitude test

Status: Open.

#100 In Certora/CertoraProver;

· intrigus-lgtm opened on Jul 21, 2026

smod: incorrect encoding leads to incorrectly pruned path

Status: Open.

#99 In Certora/CertoraProver;

· intrigus-lgtm opened on Jul 21, 2026

havoc: potentially missing havoc for unresolved call

Status: Open.

#98 In Certora/CertoraProver;

· intrigus-lgtm opened on Jul 21, 2026

cvl: havoc of a packed storage field is incorrectly pinned to zero

Status: Open.

#97 In Certora/CertoraProver;

· intrigus-lgtm opened on Jul 21, 2026