Crash in translator

[MikaelMayer]

Dafny version

4.1.0

Code to produce this issue

function Crash(e: nat, max: nat): string
{
  assert match e { case _ => e < max };
  ""
}

Command to run and resulting output

Paste in VSCode

What happened?

It crashes with the following stack trace:

Dafny encountered an internal error. Please report it at <https://github.com/dafny-lang/dafny/issues>.
cce+UnreachableException: Exception of type 'cce+UnreachableException' was thrown.
   at Microsoft.Dafny.Translator.CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.CheckWellformed(Expression expr, WFOptions options, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrStmt_CheckWellformed(Expression expr, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran, Boolean subsumption, Boolean lValueContext)
   at Microsoft.Dafny.Translator.TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions options, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.AddWellformednessCheck(Function f)
   at Microsoft.Dafny.Translator.AddFunction_Top(Function f, Boolean includeAllMethods)
   at Microsoft.Dafny.Translator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods, Boolean includeInformationAboutType)
   at Microsoft.Dafny.Translator.AddTypeDecl(RevealableTypeDecl d)
   at Microsoft.Dafny.Translator.DoTranslation(Program p, ModuleDefinition forModule)
   at Microsoft.Dafny.Translator.Translate(Program p, ErrorReporter reporter, TranslatorFlags flags)+MoveNext()
   at System.Collections.Generic.List`1..ctor(IEnumerable`1 collection)
   at System.Linq.Enumerable.ToList[TSource](IEnumerable`1 source)
   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.<>c__DisplayClass5_0.<GetVerificationTasksAsync>b__1()
   at System.Threading.Tasks.Task`1.InnerInvoke()
   at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
--- End of stack trace from previous location ---
   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(DocumentAfterResolution document, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.Compilation.PrepareVerificationTasksAsync(DocumentAfterResolution loaded, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.Compilation.TranslateAsync()

What type of operating system are you experiencing the problem on?

Windows

[DavePearce]

FYI: this looks related to issue #4000, though the exception raised does differ.

[stefan-aws]

Can confirm the crash on my Mac in VSCode with 4.1.0.