Error: Dafny encountered an internal error while waiting for this symbol to verify.

[benreynwar]

Dafny version

4.6.0

Code to produce this issue

I'm hitting in a reproducible error in a github action for my project.
I'm pretty new to dafny so I expect the real cause is that I'm doing something silly, but presumably it shouldn't be giving this error despite that.
Sorry for not creating a minimal example to show what the problem is. Feel free to ignore this issue. I'm mostly just submitting the issue because the error message told me too :).

https://github.com/benreynwar/SiLemma/actions/runs/8546419158/job/23416730258

The error message is:

Utils/SetExt.dfy(27,39):
Utils/SetExt.dfy(27,39): Error: Dafny encountered an internal error while waiting for this symbol to verify. Please report it at <https://github.com/dafny-lang/dafny/issues>.
 
   |
27 |     lemma {:vcs_split_on_every_assert} ThereIsAMinimum<T(!new)>(s: set<T>, R: (T, T)->bool)
   |                                        ^^^^^^^^^^^^^^^
Dafny program verifier finished with 105 verified, 0 errors
: Dafny encountered an internal error while waiting for this symbol to verify. Please report it at <https://github.com/dafny-lang/dafny/issues>.
 
   |
27 |     lemma {:vcs_split_on_every_assert} ThereIsAMinimum<T(!new)>(s: set<T>, R: (T, T)->bool)
   |                                        ^^^^^^^^^^^^^^^
Dafny program verifier finished with 105 verified, 0 errors

Command to run and resulting output

https://github.com/benreynwar/SiLemma/actions/runs/8546419158/job/23416730258

What happened?

Utils/SetExt.dfy(27,39): Error: Dafny encountered an internal error while waiting for this symbol to verify. Please report it at <https://github.com/dafny-lang/dafny/issues>.
 
   |
27 |     lemma {:vcs_split_on_every_assert} ThereIsAMinimum<T(!new)>(s: set<T>, R: (T, T)->bool)
   |                                        ^^^^^^^^^^^^^^^
Dafny program verifier finished with 105 verified, 0 errors

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

Linux

[benreynwar]

Also this bug appeared after I added --verification-time-limit=30 to the command line arguments for dafny verify so it may be related to that. The verification for the previous commit was taking a long time so I cancelled a job. After adding this argument the job quickly failed with the internal error shown above.

[keyboardDrummer]

Thanks for reporting. This is useful.

For the Dafny maintainer, a program such as:

lemma f() {
    var a:int := 0x0000_0010_DEAD_BEEF;
    var testbv:bv64 := a as bv64;
    var testval:int := testbv as int;

    assert testval == a; // "Timed out on: assertion violation"
}

Currently causes the Boogie verification to hang, ignoring any specified time out, and then the Dafny front-end detects the hang and reports the internal error.

We should fix the Boogie handling of the time out.

[kjx]

For what it's worth, I've had the same problem or at least seen the same symptoms.
I had fantasies of finishing something this week so don't really have time to minimise my example, /
but it is here - #5209

If it helps, I can confirm absolutely that I do not see this but at all in version 4.4.0+598c2c3ec6bf5c78a3c5c4f30b570f23cca417a9