Error reporting

[Osmansiddiquer]

Dafny version

4.10.0

Code to produce this issue

pset3_definitions.dfy:
// This file defines some functions that we ask you to prove lemmas about.
// Please don't modify it or turn it in.

module Defs {
  datatype list<T> = Nil | Cons(head: T, tail: list<T>)

  function Length<T>(l: list<T>): nat {
    match l
    case Nil => 0
    case Cons(_, l') => 1 + Length(l')
  }

  type binary = list<bool>

  datatype trie = Leaf(included: bool) | Node(included: bool, left: trie, right: trie)

  predicate Member(b: binary, t: trie) {
    match t
    case Leaf(inc) => inc && b == Nil
    case Node(inc, left, right) =>
      match b
      case Nil => inc
      case Cons(false, b') => Member(b', left)
      case Cons(true, b') => Member(b', right)
  }
}

pset.dfy
include "pset3_definitions.dfy"


lemma Add_correct(n: Defs.binary, m: Defs.binary)
    requires Defs.Length(n) == Defs.Length(m)
    ensures BinaryToNat(Add(n, m)) == BinaryToNat(n) + BinaryToNat(m) 
  {
    match n
    case Nil => {}
    case Cons(head, Nil) => {

    }
    case Cons(head, tail) => {
      var (sum, carry) := addBits(head, m.head, false);
      assert n == Defs.Nil ==> m == Defs.Nil;
      assert q: tail != Defs.Nil && m.tail != Defs.Nil;
      assert AddWithCarry(n, m, false) == Defs.Cons(sum, AddWithCarry(tail, m.tail, carry))
      by { reveal q; }
      calc == {
        BinaryToNat(Add(n, m));
        BinaryToNat(AddWithCarry(n, m, false));
        BinaryToNat(Defs.Cons(sum, AddWithCarry(tail, m.tail, carry)));
        BinaryToNat(Add(tail, m.tail));
        BinaryToNat(tail) + BinaryToNat(m.tail);
        BinaryToNat(Defs.Cons(head, tail)) + BinaryToNat(m);
        BinaryToNat(n) + BinaryToNat(m);
      }
    }
  }

Command to run and resulting output

Open vscode, try saving file (to trigger testing)

What happened?

Here is the error log: Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)

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

Windows