minor fix-ups

diff --git a/Makefile.am b/Makefile.am
index 2edd33820faecabc16fb5faf73ea3909889dcab2..b72c710319323a00526e70d7fe66079e27432886 100644 (file)
--- a/Makefile.am
+++ b/Makefile.am
@@ -111,11 +111,16 @@ EXTRA_DIST = \
        doc/libcvc4compat.3.in
 man_MANS = \
        doc/cvc4.1 \
+       doc/pcvc4.1 \
        doc/cvc4.5 \
        doc/libcvc4.3 \
        doc/libcvc4parser.3 \
        doc/libcvc4compat.3
 
+doc/pcvc4.1:
+       rm -f doc/pcvc4.1
+       $(LN_S) cvc4.1 doc/pcvc4.1
+
 dist-hook:
        cp -p "$(srcdir)/Makefile" "$(distdir)/Makefile"
 

diff --git a/doc/cvc4.1.in b/doc/cvc4.1.in
index dfc7e01a0261e70cca5b8be797caf0ec610cc98d..6c6a9768ca4b4be111e69757e4b285f8c06d51d8 100644 (file)
--- 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