Fix Rlimitouts0.bpl

boogie-org · Aug 8, 2024 · 830ac55 · 830ac55
1 parent 735fee4
commit 830ac55
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 7 deletions.
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
@@ -65,7 +65,10 @@ public static int Main(string[] args)
       Helpers.ExtraTraceInformation(options, "Becoming sentient");
 
       var source = new CancellationTokenSource();
-      source.CancelAfter(TimeSpan.FromSeconds(options.ProcessTimeLimit));
+      if (options.ProcessTimeLimit != 0)
+      {
+        source.CancelAfter(TimeSpan.FromSeconds(options.ProcessTimeLimit));
+      }
 
       var success = executionEngine.ProcessFiles(Console.Out, fileList, cancellationToken: source.Token).Result;
       if (options.XmlSink != null)

diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs
@@ -126,9 +126,13 @@ private async IAsyncEnumerable<IVerificationStatus> StartRun([EnumeratorCancella
       yield return new Running();
 
       var collector = new VerificationResultCollector(Split.Options);
-      await engine.LargeThreadTaskFactory.StartNew(() => Split.BeginCheck(Split.Run.OutputWriter, checker, collector,
-        modelViewInfo, timeout, Split.Run.Implementation.GetResourceLimit(Split.Options), cancellationToken), cancellationToken).Unwrap().
-        WaitAsync(TimeSpan.FromSeconds(timeout), cancellationToken);
+      var beginCheckTask = engine.LargeThreadTaskFactory.StartNew(() => Split.BeginCheck(Split.Run.OutputWriter, checker, collector,
+        modelViewInfo, timeout, Split.Run.Implementation.GetResourceLimit(Split.Options), cancellationToken), cancellationToken).Unwrap();
+      if (timeout != 0)
+      {
+        beginCheckTask = beginCheckTask.WaitAsync(TimeSpan.FromSeconds(timeout), cancellationToken);
+      }
+      await beginCheckTask;
 
       await checker.ProverTask.WaitAsync(cancellationToken);
       var result = Split.ReadOutcome(0, checker, collector);

diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs
@@ -151,8 +151,13 @@ await run.OutputWriter.WriteLineAsync(string.Format(CultureInfo.InvariantCulture
       var timeout = KeepGoing && split.LastChance ? options.VcsFinalAssertTimeout :
         KeepGoing ? options.VcsKeepGoingTimeout :
         run.Implementation.GetTimeLimit(options);
-      await split.BeginCheck(run.OutputWriter, checker, callback, mvInfo, timeout,
-        Implementation.GetResourceLimit(options), cancellationToken).WaitAsync(TimeSpan.FromSeconds(timeout), cancellationToken);
+      var beginCheckTask = split.BeginCheck(run.OutputWriter, checker, callback, mvInfo, timeout,
+        Implementation.GetResourceLimit(options), cancellationToken);
+      if (timeout != 0)
+      {
+        beginCheckTask = beginCheckTask.WaitAsync(TimeSpan.FromSeconds(timeout), cancellationToken);
+      }
+      await beginCheckTask;
     }
 
     private Implementation Implementation => run.Implementation;

diff --git a/Test/test2/Rlimitouts0.bpl b/Test/test2/Rlimitouts0.bpl
@@ -1,5 +1,5 @@
 // We use boogie here because parallel-boogie doesn't work well with -proverLog
-// RUN: %boogie -rlimit:800000 -proverLog:"%t.smt2" "%s"
+// RUN: %boogie -processTimeLimit:0 -timeLimit:0 -rlimit:800000 -proverLog:"%t.smt2" "%s"
 // RUN: %OutputCheck --file-to-check "%t.smt2" "%s"
 // CHECK-L: (set-option :timeout 4000)
 // CHECK-L: (set-option :rlimit 800000)