a_timed_out_goal_is_retried_at_double_the_timeout fails on a slow host
because it asserts that no goal flips, while its own fixture has a provable goal
whose time is a property of the machine.
Reproduction
Ubuntu 24.04 riscv64 in qemu-system-riscv64 (TCG, 16 vCPU), Frama-C 33.0,
Alt-Ergo 2.6.3, at main plus #25. It fails when run alone and in all three full
stdio runs:
cargo test --test test-mcp-stdio a_timed_out_goal_is_retried_at_double_the_timeout
panicked at tests/test-mcp-stdio.rs:7599:5
"timed_out_first_pass": 2, "still_unproved": 1,
"flipped": [{"wpo_id": "typed_nocast_slow_assert_rte_signed_overflow",
"name": "Assertion 'rte,signed_overflow'", "property": "#p18"}]
It passes on macOS (Apple Silicon).
Cause
tests/fixtures/prover-timeout.c asserts
(a*a*a + b*b*b != c*c*c) || (a == 0 && b == 0 && c == 0) under
0 <= a, b, c <= 1000. No prover discharges that assertion. RTE adds
signed-overflow obligations for the cubes, and those are provable, since
1000³ fits in an int, but nonlinear.
At a 1 s timeout on this host, two goals time out: one of those overflow
obligations, and one that stays unproved at 2 s. The overflow obligation proves
at the 2 s retry, so it flips.
The test already says the count depends on the machine (lines 7595-7596):
how many of the overflow obligations exhaust one second is a fact about the
machine
It then asserts (lines 7599-7600) that every goal that timed out is still
unproved and that flipped is empty. That only holds when every overflow
obligation that exceeds 1 s also exceeds 2 s. The doc comment (lines 7559-7563)
gives the reason for leaving flips to the unit test
a_flip_is_a_goal_that_timed_out_and_then_proved: a real flip "is a fact about
the machine rather than about the fixture". That same fact is what makes these
two assertions depend on the machine.
Suggested direction
Pin only what the fixture guarantees. The Fermat assertion never proves, so it
is always timed out and never flipped. Checking timed_out = still_unproved + flipped.len(), and that no flipped entry is the assertion itself, keeps the
retry, the doubled timeout and the cache check without assuming how fast the
overflow obligations are.
a_timed_out_goal_is_retried_at_double_the_timeoutfails on a slow hostbecause it asserts that no goal flips, while its own fixture has a provable goal
whose time is a property of the machine.
Reproduction
Ubuntu 24.04 riscv64 in qemu-system-riscv64 (TCG, 16 vCPU), Frama-C 33.0,
Alt-Ergo 2.6.3, at main plus #25. It fails when run alone and in all three full
stdio runs:
It passes on macOS (Apple Silicon).
Cause
tests/fixtures/prover-timeout.casserts(a*a*a + b*b*b != c*c*c) || (a == 0 && b == 0 && c == 0)under0 <= a, b, c <= 1000. No prover discharges that assertion. RTE addssigned-overflow obligations for the cubes, and those are provable, since
1000³ fits in an
int, but nonlinear.At a 1 s timeout on this host, two goals time out: one of those overflow
obligations, and one that stays unproved at 2 s. The overflow obligation proves
at the 2 s retry, so it flips.
The test already says the count depends on the machine (lines 7595-7596):
It then asserts (lines 7599-7600) that every goal that timed out is still
unproved and that
flippedis empty. That only holds when every overflowobligation that exceeds 1 s also exceeds 2 s. The doc comment (lines 7559-7563)
gives the reason for leaving flips to the unit test
a_flip_is_a_goal_that_timed_out_and_then_proved: a real flip "is a fact aboutthe machine rather than about the fixture". That same fact is what makes these
two assertions depend on the machine.
Suggested direction
Pin only what the fixture guarantees. The Fermat assertion never proves, so it
is always timed out and never flipped. Checking
timed_out = still_unproved + flipped.len(), and that no flipped entry is the assertion itself, keeps theretry, the doubled timeout and the cache check without assuming how fast the
overflow obligations are.