Adding background model to fixedpoint counterexamples and small code contracts fixes

1 files changed, 12 insertions, 1 deletions

diff --git a/Source/VCGeneration/RPFP.cs b/Source/VCGeneration/RPFP.cs
index 9048f0f5..f6a42a43 100644
--- a/Source/VCGeneration/RPFP.cs
+++ b/Source/VCGeneration/RPFP.cs
@@ -566,10 +566,21 @@ namespace Microsoft.Boogie
             public List<Node> nodes = new List<Node>();

         };

 

+        /** Set the model of the background theory used in a counterexample. */

+        public void SetBackgroundModel(Model m)

+        {

+            dualModel = m;

+        }

+

+        /** Set the model of the background theory used in a counterexample. */

+        public Model GetBackgroundModel()

+        {

+            return dualModel;

+        }

 

         private int nodeCount = 0;

         private int edgeCount = 0;

-        // private Model dualModel;

+        private Model dualModel;

         // private LabeledLiterals dualLabels;

         private Stack<stack_entry> stack;

         public List<Node> nodes = new List<Node>();