changed the procedure Check so that the conflict clause is blocked only when more than one counterexample is needed.

3 files changed, 34 insertions, 37 deletions

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index 9109e755..c444e8a1 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -90,7 +90,6 @@ namespace Microsoft.Boogie.Z3
         string GetDeclName(Z3ConstDeclAst constDeclAst);

         Z3PatternAst MakePattern(List<Z3TermAst> exprs);

         Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body);

-        List<string> BuildConflictClause(Z3LabeledLiterals relevantLabels);

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

         void TypeCheckBool(Z3TermAst t);

         void TypeCheckInt(Z3TermAst t);

diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index addfa613..0e3d35ea 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -321,26 +321,6 @@ namespace Microsoft.Boogie.Z3
             return true;

         }

 

-        public List<string> BuildConflictClause(Z3LabeledLiterals z3relevantLabels)

-        {

-            List<string> lbls = new List<string>();

-            LabeledLiterals relevantLabels = ((Z3SafeLabeledLiterals)z3relevantLabels).LabeledLiterals;

-            uint num_labels = relevantLabels.GetNumLabels();

-            for (uint i = 0; i < num_labels; ++i)

-            {

-                Symbol sym = relevantLabels.GetLabel(i);

-                string labelName = z3.GetSymbolString(sym);

-                if (!labelName.StartsWith("@"))

-                {

-                    relevantLabels.Disable(i);

-                }

-                lbls.Add(labelName);

-            }

-            z3.BlockLiterals(relevantLabels);

-

-            return lbls;

-        }

-

         private Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List<string> relevantLabels)

         {

             BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this);

@@ -362,32 +342,53 @@ namespace Microsoft.Boogie.Z3
             Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");

             boogieErrors = new List<Z3ErrorModelAndLabels>();

             LBool outcome = LBool.Undef;

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

+            Debug.Assert(0 < this.config.Counterexamples);

+            while (true)

             {

                 Model z3Model;

-                //System.Console.WriteLine("Check Begin");

                 outcome = z3.CheckAndGetModel(out z3Model);

                 log("check-and-get-model");

-                //System.Console.WriteLine("Check End");

-                if (outcome != LBool.False)

-                {

-                    Debug.Assert(z3Model != null);

+                if (outcome == LBool.False)

+                    break;

+

+                Debug.Assert(z3Model != null);

+                LabeledLiterals labels = z3.GetRelevantLabels();

+                Debug.Assert(labels != null);

 

-                    LabeledLiterals labels = z3.GetRelevantLabels();

-                    List<string> labelStrings = BuildConflictClause(new Z3SafeLabeledLiterals(labels));

-                    boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));

-                    labels.Dispose();

+                List<string> labelStrings = new List<string>();

+                uint numLabels = labels.GetNumLabels();

+                for (uint i = 0; i < numLabels; ++i)

+                {

+                    Symbol sym = labels.GetLabel(i);

+                    string labelName = z3.GetSymbolString(sym);

+                    if (!labelName.StartsWith("@"))

+                    {

+                        labels.Disable(i);

+                    }

+                    labelStrings.Add(labelName);

+                }

+                boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));

 

-                    if (z3Model != null)

-                        z3Model.Dispose();

+                if (boogieErrors.Count < this.config.Counterexamples)

+                {

+                    z3.BlockLiterals(labels);

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

                 }

-                else

+

+                labels.Dispose();

+                z3Model.Dispose();

+                if (boogieErrors.Count == this.config.Counterexamples)

                     break;

             }

+

             if (boogieErrors.Count > 0)

+            {

                 return ProverInterface.Outcome.Invalid;

+            }

             else if (outcome == LBool.False)

+            {

                 return ProverInterface.Outcome.Valid;

+            }

             else

             {

                 Debug.Assert(outcome == LBool.Undef);

diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
index 17435e14..28c71751 100644
--- a/Source/Provers/Z3api/StubContext.cs
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -31,9 +31,6 @@ namespace Microsoft.Boogie.Z3 {
     public Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {

         return new Z3StubTermAst();

     }

-    public List<string> BuildConflictClause(Z3LabeledLiterals relevantLabels) {

-      return new List<string>();

-    }

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

       boogieErrors = new List<Z3ErrorModelAndLabels>();

       return ProverInterface.Outcome.Undetermined;