Boogie: Removed trailing spaces in code

6 files changed, 9 insertions, 9 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index b211b8f4..881df2ce 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -180,7 +180,7 @@ void ObjectInvariant()
     internal const string iffName = "iff"; // logical equivalence

     internal const string eqName = "="; // equality

     internal const string lessName = "<";

-    internal const string greaterName = ">"; 

+    internal const string greaterName = ">";
     internal const string atmostName = "<=";

     internal const string atleastName = ">=";

     internal const string TRUEName = "true"; // nullary predicate that is always true

@@ -358,7 +358,7 @@ void ObjectInvariant()
 

       Linearise(node.Body, options);

 

-      WriteTriggers(node.Triggers, options);        

+      WriteTriggers(node.Triggers, options);
       wr.Write(")");

 

       return true;

@@ -591,7 +591,7 @@ void ObjectInvariant()
           }

         }

 

-        return true;        

+        return true;
       }

 

       public bool VisitEqOp       (VCExprNAry node, LineariserOptions options) {

diff --git a/Source/Provers/Simplify/Prover.cs b/Source/Provers/Simplify/Prover.cs
index 6db18cb4..b8810e00 100644
--- a/Source/Provers/Simplify/Prover.cs
+++ b/Source/Provers/Simplify/Prover.cs
@@ -97,7 +97,7 @@ namespace Microsoft.Boogie.Simplify {
     }

 

     public void Close()

-      //modifies this.*; 

+      //modifies this.*;
     {

       cce.BeginExpose(this);

       {

diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs
index 90284358..6425dd00 100644
--- a/Source/Provers/Z3/Inspector.cs
+++ b/Source/Provers/Z3/Inspector.cs
@@ -44,7 +44,7 @@ void ObjectInvariant()
           Labels[lab.label] = lab.pos;

         }

       }

-      return true;      

+      return true;
     }

   }

 

diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 14b551df..208f934b 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -675,7 +675,7 @@ void ObjectInvariant()
           cce.Owner.AssignSame(boxedN, cce.Owner.ElementProxy(partitionToValue));

           partitionToValue.Add(boxedN);

           Contract.Assume( !valueToPartition.ContainsKey(boxedN));  // a RHS value should occur only once in the Z3 output

-          valueToPartition.Add(boxedN, zID); 

+          valueToPartition.Add(boxedN, zID);
         } else if (type.StartsWith("bv") && BigNum.TryParse(number, out bvVal) && int.TryParse(type.Substring(2), out bvSize)) {

           BvConst bitV = new BvConst(bvVal, bvSize);

           cce.Owner.AssignSame(bitV, cce.Owner.ElementProxy(partitionToValue));

@@ -1131,7 +1131,7 @@ void ObjectInvariant()
         writer.WriteLine("identifierToPartition:");

         foreach (KeyValuePair<string, int> kvp in identifierToPartition) {

           Contract.Assert(kvp.Key!=null);

-          writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);  

+          writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
         }

         

         writer.WriteLine("valueToPartition:");

diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 994cb282..689f1024 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -90,7 +90,7 @@ void ObjectInvariant()
     public int Timeout { get { return TimeLimit / 1000; } }

     public bool Typed {

       get { 

-        return CommandLineOptions.Clo.Z3types || BitVectors == CommandLineOptions.BvHandling.Z3Native; 

+        return CommandLineOptions.Clo.Z3types || BitVectors == CommandLineOptions.BvHandling.Z3Native;
       } 

     }

     public int Lets {

diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs
index d972eba2..892e7a88 100644
--- a/Source/Provers/Z3/TypeDeclCollector.cs
+++ b/Source/Provers/Z3/TypeDeclCollector.cs
@@ -282,7 +282,7 @@ void ObjectInvariant()
 

     private string ExtractBuiltin(Function f) {

       Contract.Requires(f != null);

-      string retVal = null; 

+      string retVal = null;
       if (NativeBv) {

         retVal = f.FindStringAttribute("bvbuiltin");

       }