dafny
dafny copied to clipboard
Unstable test: System.NullReferenceException at Microsoft.Boogie.ReadOnlyVisitor.VisitVariable
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()