summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/SMTLibProverOptions.cs
diff options
context:
space:
mode:
authorGravatar Pantazis Deligiannis <pdeligia@me.com>2013-07-15 14:04:50 +0100
committerGravatar Pantazis Deligiannis <pdeligia@me.com>2013-07-15 14:04:50 +0100
commitcf4543349ed64553d9d5a07a8d238a80a913eebb (patch)
tree974ba372fe73e268e4d85d9aa838e55546425fc3 /Source/Provers/SMTLib/SMTLibProverOptions.cs
parent2f07af6ca66175d492623d2b46496da3dd0c3c8c (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.cs2
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'");