summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/ConditionGeneration.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs13
1 files changed, 12 insertions, 1 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 1f010757..ae0a1147 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -85,6 +85,7 @@ namespace Microsoft.Boogie {
public string RequestId;
public abstract byte[] Checksum { get; }
public byte[] SugaredCmdChecksum;
+ public bool IsAuxiliaryCexForDiagnosingTimeouts;
public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;
@@ -313,7 +314,7 @@ namespace Microsoft.Boogie {
public abstract int GetLocation();
}
- public class CounterexampleComparer : IComparer<Counterexample> {
+ public class CounterexampleComparer : IComparer<Counterexample>, IEqualityComparer<Counterexample> {
private int Compare(List<Block> bs1, List<Block> bs2)
{
@@ -375,6 +376,16 @@ namespace Microsoft.Boogie {
}
return -1;
}
+
+ public bool Equals(Counterexample x, Counterexample y)
+ {
+ return Compare(x, y) == 0;
+ }
+
+ public int GetHashCode(Counterexample obj)
+ {
+ return 0;
+ }
}
public class AssertCounterexample : Counterexample {