diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-07-15 14:04:50 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-15 14:04:50 +0100 |
| commit | cf4543349ed64553d9d5a07a8d238a80a913eebb (patch) | |
| tree | 974ba372fe73e268e4d85d9aa838e55546425fc3 | |
| parent | 2f07af6ca66175d492623d2b46496da3dd0c3c8c (diff) | |
fix: can now setup CVC4 logic properly, default is ALL_SUPPORTED, other logics can be set with the previously existing command e.g. /proverOpt:LOGIC=QF_ALL_SUPPORTED
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 16 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProverOptions.cs | 2 |
2 files changed, 9 insertions, 9 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 33b30d0a..3cd34158 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -1179,14 +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));
- }
+ 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)
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index 84d0ba47..3f4ef5ac 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -92,7 +92,7 @@ namespace Microsoft.Boogie.SMTLib break;
case "cvc4":
Solver = SolverKind.CVC4;
- Logic = "QF_ALL_SUPPORTED";
+ if (Logic.Equals("")) Logic = "ALL_SUPPORTED";
break;
default:
ReportError("Invalid SOLVER value; must be 'z3' or 'cvc4'");
|