diff options
| author |  wuestholz <unknown> | 2014-10-15 10:51:30 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-10-15 10:51:30 +0200 |
| commit | c5cb5a9b5b7f8290267aae63fdd7235f2e90edb8 (patch) | |
| tree | 5d31cc59aaee623c69ad3a75f88f434f6c9c77e6 /Source/VCGeneration | |
| parent | 3c2c0f9b5705e57ee888ea03981f42409f8ea3fe (diff) | |
Fix issue in verification result caching.
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 52db07d9..1d5c3e56 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1652,7 +1652,7 @@ namespace VC { var identExpr = assign.Lhss[0].AsExpr as IdentifierExpr;
if (identExpr != null && identExpr.Decl != null && QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption"))
{
- passiveCmds.Add(new AssumeCmd(c.tok, new IdentifierExpr(Token.NoToken, currentImplementation.InjectedAssumptionVariables.First())));
+ passiveCmds.Add(new AssumeCmd(c.tok, new IdentifierExpr(Token.NoToken, identExpr.Decl)));
}
}
}
|