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