Update version, and remove race condition

Source/Directory.Build.props

@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.0.6</Version>
+    <Version>3.0.7</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

Source/Provers/SMTLib/ProverInterface.cs

@@ -270,16 +270,10 @@ public virtual void SetRlimit(uint limit)
   {
   }
 
-  // Sets a local SMT option (cleared with ClearLocalSMTOptions)
-  public virtual void SetLocalSMTOption(string name, string value)
+  public virtual void SetAdditionalSmtOptions(IEnumerable<OptionValue> entries)
   {
   }
-
-  // Clear options set with SetLocalSMTOption
-  public virtual void ClearLocalSMTOptions()
-  {
-  }
-
+
   public virtual Task<int> GetRCount()
   {
     throw new NotImplementedException();

Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs

@@ -1,5 +1,4 @@
 using System;
-using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.IO;
 using System.Linq;
@@ -8,7 +7,6 @@
 using Microsoft.Boogie.VCExprAST;
 using Microsoft.Boogie.TypeErasure;
 using System.Text;
-using System.Runtime.CompilerServices;
 
 namespace Microsoft.Boogie.SMTLib
 {
@@ -19,6 +17,7 @@ public abstract class SMTLibProcessTheoremProver : ProverInterface
     protected SMTLibProverContext ctx;
     protected VCExpressionGenerator gen;
     protected SMTLibSolverOptions options;
+    protected IEnumerable<OptionValue> additionalSmtOptions = Array.Empty<OptionValue>();
     protected bool usingUnsatCore;
     private string backgroundPredicates;
 
@@ -346,7 +345,7 @@ protected virtual void PrepareCommon()
           SendCommon("(set-option :produce-models true)");
         }
 
-        foreach (var opt in options.SmtOptions)
+        foreach (var opt in SmtOptions())
         {
           SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");
         }
@@ -393,6 +392,11 @@ protected virtual void PrepareCommon()
       }
     }
 
+    private IEnumerable<OptionValue> SmtOptions()
+    {
+      return options.SmtOptions.Concat(additionalSmtOptions);
+    }
+
     private void SetupAxioms()
     {
       var axioms = ctx.Axioms;
@@ -440,8 +444,9 @@ protected void SendVCOptions()
         }
       }
 
-      foreach (var entry in options.SmtOptions) {
-        SendThisVC("(set-option :" + entry.Option + " " + entry.Value + ")");
+      foreach (var opt in SmtOptions())
+      {
+        SendThisVC("(set-option :" + opt.Option + " " + opt.Value + ")");
       }
     }
 
@@ -1172,18 +1177,10 @@ public override void SetRlimit(uint limit)
       options.ResourceLimit = limit;
     }
 
-    public override void SetLocalSMTOption(string name, string value)
+    public override void SetAdditionalSmtOptions(IEnumerable<OptionValue> entries)
     {
-      options.SmtOptions.Add(new OptionValue(name, value));
+      additionalSmtOptions = entries;
     }
-
-    public override void ClearLocalSMTOptions()
-    {
-      // Go back to global options
-      options.SmtOptions.Clear();
-      options.Parse(libOptions.ProverOptions);
-    }
-
     protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown)
     {
       var result = Outcome.Undetermined;

Source/Provers/SMTLib/SMTLibSolverOptions.cs

@@ -38,13 +38,13 @@ public class SMTLibSolverOptions : ProverOptions
     public bool UseWeights = true;
     public bool UseTickleBool => Solver == SolverKind.Z3;
     public SolverKind Solver = SolverKind.Z3;
-    public List<OptionValue> SmtOptions = new List<OptionValue>();
-    public List<string> SolverArguments = new List<string>();
+    public List<OptionValue> SmtOptions = new();
+    public List<string> SolverArguments = new();
     public string Logic = null;
 
     // Z3 specific (at the moment; some of them make sense also for other provers)
     public string Inspector = null;
-
+    
     public SMTLibSolverOptions(SMTLibOptions libOptions) : base(libOptions)
     {
     }

Source/VCGeneration/Split.cs

@@ -1353,9 +1353,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa
           Print();
         }
 
-        foreach (var entry in Implementation.GetExtraSMTOptions()) {
-          checker.TheoremProver.SetLocalSMTOption(entry.Key, entry.Value);
-        }
+        checker.TheoremProver.SetAdditionalSmtOptions(Implementation.GetExtraSMTOptions().Select(kv => new OptionValue(kv.Key, kv.Value)));
         await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, cancellationToken);
       }
 

Source/VCGeneration/SplitAndVerifyWorker.cs

@@ -193,8 +193,6 @@ private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Ch
         batchCompletions.OnNext((split, result));
         await checker.GoBackToIdle();
       }
-
-      checker.TheoremProver.ClearLocalSMTOptions();
     }
 
     private static bool IsProverFailed(ProverInterface.Outcome outcome)