From 1d03f0abe500779ee7bde821b0f51f348450f7d4 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Fri, 3 Oct 2014 10:19:49 +0530
Subject: minor fixes to interpolating TP

---
 Source/Provers/SMTLib/ProverInterface.cs | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 01b8f3f6..d4767511 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -163,7 +163,7 @@ namespace Microsoft.Boogie.SMTLib
     readonly List<string> proverErrors = new List<string>();
     readonly List<string> proverWarnings = new List<string>();
     readonly StringBuilder common = new StringBuilder();
-    TextWriter currentLogFile;
+    protected TextWriter currentLogFile;
     protected volatile ErrorHandler currentErrorHandler;
 
     private void FeedTypeDeclsToProver()
@@ -2102,9 +2102,16 @@ namespace Microsoft.Boogie.SMTLib
   {
       public SMTLibInterpolatingProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen,
                                         SMTLibProverContext ctx)
-          : base(options, gen, ctx)
+          : base(AddInterpOption(options), gen, ctx)
       {
-          // anything else?
+
+      }
+
+      private static ProverOptions AddInterpOption(ProverOptions options)
+      {
+          var opts = (SMTLibProverOptions)options;
+          opts.AddSmtOption("produce-interpolants", "true");
+          return opts;
       }
 
       public override void AssertNamed(VCExpr vc, bool polarity, string name)
@@ -2232,6 +2239,7 @@ namespace Microsoft.Boogie.SMTLib
 
           vcStr = "(get-interpolant (and\r\n" + vcStr + "\r\n))";
           SendThisVC(vcStr);
+          if(currentLogFile != null) currentLogFile.Flush();
 
           List<SExpr> interpolantList;
           Outcome result2 = GetTreeInterpolantResponse(out interpolantList);
-- 
cgit v1.2.3