[SwayamInSync]

Two chooses with the same condition were two unrelated choices, so this fails with a counterexample on 0.1.1 and main:

cv::proof void same(int n)
  cv::post(cv::choose(k, k > n) == cv::choose(k, k > n))
{
}

error: verification failed: same [...::postcondition@2:33] (counterexample: n [ssa=n_0] [type=i32] = <unknown>) [backend=z3] [reason=counterexample]

and so does a choice over memory across a write to another object:

void write_other(const int *a, int n, int *b, int x)
  cv::pre(valid(a, n) && n >= 1 && n <= 100 && valid(b, 1))
  cv::modifies(*b)
  cv::post(cv::choose(k, 0, n, a[k] == x) == cv::old(cv::choose(k, 0, n, a[k] == x)))
{
  *b = 5;
}

DESIGN says a choose "is a function of the values its body mentions, so it is the same for the same values". Neither failure is a counterexample under that meaning. Three things broke it:

• convertChoose lifted every occurrence to a function of its own (__cppverify_choose_0, __cppverify_choose_1), so the two sides of same were different functions.
• A choice that reads memory is a function of the whole heap. Nothing related its applications in two heap versions, so a write to *b freed the choice over a.
• The certifier reads a choice's value from the model and checks only its axiom, so it certified two different values for one choice whose condition read the same values.

The change:

• Lifted chooses with the same condition are one function. The key is a structural serialization of the range and body: types, callee identities, and memory names included, with bound variables named by position. This is how Verus's AIR shares one closure function among chooses with the same condition (choose_map in air/src/closure.rs). A condition written differently is another choice even when it is equivalent (k > n and n < k), as in Verus.
• addFrameInstances relates each application of a choice that reads memory across every step back from its heap: agree -> c(after) == c(before). The antecedent agree (choiceReadsAgree) states that every load of the condition, at every binder value where it is evaluated, reads the same value in both memories, with its address read in each memory, and the same for every application in it that reads memory. That is the documented meaning stated as a fact, so the array theory does the address reasoning. It covers a store, a call's frame, a store of the value already there, and indirect addresses such as c[a[k]].
• Evaluator::checkChoices accepts two values of one choice with the same other arguments only when some value its condition reads differs between the two memories. readsApart builds a formula that follows the condition's evaluation order: a read differs if its address does or its value does, the right operand of && counts only where the left one held, and a quantifier gives an exists. The certifier's quantifier evaluation decides it. Otherwise the counterexample is unchecked.

Docs: ch13 explains what "the same" means, with checked examples (written alike, a write elsewhere, a write inside, written differently). DESIGN and ARCHITECTURE describe the sharing, the frame, and the certifier's rule. The release notes get an entry under "Failures that were not real".

Testing: Verify/suite/choose_identity.cpp covers:

• chooses that are one choice: written alike, renamed, a quantifier inside the condition, and in ghost code;
• chooses that are not: another condition, another value, another range;
• writes that keep the choice: a store elsewhere, a call that writes elsewhere, and an indirect read;
• a write inside the cells the condition reads, which fails with a checked counterexample.

CertifyTest.ChoicesAreFunctionsOfTheValuesTheyRead gives the certifier two memories that agree on the cells a choice reads (undetermined), and two that differ in one (certified). The lit test fails on main. Each of four mutations fails a test:

• no sharing fails same, renamed, write_other, and call_writes_other;
• no frame fails the three writes elsewhere;
• no certifier check fails the unit test;
• a key with each quantifier's own variable name fails same_inner.

Checked: Verify suite 424 passed, 1 unsupported; VerifyTests 61 passed, 1 skipped (encoding parity, which needs archives). Together with #43, in a build with assertions, the Verify suite passes (425, 1 unsupported). A verdict differential against main over 431 Verify sources (the ULEB128 exhaustive decoder left out: it has no choose, and every change runs only for choices) changes choose_identity.cpp and llvm_uleb128.cpp. In the latter, decode_uleb128_canonical (and roundtrip_uleb128, which relies on it) timed out in main's run under the differential's load; main's binary run alone on that file verifies both, in 60 s. choose_axioms.cpp took 9.7 s instead of 35.4 s, with the same verdicts.