Add :reproducible_resource_limit attribute (#796)

This doesn't multiply by 1000, unlike `:rlimit`. The corresponding CLI
flag is `/reproducibleResourceLimit`.

I'm a little unsure about the name. It's a bit of a mouthful. Maybe
leaving out "reproducible" would be better.

Fixes #795.

Source/ExecutionEngine/CommandLineOptions.cs

@@ -1206,7 +1206,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
           return true;
 
         case "rlimit":
-          ps.GetUnsignedNumericArgument(x => ResourceLimit = x, null);
+          ps.GetUnsignedNumericArgument(x => ResourceLimit = x);
           return true;
 
         case "timeLimitPerAssertionInPercent":
@@ -1978,7 +1978,7 @@ 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
+                Limit the Z3 resource spent trying to verify each procedure.
   /errorTrace:<n>
                 0 - no Trace labels in the error output,
                 1 (default) - include useful Trace labels in error output,

Source/VCGeneration/Checker.cs

@@ -150,7 +150,7 @@ private void SetTimeout(uint timeout)
 
     private void SetRlimit(uint rlimit)
     {
-      TheoremProver.SetRlimit(Util.BoundedMultiply(rlimit, 1000));
+      TheoremProver.SetRlimit(rlimit);
     }
 
     /// <summary>

Test/test0/MaxKeepGoingSplits.bpl

@@ -16,7 +16,7 @@ function f(i:int, j:int) returns (int)
 }
 
 // Without the max keep going splits this runs out of resources.
-procedure {:rlimit 150} test1(x:int)
+procedure {:rlimit 150000} test1(x:int)
 {
     assert(f(8,3) == 0);
     assert(f(8,4) == 0);
@@ -25,7 +25,7 @@ procedure {:rlimit 150} test1(x:int)
 }
 
 // Runs out of resources
-procedure {:rlimit 150} test2(x:int)
+procedure {:rlimit 150000} test2(x:int)
 {
     assert(f(8,3) == 0 && f(8,4) == 0 && f(8,5) == 0 && f(9,2) == 0);
 }

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 {:rlimit 1000} 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;
 

Test/test2/git-issue-366.bpl

@@ -1,4 +1,4 @@
-// RUN: %parallel-boogie -rlimit:5 /proverOpt:O:smt.qi.eager_threshold=100 "%s" > "%t"
+// RUN: %parallel-boogie -rlimit:5000 /proverOpt:O:smt.qi.eager_threshold=100 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function f(i:int, j:int) returns (int)