Added /z3lets switch, which governs which kinds of LET expressions are sent to Z3. By default, both LET TERM and LET FORMULA expressions are used. Mode /z3lets:2 uses only LET FORMULA, which works around a current Z3 issue with LET expressions and nested quantifiers.

1 files changed, 15 insertions, 3 deletions

diff --git a/Source/Provers/Z3/ProverInterface.ssc b/Source/Provers/Z3/ProverInterface.ssc
index 02b4f505..c3a61fe3 100644
--- a/Source/Provers/Z3/ProverInterface.ssc
+++ b/Source/Provers/Z3/ProverInterface.ssc
@@ -75,6 +75,13 @@ namespace Microsoft.Boogie.Z3
         return CommandLineOptions.Clo.Z3types || BitVectors == CommandLineOptions.BvHandling.Z3Native; 

       } 

     }

+    public int Lets {

+      get

+        ensures 0 <= result && result < 4;

+      {

+        return CommandLineOptions.Clo.Z3lets;

+      }

+    }

     public bool V1 = false;

     public bool V2 = false; // default set in PostParse

     public bool DistZ3 = false;

@@ -107,8 +114,8 @@ namespace Microsoft.Boogie.Z3
         ExeName = "z3-v1.3.exe";

       }

       if (DistZ3) {

-		ExeName = "z3-dist.exe";

-		CommandLineOptions.Clo.RestartProverPerVC = true;

+        ExeName = "z3-dist.exe";

+        CommandLineOptions.Clo.RestartProverPerVC = true;

       }

       

     }

@@ -227,7 +234,6 @@ namespace Microsoft.Boogie.Z3
           eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);

           break;

       }

-      

       VCExpr! exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;

       

       LetBindingSorter! letSorter = new LetBindingSorter(Gen);

@@ -243,6 +249,12 @@ namespace Microsoft.Boogie.Z3
         sortedExpr = flattener.Flatten(sortedExpr);

         sortedAxioms = flattener.Flatten(sortedAxioms);

       }

+      if (Opts.Lets != 3) {

+        // replace let expressions with implies

+        Let2ImpliesMutator letImplier = new Let2ImpliesMutator(Gen, Opts.Lets == 1, Opts.Lets == 2);

+        sortedExpr = letImplier.Mutate(sortedExpr);

+        sortedAxioms = letImplier.Mutate(sortedAxioms);

+      }

 

       //////////////////////////////////////////////////////////////////////////

       //SubtermCollector! coll = new SubtermCollector (gen);