Allow /prune:0 to disable pruning

Source/Directory.Build.props

@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.0.11</Version>
+    <Version>3.0.12</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

Source/ExecutionEngine/CommandLineOptions.cs

@@ -1257,6 +1257,10 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
           ps.GetIntArgument(x => normalizeDeclarationOrder = x);
           return true;
 
+        case "prune":
+          ps.GetIntArgument(x => Prune = x);
+          return true;
+
         default:
           bool optionValue = false;
           if (ps.CheckBooleanFlag("printUnstructured", x => optionValue = x))
@@ -1318,7 +1322,6 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
               ps.CheckBooleanFlag("trustSequentialization", x => trustSequentialization = x) ||
               ps.CheckBooleanFlag("useBaseNameForFileName", x => UseBaseNameForFileName = x) ||
               ps.CheckBooleanFlag("freeVarLambdaLifting", x => FreeVarLambdaLifting = x) ||
-              ps.CheckBooleanFlag("prune", x => Prune = x) ||
               ps.CheckBooleanFlag("warnNotEliminatedVars", x => WarnNotEliminatedVars = x)
           )
           {
@@ -1889,12 +1892,14 @@ Boogie automatically detects monomorphic programs and enables
                 the SMT theory of arrays. This option allows the use of axioms instead.
   /reflectAdd   In the VC, generate an auxiliary symbol, elsewhere defined
                 to be +, instead of +.
-  /prune
-                Turn on pruning. Pruning will remove any top-level Boogie declarations 
-                that are not accessible by the implementation that is about to be verified.
-                Without pruning, due to the unstable nature of SMT solvers,
-                a change to any part of a Boogie program has the potential 
-                to affect the verification of any other part of the program.
+  /prune:<n>
+                0 - Turn off pruning.
+                1 - Turn on pruning (default). Pruning will remove any top-level
+                Boogie declarations that are not accessible by the implementation
+                that is about to be verified. Without pruning, due to the unstable
+                nature of SMT solvers, a change to any part of a Boogie program
+                has the potential to affect the verification of any other part of
+                the program.
 
                 Only use this if your program contains uses clauses
                 where required, otherwise pruning will break your program.

Test/commandline/noprune.bpl

@@ -0,0 +1,12 @@
+// RUN: %parallel-boogie -quiet -prune:0 -normalizeNames:0 -proverLog:"%t.noprune.smt2" "%s"
+// RUN: %OutputCheck --file-to-check "%t.noprune.smt2" "%s"
+// CHECK: ThisIsAFunction
+
+function ThisIsAFunction(): int uses {
+  axiom ThisIsAFunction() == 2;
+}
+
+procedure P()
+{
+  assert 1 == 1;
+}

Test/dafny/dafny-issue-4804.bpl

@@ -1,4 +1,4 @@
-// RUN: %parallel-boogie /proverOpt:O:auto_config=false /proverOpt:O:type_check=true /proverOpt:O:smt.qi.eager_threshold=100 /proverOpt:O:smt.delay_units=true /rlimit:10000 /prune "%s" > "%t"
+// RUN: %parallel-boogie /proverOpt:O:auto_config=false /proverOpt:O:type_check=true /proverOpt:O:smt.qi.eager_threshold=100 /proverOpt:O:smt.delay_units=true /rlimit:10000 /prune:1 "%s" > "%t"
 // RUN: %OutputCheck "%s" --file-to-check="%t"
 // CHECK: Boogie program verifier finished with 3 verified, 0 errors, 1 out of resource
 // dafny 4.3.0.0

Test/pruning/IncludeDep.bpl

@@ -1,4 +1,4 @@
-// RUN: %parallel-boogie /prune /errorTrace:0 "%s" > "%t"
+// RUN: %parallel-boogie /prune:1 /errorTrace:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function f1 (x: int) : int;

Test/pruning/MonomorphicSplit.bpl

@@ -1,4 +1,4 @@
-// RUN: %parallel-boogie /prune /errorTrace:0 /printPruned:"%t" "%s" > "%t"
+// RUN: %parallel-boogie /prune:1 /errorTrace:0 /printPruned:"%t" "%s" > "%t"
 // RUN: %OutputCheck "%s" --file-to-check="%t-after-monomorphicSplit.bpl"
 
 // The following checks are a bit simplistic, but this is

Test/pruning/NonmonomorphicSplit.bpl

@@ -1,4 +1,4 @@
-// RUN: %parallel-boogie /prune /trace /errorTrace:0 "%s" > "%t"
+// RUN: %parallel-boogie /prune:1 /trace /errorTrace:0 "%s" > "%t"
 // RUN: %OutputCheck "%s" --file-to-check="%t"
 
 // Related PR #767.

Test/pruning/Triggers.bpl

@@ -1,4 +1,4 @@
- // RUN: %parallel-boogie /prune /errorTrace:0 "%s" > "%t"
+ // RUN: %parallel-boogie /prune:n /errorTrace:0 "%s" > "%t"
  // RUN: %diff "%s.expect" "%t"
 
 function f1 (x: int) : bool;
@@ -32,4 +32,4 @@ axiom (forall x: int :: {f5(f4(x)), f4(x)} f4(x));
 procedure twoTriggers(x : int)
   ensures f4(x);
 {
-}
+}

Test/pruning/UsesClauses.bpl

@@ -1,4 +1,4 @@
-// RUN: %parallel-boogie /prune /printPruned:"%tpruned" /errorTrace:0 "%s" > "%t"
+// RUN: %parallel-boogie /prune:1 /printPruned:"%tpruned" /errorTrace:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 // UNSUPPORTED: batch_mode