CVC5 VS Code Extension
A Visual Studio Code extension for editing and executing SMT-LIB 2 (.smt2) scripts using the cvc5 and WebAssembly (WASM) build.
No native binary installation is required! The solver runs entirely inside Node.js/V8 via an embedded WebAssembly build of cvc5.
[!TIP]
If you are looking for Z3 support, check out the SMT Z3 which provides similar functionality for Z3.
Features
- Run
cvc5 checks right in your editor without installing or compiling C++ binaries or setting up $PATH.
- Full TextMate grammar (
source.smt) and language configuration (.smt2) support including keywords, commands, sorts, and constants.
- Interactive CodeLens Buttons
- Isolated Execution Process
- Configurable Timeout & Display
🛠️ Usage
- Open any
.smt2 file in VS Code.
- Click the
▶ Execute CodeLens button at the top of the file or on your current line.
(Alternatively, use the command palette Ctrl+Shift+P / Cmd+Shift+P and select Execute cvc5).
- View the results instantly in the cvc5 Output webview panel alongside your editor.
- If a query is running too long, click
⏹ Stop (or select Stop cvc5 from the command palette).
Example SMT-LIB 2 Script
(set-logic QF_LIA)
(set-option :produce-models true)
(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 10))
(assert (= (- x y) 4))
(check-sat)
(get-model)
Result Output Panel:
;; Solver result (re)generated at 2026-07-09 21:00:00
;; Execution time: 14ms
sat
(
(define-fun x () Int 7)
(define-fun y () Int 3)
)
Extension Settings
This extension contributes the following settings under the cvc5 category (Settings -> Extensions -> cvc5 Configuration):
| Setting |
Type |
Default |
Description |
cvc5.timeout |
number |
60000 |
Timeout in milliseconds before a running cvc5 process is automatically terminated (SIGKILL). |
cvc5.showCurrentLineCodeLens |
boolean |
true |
Show ▶ Execute / ⏹ Stop CodeLens buttons above the currently active line in the editor. |
cvc5.showSolveTime |
boolean |
true |
Display the execution timestamp and total time elapsed (ms) inside the result panel. |
cvc5.produceModels |
boolean |
true |
Automatically pass --produce-models (-m) to cvc5 so get-model and get-value commands work cleanly. |
cvc5.incremental |
boolean |
true |
Automatically pass --incremental (-i) to cvc5 to support incremental solving (push/pop). |
cvc5.additionalArgs |
string[] |
[] |
Additional command-line arguments to pass to the cvc5 solver process (e.g., ["--verbose"]). |
cvc5.showWarnings |
boolean |
true |
Show diagnostic warnings and stderr output (e.g., missing set-logic recommendations) inside the result panel. |
You can quickly open these settings anytime by running the Open Settings command from the command palette.
Commands
| Command ID |
Title |
Description |
cvc5.run |
Execute cvc5 |
Executes the active .smt2 document inside the cvc5 WebAssembly engine. |
cvc5.stop |
Stop cvc5 |
Kills the currently running cvc5 child process. |
cvc5.openSettings |
Open Settings |
Opens the VS Code settings UI directly to the cvc5 configuration section. |
License
This extension is licensed under the MIT License. See LICENSE for more information.
For cvc5 and the underlying dependencies (e.g., SAT Solvers), see the cvc5 License (COPYING)
Acknowledgements
