diff --git a/README.md b/README.md index 1e209938..59ae61e6 100644 --- a/README.md +++ b/README.md @@ -152,7 +152,7 @@ return either an error or the result from the solver. A default ``smtchecker.js`` which exports the ``smtCallback`` function that takes 1) a function that takes queries and returns the solving result, and 2) a solver configuration object. The module ``smtsolver.js`` has a few predefined solver -configurations, and relies on Z3, Eldarica or CVC4 being installed locally. It +configurations, and relies on Z3, Eldarica or cvc5 being installed locally. It exports the list of locally found solvers and a function that invokes a given solver. diff --git a/smtsolver.ts b/smtsolver.ts index 9bd73b36..29993a18 100644 --- a/smtsolver.ts +++ b/smtsolver.ts @@ -18,8 +18,8 @@ const potentialSolvers = [ params: '-horn -t:' + (timeout / 1000) // Eldarica takes timeout in seconds. }, { - name: 'cvc4', - command: 'cvc4', + name: 'cvc5', + command: 'cvc5', params: '--lang=smt2 --tlimit=' + timeout } ];