Merge remote-tracking branch 'upstream/master' into concurrent-split-…

…coverage

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