Enable optimization for more prover queries.

alexanderjsummers · Dec 27, 2015 · 1c16dc8 · 1c16dc8
1 parent eb64daf
commit 1c16dc8
Showing 1 changed file with 14 additions and 7 deletions.
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
@@ -421,13 +421,7 @@ public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler
 
       SendThisVC(vcString);
 
-      if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count)
-      {
-        foreach (var r in OptimizationRequests)
-        {
-          SendThisVC(r);
-        }
-      }
+      SendOptimizationRequests();
 
       FlushLogFile();
 
@@ -442,6 +436,17 @@ public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler
       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 @@ private void FlushPushedAssertions()
 
     public override void Assert(VCExpr vc, bool polarity)
     {
+        OptimizationRequests.Clear();
         string a = "";
         if (polarity)
         {
@@ -2148,6 +2154,7 @@ public override void Assert(VCExpr vc, bool polarity)
         }
         AssertAxioms();
         SendThisVC(a);
+        SendOptimizationRequests();
     }
 
     public override void DefineMacro(Macro f, VCExpr vc) {