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

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