.verifier.expect file cause compilation tests to be ignored

[RustanLeino]

Dafny version

4.2.0

Code to produce this issue

===== TestIt.dfy
// RUN: %testDafnyForEachCompiler "%s"

method Main() {
  ghost var n := 15;
  if j :| 0 <= j < n { // this gives a no-trigger warning
  }
  print "hello\n";
}
===== TestIt.dfy.verifier.expect
TestIt.dfy(5,5): Warning: /!\ No terms found to trigger on.
===== TestIt.dfy.expect
good bye

Command to run and resulting output

DAFNY/Test/dafny0> lit TestIt.dfy
...
-- Testing: 1 tests, 1 workers --
PASS: Dafny :: dafny0/TestIt.dfy (1 of 1)

Testing Time: 2.07s
  Passed: 1

What happened?

When a test in the Dafny test suite has a .verifier.expect file that consists of only warning messages, then TestDafny for-each-compiler never calls the compiler.

As demonstrated by the repro above, the compiled program prints hello and the .expect file expects good bye. Yet, the test passes.

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

Mac