summaryrefslogtreecommitdiff
path: root/doc/cvc4.1.in
diff options
context:
space:
mode:
Diffstat (limited to 'doc/cvc4.1.in')
-rw-r--r--doc/cvc4.1.in11
1 files changed, 10 insertions, 1 deletions
diff --git a/doc/cvc4.1.in b/doc/cvc4.1.in
index dfc7e01a0..6c6a9768c 100644
--- a/doc/cvc4.1.in
+++ b/doc/cvc4.1.in
@@ -3,17 +3,26 @@
.\"
.TH CVC4 1 "@MAN_DATE@" "CVC4 release @VERSION@" "User Manuals"
.SH NAME
-cvc4 \- an automated theorem prover
+cvc4, pcvc4 \- an automated theorem prover
.SH SYNOPSIS
.B cvc4 [
.I options
.B ] [
.I file
.B ]
+.P
+.B pcvc4 [
+.I options
+.B ] [
+.I file
+.B ]
.SH DESCRIPTION
.B cvc4
is an automated theorem prover for first-order formulas with respect
to background theories of interest.
+.B pcvc4
+is CVC4's "portfolio" variant, which is capable of running multiple
+CVC4 instances in parallel, configured differently.
With
.I file
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback