eliminated class ErrorModel

3 files changed, 15 insertions, 15 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 48791385..c65406b4 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -428,8 +428,8 @@ namespace Microsoft.Boogie.SMTLib
               labels = CalculatePath(0);

               xlabels = labels;

             }

-            ErrorModel errorModel = GetErrorModel();

-            handler.OnModel(xlabels, errorModel);

+            Model model = GetErrorModel();

+            handler.OnModel(xlabels, model);

           }

 

           if (labels == null || errorsLeft == 0) break;

@@ -489,7 +489,7 @@ namespace Microsoft.Boogie.SMTLib
       return path.ToArray();

     }

 

-    private ErrorModel GetErrorModel() {

+    private Model GetErrorModel() {

       if (!options.ExpectingModel())

         return null;

       SendThisVC("(get-model)");

@@ -528,7 +528,7 @@ namespace Microsoft.Boogie.SMTLib
         else

           theModel = models[0];

       }

-      return new ErrorModel(theModel);

+      return theModel;

     }

 

     private string[] GetLabelsInfo()

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index f0aa3906..e0fddc63 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -261,7 +261,7 @@ namespace Microsoft.Boogie.Z3 {
         sw.WriteLine("*** END_MODEL");

         var sr = new StringReader(sw.ToString());

         var models = Microsoft.Boogie.Model.ParseModels(sr);

-        Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List<string>(labelStrings));

+        Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings));

         boogieErrors.Add(e);

 

         if (boogieErrors.Count < this.counterexamples) {

@@ -332,7 +332,7 @@ namespace Microsoft.Boogie.Z3 {
         sw.WriteLine("*** END_MODEL");

         var sr = new StringReader(sw.ToString());

         var models = Microsoft.Boogie.Model.ParseModels(sr);

-        Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List<string>(labelStrings));

+        Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings));

         boogieErrors.Add(e);

 

         labels.Dispose();

@@ -442,16 +442,16 @@ namespace Microsoft.Boogie.Z3 {
   }

 

   public class Z3ErrorModelAndLabels {

-    private ErrorModel _errorModel;

+    private Model _model;

     private List<string> _relevantLabels;

-    public ErrorModel ErrorModel {

-      get { return this._errorModel; }

+    public Model Model {

+      get { return this._model; }

     }

     public List<string> RelevantLabels {

       get { return this._relevantLabels; }

     }

-    public Z3ErrorModelAndLabels(ErrorModel errorModel, List<string> relevantLabels) {

-      this._errorModel = errorModel;

+    public Z3ErrorModelAndLabels(Model model, List<string> relevantLabels) {

+      this._model = model;

       this._relevantLabels = relevantLabels;

     }

   }

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 3b7b8f43..d72705f3 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -230,10 +230,10 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
             outcome = context.Check(out z3LabelModels);

         }

 

-        public override void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)

+        public override ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler)

         {

             LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

-            outcome = context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);

+            return context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);

         }

 

         public override void Push()

@@ -285,7 +285,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
                 foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels)

                 {

                     List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);

-                    handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);

+                    handler.OnModel(unprefixedLabels, z3LabelModel.Model);

                 }

             }

             return outcome;

@@ -295,7 +295,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
           if (outcome == Outcome.Invalid) {

             foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) {

               List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);

-              handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);

+              handler.OnModel(unprefixedLabels, z3LabelModel.Model);

             }

           }

           return outcome;