Worked on the verification result caching (statement checksums).

2 files changed, 2 insertions, 5 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index d14250c1..b5581ea6 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -3216,10 +3216,7 @@ namespace Microsoft.Boogie {
       if (stream.UseForComputingChecksums && QKeyValue.FindBoolAttribute(Attributes, "precondition_previous_snapshot")) { return; }

 

       stream.Write(this, level, "assume ");

-      if (!stream.UseForComputingChecksums)

-      {

-        EmitAttributes(stream, Attributes);

-      }

+      EmitAttributes(stream, Attributes);

       this.Expr.Emit(stream);

       stream.WriteLine(";");

     }

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index e2113ab5..4a7db752 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -754,7 +754,7 @@ namespace Microsoft.Boogie {
     }

     public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

       //Contract.Requires(stream != null);

-      if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

+      if (CommandLineOptions.Clo.PrintWithUniqueASTIds && !stream.UseForComputingChecksums) {

         stream.Write("{0}^^", this.Decl == null ? "NoDecl" : "h" + this.Decl.GetHashCode());

       }

       stream.Write(this, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name));