diff options
author | 2013-07-15 13:19:31 +0100 | |
---|---|---|
committer | 2013-07-15 13:19:31 +0100 | |
commit | 2f07af6ca66175d492623d2b46496da3dd0c3c8c (patch) | |
tree | 5887b52adbcc8e4ebd7e3dce7e0c65e2c08e106d /Source/Provers/SMTLib/ProverInterface.cs | |
parent | 345242630d744204df5908f5395d16dc92945686 (diff) |
fix for SetTimeOut in ProverInterface to work only under Z3 parser
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 72b35f01..33b30d0a 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -46,7 +46,7 @@ namespace Microsoft.Boogie.SMTLib [NotDelayed]
public SMTLibProcessTheoremProver (ProverOptions options, VCExpressionGenerator gen,
- SMTLibProverContext ctx)
+ SMTLibProverContext ctx)
{
Contract.Requires (options != null);
Contract.Requires (gen != null);
@@ -401,7 +401,7 @@ namespace Microsoft.Boogie.SMTLib }
private RPFP.Node SExprToCex (SExpr resp, ErrorHandler handler,
- Dictionary<int,Dictionary<string,string>> varSubst)
+ Dictionary<int,Dictionary<string,string>> varSubst)
{
Dictionary<string, RPFP.Node> nmap = new Dictionary<string,RPFP.Node> ();
Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node> ();
@@ -552,8 +552,8 @@ namespace Microsoft.Boogie.SMTLib }
public override Outcome CheckRPFP (string descriptiveName, RPFP _rpfp, ErrorHandler handler,
- out RPFP.Node cex,
- Dictionary<int,Dictionary<string,string>> varSubst)
+ out RPFP.Node cex,
+ Dictionary<int,Dictionary<string,string>> varSubst)
{
//Contract.Requires(descriptiveName != null);
//Contract.Requires(vc != null);
@@ -1179,12 +1179,14 @@ namespace Microsoft.Boogie.SMTLib public override void SetTimeOut(int ms)
{
+ if (options.Solver == SolverKind.Z3) {
var name = Z3.SetTimeoutOption();
var value = ms.ToString();
options.TimeLimit = ms;
options.SmtOptions.RemoveAll(ov => ov.Option == name);
options.AddSmtOption(name, value);
SendThisVC(string.Format("(set-option :{0} {1})", name, value));
+ }
}
public override object Evaluate(VCExpr expr)
|