Simplify use of SMT options

Source/Provers/SMTLib/ProverInterface.cs

@@ -274,7 +274,7 @@ public virtual void SetOtherSMTOption(string name, string value)
   {
   }
 
-  public virtual void ClearOtherSMTOptions()
+  public virtual void ClearLocalSMTOptions()
   {
   }
 

Source/Provers/SMTLib/ProverUtil.cs

@@ -22,7 +22,6 @@ public class ProverOptions
     public uint ResourceLimit = 0;
     // Other options suitable for (set-option :key value)
     // TODO: put ResourceLimit in here?
-    public Dictionary<string, string> OtherOptions = new();
     public int? RandomSeed = null;
     public int MemoryLimit = 0;
     public int Verbosity = 0;

Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Concurrent;
 using System.Collections.Generic;
+using System.ComponentModel.Design;
 using System.IO;
 using System.Linq;
 using System.Diagnostics;
@@ -433,15 +434,14 @@ protected void SendVCOptions()
       if (options.Solver == SolverKind.Z3 || options.Solver == SolverKind.NoOpWithZ3Options)
       {
         SendThisVC("(set-option :" + Z3.TimeoutOption + " " + options.TimeLimit + ")");
-        SendThisVC("(set-option :" + Z3.RlimitOption + " " + options.ResourceLimit + ")");
         if (options.RandomSeed != null) {
           SendThisVC("(set-option :" + Z3.SmtRandomSeed + " " + options.RandomSeed.Value + ")");
           SendThisVC("(set-option :" + Z3.SatRandomSeed + " " + options.RandomSeed.Value + ")");
         }
       }
 
-      foreach (var entry in options.OtherOptions) {
-        SendThisVC("(set-option :" + entry.Key + " " + entry.Value + ")");
+      foreach (var entry in options.SmtOptions) {
+        SendThisVC("(set-option :" + entry.Option + " " + entry.Value + ")");
       }
     }
 
@@ -1162,26 +1162,36 @@ public override void AssertAxioms()
       FlushAxioms();
     }
 
+    // This doesn't use SetOtherSMTOption because it may be set using
+    // different mechanisms than set-option in some cases.
     public override void SetTimeout(uint ms)
     {
       options.TimeLimit = ms;
     }
 
-    // TODO: make this use SetOtherSMTOption?
+    // Don't use SetOtherSMTOption directly, because we want a
+    // connection to TimeLimit.
     public override void SetRlimit(uint limit)
     {
-      options.ResourceLimit = limit;
+      if (options.Solver == SolverKind.Z3) {
+        SetOtherSMTOption(Z3.RlimitOption, limit.ToString());
+        if (limit > 0) {
+          SetTimeout(0);
+        }
+      }
     }
 
     // Note: must be re-set for every query
     public override void SetOtherSMTOption(string name, string value)
     {
-      options.OtherOptions[name] = value;
+      options.SmtOptions.Add(new OptionValue(name, value));
     }
 
-    public override void ClearOtherSMTOptions()
+    public override void ClearLocalSMTOptions()
     {
-      options.OtherOptions.Clear();
+      // Go back to global options
+      options.SmtOptions.Clear();
+      options.Parse(libOptions.ProverOptions);
     }
 
     protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown)

Source/VCGeneration/Checker.cs

@@ -306,7 +306,7 @@ private async Task Check(string descriptiveName, VCExpr vc, CancellationToken ca
       proverRunTime = ProverStopwatch.Elapsed;
     }
 
-    public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, uint timeout, uint rlimit, Dictionary<string, string> otherSMTOptions, CancellationToken cancellationToken)
+    public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, CancellationToken cancellationToken)
     {
       Contract.Requires(descriptiveName != null);
       Contract.Requires(vc != null);
@@ -319,16 +319,6 @@ public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.
       this.handler = handler;
 
       await thmProver.Reset(gen);
-      if (0 < rlimit)
-      {
-        timeout = 0;
-      }
-
-      thmProver.SetTimeout(timeout);
-      thmProver.SetRlimit(rlimit);
-      foreach (var entry in otherSMTOptions) {
-        thmProver.SetOtherSMTOption(entry.Key, entry.Value);
-      }
 
       ProverStart = DateTime.UtcNow;
       ProverStopwatch.Restart();

Source/VCGeneration/SmokeTester.cs

@@ -305,8 +305,10 @@ async Task<bool> CheckUnreachable(TextWriter traceWriter, Block cur, List<Cmd> s
           Emit();
         }
       }
-      await checker.BeginCheck(cce.NonNull(Implementation.Name + "_smoke" + id++), vc, new ErrorHandler(Options, absyIds, callback),
-        Options.SmokeTimeout, Options.ResourceLimit, new(), CancellationToken.None);
+
+      checker.TheoremProver.SetTimeout(Options.SmokeTimeout);
+      checker.TheoremProver.SetRlimit(Options.ResourceLimit);
+      await checker.BeginCheck(cce.NonNull(Implementation.Name + "_smoke" + id++), vc, new ErrorHandler(Options, absyIds, callback), CancellationToken.None);
 
       await checker.ProverTask;
 

Source/VCGeneration/Split.cs

@@ -1353,8 +1353,12 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa
           Print();
         }
 
-        var extraSMTOpts = Implementation.GetExtraSMTOptions();
-        await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, extraSMTOpts, cancellationToken);
+        checker.TheoremProver.SetTimeout(Util.BoundedMultiply(timeout, 1000));
+        checker.TheoremProver.SetRlimit(rlimit);
+        foreach (var entry in Implementation.GetExtraSMTOptions()) {
+          checker.TheoremProver.SetOtherSMTOption(entry.Key, entry.Value);
+        }
+        await checker.BeginCheck(Description, vc, reporter, cancellationToken);
       }
 
       public string Description

Source/VCGeneration/SplitAndVerifyWorker.cs

@@ -194,7 +194,7 @@ private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Ch
         await checker.GoBackToIdle();
       }
 
-      checker.TheoremProver.ClearOtherSMTOptions();
+      checker.TheoremProver.ClearLocalSMTOptions();
     }
 
     private static bool IsProverFailed(ProverInterface.Outcome outcome)