No Counterexample states generated when using the attribute {:isolate_assertions}

[TomSMaier]

Dafny version

4.8.1

Code to produce this issue

// dafny verify --extract-counterexample input.dfy

// counterexample generated
method F(x: int) {
  assert x != 1;
}
// counterexample not generated
method {:isolate_assertions} F1(x: int) {
  assert x != 1;
}

Command to run and resulting output

$ dafny verify --extract-counterexample input.dfy
input.dfy(5,9): Error: assertion might not hold
 Related counterexample:
 WARNING: the following counterexample may be inconsistent or invalid. See dafny.org/dafny/DafnyRef/DafnyRef#sec-counterexamples
 input.dfy(4,17): initial state:
 assume 1 == x;
 
  |
5 |   assert x != 1;
  |          ^^^^^^

input.dfy(9,9): Error: assertion might not hold
 Related counterexample:
 WARNING: the following counterexample may be inconsistent or invalid. See dafny.org/dafny/DafnyRef/DafnyRef#sec-counterexamples
 
  |
9 |   assert x != 1;
  |          ^^^^^^


Dafny program verifier finished with 1 verified, 2 errors

What happened?

The example has two methods with failing assertions and uses dafny's flag --extract-counterexample for verification.
Dafny behaves as expected for method F and generates a counterexample with assume x == 1.
This line is missing in the output for method F1, which is identical to F, but is annotated with the {:isolated_assertions} attribute.

Discussed with @RustanLeino in-person a few weeks ago.

What type of operating system are you experiencing the problem on?

Mac