diff options
Diffstat (limited to 'Source/VCGeneration/RPFP.cs')
| -rw-r--r-- | Source/VCGeneration/RPFP.cs | 13 |
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>();
|