assigned causes crash with relaxed definite assignment

[RustanLeino]

Dafny version

4.9.1

Code to produce this issue

method M() {
  var x := 3;
  assert assigned(x); // this crashes with:  dafny verify --relax-definite-assignment test.dfy
}

Command to run and resulting output

% dafny verify --relax-definite-assignment test.dfy
Encountered internal compilation exception: Object reference not set to an instance of an object.
test.dfy(1,7): Error: Internal error occurred during verification: Object reference not set to an instance of an object.
    at Microsoft.Dafny.BoogieGenerator.SplitExprInfo..ctor(Boolean reportRanges, K kind, Expr e) in DAFNY/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs:line 660
    at Microsoft.Dafny.BoogieGenerator.ToSplitExprInfo(K kind, Expr e) in DAFNY/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs:line 644
    at Microsoft.Dafny.BoogieGenerator.TrSplitExpr(BodyTranslationContext context, Expression expr, List`1 splits, Boolean position, Int32 heightLimit, Boolean applyInduction, ExpressionTranslator etran) in DAFNY/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs:line 434
    at Microsoft.Dafny.BoogieGenerator.TrSplitExpr(BodyTranslationContext context, Expression expr, ExpressionTranslator etran, Boolean applyInduction, Boolean& splitHappened) in DAFNY/Source/DafnyCore/Verifier/BoogieGenerator.cs:line 4506
    at Microsoft.Dafny.BoogieGenerator.TrAssertCondition(PredicateStmt stmt, ExpressionTranslator etran, BoogieStmtListBuilder proofBuilder) in DAFNY/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs:line 150
    at Microsoft.Dafny.BoogieGenerator.TrAssertStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran) in DAFNY/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs:line 86
    at Microsoft.Dafny.BoogieGenerator.TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran) in DAFNY/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs:line 24
    at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran) in DAFNY/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs:line 32
    at Microsoft.Dafny.BoogieGenerator.TrStmtList(List`1 stmts, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran, IOrigin scopeRange, Boolean processLabels) in DAFNY/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs:line 843
    at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran) in DAFNY/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs:line 293
    at Microsoft.Dafny.BoogieGenerator.TrMethodBody(Method m, BoogieStmtListBuilder builder, Variables localVariables, ExpressionTranslator etran) in DAFNY/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs:line 818
    at Microsoft.Dafny.BoogieGenerator.AddMethodImpl(Method m, Procedure proc, Boolean wellformednessProc) in DAFNY/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs:line 563
    at Microsoft.Dafny.BoogieGenerator.AddMethod_Top(Method m, Boolean isByMethod, Boolean includeAllMethods) in DAFNY/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs:line 213
    at Microsoft.Dafny.BoogieGenerator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods, Boolean includeInformationAboutType) in DAFNY/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs:line 82
    at Microsoft.Dafny.BoogieGenerator.AddRevealableTypeDecl(RevealableTypeDecl d) in DAFNY/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs:line 884
    at Microsoft.Dafny.BoogieGenerator.DoTranslation(Program p, ModuleDefinition forModule) in DAFNY/Source/DafnyCore/Verifier/BoogieGenerator.cs:line 805
    at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.<>c__DisplayClass3_1.<GetVerificationTasksAsync>b__0() in DAFNY/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs:line 53
    at System.Threading.Tasks.Task`1.InnerInvoke()
    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(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken) in DAFNY/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs:line 46
    at Microsoft.Dafny.Compilation.<>c__DisplayClass58_1.<<VerifyUnverifiedSymbol>b__1>d.MoveNext() in DAFNY/Source/DafnyCore/Pipeline/Compilation.cs:line 344
 --- End of stack trace from previous location ---
    at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed) in DAFNY/Source/DafnyCore/Pipeline/Compilation.cs:line 343
    at DafnyDriver.Commands.CliCompilation.VerifyAllLazily(Nullable`1 randomSeed)+MoveNext() in DAFNY/Source/DafnyDriver/CliCompilation.cs:line 275
  |
1 | method M() {
  | ^^^^^^^^^^^^

What happened?

The assigned function crashes the dafny tool under --relax-definite-assignment.

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

Mac