z3api: Bug fix with timeout. Use CheckAssumptions.

4 files changed, 16 insertions, 23 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 42bd1406..11406dbc 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1512,6 +1512,10 @@ namespace Microsoft.Boogie {
         TypeEncodingMethod = TypeEncoding.Monomorphic;

         UseArrayTheory = true;

         UseAbstractInterpretation = false;

+        if (ProverName == "Z3API")

+        {

+            ProverCCLimit = 1;

+        }

       }

     }

 

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index fd9944ee..2f2f03ce 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -48,9 +48,9 @@ namespace Microsoft.Boogie.Z3
         {

             base.Close();

             Z3SafeContext cm = context.cm;

+            cm.CloseLog();

             cm.z3.Dispose();

             cm.config.Config.Dispose();

-            cm.CloseLog();

         }

 

         public void PushAxiom(VCExpr axiom)

@@ -196,7 +196,7 @@ namespace Microsoft.Boogie.Z3
         public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen)

             : base(gen, new VCGenerationOptions(new List<string>()))

         {

-            Z3Config config = BuildConfig(opts.Timeout, true);

+            Z3Config config = BuildConfig(opts.Timeout * 1000, true);

             this.cm = new Z3SafeContext(this, config, gen);

         }

         private static Z3Config BuildConfig(int timeout, bool nativeBv)

diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index ba75c772..f3a42670 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -98,8 +98,8 @@ namespace Microsoft.Boogie.Z3
         public Z3SafeContext(Z3apiProverContext ctxt, Z3Config config, VCExpressionGenerator gen)

         {

             Context z3 = new Context(config.Config);

-            //if (config.LogFilename != null)

-            //    z3.OpenLog(config.LogFilename);

+            if (config.LogFilename != null)

+                z3.OpenLog(config.LogFilename);

             foreach (string tag in config.DebugTraces)

                 z3.EnableDebugTrace(tag);

             this.ctxt = ctxt;

@@ -109,25 +109,13 @@ namespace Microsoft.Boogie.Z3
             this.gen = gen;

             this.namer = new UniqueNamer();

             this.z3.SetPrintMode(PrintMode.Smtlib2Compliant);

-            this.z3.TraceToFile("trace.c");

             this.z3log = null;

-            

-            try

-            {

-                if (config.LogFilename != null)

-                {

-                    this.z3log = new StreamWriter(config.LogFilename);

-                    this.z3log.NewLine = "\n";

-                }

-            }

-            catch (Exception _)

-            {

-                this.z3log = null;

-            }

         }

 

         public void log(string format, params object[] args)

         {

+            // Currently, this is a no-op because z3log is always null

+            // We use the default (automatic) tracing facility of z3

             if (z3log != null)

             {

                 var str = string.Format(format, args);

@@ -140,6 +128,7 @@ namespace Microsoft.Boogie.Z3
 

         public void CloseLog()

         {

+            z3.CloseLog();

             if (z3log != null)

             {

                 z3log.Close();

@@ -375,7 +364,7 @@ namespace Microsoft.Boogie.Z3
                 if (boogieErrors.Count < this.config.Counterexamples)

                 {

                     z3.BlockLiterals(labels);

-                    log("block-literals {0}", labels.ToString());

+                    log("block-literals {0}", labels);

                 }

 

                 labels.Dispose();

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index d0e3bf2e..303a78ce 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -736,7 +736,7 @@ namespace VC
             {

                 checker.TheoremProver.LogComment(str);

             }

-            /*

+            

             public override Outcome CheckAssumptions(List<VCExpr> assumptions)

             {

                 if (assumptions.Count == 0)

@@ -744,11 +744,11 @@ namespace VC
                     return CheckVC();

                 }

 

-                TheoremProver.Push();

+                //TheoremProver.Push();

                 TheoremProver.AssertAxioms();

                 TheoremProver.CheckAssumptions(assumptions);

                 ProverInterface.Outcome outcome = TheoremProver.CheckOutcome(reporter);

-                TheoremProver.Pop();

+                //TheoremProver.Pop();

                 numQueries++;

 

                 switch (outcome)

@@ -768,7 +768,7 @@ namespace VC
                         throw new cce.UnreachableException();

                 }

             }

-             */

+             

         }

 

         // Store important information related to a single VerifyImplementation query