Fixed minor issue.

4 files changed, 7 insertions, 7 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 041993a7..9f7e57cf 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -128,10 +128,10 @@ namespace Microsoft.Boogie {
     public Absy(IToken tok) {

       Contract.Requires(tok != null);

       this._tok = tok;

-      this.uniqueId = System.Threading.Interlocked.Increment(ref AbsyNodeCount);

+      this.uniqueId = System.Threading.Interlocked.Increment(ref CurrentAbsyNodeId);

     }

 

-    private static int AbsyNodeCount = 0;

+    private static int CurrentAbsyNodeId = -1;

 

     // We uniquely number every AST node to make them

     // suitable for our implementation of functional maps.

@@ -162,7 +162,7 @@ namespace Microsoft.Boogie {
     public virtual Absy Clone() {

       Contract.Ensures(Contract.Result<Absy>() != null);

       Absy/*!*/ result = cce.NonNull((Absy/*!*/)this.MemberwiseClone());

-      result.uniqueId = System.Threading.Interlocked.Increment(ref AbsyNodeCount); // BUGBUG??

+      result.uniqueId = System.Threading.Interlocked.Increment(ref CurrentAbsyNodeId); // BUGBUG??

 

       if (InternalNumberedMetadata != null) {

         // This should probably use the lock

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index e7783943..86338d30 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -622,7 +622,7 @@ namespace Microsoft.Boogie {
   public abstract class QuantifierExpr : BinderExpr {

     public Trigger Triggers;

 

-    static int SkolemIds = 0;

+    static int SkolemIds = -1;

     public static int GetNextSkolemId() {

       return System.Threading.Interlocked.Increment(ref SkolemIds);

     }

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index f8428942..4afd6f69 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -676,13 +676,13 @@ namespace Microsoft.Boogie {
       // any filename extension specified by the user.  We base our

       // calculations on that there is at most one occurrence of @PROC@.

       if (180 <= fileName.Length - 6 + pn.Length) {

-        pn = pn.Substring(0, Math.Max(180 - (fileName.Length - 6), 0)) + "-n" + System.Threading.Interlocked.Increment(ref sequenceNumber);

+        pn = pn.Substring(0, Math.Max(180 - (fileName.Length - 6), 0)) + "-n" + System.Threading.Interlocked.Increment(ref sequenceId);

       }

 

       return fileName.Replace("@PROC@", pn);

     }

 

-    private static int sequenceNumber = 0;

+    private static int sequenceId = -1;

 

   }

 }

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 45ce6a02..560f55b4 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -521,7 +521,7 @@ namespace VC {
       readonly List<Block> big_blocks = new List<Block>();

       readonly Dictionary<Block/*!*/, BlockStats/*!*/>/*!*/ stats = new Dictionary<Block/*!*/, BlockStats/*!*/>();

       readonly int id;

-      static int current_id;

+      static int current_id = -1;

       Block split_block;

       bool assert_to_assume;

       List<Block/*!*/>/*!*/ assumized_branches = new List<Block/*!*/>();