dafny icon indicating copy to clipboard operation
dafny copied to clipboard

Unstable test: System.NullReferenceException at Microsoft.Boogie.ReadOnlyVisitor.VisitVariable

Open keyboardDrummer opened this issue 11 months ago • 3 comments

Run: https://github.com/dafny-lang/dafny/actions/runs/5760643103/job/15617339950?pr=4357

[xUnit.net 00:19:12.55]   Finished:    IntegrationTests
  Failed VSI-Benchmarks/b6.dfy [14 s]
  Error Message:
   System.Exception : Command returned non-zero exit code (134): dotnet /home/runner/work/dafny/dafny/dafny/Source/IntegrationTests/bin/Debug/net6.0/Dafny.dll /vcsCores:2 /useBaseNameForFileName /compileVerbose:0 /timeLimit:300 /showSnippets:0 /compile:0 TestFiles/LitTests/LitTest/VSI-Benchmarks/b6.dfy > /home/runner/work/dafny/dafny/dafny/Source/IntegrationTests/bin/Debug/net6.0/TestFiles/LitTests/LitTest/VSI-Benchmarks/Output/b6.dfy.tmp
Output:

Error:
Unhandled exception. 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.Boogie.ReadOnlyVisitor.VisitVariable(Variable node)
   at Microsoft.Boogie.ReadOnlyVisitor.VisitVariableSeq(List`1 variableSeq)
   at Microsoft.Boogie.ReadOnlyVisitor.VisitImplementation(Implementation node)
   at Microsoft.Boogie.Implementation.StdDispatch(StandardVisitor visitor)
   at Microsoft.Boogie.ReadOnlyVisitor.Visit(Absy node)
   at Microsoft.Boogie.ReadOnlyVisitor.VisitDeclarationList(List`1 declarationList)
   at Microsoft.Boogie.ReadOnlyVisitor.VisitProgram(Program node)
   at Microsoft.Boogie.Program.StdDispatch(StandardVisitor visitor)
   at Microsoft.Boogie.ReadOnlyVisitor.Visit(Absy node)
   at Microsoft.Boogie.BasicTypeVisitor..ctor(Absy absy)
   at Microsoft.Boogie.Checker.Target(Program prog, ProverContext ctx, Split split)
   at VC.CheckerPool.PrepareChecker(Program program, Split split, Checker checker)
   at VC.CheckerPool.FindCheckerFor(ConditionGeneration vcgen, Split split, CancellationToken cancellationToken)
   at VC.SplitAndVerifyWorker.DoWork(Int32 iteration, Split split, CancellationToken cancellationToken)
   at VC.SplitAndVerifyWorker.DoWorkForMultipleIterations(Split split, CancellationToken cancellationToken)
   at VC.SplitAndVerifyWorker.WorkUntilDone(CancellationToken cancellationToken)
   at VC.VCGen.VerifyImplementation(ImplementationRun run, VerifierCallback callback, CancellationToken cancellationToken, IObserver`1 batchCompletedObserver)
   at VC.ConditionGeneration.VerifyImplementation(ImplementationRun run, IObserver`1 batchCompletedObserver, CancellationToken cancellationToken)
   at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass47_0.<<VerifyImplementationWithoutCaching>b__0>d.MoveNext()

keyboardDrummer avatar Aug 04 '23 10:08 keyboardDrummer