diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-06-29 16:50:57 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-06-29 16:50:57 -0700 |
| commit | efe732baac2d81573bdd220e41bffaedf1f9eab4 (patch) | |
| tree | 0edfc0fd97211a11006f2ddb7d23ec1ff80d200d /Source/VCExpr/TypeErasure.cs | |
| parent | 507b50ed1ccc51bbd24f3cea6f3c287b97b3d299 (diff) | |
Boogie: use (WEIGHT 0) with the select-of-store axioms
Diffstat (limited to 'Source/VCExpr/TypeErasure.cs')
| -rw-r--r-- | Source/VCExpr/TypeErasure.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 93adec82..fb91d326 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -287,7 +287,7 @@ namespace Microsoft.Boogie.TypeErasure { return eq;
return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(),
- "ctor:" + typeRepr.Name, eq);
+ "ctor:" + typeRepr.Name, -1, eq);
}
// generate an axiom (forall x0, x1, ... :: invFun(fun(x0, x1, ...) == xi)
@@ -305,7 +305,7 @@ namespace Microsoft.Boogie.TypeErasure { List<VCTrigger/*!*/>/*!*/ triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp)));
Contract.Assert(cce.NonNullElements(triggers));
- return Gen.Forall(quantifiedVars, triggers, "typeInv:" + invFun.Name, eq);
+ return Gen.Forall(quantifiedVars, triggers, "typeInv:" + invFun.Name, -1, eq);
}
///////////////////////////////////////////////////////////////////////////
|