Merge pull request #134 from bkragl/drop-dead-options

Remove dead Boogie options
boogie-org · Oct 29, 2020 · 4dcf5fb · 4dcf5fb
2 parents 90ee3e9 + 36da229
commit 4dcf5fb
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 12 deletions.
diff --git a/source/CoreLib/VerificationPasses.cs b/source/CoreLib/VerificationPasses.cs
@@ -1158,7 +1158,6 @@ public override CBAProgram runCBAPass(CBAProgram program)
                 Debug.Assert(onlyEnsures());
                 // Turn on summary computation in Boogie
                 Debug.Assert(CommandLineOptions.Clo.StratifiedInlining > 0);
-                CommandLineOptions.Clo.StratifiedInliningOption = 1;
             }
 
             // Insert summaries
@@ -1694,14 +1693,7 @@ protected void PruneIrrelevantImpls(Program program)
 
         public override ErrorTrace mapBackTrace(ErrorTrace trace)
         {
-            var ret = trace;
-            if(ExtractLoops) ret = elPass.mapBackTrace(trace);
-
-            if (!runHoudini)
-            {
-                CommandLineOptions.Clo.StratifiedInliningOption = 0;
-            }
-            return ret;
+            return ExtractLoops ? elPass.mapBackTrace(trace) : trace;
         }
     }
 

diff --git a/source/Util/BoogieUtil.cs b/source/Util/BoogieUtil.cs
@@ -45,9 +45,6 @@ public static bool InitializeBoogie(string clo)
             if (!CommandLineOptions.Clo.Parse(args.ToArray()))
                 return true;
 
-            // No Max: avoids theorem prover restarts
-            CommandLineOptions.Clo.MaxProverMemory = 0;
-
             return false;
         }