search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.94k stars 263 forks source link

Dafny doesn't always respect `/timeLimit` or `--verification-time-limit` #3894

Open atomb opened 1 year ago

atomb commented 1 year ago

Dafny version

4.0.0

Code to produce this issue

Unfortunately, I don't have an example input handy at the moment. I'll edit this issue to add one when I do.

Command to run and resulting output

$ dafny /timeLimit:1 foo.dfy
... hangs ...

What happened?

It should report that the proof has timed out.

The issue is that the parameter to Z3 that controls the time limit for an individual query is a "soft" limit. If the solver gets stuck too deeply in one decision procedure, it may not check the time and therefore may not quit. The solver also has a "hard" time limit, but that limit causes Z3 to unceremoniously quit after the process has been running for a particular amount of time, which doesn't play well with keeping a long-running process to solve many queries in a row.

So, what we should probably do is set a timer in Dafny when issuing a query. If Z3 hasn't responded when the timer goes off, restart Z3 and report a timeout.

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

Mac

kjx commented 1 year ago

for what it's worth, I think I've seen this too...

OlivierTOMATO commented 3 months ago

I have this problem as well. Is there any solution till now?

keyboardDrummer commented 3 months ago

I have this problem as well. Is there any solution till now?

Any chance you could provide a reproduction?

kjx commented 3 months ago

Not in anything small, I'm afraid, not..

the nightly seems to loop much less often