Simplify to just removing rlimit multiplication

boogie-org · Oct 17, 2023 · 05db7d3 · 05db7d3
1 parent d282653
commit 05db7d3
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 16 deletions.
diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
@@ -730,11 +730,7 @@ public uint GetTimeLimit(CoreOptions options)
     public uint GetResourceLimit(CoreOptions options)
     {
       uint rl = options.ResourceLimit;
-      if(CheckUIntAttribute("rlimit", ref rl)) {
-          rl = Util.BoundedMultiply(rl, 1000);
-      }
-      // If the new option exists, it takes precedence.
-      CheckUIntAttribute("reproducible_resource_limit", ref rl);
+      CheckUIntAttribute("rlimit", ref rl);
       if (rl < 0) {
         rl = options.ResourceLimit;
       }

diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs
@@ -1206,11 +1206,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
           return true;
 
         case "rlimit":
-          ps.GetUnsignedNumericArgument(x => ResourceLimit = Util.BoundedMultiply(x, 1000), null);
-          return true;
-
-        case "reproducibleResourceLimit":
-          ps.GetUnsignedNumericArgument(x => ResourceLimit = x, null);
+          ps.GetUnsignedNumericArgument(x => ResourceLimit = x);
           return true;
 
         case "timeLimitPerAssertionInPercent":
@@ -1982,9 +1978,6 @@ Set num to 0 to find as many assertion failures as possible.
                 Limit the number of seconds spent trying to verify
                 each procedure
   /rlimit:<num>
-                Limit the Z3 resource spent trying to verify each procedure,
-                where <num> is multiplied by 1000 before being sent to Z3.
-  /reproducibleResourceLimit:<num>
                 Limit the Z3 resource spent trying to verify each procedure.
   /errorTrace:<n>
                 0 - no Trace labels in the error output,

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:800 -proverLog:"%t.smt2" "%s"
+// RUN: %boogie -rlimit:800000 -proverLog:"%t.smt2" "%s"
 // RUN: %OutputCheck --file-to-check "%t.smt2" "%s"
 // CHECK-L: (set-option :timeout 0)
 // CHECK-L: (set-option :rlimit 800000)
@@ -43,7 +43,7 @@ procedure TestTimeouts1(in: [int]int, len: int) returns (out: [int]int);
   requires 0 < len;
   ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);
 
-implementation {:rlimit 900} TestTimeouts1(in: [int]int, len: int) returns (out: [int]int)
+implementation {:rlimit 900000} TestTimeouts1(in: [int]int, len: int) returns (out: [int]int)
 {
     var i : int;
 
@@ -72,7 +72,7 @@ procedure TestTimeouts2(in: [int]int, len: int) returns (out: [int]int);
   requires 0 < len;
   ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);
 
-implementation {:reproducible_resource_limit 1000000} TestTimeouts2(in: [int]int, len: int) returns (out: [int]int)
+implementation {:rlimit 1000000} TestTimeouts2(in: [int]int, len: int) returns (out: [int]int)
 {
     var i : int;