.\" Process this file with
.\" groff -man -Tascii SmtEngine.3cvc
.\"
.TH SMTENGINE 3cvc "2020-10-25" "CVC4 release CVC4_RELEASE_STRING" "CVC4 Library Interfaces"
.SH NAME
SmtEngine \- the primary interface to CVC4's theorem-proving capabilities
.SH DESCRIPTION
.B SmtEngine
is the main entry point into the CVC4 theorem prover API.

.SH SMTENGINE OPTIONS

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

.ad l

.RS
.TP 10
.I "COMMON OPTIONS"
$

$
.PD
.RE

.ad b

.SH VERSION
This manual page refers to
.B CVC4
version CVC4_RELEASE_STRING.
.SH BUGS
An issue tracker for the CVC4 project is maintained at
.BR https://github.com/CVC4/CVC4/issues .
.SH AUTHORS
.B 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.
.SH "SEE ALSO"
.BR libcvc4 (3),
.BR libcvc4parser (3)

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