Enable optimization for more prover queries.

1 files changed, 14 insertions, 7 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index ca530da2..b8fd2f50 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -421,13 +421,7 @@ namespace Microsoft.Boogie.SMTLib
 
       SendThisVC(vcString);
 
-      if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count)
-      {
-        foreach (var r in OptimizationRequests)
-        {
-          SendThisVC(r);
-        }
-      }
+      SendOptimizationRequests();
 
       FlushLogFile();
 
@@ -442,6 +436,17 @@ namespace Microsoft.Boogie.SMTLib
       FlushLogFile();
     }
 
+    private void SendOptimizationRequests()
+    {
+      if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count)
+      {
+        foreach (var r in OptimizationRequests)
+        {
+          SendThisVC(r);
+        }
+      }
+    }
+
     public override void Reset(VCExpressionGenerator gen)
     {
       if (options.Solver == SolverKind.Z3)
@@ -2137,6 +2142,7 @@ namespace Microsoft.Boogie.SMTLib
 
     public override void Assert(VCExpr vc, bool polarity)
     {
+        OptimizationRequests.Clear();
         string a = "";
         if (polarity)
         {
@@ -2148,6 +2154,7 @@ namespace Microsoft.Boogie.SMTLib
         }
         AssertAxioms();
         SendThisVC(a);
+        SendOptimizationRequests();
     }
 
     public override void DefineMacro(Macro f, VCExpr vc) {