diff options
| author |  Ally Donaldson <unknown> | 2015-01-10 11:01:14 +0000 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2015-01-10 11:01:14 +0000 |
| commit | 7b1b91e940fd8ec7ac60074c843eb08f5715bc91 (patch) | |
| tree | 724d2b63de4490a0ed2c226cd021adcf85c00776 /Source/Core/Absy.cs | |
| parent | dfc5ba21c5da1c8c4133b4aa260a90dc1a9404f4 (diff) | |
Removed unnecessary stage-related attributes from candidate annotations.
Diffstat (limited to 'Source/Core/Absy.cs')
| -rw-r--r-- | Source/Core/Absy.cs | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 7622cbdf..2fd442d4 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1287,17 +1287,16 @@ namespace Microsoft.Boogie { private int invariantGenerationCounter = 0;
- public Constant MakeExistentialBoolean(int StageId) {
+ public Constant MakeExistentialBoolean() {
Constant ExistentialBooleanConstant = new Constant(Token.NoToken, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false);
invariantGenerationCounter++;
ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True });
- ExistentialBooleanConstant.AddAttribute("stage_id", new object[] { new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(StageId)) });
AddTopLevelDeclaration(ExistentialBooleanConstant);
return ExistentialBooleanConstant;
}
- public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null, int StageId = 0) {
- Constant ExistentialBooleanConstant = MakeExistentialBoolean(StageId);
+ public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null) {
+ Constant ExistentialBooleanConstant = MakeExistentialBoolean();
IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant);
PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e));
if (tag != null)
|