Fix issue in computation of checksums for indented statements.

2 files changed, 6 insertions, 3 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 098a47fa..a419fead 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -4074,7 +4074,7 @@ namespace Microsoft.Boogie {
     public override void Emit(TokenTextWriter stream, int level) {

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

       stream.WriteLine();

-      stream.WriteLine("{0};", Indent(level));

+      stream.WriteLine("{0};", Indent(stream.UseForComputingChecksums ? 0 : level));

       first.Emit(stream, level + 1);

       second.Emit(stream, level + 1);

     }

@@ -4099,7 +4099,7 @@ namespace Microsoft.Boogie {
     public override void Emit(TokenTextWriter stream, int level) {

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

       stream.WriteLine();

-      stream.WriteLine("{0}[]", Indent(level));

+      stream.WriteLine("{0}[]", Indent(stream.UseForComputingChecksums ? 0 : level));

       foreach (RE/*!*/ r in rs) {

         Contract.Assert(r != null);

         r.Emit(stream, level + 1);

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index 0a2e5a22..06e4fcf0 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -313,7 +313,10 @@ namespace Microsoft.Boogie {
     }

 

     public void WriteIndent(int level) {

-      this.Write(Indent(level));

+      if (!UseForComputingChecksums)

+      {

+        this.Write(Indent(level));

+      }

     }

 

     public void Write(string text, params object[] args) {