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 /Source/Provers/SMTLib/SMTLibProverOptions.cs | |
| 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
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibProverOptions.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProverOptions.cs | 2 |
1 files changed, 1 insertions, 1 deletions
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'");
|