---
name: "SmtEngine"
section: "3cvc"
platform: "linux"
package: "cvc4"
version: "1.8-3"
release: "Arch Linux 2026-11-01"
platforms: ["linux"]
url: "https://new.carta.tech/SmtEngine"
---

# SmtEngine(3cvc)

the primary interface to CVC4's theorem-proving capabilities

## NAME

SmtEngine - the primary interface to CVC4's theorem-proving capabilities

## DESCRIPTION

**SmtEngine** is the main entry point into the CVC4 theorem prover API.

## SMTENGINE OPTIONS

The SmtEngine is in charge of setting and getting information and options. Numerous options are available via the *SmtEngine::setOption()* call. *SmtEngine::setOption()* and *SmtEngine::getOption()* use the following option keys.

- *COMMON OPTIONS*

  $

  $

## VERSION

This manual page refers to **CVC4** version CVC4\_RELEASE\_STRING.

## BUGS

An issue tracker for the CVC4 project is maintained at **https://github.com/CVC4/CVC4/issues**.

## AUTHORS

**CVC4** is developed by a team of researchers at Stanford University and the University of Iowa. See the AUTHORS file in the distribution for a full list of contributors.

## SEE ALSO

[**libcvc4**(3)](/libcvc4/3.md), [**libcvc4parser**(3)](/libcvc4parser/3.md)

Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4.  It is maintained at **http://cvc4.cs.stanford.edu/wiki/**.