1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Mar 11 09:09:51 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Mar 11 10:13:24 2010 +0100
     1.3 @@ -150,12 +150,12 @@
     1.4  \textbf{begin}
     1.5  \postw
     1.6  
     1.7 -The results presented here were obtained using the JNI version of MiniSat and
     1.8 -with multithreading disabled to reduce nondeterminism and a time limit of
     1.9 -15~seconds (instead of 30~seconds). This was done by adding the line
    1.10 +The results presented here were obtained using the JNI (Java Native Interface)
    1.11 +version of MiniSat and with multithreading disabled to reduce nondeterminism.
    1.12 +This was done by adding the line
    1.13  
    1.14  \prew
    1.15 -\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\textit{timeout} = 15$\,s$]
    1.16 +\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
    1.17  \postw
    1.18  
    1.19  after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
    1.20 @@ -2203,11 +2203,9 @@
    1.21  Specifies the maximum number of potential counterexamples to display. Setting
    1.22  this option to 0 speeds up the search for a genuine counterexample. This option
    1.23  is implicitly set to 0 for automatic runs. If you set this option to a value
    1.24 -greater than 1, you will need an incremental SAT solver: For efficiency, it is
    1.25 -recommended to install the JNI version of MiniSat and set \textit{sat\_solver} =
    1.26 -\textit{MiniSat\_JNI}. Also be aware that many of the counterexamples may look
    1.27 -identical, unless the \textit{show\_all} (\S\ref{output-format}) option is
    1.28 -enabled.
    1.29 +greater than 1, you will need an incremental SAT solver, such as
    1.30 +\textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of
    1.31 +the counterexamples may be identical.
    1.32  
    1.33  \nopagebreak
    1.34  {\small See also \textit{check\_potential} (\S\ref{authentication}) and
    1.35 @@ -2215,11 +2213,9 @@
    1.36  
    1.37  \opdefault{max\_genuine}{int}{$\mathbf{1}$}
    1.38  Specifies the maximum number of genuine counterexamples to display. If you set
    1.39 -this option to a value greater than 1, you will need an incremental SAT solver:
    1.40 -For efficiency, it is recommended to install the JNI version of MiniSat and set
    1.41 -\textit{sat\_solver} = \textit{MiniSat\_JNI}. Also be aware that many of the
    1.42 -counterexamples may look identical, unless the \textit{show\_all}
    1.43 -(\S\ref{output-format}) option is enabled.
    1.44 +this option to a value greater than 1, you will need an incremental SAT solver,
    1.45 +such as \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that
    1.46 +many of the counterexamples may be identical.
    1.47  
    1.48  \nopagebreak
    1.49  {\small See also \textit{check\_genuine} (\S\ref{authentication}) and
    1.50 @@ -2330,13 +2326,11 @@
    1.51  and 2.0 beta (2007-07-21).
    1.52  
    1.53  \item[$\bullet$] \textbf{\textit{MiniSat\_JNI}}: The JNI (Java Native Interface)
    1.54 -version of MiniSat is bundled in \texttt{nativesolver.\allowbreak tgz}, which
    1.55 -you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
    1.56 +version of MiniSat is bundled with Kodkodi and is precompiled for the major
    1.57 +platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
    1.58 +which you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
    1.59  version of MiniSat, the JNI version can be used incrementally.
    1.60  
    1.61 -%%% No longer true:
    1.62 -%%% "It is bundled with Kodkodi and requires no further installation or
    1.63 -%%% configuration steps. Alternatively,"
    1.64  \item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
    1.65  written in C. You can install a standard version of
    1.66  PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
    1.67 @@ -2355,8 +2349,9 @@
    1.68  versions 2004-05-13, 2004-11-15, and 2007-03-12.
    1.69  
    1.70  \item[$\bullet$] \textbf{\textit{zChaff\_JNI}}: The JNI version of zChaff is
    1.71 -bundled in \texttt{native\-solver.\allowbreak tgz}, which you will find on
    1.72 -Kodkod's web site \cite{kodkod-2009}.
    1.73 +bundled with Kodkodi and is precompiled for the major
    1.74 +platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
    1.75 +which you will find on Kodkod's web site \cite{kodkod-2009}.
    1.76  
    1.77  \item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in
    1.78  \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the