summaryrefslogtreecommitdiff
path: root/Source/Core/AbsyCmd.cs
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-07-10 12:40:36 +0200
committerGravatar wuestholz <unknown>2014-07-10 12:40:36 +0200
commit5e52d81030d85b76cc6a0209617af8c21159755d (patch)
tree8ff5d6c98131542b2ca3fa21d9123744c62f4eb1 /Source/Core/AbsyCmd.cs
parente721ac469b8aa3f964ad24917757168288826da1 (diff)
Worked on the more advanced verification result caching (ignore comments for computing statement checksums).
Diffstat (limited to 'Source/Core/AbsyCmd.cs')
-rw-r--r--Source/Core/AbsyCmd.cs3
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index e2781b6f..fae4464a 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1225,7 +1225,8 @@ namespace Microsoft.Boogie {
Comment = c;
}
public override void Emit(TokenTextWriter stream, int level) {
-
+ if (stream.UseForComputingChecksums) { return; }
+
if (this.Comment.Contains("\n")) {
stream.WriteLine(this, level, "/* {0} */", this.Comment);
} else {