Make /randomizeVcIterations:1 the same as normalizeNames:1

Source/Core/CoreOptions.cs

@@ -78,7 +78,7 @@ public enum VerbosityLevel
     bool RunDiagnosticsOnTimeout { get; }
     string ProverLogFilePath { get; set; }
     bool ProverLogFileAppend { get; }
-    int? RandomSeed { get; }
+    int RandomSeed { get; set; }
     int VcsMaxSplits { get; }
     int VcsMaxKeepGoingSplits { get; }
     double VcsMaxCost { get; }

Source/ExecutionEngine/CommandLineOptions.cs

@@ -197,9 +197,9 @@ public bool InstrumentWithAsserts
 
     public CoreOptions.InstrumentationPlaces InstrumentInfer { get; set; } = CoreOptions.InstrumentationPlaces.LoopHeaders;
 
-    public int? RandomSeed { get; set; }
+    public int RandomSeed { get; set; } = 0;
 
-    public int RandomizeVcIterations { get; set; } = 1;
+    public int RandomizeVcIterations { get; set; } = 0;
 
     public bool PrintWithUniqueASTIds {
       get => printWithUniqueAstIds;
@@ -1234,7 +1234,6 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
         case "randomSeedIterations": // old name of the option that should be removed soon
         case "randomizeVcIterations":
           ps.GetIntArgument(x => RandomizeVcIterations = x, a => 1 <= a);
-          RandomSeed ??= 0; // Set to 0 if not already set
           return true;
 
         case "vcsLoad":

Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs

@@ -74,12 +74,9 @@ public SMTLibProcessTheoremProver(SMTLibOptions libOptions, SMTLibSolverOptions
     }
     protected static ScopedNamer GetNamer(SMTLibOptions libOptions, ProverOptions options, ScopedNamer namer = null)
     {
-      return (options.RandomSeed, libOptions.NormalizeNames) switch
-      {
-        (0, true) => NormalizeNamer.Create(namer),
-        (0, false) => KeepOriginalNamer.Create(namer),
-        _ => RandomiseNamer.Create(new Random(options.RandomSeed), namer)
-      };
+      return libOptions.NormalizeNames || libOptions.RandomizeVcIterations > 0
+        ? RandomiseNamer.Create(new Random(options.RandomSeed), namer)
+        : KeepOriginalNamer.Create(namer);
     }
 
     protected ScopedNamer ResetNamer(ScopedNamer namer) {
@@ -438,10 +435,8 @@ protected void SendVCOptions()
       {
         SendThisVC("(set-option :" + Z3.TimeoutOption + " " + options.TimeLimit + ")");
         SendThisVC("(set-option :" + Z3.RlimitOption + " " + options.ResourceLimit + ")");
-        if (options.RandomSeed != 0) {
-          SendThisVC("(set-option :" + Z3.SmtRandomSeed + " " + options.RandomSeed + ")");
-          SendThisVC("(set-option :" + Z3.SatRandomSeed + " " + options.RandomSeed + ")");
-        }
+        SendThisVC("(set-option :" + Z3.SmtRandomSeed + " " + options.RandomSeed + ")");
+        SendThisVC("(set-option :" + Z3.SatRandomSeed + " " + options.RandomSeed + ")");
       }
 
       foreach (var opt in SmtOptions())

Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs

@@ -72,8 +72,8 @@ public async Task SomeVariablesAreRenamed()
   {
     var options = CommandLineOptions.FromArguments(TextWriter.Null);
     options.RandomSeed = randomSeed;
-    options.NormalizeNames = false;
+    options.NormalizeNames = true;
     var randomOptionsLogs = await GetProverLogs.GetProverLogForProgram(options, program);
-    Assert.IsTrue(randomOptionsLogs.Contains("random2084218992"));
+    Assert.IsTrue(randomOptionsLogs.Contains("random506996257"));
   }
-}
+}

Source/VCGeneration/Checker.cs

@@ -119,7 +119,7 @@ public Checker(CheckerPool pool, string /*?*/ logFilePath, bool appendLogFile)
 
       var ctx = Pool.Options.TheProverFactory.NewProverContext(SolverOptions);
 
-      SolverOptions.RandomSeed = Options.RandomSeed ?? 0;
+      SolverOptions.RandomSeed = Options.RandomSeed;
       var prover = Pool.Options.TheProverFactory.SpawnProver(Pool.Options, SolverOptions, ctx);
 
       thmProver = prover;
@@ -157,7 +157,7 @@ private void SetRlimit(uint rlimit)
     /// </summary>
     private void Setup(Program program, ProverContext ctx, Split split)
     {
-      SolverOptions.RandomSeed = 1 < Options.RandomizeVcIterations ? split.NextRandom() : split.RandomSeed;
+      SolverOptions.RandomSeed = split.NextRandom();
 
       Program = program;
       // TODO(wuestholz): Is this lock necessary?

Source/VCGeneration/Split.cs

@@ -84,7 +84,7 @@ public Split(VCGenOptions options, List<Block /*!*/> /*!*/ blocks,
         PrintTopLevelDeclarationsForPruning(par.program, Implementation, "before");
         TopLevelDeclarations = Prune.GetLiveDeclarations(options, par.program, blocks).ToList();
         PrintTopLevelDeclarationsForPruning(par.program, Implementation, "after");
-        RandomSeed = randomSeed ?? Implementation.RandomSeed ?? Options.RandomSeed ?? 0;
+        RandomSeed = randomSeed ?? Implementation.RandomSeed ?? Options.RandomSeed;
         randomGen = new Random(RandomSeed);
       }
 
@@ -1051,7 +1051,11 @@ private void SoundnessCheck(HashSet<List<Block> /*!*/> /*!*/ cache, Block /*!*/
 
       public int NextRandom()
       {
-        return randomGen.Next();
+        var r = RandomSeed;
+        if (Options.RandomizeVcIterations > 0) {
+          RandomSeed = randomGen.Next();
+        }
+        return r;
       }
     }
-}
+}

Source/VCGeneration/SplitAndVerifyWorker.cs

@@ -109,7 +109,7 @@ async Task DoWorkForMultipleIterations(Split split, CancellationToken cancellati
     {
       int currentSplitNumber = DoSplitting ? Interlocked.Increment(ref splitNumber) - 1 : -1;
       split.SplitIndex = currentSplitNumber;
-      var tasks = Enumerable.Range(0, options.RandomizeVcIterations).Select(iteration =>
+      var tasks = Enumerable.Range(0, Math.Max(options.RandomizeVcIterations, 1)).Select(iteration =>
         DoWork(iteration, split, cancellationToken));
       await Task.WhenAll(tasks);
     }
@@ -138,7 +138,7 @@ private async Task StartCheck(int iteration, Split split, Checker checker, Cance
       if (options.Trace && DoSplitting)
       {
         var splitNum = split.SplitIndex + 1;
-        var splitIdxStr = options.RandomizeVcIterations > 1 ? $"{splitNum} (iteration {iteration})" : $"{splitNum}";
+        var splitIdxStr = options.RandomizeVcIterations > 0 ? $"{splitNum} (iteration {iteration})" : $"{splitNum}";
         run.OutputWriter.WriteLine("    checking split {1}/{2}, {3:0.00}%, {0} ...",
           split.Stats, splitIdxStr, total, 100 * provenCost / (provenCost + remainingCost));
       }