From e737198c1dd35f3fa460d346bda346f2e37799a4 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Sat, 27 Nov 2010 08:31:52 +0000
Subject: changed the procedure Check so that the conflict clause is blocked
 only when more than one counterexample is needed.

---
 Source/Provers/Z3api/SafeContext.cs | 67 +++++++++++++++++++------------------
 1 file changed, 34 insertions(+), 33 deletions(-)

(limited to 'Source/Provers/Z3api/SafeContext.cs')

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);
-- 
cgit v1.2.3