Allow /prune:0 to disable pruning (#848)

Add a `/noprune` flag to turn off pruning. It's off by default, but this
can be convenient if a) it's turned on earlier on the command line, or
b) Boogie is being used from another system like Dafny.

I would have made it `/prune:{1,0}`, but it's harder to make that
backward compatible with the current behavior.

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/coverage/verificationCoverage.bpl

@@ -91,13 +91,13 @@
 // CHECK:   xy_sum
 // RUN: %boogie -trackVerificationCoverage "%s" > "%t.coverage"
 // RUN: %diff "%s.expect" "%t.coverage"
-// RUN: %boogie -trackVerificationCoverage -typeEncoding:a -prune "%s" > "%t.coverage-a"
+// RUN: %boogie -trackVerificationCoverage -typeEncoding:a -prune:1 "%s" > "%t.coverage-a"
 // RUN: %diff "%s.expect" "%t.coverage-a"
-// RUN: %boogie -trackVerificationCoverage -typeEncoding:p -prune "%s" > "%t.coverage-p"
+// RUN: %boogie -trackVerificationCoverage -typeEncoding:p -prune:1 "%s" > "%t.coverage-p"
 // RUN: %diff "%s.expect" "%t.coverage-p"
-// RUN: %boogie -trackVerificationCoverage -normalizeDeclarationOrder:1 -prune "%s" > "%t.coverage-d"
+// RUN: %boogie -trackVerificationCoverage -normalizeDeclarationOrder:1 -prune:1 "%s" > "%t.coverage-d"
 // RUN: %diff "%s.expect" "%t.coverage-d"
-// RUN: %boogie -trackVerificationCoverage -normalizeNames:1 -prune "%s" > "%t.coverage-n"
+// RUN: %boogie -trackVerificationCoverage -normalizeNames:1 -prune:1 "%s" > "%t.coverage-n"
 // RUN: %diff "%s.expect" "%t.coverage-n"
 
 procedure testRequiresAssign(n: int)

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:1 /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
 

Test/test15/CommonVariablesPruning.bpl

@@ -1,6 +1,6 @@
 // VcsCores:1 means we only use a single solver for both procedures in this Boogie program.
 // Prune triggers a full reset after using the solver on one problem
-// RUN: %boogie "%s" -typeEncoding:p -vcsCores:1 -normalizeNames:1 -prune -mv:- > "%t"
+// RUN: %boogie "%s" -typeEncoding:p -vcsCores:1 -normalizeNames:1 -prune:1 -mv:- > "%t"
 // RUN: %diff "%s.expect" "%t" --ignore-matching-lines='else ->'
 
 // Part of the MultiDimArray test from Dafny: https://github.com/dafny-lang/dafny/blob/cc913d9159ded2ad131c048135f817e49f500e50/Test/dafny0/MultiDimArray.dfy