diff options
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 21 |
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) { |