diff options
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index b85fdec1..01b8f3f6 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -2100,7 +2100,7 @@ namespace Microsoft.Boogie.SMTLib public class SMTLibInterpolatingProcessTheoremProver : SMTLibProcessTheoremProver
{
- SMTLibInterpolatingProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen,
+ public SMTLibInterpolatingProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen,
SMTLibProverContext ctx)
: base(options, gen, ctx)
{
@@ -2372,6 +2372,9 @@ namespace Microsoft.Boogie.SMTLib public class Factory : ProverFactory
{
+ // Set programmatically
+ public static bool UseInterpolation = false;
+
public override object SpawnProver(ProverOptions options, object ctxt)
{
//Contract.Requires(ctxt != null);
@@ -2414,6 +2417,9 @@ namespace Microsoft.Boogie.SMTLib Contract.Requires(ctx != null);
Contract.Ensures(Contract.Result<SMTLibProcessTheoremProver>() != null);
+ if (UseInterpolation)
+ return new SMTLibInterpolatingProcessTheoremProver(options, gen, ctx);
+
return new SMTLibProcessTheoremProver(options, gen, ctx);
}
|