Remy Willems

Thanks for the feedback. I believe you're correct that the current behavior is confusing. I believe intuitive syntax is critical for a compelling language and I hope we can prioritize...

Marking as enhancement instead of bug, since this is documented behavior.

This is an error reporting issue. The message `Error: trigger must mention all quantified variables, but does not mention: o#0` comes from Boogie but is emitted is a non-standard way,...

I haven't been able to reproduce this on macOS. Could you look in the `Dafny VSCode` output channel? It should say which Dafny binary it's launching, like this: ``` Language...

> I have a copy of Z3 installed already - is there a way to tell it to use the system version You can use the `--solver-path=pathToYourZ3binary` option to specify...

More logging PR, to show the entire stacktrace: https://github.com/dafny-lang/dafny/pull/5387

Still occurs: https://github.com/dafny-lang/dafny/actions/runs/10417507125/job/28851913718?pr=5695

Now we have the stacktrace, so maybe we can fix it: ``` at System.Collections.Generic.Dictionary`2.Enumerator.MoveNext() at System.Linq.Enumerable.ToDictionary[TSource,TKey,TElement](IEnumerable`1 source, Func`2 keySelector, Func`2 elementSelector, IEqualityComparer`1 comparer) at System.Linq.Enumerable.ToDictionary[TSource,TKey,TElement](IEnumerable`1 source, Func`2 keySelector, Func`2 elementSelector)...

I could reproduce this

I can't reproduce this on 4.6, neither in the IDE nor the CLI: ``` rwillems@bcd0745419f2 Sync % dafny --version 4.6.0 rwillems@bcd0745419f2 Sync % dafny verify ./temp.dfy Temp/temp.dfy(4,6): Error: the type...