summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-07-09 20:13:23 +0000
committerMorgan Deters <mdeters@gmail.com>2012-07-09 20:13:23 +0000
commit42e7a38f0a0b38722c2f58ff028a5d3af9337347 (patch)
tree5f9dac3afecc40138b6f98d7db7425db792e93ab /doc
parent95ff2500c189a1c6a2dc6a6b29b1e8f9e792ac1d (diff)
minor fix-ups
Diffstat (limited to 'doc')
-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