From 3ba9758912ab62a5fad964142836079e97ede344 Mon Sep 17 00:00:00 2001 From: r0qs Date: Mon, 10 Jun 2024 13:28:22 +0200 Subject: [PATCH] Update cvc4 to cvc5 --- README.md | 2 +- smtsolver.ts | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) 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 } ];