Merge pull request boogie-org#119 from smackers/update-boogie

Updated Boogie to the latest commit

Author: akashlal

boogie

@@ -437,9 +437,7 @@ private HashSet<string> FindConstantLoops(IEnumerable<Implementation> candidates
 
             // set strong array theory
             var ua_old = CommandLineOptions.Clo.UseArrayTheory;
-            var wa_old = CommandLineOptions.Clo.WeakArrayTheory;
             CommandLineOptions.Clo.UseArrayTheory = true;
-            CommandLineOptions.Clo.WeakArrayTheory = false; 
 
             var to = CommandLineOptions.Clo.ProverKillTime;
             CommandLineOptions.Clo.ProverKillTime = 5;
@@ -476,7 +474,6 @@ private HashSet<string> FindConstantLoops(IEnumerable<Implementation> candidates
 
             // Reset options
             CommandLineOptions.Clo.UseArrayTheory = ua_old;
-            CommandLineOptions.Clo.WeakArrayTheory = wa_old; 
 
             CommandLineOptions.Clo.ProverKillTime = to;
 

source/ConstLoop.cs

@@ -153,12 +153,12 @@ public static void Initialize(Configs config)
             CommandLineOptions.Clo.PrintInstrumented = true;
             CommandLineOptions.Clo.ProcedureInlining = CommandLineOptions.Inlining.Assume;
             CommandLineOptions.Clo.StratifiedInliningVerbose = config.verboseMode;
+            CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
 
             // /noRemoveEmptyBlocks is needed for field refinement. It ensures that
             // we get an actual path in the program (so that we can concretize it)
             boogieOptions +=
                 "/removeEmptyBlocks:0 /coalesceBlocks:0 " +
-                "/typeEncoding:m " +
                 "/subsumption:0 ";
 
             InstrumentationConfig.UseOldInstrumentation = false;

source/Driver.cs

@@ -1150,13 +1150,14 @@ private static Expr ExpandITE(IAppliable fun, Expr a, Expr b, Expr c, Expr f, bo
         public static bool ParseCommandLine(string clo)
         {
             //without the next line, it fails to find the right prover!!
-            var boogieOptions = "/typeEncoding:m /doModSetAnalysis -timeLimit:100  -removeEmptyBlocks:0 /errorLimit:1 /printInstrumented " + clo;
+            var boogieOptions = "/doModSetAnalysis -timeLimit:100  -removeEmptyBlocks:0 /errorLimit:1 /printInstrumented " + clo;
             var oldArgs = boogieOptions.Split(' ');
             string[] args;
             //Custom parser to look and remove RootCause specific options
             var help = ParseArgs(oldArgs, out args);
             CommandLineOptions.Install(new CommandLineOptions());
             CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;
+            CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
             CommandLineOptions.Clo.Parse(args);
             return !help;
         }