diff options
| author |  wuestholz <unknown> | 2014-11-10 14:01:58 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-11-10 14:01:58 +0100 |
| commit | c7a2a70a879e2506f6470e0abab2e03b1b60408a (patch) | |
| tree | f6409b622256e50318afd43f6040c95bd0d9eb0e /Source/Core | |
| parent | 75542ea0ee9f14ef18eee6e3349747a8f7181b51 (diff) | |
Fixed issue in the verification result caching.
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.cs | 8 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 4 |
2 files changed, 7 insertions, 5 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index ef2676d0..a53165b6 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -3218,14 +3218,18 @@ namespace Microsoft.Boogie { return ErrorChecksumToCachedError.ContainsKey(checksum);
}
- public void SetErrorChecksumToCachedError(IEnumerable<Tuple<byte[], object>> errors)
+ public void SetErrorChecksumToCachedError(IEnumerable<Tuple<byte[], byte[], object>> errors)
{
Contract.Requires(errors != null);
ErrorChecksumToCachedError = new Dictionary<byte[], object>(ChecksumComparer.Default);
foreach (var kv in errors)
{
- ErrorChecksumToCachedError[kv.Item1] = kv.Item2;
+ ErrorChecksumToCachedError[kv.Item1] = kv.Item3;
+ if (kv.Item2 != null)
+ {
+ ErrorChecksumToCachedError[kv.Item2] = null;
+ }
}
}
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 8f7aa185..066808ae 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -994,9 +994,7 @@ namespace Microsoft.Boogie { var assertRequiresCmd = assertCmd as AssertRequiresCmd;
if (assertRequiresCmd != null)
{
- // Add the checksum of the call instead of the assertion itself
- // because a corresponding counterexample will also have the
- // checksum of the failing call.
+ impl.AddAssertionChecksum(assertRequiresCmd.Checksum);
impl.AddAssertionChecksum(assertRequiresCmd.Call.Checksum);
assertRequiresCmd.SugaredCmdChecksum = assertRequiresCmd.Call.Checksum;
}
|