diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-09-26 17:30:05 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-09-26 17:30:05 -0700 |
| commit | 3925750a1b2145ebd81bea338b33898e61ef10f7 (patch) | |
| tree | 8b3c12cf68036b92246f8c4cfb0b7169ae49258b /Source/VCGeneration | |
| parent | 9dc8e1c990bcb92e7992041f17dd9e0bb88f1b21 (diff) | |
Name the constant used in @MV_state function applications - otherwise we get invalid Z3 files
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 000126de..a52a7087 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1533,7 +1533,7 @@ namespace VC { new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Bool), false));
- public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int));
+ public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "@MV_state_const", Bpl.Type.Int));
public ModelViewInfo(Program program, Implementation impl) {
Contract.Requires(program != null);
|