[SwayamInSync]

A spec that applied itself inside cppverify::choose was not recursive to the verifier: the calls in a choose's body were never checked against the measure, so a definition could contradict itself, and a proof could use it to show anything.

cppverify::spec int stuck(int n)
  cppverify::decreases(n)
{
  return n <= 0 ? 0 : stuck(n - 1) + cppverify::choose(k, n == 1 ? k == stuck(n) + 1 : k == 0);
}

int forty_two(int x)
  cppverify::post(cppverify::result == 42)
{
  cppverify::check(stuck(x) == stuck(x));
  if (x == 1)
    return 0;
  return 42;
}

stuck(1) would have to equal stuck(1) + 1. On main both the termination of stuck and forty_two verify, although forty_two(1) returns 0. Without decreases, such a spec was accepted as a plain axiom, and an inductive predicate could apply itself inside a choose, where it is not positive.

A choose is lifted to a function of its own, but it is evaluated where it is written, so its calls now belong to that function:

• A function reaches what its chooses apply. A spec that applies itself inside a choose is recursive and needs decreases, and an inductive predicate whose group is applied inside one is rejected.
• Every call in a choose's body must lower the measure for every value of its binder, as under forall and exists.
• In the spec's own termination and post checks, the choose's axiom is assumed only where those calls lower the measure, like the facts of its other recursive calls. The counterexample is then certified (stuck fails at n = 1) instead of needing the spec's own hidden definition.

Testing: suite/choose_recursion.cpp and suite/choose_recursion_errors.cpp fail on main, where forty_two verifies in both, stuck terminates, unbounded is an axiom, and liar is accepted. Removing the axiom guard from either check turns stuck or stuck_post into spec.hidden; never assuming the axiom fails pick, whose termination needs it. Verify suite: 399 passed, 1 unsupported. A verdict differential against main over the 405 Verify sources (2142 verdicts) changes nothing.