Support @proc@ for the -mv option (boogie-org#530)

keyboardDrummer · web-flow · commit ee3c6d6f76f1 · 2022-03-10T23:20:00.000Z
diff --git a/Source/Core/Helpers.cs b/Source/Core/Helpers.cs
@@ -1,4 +1,6 @@
 using System;
+using System.Collections.Concurrent;
+using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 
 namespace Microsoft.Boogie
@@ -263,18 +265,30 @@ public static void ExtraTraceInformation(CoreOptions options, string point)
       }
     }
 
-    // Substitute @PROC@ in a filename with the given descName
-    public static string SubstituteAtPROC(string descName, string fileName)
+    private static readonly ConcurrentDictionary<string, int> UsedLogNames = new();
+    public static (string fileName, bool reused) GetLogFilename(string descriptiveName, string filename, bool allowReuse)
     {
-      Contract.Requires(fileName != null);
-      Contract.Requires(descName != null);
+      filename = SubstituteAtPROC(descriptiveName, cce.NonNull(filename));
+
+      var reused = false;
+      var index = UsedLogNames.AddOrUpdate(filename, 0, (_, i) => {
+        reused = allowReuse;
+        return allowReuse ? i : i + 1;
+      });
+      var filenameWithIndex = index > 0 ? filename + "." + index : filename;
+
+      return (filenameWithIndex, reused);
+    }
+
+    private static string SubstituteAtPROC(string descriptiveName, string filename)
+    {
+      Contract.Requires(filename != null);
+      Contract.Requires(descriptiveName != null);
       Contract.Ensures(Contract.Result<string>() != null);
-      System.Text.StringBuilder /*!*/
-        sb =
-          new System.Text.StringBuilder(descName.Length);
+      var /*!*/ sb = new System.Text.StringBuilder(descriptiveName.Length);
       // quote the name, characters like ^ cause trouble in CMD
       // while $ could cause trouble in SH
-      foreach (char c in descName)
+      foreach (char c in descriptiveName)
       {
         if (Char.IsLetterOrDigit(c) || c == '.')
         {
@@ -291,13 +305,13 @@ public static string SubstituteAtPROC(string descName, string fileName)
       // do it by truncating the @PROC@ replacement, which leaves unchanged
       // any filename extension specified by the user.  We base our
       // calculations on that there is at most one occurrence of @PROC@.
-      if (180 <= fileName.Length - 6 + pn.Length)
+      if (180 <= filename.Length - 6 + pn.Length)
       {
-        pn = pn.Substring(0, Math.Max(180 - (fileName.Length - 6), 0)) + "-n" +
+        pn = pn.Substring(0, Math.Max(180 - (filename.Length - 6), 0)) + "-n" +
              System.Threading.Interlocked.Increment(ref sequenceId);
       }
 
-      return fileName.Replace("@PROC@", pn);
+      return filename.Replace("@PROC@", pn);
     }
 
     private static int sequenceId = -1;
diff --git a/Source/ExecutionEngine/ConsolePrinter.cs b/Source/ExecutionEngine/ConsolePrinter.cs
@@ -142,7 +142,7 @@ public void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, boo
     }
 
     tw.Write(errorInfo.Out.ToString());
-    tw.Write(errorInfo.Model.ToString());
+    tw.Write(errorInfo.ModelWriter.ToString());
     tw.Flush();
   }
 
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -99,7 +99,7 @@ public class ErrorInformation
     public ErrorKind Kind { get; set; }
     public string ImplementationName { get; set; }
     public TextWriter Out = new StringWriter();
-    public TextWriter Model = new StringWriter();
+    public TextWriter ModelWriter = new StringWriter();
 
     public string FullMsg
     {
@@ -1501,7 +1501,7 @@ public void ProcessErrors(List<Counterexample> errors, VC.VCGen.Outcome outcome,
           }
 
           if (Options.ModelViewFile != null) {
-            error.PrintModel(errorInfo.Model, error);
+            error.PrintModel(errorInfo.ModelWriter, error);
           }
 
           printer.WriteErrorInformation(errorInfo, tw);
diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs
@@ -109,7 +109,7 @@ private Tuple<Variable, Variable> createNewExplainConstants(Variable v)
   }
 
 
-  public class HoudiniSession
+  public class HoudiniSession : ProofRun
   {
     public class HoudiniStatistics
     {
@@ -120,7 +120,7 @@ public class HoudiniStatistics
       public int numUnsatCorePrunings = 0;
     }
 
-    public string descriptiveName;
+    public string Description { get; }
     private readonly Houdini houdini;
     public HoudiniStatistics stats;
     private VCExpr conjecture;
@@ -155,7 +155,7 @@ public bool InUnsatCore(Variable constant)
     public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program,
       Implementation impl, HoudiniStatistics stats, int taskID = -1)
     {
-      this.descriptiveName = impl.Name;
+      this.Description = impl.Name;
       this.houdini = houdini;
       this.stats = stats;
       collector = new ConditionGeneration.VerificationResultCollector(houdini.Options);
@@ -186,12 +186,12 @@ public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterf
       VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(absyIds.GetId(impl.Blocks[0]))));
       conjecture = exprGen.Implies(eqExpr, conjecture);
 
-      Macro macro = new Macro(Token.NoToken, descriptiveName, new List<Variable>(),
+      Macro macro = new Macro(Token.NoToken, Description, new List<Variable>(),
         new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false));
       proverInterface.DefineMacro(macro, conjecture);
       conjecture = exprGen.Function(macro);
       handler = new VCGen.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, vcgen.debugInfos, collector,
-        mvInfo, proverInterface.Context, program);
+        mvInfo, proverInterface.Context, program, this);
     }
 
     private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary<Variable, bool> currentAssignment)
@@ -254,13 +254,13 @@ public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionar
 
       if (Options.Trace)
       {
-        Console.WriteLine("Verifying " + descriptiveName);
+        Console.WriteLine("Verifying " + Description);
       }
 
       DateTime now = DateTime.UtcNow;
 
       VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture);
-      proverInterface.BeginCheck(descriptiveName, vc, handler);
+      proverInterface.BeginCheck(Description, vc, handler);
       ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, errorLimit, CancellationToken.None).Result;
 
       double queryTime = (DateTime.UtcNow - now).TotalSeconds;
@@ -380,7 +380,7 @@ public void Explain(ProverInterface proverInterface,
 
       if (Options.Trace)
       {
-        Console.WriteLine("Verifying (MaxSat) " + descriptiveName);
+        Console.WriteLine("Verifying (MaxSat) " + Description);
       }
 
       DateTime now = DateTime.UtcNow;
@@ -393,8 +393,8 @@ public void Explain(ProverInterface proverInterface,
       do
       {
         hardAssumptions.Add(controlExprNoop);
-        (outcome, var unsatisfiedSoftAssumptions) = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions, 
-          handler, CancellationToken.None).Result;
+        (outcome, var unsatisfiedSoftAssumptions) = proverInterface.CheckAssumptions(hardAssumptions,
+          softAssumptions, handler, CancellationToken.None).Result;
         hardAssumptions.RemoveAt(hardAssumptions.Count - 1);
 
         if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory ||
@@ -428,7 +428,7 @@ public void Explain(ProverInterface proverInterface,
           hardAssumptions.Add(softAssumptions[i]);
         }
 
-        (outcome, var unsatisfiedSoftAssumptions2) = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, 
+        (outcome, var unsatisfiedSoftAssumptions2) = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2,
           handler, CancellationToken.None).Result;
 
         if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory ||
@@ -451,22 +451,22 @@ public void Explain(ProverInterface proverInterface,
         foreach (var r in reason)
         {
           Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name,
-            r, descriptiveName);
+            r, Description);
         }
 
         //also add the removed reasons using dotted edges (requires- x != 0, requires- x == 0 ==> assert x != 0)
         foreach (var r in reason1)
         {
           Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=blue style=dotted ];",
-            refutedConstant.Name, r, descriptiveName);
+            refutedConstant.Name, r, Description);
         }
       } while (false);
 
       if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory ||
           outcome == ProverInterface.Outcome.OutOfResource || outcome == ProverInterface.Outcome.Undetermined)
       {
         Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name,
-          "TimeOut", descriptiveName);
+          "TimeOut", Description);
       }
 
       Options.ErrorLimit = el;
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
@@ -3,6 +3,7 @@
 using System.Diagnostics.Contracts;
 using System.Threading;
 using System.Threading.Tasks;
+using Microsoft.Boogie.SMTLib;
 using Microsoft.Boogie.VCExprAST;
 
 namespace Microsoft.Boogie;
diff --git a/Source/Provers/SMTLib/ProverUtil.cs b/Source/Provers/SMTLib/ProverUtil.cs
@@ -298,7 +298,7 @@ public virtual TextWriter OpenLog(string /*?*/ descName)
         Contract.Assert(filename != null);
         if (descName != null)
         {
-          filename = Helpers.SubstituteAtPROC(descName, filename);
+          filename = Helpers.GetLogFilename(descName, filename, true).fileName;
         }
 
         return new StreamWriter(filename, AppendLogFile);
diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs
@@ -524,22 +524,10 @@ protected TextWriter OpenOutputFile(string descriptiveName)
       Contract.Requires(descriptiveName != null);
       Contract.Ensures(Contract.Result<TextWriter>() != null);
 
-      string filename = options.LogFilename;
-      filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename));
-      var curFilename = filename;
+      string filenameTemplate = options.LogFilename;
+      var (filename, reused) = Helpers.GetLogFilename(descriptiveName, filenameTemplate, false);
 
-      lock (usedLogNames)
-      {
-        int n = 1;
-        while (usedLogNames.Contains(curFilename))
-        {
-          curFilename = filename + "." + n++;
-        }
-
-        usedLogNames.Add(curFilename);
-      }
-
-      return new StreamWriter(curFilename, false);
+      return new StreamWriter(filename, reused);
     }
 
     protected void FlushProverWarnings()
diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs
@@ -5,6 +5,7 @@
 using System.Threading;
 using Microsoft.Boogie.VCExprAST;
 using System.Threading.Tasks;
+using Microsoft.Boogie.SMTLib;
 using VC;
 
 namespace Microsoft.Boogie
@@ -261,7 +262,7 @@ public Task<int> GetProverResourceCount()
       return thmProver.GetRCount();
     }
 
-    private async Task WaitForOutput(object dummy, CancellationToken cancellationToken)
+    private async Task WaitForOutput(CancellationToken cancellationToken)
     {
       try {
         outcome = await thmProver.CheckOutcome(cce.NonNull(handler), Options.ErrorLimit,
@@ -328,7 +329,7 @@ public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorH
       thmProver.BeginCheck(descriptiveName, vc, handler);
       //  gen.ClearSharedFormulas();    PR: don't know yet what to do with this guy
 
-      ProverTask = WaitForOutput(null, cancellationToken);
+      ProverTask = WaitForOutput(cancellationToken);
     }
 
     public ProverInterface.Outcome ReadOutcome()
diff --git a/Source/VCGeneration/Counterexample.cs b/Source/VCGeneration/Counterexample.cs
@@ -74,6 +74,7 @@ void ObjectInvariant()
       Contract.Invariant(cce.NonNullDictionaryAndValues(calleeCounterexamples));
     }
 
+    public ProofRun ProofRun { get; }
     protected readonly VCGenOptions options;
     [Peer] public List<Block> Trace;
     public List<object> AugmentedTrace;
@@ -88,7 +89,8 @@ void ObjectInvariant()
 
     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;
 
-    internal Counterexample(VCGenOptions options, List<Block> trace, List<object> augmentedTrace, Model model, VC.ModelViewInfo mvInfo, ProverContext context)
+    internal Counterexample(VCGenOptions options, List<Block> trace, List<object> augmentedTrace, Model model,
+      VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun)
     {
       Contract.Requires(trace != null);
       Contract.Requires(context != null);
@@ -97,6 +99,7 @@ internal Counterexample(VCGenOptions options, List<Block> trace, List<object> au
       this.Model = model;
       this.MvInfo = mvInfo;
       this.Context = context;
+      this.ProofRun = proofRun;
       this.calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();
       // the call to instance method GetModelValue in the following code requires the fields Model and Context to be initialized
       if (augmentedTrace != null)
@@ -213,14 +216,12 @@ public void Print(int indent, TextWriter tw, Action<Block> blockAction = null)
       }
     }
 
-    public static bool firstModelFile = true;
-
     public void PrintModel(TextWriter tw, Counterexample counterexample)
     {
       Contract.Requires(counterexample != null);
 
-      var filename = options.ModelViewFile;
-      if (Model == null || filename == null || options.StratifiedInlining > 0)
+      var filenameTemplate = options.ModelViewFile;
+      if (Model == null || filenameTemplate == null || options.StratifiedInlining > 0)
       {
         return;
       }
@@ -238,14 +239,14 @@ public void PrintModel(TextWriter tw, Counterexample counterexample)
         Model.ModelHasStatesAlready = true;
       }
 
-      if (filename == "-")
+      if (filenameTemplate == "-")
       {
         Model.Write(tw);
         tw.Flush();
       }
       else {
-        using var wr = new StreamWriter(filename, !firstModelFile);
-        firstModelFile = false;
+        var (filename, reused) = Helpers.GetLogFilename(ProofRun.Description, filenameTemplate, true);
+        using var wr = new StreamWriter(filename, reused);
         Model.Write(wr);
       }
     }
@@ -476,8 +477,8 @@ void ObjectInvariant()
 
 
     public AssertCounterexample(VCGenOptions options, List<Block> trace, List<object> augmentedTrace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo,
-      ProverContext context)
-      : base(options, trace, augmentedTrace, model, mvInfo, context)
+      ProverContext context, ProofRun proofRun)
+      : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun)
     {
       Contract.Requires(trace != null);
       Contract.Requires(failingAssert != null);
@@ -497,7 +498,7 @@ public override byte[] Checksum
 
     public override Counterexample Clone()
     {
-      var ret = new AssertCounterexample(options, Trace, AugmentedTrace, FailingAssert, Model, MvInfo, Context);
+      var ret = new AssertCounterexample(options, Trace, AugmentedTrace, FailingAssert, Model, MvInfo, Context, ProofRun);
       ret.calleeCounterexamples = calleeCounterexamples;
       return ret;
     }
@@ -517,8 +518,8 @@ void ObjectInvariant()
 
 
     public CallCounterexample(VCGenOptions options, List<Block> trace, List<object> augmentedTrace, CallCmd failingCall, Requires failingRequires, Model model,
-      VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum = null)
-      : base(options, trace, augmentedTrace, model, mvInfo, context)
+      VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, byte[] checksum = null)
+      : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun)
     {
       Contract.Requires(!failingRequires.Free);
       Contract.Requires(trace != null);
@@ -545,7 +546,7 @@ public override byte[] Checksum
 
     public override Counterexample Clone()
     {
-      var ret = new CallCounterexample(options, Trace, AugmentedTrace, FailingCall, FailingRequires, Model, MvInfo, Context, Checksum);
+      var ret = new CallCounterexample(options, Trace, AugmentedTrace, FailingCall, FailingRequires, Model, MvInfo, Context, ProofRun, Checksum);
       ret.calleeCounterexamples = calleeCounterexamples;
       return ret;
     }
@@ -565,8 +566,8 @@ void ObjectInvariant()
 
 
     public ReturnCounterexample(VCGenOptions options, List<Block> trace, List<object> augmentedTrace, TransferCmd failingReturn, Ensures failingEnsures, Model model,
-      VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum)
-      : base(options, trace, augmentedTrace, model, mvInfo, context)
+      VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, byte[] checksum)
+      : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun)
     {
       Contract.Requires(trace != null);
       Contract.Requires(context != null);
@@ -595,7 +596,7 @@ public override byte[] Checksum
 
     public override Counterexample Clone()
     {
-      var ret = new ReturnCounterexample(options, Trace, AugmentedTrace, FailingReturn, FailingEnsures, Model, MvInfo, Context, checksum);
+      var ret = new ReturnCounterexample(options, Trace, AugmentedTrace, FailingReturn, FailingEnsures, Model, MvInfo, Context, ProofRun, checksum);
       ret.calleeCounterexamples = calleeCounterexamples;
       return ret;
     }
diff --git a/Source/VCGeneration/ProofRun.cs b/Source/VCGeneration/ProofRun.cs
@@ -0,0 +1,5 @@
+namespace VC;
+
+public interface ProofRun {
+  string Description { get; }
+}
diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs
diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs
diff --git a/Test/test15/MoreCapturedStates.bpl b/Test/test15/MoreCapturedStates.bpl
diff --git a/Test/test15/MoreCapturedStates.bpl.expect b/Test/test15/MoreCapturedStates.bpl.expect

Original file line number	Diff line number	Diff line change
`@@ -142,7 +142,7 @@ public void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, boo`
`142`	`142`	`}`
`143`	`143`
`144`	`144`	`tw.Write(errorInfo.Out.ToString());`
`145`		`- tw.Write(errorInfo.Model.ToString());`
	`145`	`+ tw.Write(errorInfo.ModelWriter.ToString());`
`146`	`146`	`tw.Flush();`
`147`	`147`	`}`
`148`	`148`
Original file line number	Diff line number	Diff line change
`@@ -99,7 +99,7 @@ public class ErrorInformation`
`99`	`99`	`public ErrorKind Kind { get; set; }`
`100`	`100`	`public string ImplementationName { get; set; }`
`101`	`101`	`public TextWriter Out = new StringWriter();`
`102`		`- public TextWriter Model = new StringWriter();`
	`102`	`+ public TextWriter ModelWriter = new StringWriter();`
`103`	`103`
`104`	`104`	`public string FullMsg`
`105`	`105`	`{`
`@@ -1501,7 +1501,7 @@ public void ProcessErrors(List<Counterexample> errors, VC.VCGen.Outcome outcome,`
`1501`	`1501`	`}`
`1502`	`1502`
`1503`	`1503`	`if (Options.ModelViewFile != null) {`
`1504`		`- error.PrintModel(errorInfo.Model, error);`
	`1504`	`+ error.PrintModel(errorInfo.ModelWriter, error);`
`1505`	`1505`	`}`
`1506`	`1506`
`1507`	`1507`	`printer.WriteErrorInformation(errorInfo, tw);`
Original file line number	Diff line number	Diff line change
`@@ -109,7 +109,7 @@ private Tuple<Variable, Variable> createNewExplainConstants(Variable v)`
`109`	`109`	`}`
`110`	`110`
`111`	`111`
`112`		`- public class HoudiniSession`
	`112`	`+ public class HoudiniSession : ProofRun`
`113`	`113`	`{`
`114`	`114`	`public class HoudiniStatistics`
`115`	`115`	`{`
`@@ -120,7 +120,7 @@ public class HoudiniStatistics`
`120`	`120`	`public int numUnsatCorePrunings = 0;`
`121`	`121`	`}`
`122`	`122`
`123`		`- public string descriptiveName;`
	`123`	`+ public string Description { get; }`
`124`	`124`	`private readonly Houdini houdini;`
`125`	`125`	`public HoudiniStatistics stats;`
`126`	`126`	`private VCExpr conjecture;`
`@@ -155,7 +155,7 @@ public bool InUnsatCore(Variable constant)`
`155`	`155`	`public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program,`
`156`	`156`	`Implementation impl, HoudiniStatistics stats, int taskID = -1)`
`157`	`157`	`{`
`158`		`- this.descriptiveName = impl.Name;`
	`158`	`+ this.Description = impl.Name;`
`159`	`159`	`this.houdini = houdini;`
`160`	`160`	`this.stats = stats;`
`161`	`161`	`collector = new ConditionGeneration.VerificationResultCollector(houdini.Options);`
`@@ -186,12 +186,12 @@ public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterf`
`186`	`186`	`VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(absyIds.GetId(impl.Blocks[0]))));`
`187`	`187`	`conjecture = exprGen.Implies(eqExpr, conjecture);`
`188`	`188`
`189`		`- Macro macro = new Macro(Token.NoToken, descriptiveName, new List<Variable>(),`
	`189`	`+ Macro macro = new Macro(Token.NoToken, Description, new List<Variable>(),`
`190`	`190`	`new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false));`
`191`	`191`	`proverInterface.DefineMacro(macro, conjecture);`
`192`	`192`	`conjecture = exprGen.Function(macro);`
`193`	`193`	`handler = new VCGen.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, vcgen.debugInfos, collector,`
`194`		`- mvInfo, proverInterface.Context, program);`
	`194`	`+ mvInfo, proverInterface.Context, program, this);`
`195`	`195`	`}`
`196`	`196`
`197`	`197`	`private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary<Variable, bool> currentAssignment)`
`@@ -254,13 +254,13 @@ public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionar`
`254`	`254`
`255`	`255`	`if (Options.Trace)`
`256`	`256`	`{`
`257`		`- Console.WriteLine("Verifying " + descriptiveName);`
	`257`	`+ Console.WriteLine("Verifying " + Description);`
`258`	`258`	`}`
`259`	`259`
`260`	`260`	`DateTime now = DateTime.UtcNow;`
`261`	`261`
`262`	`262`	`VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture);`
`263`		`- proverInterface.BeginCheck(descriptiveName, vc, handler);`
	`263`	`+ proverInterface.BeginCheck(Description, vc, handler);`
`264`	`264`	`ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, errorLimit, CancellationToken.None).Result;`
`265`	`265`
`266`	`266`	`double queryTime = (DateTime.UtcNow - now).TotalSeconds;`
`@@ -380,7 +380,7 @@ public void Explain(ProverInterface proverInterface,`
`380`	`380`
`381`	`381`	`if (Options.Trace)`
`382`	`382`	`{`
`383`		`- Console.WriteLine("Verifying (MaxSat) " + descriptiveName);`
	`383`	`+ Console.WriteLine("Verifying (MaxSat) " + Description);`
`384`	`384`	`}`
`385`	`385`
`386`	`386`	`DateTime now = DateTime.UtcNow;`
`@@ -393,8 +393,8 @@ public void Explain(ProverInterface proverInterface,`
`393`	`393`	`do`
`394`	`394`	`{`
`395`	`395`	`hardAssumptions.Add(controlExprNoop);`
`396`		`- (outcome, var unsatisfiedSoftAssumptions) = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions,`
`397`		`- handler, CancellationToken.None).Result;`
	`396`	`+ (outcome, var unsatisfiedSoftAssumptions) = proverInterface.CheckAssumptions(hardAssumptions,`
	`397`	`+ softAssumptions, handler, CancellationToken.None).Result;`
`398`	`398`	`hardAssumptions.RemoveAt(hardAssumptions.Count - 1);`
`399`	`399`
`400`	`400`	`if (outcome == ProverInterface.Outcome.TimeOut \|\| outcome == ProverInterface.Outcome.OutOfMemory \|\|`
`@@ -428,7 +428,7 @@ public void Explain(ProverInterface proverInterface,`
`428`	`428`	`hardAssumptions.Add(softAssumptions[i]);`
`429`	`429`	`}`
`430`	`430`
`431`		`- (outcome, var unsatisfiedSoftAssumptions2) = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2,`
	`431`	`+ (outcome, var unsatisfiedSoftAssumptions2) = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2,`
`432`	`432`	`handler, CancellationToken.None).Result;`
`433`	`433`
`434`	`434`	`if (outcome == ProverInterface.Outcome.TimeOut \|\| outcome == ProverInterface.Outcome.OutOfMemory \|\|`
`@@ -451,22 +451,22 @@ public void Explain(ProverInterface proverInterface,`
`451`	`451`	`foreach (var r in reason)`
`452`	`452`	`{`
`453`	`453`	`Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name,`
`454`		`- r, descriptiveName);`
	`454`	`+ r, Description);`
`455`	`455`	`}`
`456`	`456`
`457`	`457`	`//also add the removed reasons using dotted edges (requires- x != 0, requires- x == 0 ==> assert x != 0)`
`458`	`458`	`foreach (var r in reason1)`
`459`	`459`	`{`
`460`	`460`	`Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=blue style=dotted ];",`
`461`		`- refutedConstant.Name, r, descriptiveName);`
	`461`	`+ refutedConstant.Name, r, Description);`
`462`	`462`	`}`
`463`	`463`	`} while (false);`
`464`	`464`
`465`	`465`	`if (outcome == ProverInterface.Outcome.TimeOut \|\| outcome == ProverInterface.Outcome.OutOfMemory \|\|`
`466`	`466`	`outcome == ProverInterface.Outcome.OutOfResource \|\| outcome == ProverInterface.Outcome.Undetermined)`
`467`	`467`	`{`
`468`	`468`	`Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name,`
`469`		`- "TimeOut", descriptiveName);`
	`469`	`+ "TimeOut", Description);`
`470`	`470`	`}`
`471`	`471`
`472`	`472`	`Options.ErrorLimit = el;`
Original file line number	Diff line number	Diff line change
`@@ -298,7 +298,7 @@ public virtual TextWriter OpenLog(string /?/ descName)`
`298`	`298`	`Contract.Assert(filename != null);`
`299`	`299`	`if (descName != null)`
`300`	`300`	`{`
`301`		`- filename = Helpers.SubstituteAtPROC(descName, filename);`
	`301`	`+ filename = Helpers.GetLogFilename(descName, filename, true).fileName;`
`302`	`302`	`}`
`303`	`303`
`304`	`304`	`return new StreamWriter(filename, AppendLogFile);`
Original file line number	Diff line number	Diff line change
`@@ -74,6 +74,7 @@ void ObjectInvariant()`
`74`	`74`	`Contract.Invariant(cce.NonNullDictionaryAndValues(calleeCounterexamples));`
`75`	`75`	`}`
`76`	`76`
	`77`	`+ public ProofRun ProofRun { get; }`
`77`	`78`	`protected readonly VCGenOptions options;`
`78`	`79`	`[Peer] public List<Block> Trace;`
`79`	`80`	`public List<object> AugmentedTrace;`
`@@ -88,7 +89,8 @@ void ObjectInvariant()`
`88`	`89`
`89`	`90`	`public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;`
`90`	`91`
`91`		`- internal Counterexample(VCGenOptions options, List<Block> trace, List<object> augmentedTrace, Model model, VC.ModelViewInfo mvInfo, ProverContext context)`
	`92`	`+ internal Counterexample(VCGenOptions options, List<Block> trace, List<object> augmentedTrace, Model model,`
	`93`	`+ VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun)`
`92`	`94`	`{`
`93`	`95`	`Contract.Requires(trace != null);`
`94`	`96`	`Contract.Requires(context != null);`
`@@ -97,6 +99,7 @@ internal Counterexample(VCGenOptions options, List<Block> trace, List<object> au`
`97`	`99`	`this.Model = model;`
`98`	`100`	`this.MvInfo = mvInfo;`
`99`	`101`	`this.Context = context;`
	`102`	`+ this.ProofRun = proofRun;`
`100`	`103`	`this.calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();`
`101`	`104`	`// the call to instance method GetModelValue in the following code requires the fields Model and Context to be initialized`
`102`	`105`	`if (augmentedTrace != null)`
`@@ -213,14 +216,12 @@ public void Print(int indent, TextWriter tw, Action<Block> blockAction = null)`
`213`	`216`	`}`
`214`	`217`	`}`
`215`	`218`
`216`		`- public static bool firstModelFile = true;`
`217`		`-`
`218`	`219`	`public void PrintModel(TextWriter tw, Counterexample counterexample)`
`219`	`220`	`{`
`220`	`221`	`Contract.Requires(counterexample != null);`
`221`	`222`
`222`		`- var filename = options.ModelViewFile;`
`223`		`- if (Model == null \|\| filename == null \|\| options.StratifiedInlining > 0)`
	`223`	`+ var filenameTemplate = options.ModelViewFile;`
	`224`	`+ if (Model == null \|\| filenameTemplate == null \|\| options.StratifiedInlining > 0)`
`224`	`225`	`{`
`225`	`226`	`return;`
`226`	`227`	`}`
`@@ -238,14 +239,14 @@ public void PrintModel(TextWriter tw, Counterexample counterexample)`
`238`	`239`	`Model.ModelHasStatesAlready = true;`
`239`	`240`	`}`
`240`	`241`
`241`		`- if (filename == "-")`
	`242`	`+ if (filenameTemplate == "-")`
`242`	`243`	`{`
`243`	`244`	`Model.Write(tw);`
`244`	`245`	`tw.Flush();`
`245`	`246`	`}`
`246`	`247`	`else {`
`247`		`- using var wr = new StreamWriter(filename, !firstModelFile);`
`248`		`- firstModelFile = false;`
	`248`	`+ var (filename, reused) = Helpers.GetLogFilename(ProofRun.Description, filenameTemplate, true);`
	`249`	`+ using var wr = new StreamWriter(filename, reused);`
`249`	`250`	`Model.Write(wr);`
`250`	`251`	`}`
`251`	`252`	`}`
`@@ -476,8 +477,8 @@ void ObjectInvariant()`
`476`	`477`
`477`	`478`
`478`	`479`	`public AssertCounterexample(VCGenOptions options, List<Block> trace, List<object> augmentedTrace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo,`
`479`		`- ProverContext context)`
`480`		`- : base(options, trace, augmentedTrace, model, mvInfo, context)`
	`480`	`+ ProverContext context, ProofRun proofRun)`
	`481`	`+ : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun)`
`481`	`482`	`{`
`482`	`483`	`Contract.Requires(trace != null);`
`483`	`484`	`Contract.Requires(failingAssert != null);`
`@@ -497,7 +498,7 @@ public override byte[] Checksum`
`497`	`498`
`498`	`499`	`public override Counterexample Clone()`
`499`	`500`	`{`
`500`		`- var ret = new AssertCounterexample(options, Trace, AugmentedTrace, FailingAssert, Model, MvInfo, Context);`
	`501`	`+ var ret = new AssertCounterexample(options, Trace, AugmentedTrace, FailingAssert, Model, MvInfo, Context, ProofRun);`
`501`	`502`	`ret.calleeCounterexamples = calleeCounterexamples;`
`502`	`503`	`return ret;`
`503`	`504`	`}`
`@@ -517,8 +518,8 @@ void ObjectInvariant()`
`517`	`518`
`518`	`519`
`519`	`520`	`public CallCounterexample(VCGenOptions options, List<Block> trace, List<object> augmentedTrace, CallCmd failingCall, Requires failingRequires, Model model,`
`520`		`- VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum = null)`
`521`		`- : base(options, trace, augmentedTrace, model, mvInfo, context)`
	`521`	`+ VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, byte[] checksum = null)`
	`522`	`+ : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun)`
`522`	`523`	`{`
`523`	`524`	`Contract.Requires(!failingRequires.Free);`
`524`	`525`	`Contract.Requires(trace != null);`
`@@ -545,7 +546,7 @@ public override byte[] Checksum`
`545`	`546`
`546`	`547`	`public override Counterexample Clone()`
`547`	`548`	`{`
`548`		`- var ret = new CallCounterexample(options, Trace, AugmentedTrace, FailingCall, FailingRequires, Model, MvInfo, Context, Checksum);`
	`549`	`+ var ret = new CallCounterexample(options, Trace, AugmentedTrace, FailingCall, FailingRequires, Model, MvInfo, Context, ProofRun, Checksum);`
`549`	`550`	`ret.calleeCounterexamples = calleeCounterexamples;`
`550`	`551`	`return ret;`
`551`	`552`	`}`
`@@ -565,8 +566,8 @@ void ObjectInvariant()`
`565`	`566`
`566`	`567`
`567`	`568`	`public ReturnCounterexample(VCGenOptions options, List<Block> trace, List<object> augmentedTrace, TransferCmd failingReturn, Ensures failingEnsures, Model model,`
`568`		`- VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum)`
`569`		`- : base(options, trace, augmentedTrace, model, mvInfo, context)`
	`569`	`+ VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, byte[] checksum)`
	`570`	`+ : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun)`
`570`	`571`	`{`
`571`	`572`	`Contract.Requires(trace != null);`
`572`	`573`	`Contract.Requires(context != null);`
`@@ -595,7 +596,7 @@ public override byte[] Checksum`
`595`	`596`
`596`	`597`	`public override Counterexample Clone()`
`597`	`598`	`{`
`598`		`- var ret = new ReturnCounterexample(options, Trace, AugmentedTrace, FailingReturn, FailingEnsures, Model, MvInfo, Context, checksum);`
	`599`	`+ var ret = new ReturnCounterexample(options, Trace, AugmentedTrace, FailingReturn, FailingEnsures, Model, MvInfo, Context, ProofRun, checksum);`
`599`	`600`	`ret.calleeCounterexamples = calleeCounterexamples;`
`600`	`601`	`return ret;`
`601`	`602`	`}`