1.1 --- a/doc-src/Nitpick/nitpick.tex	Mon Nov 16 10:03:58 2009 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Mon Nov 16 10:24:28 2009 +0100
     1.3 @@ -2019,9 +2019,11 @@
     1.4  you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
     1.5  version of MiniSat, the JNI version can be used incrementally.
     1.6  
     1.7 +%%% No longer true:
     1.8 +%%% "It is bundled with Kodkodi and requires no further installation or
     1.9 +%%% configuration steps. Alternatively,"
    1.10  \item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
    1.11 -written in C. It is bundled with Kodkodi and requires no further installation or
    1.12 -configuration steps. Alternatively, you can install a standard version of
    1.13 +written in C. You can install a standard version of
    1.14  PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
    1.15  that contains the \texttt{picosat} executable. The C sources for PicoSAT are
    1.16  available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
    1.17 @@ -2078,11 +2080,11 @@
    1.18  \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
    1.19  
    1.20  \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
    1.21 -\textit{smart}, Nitpick selects the first solver among MiniSatJNI, MiniSat,
    1.22 -PicoSAT, zChaffJNI, zChaff, RSat, BerkMin, BerkMinAlloy, and Jerusat that is
    1.23 -recognized by Isabelle. If none is found, it falls back on SAT4J, which should
    1.24 -always be available. If \textit{verbose} is enabled, Nitpick displays which SAT
    1.25 -solver was chosen.
    1.26 +\textit{smart}, Nitpick selects the first solver among MiniSat,
    1.27 +PicoSAT, zChaff, RSat, BerkMin, BerkMinAlloy, Jerusat, MiniSatJNI, and zChaffJNI
    1.28 +that is recognized by Isabelle. If none is found, it falls back on SAT4J, which
    1.29 +should always be available. If \textit{verbose} (\S\ref{output-format}) is
    1.30 +enabled, Nitpick displays which SAT solver was chosen.
    1.31  \end{enum}
    1.32  \fussy
    1.33  
    1.34 @@ -2469,8 +2471,8 @@
    1.35  
    1.36  \item[$\bullet$] Local definitions are not supported and result in an error.
    1.37  
    1.38 -\item[$\bullet$] All constants and types whose names start with
    1.39 -\textit{Nitpick}{.} are reserved for internal use.
    1.40 +%\item[$\bullet$] All constants and types whose names start with
    1.41 +%\textit{Nitpick}{.} are reserved for internal use.
    1.42  \end{enum}
    1.43  
    1.44  \let\em=\sl