Dafny version

4.3.0

Code to produce this issue

// code produced by ChatGPT: https://chat.openai.com/share/820efb2e-9060-47fa-bbbd-d02fec598d10

datatype Expr =
    | Const(value: int)
    | Var(name: string)
    | Add(left: Expr, right: Expr)
    | Mult(left: Expr, right: Expr)

function Eval(expr: Expr, env: map<string, int>): int
{
    match expr
        case Const(value) => value
        case Var(name) => if name in env then env[name] else 0
        case Add(left, right) => Eval(left, env) + Eval(right, env)
        case Mult(left, right) => Eval(left, env) * Eval(right, env)
}

function Optimize(expr: Expr): Expr
{
    match expr
        case Const(value) => Const(value)
        case Var(name) => Var(name)
        case Add(left, right) =>
            match (Optimize(left), Optimize(right))
                case (Const(lv), Const(rv)) => Const(lv + rv)
                case (Const(0), rv) => rv
                case (lv, Const(0)) => lv
                case (lv, rv) => Add(lv, rv)
        case Mult(left, right) =>
            match (Optimize(left), Optimize(right))
                case (Const(lv), Const(rv)) => Const(lv * rv)
                case (Const(0), _) => Const(0)
                case (_, Const(0)) => Const(0)
                case (Const(1), rv) => rv
                case (lv, Const(1)) => lv
                case (lv, rv) => Mult(lv, rv)
}

lemma Lemma_OptimizerPreservesSemantics(expr: Expr, env: map<string, int>)
    ensures Eval(expr, env) == Eval(Optimize(expr), env)
{
    match expr
        case Const(value) =>
            // For constants, the optimized expression is the same as the original.
        case Var(name) =>
            // For variables, the optimized expression is the same as the original.
        case Add(left, right) =>
            // Inductive step for addition.
            Lemma_OptimizerPreservesSemantics(left, env);
            Lemma_OptimizerPreservesSemantics(right, env);
        case Mult(left, right) =>
            // Inductive step for multiplication.
            Lemma_OptimizerPreservesSemantics(left, env);
            Lemma_OptimizerPreservesSemantics(right, env);
}

Command to run and resulting output

dafny verify opt0_chatgpt.dfy

What happened?

% dafny verify opt0_chatgpt.dfy
Unhandled exception. System.AggregateException: One or more errors occurred. (One or more errors occurred. (One or more errors occurred. (Object reference not set to an instance of an object.)))
---> System.AggregateException: One or more errors occurred. (One or more errors occurred. (Object reference not set to an instance of an object.))
---> System.AggregateException: One or more errors occurred. (Object reference not set to an instance of an object.)
---> System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Dafny.MatchFlattener.LetBind(IdPattern var, Expression genExpr, PatternPath bodyPath) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs:line 734
at Microsoft.Dafny.MatchFlattener.LetBindNonWildCard(IdPattern idPattern, Expression expr, PatternPath bodyPath) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs:line 757
at Microsoft.Dafny.MatchFlattener.CompileHeadsContainingConstructor(MatchCompilationState mti, MatchingContext context, Cons1 matchees, Dictionary2 subst, Dictionary2 constructorByName, List1 paths) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs:line 365
at Microsoft.Dafny.MatchFlattener.CompilePatternPathsForMatchee(MatchCompilationState state, MatchingContext context, List1 paths, Cons1 consMatchees) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs:line 262
at Microsoft.Dafny.MatchFlattener.CompilePatternPaths(MatchCompilationState state, MatchingContext context, SinglyLinkedList1 matchees, List1 paths) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs:line 223
at Microsoft.Dafny.MatchFlattener.CompileNestedMatchExpr(NestedMatchExpr nestedMatchExpr) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs:line 90
at Microsoft.Dafny.MatchFlattener.<>c__DisplayClass5_0.b__0(INode node) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs:line 74
at Microsoft.Dafny.Node.Visit(Func2 beforeChildren, Action1 afterChildren) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/Generic/Node.cs:line 143
at Microsoft.Dafny.MatchFlattener.FlattenNode(Node root) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs:line 57
at Microsoft.Dafny.MatchFlattener.<>c__DisplayClass5_0.b__0(INode node) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs:line 75
at Microsoft.Dafny.Node.Visit(Func2 beforeChildren, Action1 afterChildren) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/Generic/Node.cs:line 143
at Microsoft.Dafny.MatchFlattener.FlattenNode(Node root) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs:line 57
at Microsoft.Dafny.MatchFlattener.PostResolve(ModuleDefinition module) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs:line 53
at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs:line 168
at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/Resolver/ModuleResolver.cs:line 184
at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/Resolver/ProgramResolver.cs:line 174
at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/Resolver/ProgramResolver.cs:line 68
at Microsoft.Dafny.DafnyMain.<>c__DisplayClass5_0.b__0() in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/DafnyMain.cs:line 89
at System.Threading.Tasks.Task.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 inner exception stack trace ---
at System.Threading.Tasks.Task.Wait(Int32 millisecondsTimeout, CancellationToken cancellationToken)
at System.Threading.Tasks.Task.Wait()
at Microsoft.Dafny.DafnyMain.Resolve(Program program) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/DafnyMain.cs:line 89
at Microsoft.Dafny.DafnyMain.ParseCheck(TextReader stdIn, IReadOnlyList1 files, String programName, DafnyOptions options, Program& program) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyCore/DafnyMain.cs:line 54 at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IReadOnlyList1 dafnyFiles, ReadOnlyCollection1 otherFileNames, DafnyOptions options, Boolean lookForSnapshots, String programId) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyDriver/DafnyDriver.cs:line 453 --- End of inner exception stack trace --- at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions) at System.Threading.Tasks.Task1.GetResultCore(Boolean waitCompletionNotification)
at System.Threading.Tasks.Task1.get_Result() at Microsoft.Dafny.DafnyDriver.ThreadMain(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, String[] args) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyDriver/DafnyDriver.cs:line 149 at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass11_0.<MainWithWriters>b__0() in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyDriver/DafnyDriver.cs:line 120 at System.Threading.Tasks.Task1.InnerInvoke()
at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj)
at System.Threading.ExecutionContext.RunFromThreadPoolDispatchLoop(Thread threadPoolThread, ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
at System.Threading.ExecutionContext.RunFromThreadPoolDispatchLoop(Thread threadPoolThread, ExecutionContext executionContext, ContextCallback callback, Object state)
at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
--- End of inner exception stack trace ---
at System.Threading.Tasks.Task1.GetResultCore(Boolean waitCompletionNotification) at System.Threading.Tasks.Task1.get_Result()
at Microsoft.Dafny.DafnyDriver.MainWithWriters(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, String[] args) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyDriver/DafnyDriver.cs:line 120
at Microsoft.Dafny.DafnyDriver.Main(String[] args) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/DafnyDriver/DafnyDriver.cs:line 107
at Dafny.Dafny.Main(String[] args) in /private/tmp/dafny-20230929-7192-1ta7rj5/dafny-4.3.0/Source/Dafny/Dafny.cs:line 7
zsh: abort dafny verify opt0_chatgpt.dfy

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

Linux, Mac