diff options
| -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'");
|