Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3

1 files changed, 14 insertions, 0 deletions

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 5d7e5c97..579cc0c2 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -325,12 +325,14 @@ namespace Microsoft.Boogie {
   // -----------------------------------------------------------------------------------------------

   // -----------------------------------------------------------------------------------------------

 

+  // This class will go away soon. Use Model class instead.

   public class ErrorModel {

     public Dictionary<string/*!*/, int>/*!*/ identifierToPartition;

     public List<List<string/*!>>!*/>> partitionToIdentifiers;

     public List<Object>/*!*/ partitionToValue;

     public Dictionary<object, int>/*!*/ valueToPartition;

     public Dictionary<string/*!*/, List<List<int>>/*!*/>/*!*/ definedFunctions;

+    public Model comesFrom;

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -357,8 +359,20 @@ namespace Microsoft.Boogie {
       this.definedFunctions = definedFunctions;

     }

 

+    public ErrorModel(Model m)

+    {

+      this.comesFrom = m;

+      this.identifierToPartition = new Dictionary<string, int>();

+      this.partitionToIdentifiers = new List<List<string>>();

+      this.valueToPartition = new Dictionary<object, int>();

+      this.definedFunctions = new Dictionary<string, List<List<int>>>();

+    }

+

     public Model ToModel()

     {

+      if (comesFrom != null)

+        return comesFrom;

+

       Model m = new Model();

       // create an Element for every partition

       Model.Element[] elts = new Model.Element[partitionToValue.Count];