1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Feb 23 08:08:23 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Feb 23 10:02:14 2010 +0100
     1.3 @@ -150,11 +150,11 @@
     1.4  \postw
     1.5  
     1.6  The results presented here were obtained using the JNI version of MiniSat and
     1.7 -with multithreading disabled to reduce nondeterminism. This was done by adding
     1.8 -the line
     1.9 +with multithreading disabled to reduce nondeterminism and a time limit of
    1.10 +15~seconds (instead of 30~seconds). This was done by adding the line
    1.11  
    1.12  \prew
    1.13 -\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
    1.14 +\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\,\textit{timeout} = 15$\,s$]
    1.15  \postw
    1.16  
    1.17  after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
    1.18 @@ -499,7 +499,7 @@
    1.19  
    1.20  \prew
    1.21  \textbf{lemma} ``$P~\textit{Suc}$'' \\
    1.22 -\textbf{nitpick} [\textit{card} = 1--6] \\[2\smallskipamount]
    1.23 +\textbf{nitpick} \\[2\smallskipamount]
    1.24  \slshape
    1.25  Nitpick found no counterexample.
    1.26  \postw
    1.27 @@ -1617,7 +1617,7 @@
    1.28  ``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\
    1.29  ``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\
    1.30  \textbf{nitpick} \\[2\smallskipamount]
    1.31 -\slshape Nitpick found no counterexample.
    1.32 +\slshape Nitpick ran out of time after checking 7 of 8 scopes.
    1.33  \postw
    1.34  
    1.35  \subsection{AA Trees}
    1.36 @@ -1726,7 +1726,7 @@
    1.37  ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
    1.38  ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
    1.39  \textbf{nitpick} \\[2\smallskipamount]
    1.40 -{\slshape Nitpick found no counterexample.}
    1.41 +{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
    1.42  \postw
    1.43  
    1.44  Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree