diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index bd4da57ee..73ad36949 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -62,7 +62,7 @@ jobs: # Run unit tests dotnet test --no-build -c ${{ matrix.configuration }} ${SOLUTION} # Run lit test suite - lit --param ${{ matrix.lit_param }} -v --timeout=120 -D configuration=${{ matrix.configuration }} Test + lit --param ${{ matrix.lit_param }} -v --timeout=240 -D configuration=${{ matrix.configuration }} Test - name: Deploy to nuget # Note: if you change the build matrix, update the following # line to ensure it matches only one element of the matrix. diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index 63b763de0..a4112ccf2 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -139,8 +139,10 @@ private async Task StartCheck(int iteration, Split split, Checker checker, Cance { var splitNum = split.SplitIndex + 1; var splitIdxStr = options.RandomizeVcIterations > 1 ? $"{splitNum} (iteration {iteration})" : $"{splitNum}"; - run.OutputWriter.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...", - split.Stats, splitIdxStr, total, 100 * provenCost / (provenCost + remainingCost)); + run.OutputWriter.WriteLine(" checking split {1}/{2}{3}, {4:0.00}%, {0} ...", + split.Stats, splitIdxStr, total, + split is ManualSplit manualSplit ? $" (line {manualSplit.Token.line})" : "", + 100 * provenCost / (provenCost + remainingCost)); } callback.OnProgress?.Invoke("VCprove", split.SplitIndex, total, diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index b9e426474..b9ae5c918 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie -lib:base -lib:node -vcsSplitOnEveryAssert "%s" > "%t" +// RUN: %parallel-boogie -lib:base -lib:node -vcsSplitOnEveryAssert -trace "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype LocPiece { Left(), Right() }