Fixed bug with uniformity analysis for havoc. Allowed barrier invariants to

support a more expressive class of expressions.  Refactored thread id creation
functions.

1 files changed, 10 insertions, 0 deletions

diff --git a/Source/VCGeneration/UniformityAnalyser.cs b/Source/VCGeneration/UniformityAnalyser.cs
index 849333b3..802ee2d2 100644
--- a/Source/VCGeneration/UniformityAnalyser.cs
+++ b/Source/VCGeneration/UniformityAnalyser.cs
@@ -309,6 +309,16 @@ namespace Microsoft.Boogie
                         }
                     }
                 }
+                else if (c is HavocCmd)
+                {
+                    HavocCmd havocCmd = c as HavocCmd;
+                    foreach(IdentifierExpr ie in havocCmd.Vars)
+                    {
+                        if(IsUniform(impl.Name, ie.Decl.Name)) {
+                            SetNonUniform(impl.Name, ie.Decl.Name);
+                        }
+                    }
+                }
                 else if (c is CallCmd)
                 {
                     CallCmd callCmd = c as CallCmd;