7 files changed, 95 insertions, 20 deletions
diff --git a/doc/SmtEngine.3cvc4_template.in b/doc/SmtEngine.3cvc4_template.in
new file mode 100644
index 000000000..99b0451f6
--- /dev/null
+++ b/doc/SmtEngine.3cvc4_template.in
@@ -0,0 +1,51 @@
+.\" Process this file with
+.\" groff -man -Tascii SmtEngine.3cvc4
+.\"
+.TH SMTENGINE 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "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.
+
+.RS
+.TP 10
+.I "COMMON OPTIONS"
+${common_manpage_smt_documentation}
+
+${remaining_manpage_smt_documentation}
+.PD
+.RE
+
+.SH VERSION
+This manual page refers to
+.B CVC4
+version @VERSION@.
+.SH BUGS
+A Bugzilla for the CVC4 project is maintained at
+.BR http://church.cims.nyu.edu/bugzilla3/ .
+.SH AUTHORS
+.B CVC4
+is developed by a team of researchers at New York 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),
+.BR libcvc4compat (3)
+
+Additionally, the CVC4 wiki contains useful information about the
+design and internals of CVC4.  It is maintained at
+.BR http://church.cims.nyu.edu/wiki/ .
diff --git a/doc/cvc4.1_template.in b/doc/cvc4.1_template.in
index ad8226261..5a5f90214 100644
--- a/doc/cvc4.1_template.in
+++ b/doc/cvc4.1_template.in
@@ -115,7 +115,7 @@ This manual page refers to
 version @VERSION@.
 .SH BUGS
 A Bugzilla for the CVC4 project is maintained at
-.BR http://goedel.cs.nyu.edu/bugzilla3/ .
+.BR http://church.cims.nyu.edu/bugzilla3/ .
 .SH AUTHORS
 .B CVC4
 is developed by a team of researchers at New York University
@@ -129,4 +129,4 @@ contributors.
 
 Additionally, the CVC4 wiki contains useful information about the
 design and internals of CVC4.  It is maintained at
-.BR http://goedel.cs.nyu.edu/wiki/ .
+.BR http://church.cims.nyu.edu/wiki/ .
diff --git a/doc/cvc4.5.in b/doc/cvc4.5.in
index d862eec8a..ab4e8806c 100644
--- a/doc/cvc4.5.in
+++ b/doc/cvc4.5.in
@@ -18,4 +18,4 @@ to background theories of interest.
 
 Additionally, the CVC4 wiki contains useful information about the
 design and internals of CVC4.  It is maintained at
-.BR http://goedel.cs.nyu.edu/wiki/ .
+.BR http://church.cims.nyu.edu/wiki/ .
diff --git a/doc/libcvc4.3_template.in b/doc/libcvc4.3_template.in
index 5483099c3..2ff96eb5a 100644
--- a/doc/libcvc4.3_template.in
+++ b/doc/libcvc4.3_template.in
@@ -55,21 +55,6 @@ is used to build up expressions and types, and the
 .I SmtEngine
 is used primarily to make assertions, check satisfiability/validity, and extract models and proofs.
 
-The SmtEngine is also in charge of setting and getting information and options.
-.I SmtEngine::setOption()
-and
-.I SmtEngine::getOption()
-use the following option keys.
-
-.RS
-.TP 10
-.I "COMMON OPTIONS"
-${common_manpage_smt_documentation}
-
-${remaining_manpage_smt_documentation}
-.PD
-.RE
-
 .SH "SEE ALSO"
 .BR cvc4 (1),
 .BR libcvc4parser (3),
diff --git a/doc/libcvc4compat.3.in b/doc/libcvc4compat.3.in
index e429fc815..3722557b0 100644
--- a/doc/libcvc4compat.3.in
+++ b/doc/libcvc4compat.3.in
@@ -12,4 +12,4 @@ libcvc4compat \- a CVC3 compatibility library interface for the CVC4 theorem pro
 
 Additionally, the CVC4 wiki contains useful information about the
 design and internals of CVC4.  It is maintained at
-.BR http://goedel.cs.nyu.edu/wiki/ .
+.BR http://church.cims.nyu.edu/wiki/ .
diff --git a/doc/libcvc4parser.3.in b/doc/libcvc4parser.3.in
index fa17d6d18..67ec74326 100644
--- a/doc/libcvc4parser.3.in
+++ b/doc/libcvc4parser.3.in
@@ -12,4 +12,4 @@ libcvc4parser \- a parser library interface for the CVC4 theorem prover
 
 Additionally, the CVC4 wiki contains useful information about the
 design and internals of CVC4.  It is maintained at
-.BR http://goedel.cs.nyu.edu/wiki/ .
+.BR http://church.cims.nyu.edu/wiki/ .
diff --git a/doc/options.3cvc4_template.in b/doc/options.3cvc4_template.in
new file mode 100644
index 000000000..8ee39b761
--- /dev/null
+++ b/doc/options.3cvc4_template.in
@@ -0,0 +1,39 @@
+.\" Process this file with
+.\" groff -man -Tascii options.3cvc4
+.\"
+.TH OPTIONS 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Internals Documentation"
+.SH NAME
+options \- the options infrastructure
+
+.SH AVAILABLE INTERNAL OPTIONS
+
+.RS
+.TP 10
+.I "COMMON OPTIONS"
+${common_manpage_internals_documentation}
+
+${remaining_manpage_internals_documentation}
+.PD
+.RE
+
+.SH VERSION
+This manual page refers to
+.B CVC4
+version @VERSION@.
+.SH BUGS
+A Bugzilla for the CVC4 project is maintained at
+.BR http://church.cims.nyu.edu/bugzilla3/ .
+.SH AUTHORS
+.B CVC4
+is developed by a team of researchers at New York 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),
+.BR libcvc4compat (3)
+
+Additionally, the CVC4 wiki contains useful information about the
+design and internals of CVC4.  It is maintained at
+.BR http://church.cims.nyu.edu/wiki/ .