Remy Willems

@hmijail could you use `--solver-log` to see if the logs are different for two differently behaving executions? Or otherwise, could you provide a reproduction, so I can try to do...

Thanks, having a reproduction is great. We'll schedule diving into this. > In case it helps, in a 200-iterations batch I got an even rarer error: That's a completely different...

I think a user friendly way of reproducing a certain iteration, would be for each iteration to emit which --random-seed argument should be used to reproduce that iteration. In Dafny...

> Maybe connected: I just noticed that running single iterations vs multiple iterations yields very different Resource Count values in the CSV file. > > I had a 1000-iteration CSV...

> While we're at it, what would you think of adding some more direct control of the random number being used, so that one can jump back into a given...

> causes a weird error that disappears with Is that with the released Dafny 4.4 ? Not with the nightly

> I expect that making those names consistent across all usage modes should solve the problem. I agree, it would be good to do that to prevent confusion.

I can confirm this issue does not occur when using VSCode. `dafny server` has code to kill `z3` processes when it exits, but I'm not sure if this only runs...

> but this doesn't clean up all of the instances of z3 or dotnet When I have a `dafny server` process and I kill it with SIGTERM, I see that...

Partially completed with https://github.com/dafny-lang/dafny/pull/3715