This PR is a quick fix for issues #697 and #698.

The problem: Unsound comprehensions with subset types.

For-comprehensions, Exist-comprehensions, Map-comprehensions and Set-comprehensions had a problem when encountering subset types: Dafny was not emiting the code of the subset constraint, to ensure that the constraint of the comprehension is not executed with undesirable data.
The solution implemented in this PR:
Added field [ConstraintIsCompilable](https://github.com/dafny-lang/dafny/pull/1522/files#diff-7d845d452486b0b59700ca5c133f2648f76d44616148081d51efffe32dbc6e7aR2680) for SubsetTypeDecl expressions.
If a comprehension uses a subsettype whose ConstraintIsCompilable is false, will raise two errors, the second one indicating why it is not compilable
In the compiler, the function [MaybeInjectSubsetConstraint](https://github.com/dafny-lang/dafny/pull/1522/files#diff-998a9162635a910ca366a26c8f679ea96d6bbb3f703a52ca1487fd19599de49dR4743) which injects the guard code for for-comprehensions, exists-comprehensions, map-comprehensions and set-comprehensions.

How I tested it.

I added 8 tests:

git-issues/git-issue-697.dfy: A set comprehension with compilable subset constraint that did not compile correctly and used to crash at execution. Now it compiles and does not crash.
git-issues/git-issue-697b.dfy: A map comprehension with compilable subset constraint that did not compile correctly and used to crash at execution. Now it compiles and does not crash.
git-issues/git-issue-697c.dfy: A set comprehension, a map comprehension and a forall comprehension with ghost subset constraint that used to compile and crash at execution. Now it does not compiles and raises six errors.
git-issues/git-issue-697d.dfy: A set comprehension with ghost & compilable subset constraint that used to compile and crash at execution. Now it compiles and does not crash.
git-issues/git-issue-697e.dfy: A forall comprehension with only inferred ghost subset constraint. It used to compile and crash at execution time. Now it compiles and does not crash.
git-issues/git-issue-697f.dfy: A ghost subset constraint that is never used in comprehensions. It used to compile and continues to compile, ensuring this PR does not break this existing desirable behavior.
git-issues/git-issue-698.dfy: A forall comprehension with compilable subset constraint that did not compile correctly and used to crash at execution. Now it compiles and does not crash.
git-issues/git-issue-698b.dfy: An exist comprehension with compilable subset constraint that did not compile correctly and used to crash at execution. Now it compiles and does not crash.

Previously we relied on enforcing this at review time. This PR adds a warning in the IDE and fixes all current violations. dotnet-format can only enforce this when analysing a whole project, which is surprisingly expensive (30s), so we don't make changes to the pre-commit hook at this time.
dotnet tool run dotnet-format -s error -w Source/Dafny.sln

Also moved .editorconfig so it affects all files (including the `.cs` files under `Test`).

* Move customBoogie references one level higher

* Update msbuild build file

Co-authored-by: Remy Willems <>

Adding a Python Compiler which can pass the test IKnowThisMuchIs.dfy.

…1627)

add `dotnet_style_parentheses_in_other_binary_operators` as a warning and fix violations

…tion behavior of the proof (#1612)

In DafnyOptions.cs, turn on Boogie's `Prune` and `NormaliseNames` option, and turn off `EmitDebugInformation`, to increase verification stability. Use `uses` clauses on constants and functions, both in DafnyPrelude.bpl and in generated Boogie declarations, and the `include_dep` attribute on axioms, to ensure not too much is pruned. More information on these Boogie features can be found in the PRs that introduce them: boogie-org/boogie#450, boogie-org/boogie#452, boogie-org/boogie#453, boogie-org/boogie#454, boogie-org/boogie#464

In follow-up PRs, we will replace all `include_dep` with `uses` clauses, since they allow more but still correct pruning.

This PR also updates the test `SchorrWaite.dfy` to make it more stable. Changes stolen from #1620

Resolves #1499, by introducing a new interface above the existing abstract class containing shared functionality for the constructors, along with new tests. (See the updated comment for `CompileDatatypeBase`) We don't provide an implementation of `DowncastCopy` in this PR.