Some changes to the prover interface to make way for z3-api.

1 files changed, 2 insertions, 0 deletions

diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index 76c0b957..addfa613 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -111,6 +111,7 @@ namespace Microsoft.Boogie.Z3
             this.namer = new UniqueNamer();

             this.z3.SetPrintMode(PrintMode.SmtlibFull);

             this.z3log = null;

+            

             try

             {

                 if (config.LogFilename != null)

@@ -358,6 +359,7 @@ namespace Microsoft.Boogie.Z3
 

         public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors)

         {

+            Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");

             boogieErrors = new List<Z3ErrorModelAndLabels>();

             LBool outcome = LBool.Undef;

             while (boogieErrors.Count < this.config.Counterexamples)