diff --git a/docs/ProgrammingCryptol.pdf b/docs/ProgrammingCryptol.pdf
index 04b3eae91..45190e9af 100644
Binary files a/docs/ProgrammingCryptol.pdf and b/docs/ProgrammingCryptol.pdf differ
diff --git a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
index c727b4a32..92b0ec151 100644
--- a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
+++ b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
@@ -179,30 +179,30 @@ \subsection{Generating test vectors}
 \label{sec:gentestvec}
 
 Cryptol has the ability to generate test vectors for non-polymorphic functions (there is limited support for polymorphic types) using the \texttt{:dumptests} REPL command.
-When \texttt{:dumptests} is given a file to dump the output and a function in scope, it will randomly generate inputs for the function and run them for you.
+The \texttt{:dumptests} command takes a file and an in-scope function; it randomly generates inputs for the function, executes the function on those inputs, and prints the output and inputs to the file.
 \begin{Verbatim}
   :dumptests <results file> <function>
   :dumptests results.txt myFunction
 \end{Verbatim}
-The results file will contain a tab delimited file in which the first column contains the output, and each column after contains the inputs to the function in order.
-You can set the number of tests you want to generate in your test vector by using the \texttt{:set tests=100} command. Additionally, you can also change base using \texttt{:set base=2}.
+The results file will contain a tab delimited table in which the first column contains the output, and each column after contains the inputs to the function in order.
+You can set the number of tests you want to generate in your test vector by using the \texttt{:set tests=100} command. Additionally, you can also change the base used to print to the results file using \texttt{:set base=2}.
 This is because the command \texttt{:dumptests} uses the same settings for random generation that is used in \ref{sec:quickcheck}. 
 The example below shows \texttt{:dumptests} run on an instance of a function polymorphic \texttt{f} which has two inputs. 
 \begin{code}
-  f : {n} (fin n, n >= 2) => [n] -> [n] -> [n]
-  f x y = x + 2 * y 
+  f : {n} (fin n, n >= 2) => [n] -> [n] -> [2 * n] 
+  f x y = x # (2 * y)
 \end{code}
 \begin{Verbatim}
 Cryptol> :set tests = 5
 Cryptol> :set base = 2
-Cryptol> :dumptests result.txt f`{8}
+Cryptol> :dumptests result.txt f`{4}
 Cryptol> :quit
 % cat result.txt 
-0b11011110	0b10010010	0b00100110
-0b10101111	0b01010011	0b00101110
-0b10100001	0b01001001	0b10101100
-0b10111110	0b11101100	0b01101001
-0b00110000	0b11111100	0b10011010
+0b10100000	0b1010	0b0000
+0b10111100	0b1011	0b0110
+0b11111010	0b1111	0b0101
+0b10000010	0b1000	0b1001
+0b00001000	0b0000	0b0100
 \end{Verbatim}