Use of 'const' in pattern matching results in error (unhandled exception)

[franck44]

Dafny version

4.1.0

Code to produce this issue

const BB := false 

function test(a: bool): bool 
{
    match a 
        case BB => false 
        case _ => true
}

Command to run and resulting output

dafny verify

What happened?

Running dafny verify on the previous code generates the following message:

Unhandled exception. System.AggregateException: One or more errors occurred. (Value cannot be null. (Parameter 'source'))
 ---> System.ArgumentNullException: Value cannot be null. (Parameter 'source')
   at System.Linq.ThrowHelper.ThrowArgumentNullException(ExceptionArgument argument)
   at System.Linq.Enumerable.Select[TSource,TResult](IEnumerable`1 source, Func`2 selector)
   at Microsoft.Dafny.Substituter.<>c__DisplayClass7_1.<Substitute>g__SubstituteForPattern|0(ExtendedPattern pattern)
   at Microsoft.Dafny.Substituter.Substitute(Expression expr)
   at Microsoft.Dafny.Translator.GetFunctionAxiom(Function f, Expression body, List`1 lits)
   at Microsoft.Dafny.Translator.AddFunctionAxiom(Function boogieFunction, Function f, Expression body)
   at Microsoft.Dafny.Translator.AddClassMember_Function(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 Microsoft.Dafny.DafnyDriver.Translate(ExecutionEngineOptions options, Program dafnyProgram)+MoveNext()
   at System.Collections.Generic.List`1..ctor(IEnumerable`1 collection)
   at System.Linq.Enumerable.ToList[TSource](IEnumerable`1 source)
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args)
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.<Main>b__0()
   at System.Threading.Thread.StartCallback()

If I am correct this issue did not exist with Dafny 3. However when I run dafny /dafnyVerify:1 /compile:0 /mimicVerificationOf:3.3 with Dafny 4.1.0 it results in the same error message.

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

Mac

[fabiomadge]

Thanks for the report! Fortunately, this was likely fixed by #4170. You can try the nightly build in case you want to be sure.

[franck44]

@fabiomadge Thanks for that. Yes nightly build fixes the issue.
Sorry my bad, I had a look at previous issues and filtered them to see if it had already been reported but must have missed #4170.