Replace CVC4 with cvc5

kind2-mc · Dec 13, 2022 · d3d8d02 · d3d8d02
1 parent 6e2cd64
commit d3d8d02
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/build.gradle b/build.gradle
@@ -8,7 +8,7 @@ repositories {
 }
 
 dependencies {
-  implementation 'edu.uiowa.cs.clc:kind2-java-api:0.3.0'
+  implementation 'edu.uiowa.cs.clc:kind2-java-api:0.3.1'
   implementation 'org.eclipse.lsp4j:org.eclipse.lsp4j:0.13.0'
   testImplementation 'org.junit.jupiter:junit-jupiter-api:5.7.2'
   testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.7.2'

diff --git a/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java b/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java
@@ -363,8 +363,8 @@ private SolverOption stringToSolver(String solver) {
     switch (solver.toUpperCase()) {
     case "BOOLECTOR":
       return SolverOption.BOOLECTOR;
-    case "CVC4":
-      return SolverOption.CVC4;
+    case "CVC5":
+      return SolverOption.CVC5;
     case "YICES":
       return SolverOption.YICES;
     case "YICES2":
@@ -454,9 +454,9 @@ private void setSmtSolverPath(Kind2Api api, SolverOption solver,
           api.setBoolectorBin(smtConfigs.get("boolector_bin").getAsString());
         }
         break;
-      case CVC4:
-        if (!smtConfigs.get("cvc4_bin").getAsString().equals("cvc4")) {
-          api.setBoolectorBin(smtConfigs.get("cvc4_bin").getAsString());
+      case CVC5:
+        if (!smtConfigs.get("cvc5_bin").getAsString().equals("cvc5")) {
+          api.setBoolectorBin(smtConfigs.get("cvc5_bin").getAsString());
         }
         break;
       case YICES: