# HG changeset patch
# User blanchet
# Date 1298911990 -3600
# Node ID 07573743208f1e8b21d9ebbed1d8b2c072a3146c
# Parent  7244589c8ccc98e37321934be78eaa6ce18fd739
document new "total_consts" option

diff -r 7244589c8ccc -r 07573743208f doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Mon Feb 28 17:53:10 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Mon Feb 28 17:53:10 2011 +0100
@@ -2477,6 +2477,14 @@
 Specifies the default preconstruction setting to use. This can be overridden on
 a per-term basis using the \textit{preconstr}~\qty{term} option described above.
 
+\opsmart{total\_consts}{partial\_consts}
+Specifies whether constants occurring in the problem other than constructors can
+be assumed to be considered total for the representable values that approximate
+a datatype. This option is highly incomplete; it should be used only for
+problems that do not construct datatype values explicitly. Since this option is
+(in rare cases) unsound, counterexamples generated under these conditions are
+tagged as ``quasi genuine.''
+
 \opdefault{datatype\_sym\_break}{int}{\upshape 5}
 Specifies an upper bound on the number of datatypes for which Nitpick generates
 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver