diff options
| author |  Unknown <akashl@akash-desk.fareast.corp.microsoft.com> | 2013-01-03 16:53:59 +0530 |
|---|---|---|
| committer | Unknown <akashl@akash-desk.fareast.corp.microsoft.com> | 2013-01-03 16:53:59 +0530 |
| commit | 562c3d3af84d7c364fb6aa81cca83ff17bad64d2 (patch) | |
| tree | 4f81ee47d50bbc175262c428985fc85d1cbf73c6 /Source/VCGeneration/ConditionGeneration.cs | |
| parent | bb3fd5a585f9f1be3100752f298ad633ff2624c4 (diff) | |
Use the new ProverInterface's Evaluate method in stratified inlinig
(guarded by the flag /useProverEvaluate)
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 795fc9ca..8e28362b 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -20,14 +20,15 @@ namespace Microsoft.Boogie { public class CalleeCounterexampleInfo {
public Counterexample counterexample;
- public List<Model.Element>/*!>!*/ args;
+ public List<object>/*!>!*/ args;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(args));
}
- public CalleeCounterexampleInfo(Counterexample cex, List<Model.Element/*!>!*/> x) {
+ public CalleeCounterexampleInfo(Counterexample cex, List<object/*!>!*/> x)
+ {
Contract.Requires(cce.NonNullElements(x));
counterexample = cex;
args = x;
|