diff --git a/build.gradle b/build.gradle index b305f9e..da01a5e 100644 --- a/build.gradle +++ b/build.gradle @@ -8,7 +8,7 @@ repositories { } dependencies { - implementation 'edu.uiowa.cs.clc:kind2-java-api:0.3.2' + implementation 'edu.uiowa.cs.clc:kind2-java-api:0.3.3' 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 index 1cf9c1a..7d97fbd 100644 --- a/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java +++ b/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java @@ -370,6 +370,8 @@ private SolverOption stringToSolver(String solver) { return SolverOption.BITWUZLA; case "CVC5": return SolverOption.CVC5; + case "MATHSAT": + return SolverOption.MATHSAT; case "YICES": return SolverOption.YICES; case "YICES2": @@ -464,6 +466,11 @@ private void setSmtSolverPath(Kind2Api api, SolverOption solver, api.setcvc5Bin(smtConfigs.get("cvc5_bin").getAsString()); } break; + case MATHSAT: + if (!smtConfigs.get("mathsat_bin").getAsString().equals("mathsat")) { + api.setMathSATBin(smtConfigs.get("mathsat_bin").getAsString()); + } + break; case YICES: if (!smtConfigs.get("yices_bin").getAsString().equals("yices")) { api.setYicesBin(smtConfigs.get("yices_bin").getAsString());