From cb5666e312e98188a008bb352fe27294d393ba2d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 9 Oct 2024 11:59:05 +0200 Subject: [PATCH] Increase rounding to let SubsetTypes test pass on OSX (#5816) Currently nightly is failing: https://github.com/dafny-lang/dafny/actions/runs/11237776009/job/31265011469 ### Description - Increase rounding to let SubsetTypes test pass on OSX. ### How has this been tested? - The change is to let a test pass By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy | 2 +- .../TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy index 1a450dbf14..19773e1c00 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %verify "%s" --performance-stats=10 --relax-definite-assignment --allow-axioms > "%t" +// RUN: %exits-with 4 %verify "%s" --performance-stats=100 --relax-definite-assignment --allow-axioms > "%t" // RUN: %diff "%s.expect" "%t" module AssignmentToNat { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect index ad13e6b5b6..f1a6f5942d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect @@ -91,5 +91,5 @@ SubsetTypes.dfy(459,15): Error: assertion might not hold SubsetTypes.dfy(464,13): Error: assertion might not hold Dafny program verifier finished with 13 verified, 91 errors -Total resources used is 774980 -Max resources used by VC is 101850 +Total resources used is 775000 +Max resources used by VC is 101900