Fix test

boogie-org · Apr 17, 2024 · cd51f29 · cd51f29
1 parent e64b370
commit cd51f29
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs
@@ -74,7 +74,7 @@ public SMTLibProcessTheoremProver(SMTLibOptions libOptions, SMTLibSolverOptions
     }
     protected static ScopedNamer GetNamer(SMTLibOptions libOptions, ProverOptions options, ScopedNamer namer = null)
     {
-      return libOptions.NormalizeNames
+      return libOptions.NormalizeNames || libOptions.RandomizeVcIterations > 0
         ? RandomiseNamer.Create(new Random(options.RandomSeed), namer)
         : KeepOriginalNamer.Create(namer);
     }

diff --git a/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs b/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"));
   }
-}
+}