Remy Willems

### Description - Enable the option enforce determinism for the verify command ### How has this been tested? - Updated the tests `ForbidNonDeterminism.dfy` and `ForbidNonDeterminismCompile.dfy` By submitting this pull request,...

Fixes #5671 ### Description Resolved a crash that would occur when using a match statement inside an assert by block ### How has this been tested? Added a CLI test...

### Input Code: ```dafny module M { method {:testEntry} Main() { } } module A { function UnsafeSetToSeq(s: set): seq requires false ensures forall x string, m: map): string {...

Draft 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).

Add `by { ... }` block to method calls

3

Dafny has method calls. Here's an example that shows calling a method with a precondition, and how you can prove that precondition before doing the method call: ```dafny predicate P(x:...

### Description Allow adding --enforce-determinism even when doing resolve, even though it currently has no effect then ### How has this been tested? Not By submitting this pull request, I...

Dafny currently may, when postconditions can not be proven, report a specific return location where those could not be proven, in case there are different return locations. However, this does...

Consecutive assertions meaning there are no assumptions in between. It seems arbitrary that `assert P && Q` would lead to one VC while `assert P; assert Q;` would not. Also,...

Similar to https://github.com/dafny-lang/dafny/pull/5596 but includes an updated Boogie that does not have stack overflows

### Description - Make the new type system the default ### How has this been tested? - Affects all existing tests By submitting this pull request, I confirm that my...