You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
#4798 inadvertently broke this by having dafny verify use more common code with the language server, and as a result BoogieOnce is never actually called.
Discovered while getting #5060 to work, and I may be able to fix it there, but cutting this in case it doesn't fit in that scope.
The text was updated successfully, but these errors were encountered:
…ent (#5086)
Fixes#5067
### Description
Make the error reporter for checking if Z3 is available, more consistent
between the IDE and various CLI commands
### How has this been tested?
Updated CLI and IDE tests
<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Attempting to verify source without Z3 installed used to print a big helpful error message: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyCore/DafnyMain.cs#L109
#4798 inadvertently broke this by having
dafny verify
use more common code with the language server, and as a result BoogieOnce is never actually called.Discovered while getting #5060 to work, and I may be able to fix it there, but cutting this in case it doesn't fit in that scope.
The text was updated successfully, but these errors were encountered: