diff options
| author |  wuestholz <unknown> | 2014-07-03 03:27:25 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-07-03 03:27:25 +0200 |
| commit | c7508e18b12db7a1acee981560163e2c319dfc5b (patch) | |
| tree | 711002eade12b7c52253b76b33c47547546ec31f /Source/Core/AbsyCmd.cs | |
| parent | d274c9f110459096a71b8aabbcf7cf27582bf70e (diff) | |
Made it not include free preconditions when producing partially verified preconditions.
Diffstat (limited to 'Source/Core/AbsyCmd.cs')
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index c7ad0f11..8c6685e4 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2428,7 +2428,7 @@ namespace Microsoft.Boogie { {
Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && program != null);
- var requires = procedure.Requires.Select(r => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, r.Condition, program));
+ var requires = procedure.Requires.Where(r => !r.Free).Select(r => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, r.Condition, program));
return Conjunction(requires);
}
|