From 1c16dc829c81426e17427c0d103ed831a48f1f81 Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Sun, 27 Dec 2015 15:08:38 -0600
Subject: Enable optimization for more prover queries.

---
 Source/Provers/SMTLib/ProverInterface.cs | 21 ++++++++++++++-------
 1 file 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) {
-- 
cgit v1.2.3