From 05db7d3c6d3c7f0c029e3262b3ce623b719d3d6c Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Tue, 17 Oct 2023 11:15:14 -0700
Subject: [PATCH] Simplify to just removing rlimit multiplication

---
 Source/Core/AST/Absy.cs                      | 6 +-----
 Source/ExecutionEngine/CommandLineOptions.cs | 9 +--------
 Test/test2/Rlimitouts0.bpl                   | 6 +++---
 3 files changed, 5 insertions(+), 16 deletions(-)

diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
index 7ffef6251..43e8a5ee3 100644
--- 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
index c3ef127c8..74652d52e 100644
--- 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
index f0cd1dec2..8e7efe0cd 100644
--- 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;