You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When verifying a closed-source Dafny program and pressing ctrl+C in the shell, the following exception occurs.
Unhandled exception. System.AggregateException: One or more errors occurred.(Objectreference not set to an instance of an object.)---> System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.SMTLib.SMTLibProcess.Send(String cmd)
at Microsoft.Boogie.SMTLib.SMTLibProcess.PingPong()
at Microsoft.Boogie.Checker.GoBackToIdle()
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)
at VC.ConditionGeneration.VerifyImplementation(ImplementationRun run, CancellationToken cancellationToken)
at Microsoft.Boogie.ExecutionEngine.VerifyImplementationWithoutCaching(ProcessedProgram processedProgram, PipelineStatistics stats, ErrorReporterDelegate er, CancellationToken cancellationToken, String programId, Implementation impl, TextWriter traceWriter)
at Microsoft.Boogie.ExecutionEngine.VerifyImplementation(ProcessedProgram processedProgram, PipelineStatistics stats, ErrorReporterDelegate er, CancellationToken cancellationToken, Implementation implementation, String programId, TextWriter traceWriter)
at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass38_0.<<VerifyEachImplementation>b__1>d.MoveNext()--- End of stack trace from previous location ---
at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass38_0.<<VerifyEachImplementation>b__1>d.MoveNext()--- End of stack trace from previous location ---
at Microsoft.Boogie.ExecutionEngine.VerifyEachImplementation(TextWriter output, ProcessedProgram processedProgram, PipelineStatistics stats, String programId, ErrorReporterDelegate er, String requestId, Implementation[] stablePrioritizedImpls)
at Microsoft.Boogie.ExecutionEngine.InferAndVerify(TextWriter output, Program program, PipelineStatistics stats, String programId, ErrorReporterDelegate er, String requestId)
at Microsoft.Dafny.Main.BoogiePipelineWithRerun(TextWriter output, ExecutionEngine engine, Program program, String bplFileName, String programId)
at Microsoft.Dafny.Main.BoogieOnce(TextWriter output, ExecutionEngine engine, String baseFile, String moduleName, Program boogieProgram, String programId)
at Microsoft.Dafny.DafnyDriver.BoogieOnceWithTimerAsync(TextWriter output, String baseName, String programId, String moduleName, Program program)
at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass20_0.<<BoogieAsync>b__0>d.MoveNext()--- End of stack trace from previous location ---
at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass20_0.<<BoogieAsync>b__0>d.MoveNext()--- End of stack trace from previous location ---
at Microsoft.Dafny.DafnyDriver.BoogieAsync(String baseName, IEnumerable`1 boogiePrograms, String programId)
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()
The text was updated successfully, but these errors were encountered:
When verifying a closed-source Dafny program and pressing ctrl+C in the shell, the following exception occurs.
The text was updated successfully, but these errors were encountered: