diff -r a3e6f8634a11 -r e08fa125c268 doc-src/manual.bib
--- a/doc-src/manual.bib	Fri Dec 03 18:29:14 2010 +0100
+++ b/doc-src/manual.bib	Fri Dec 03 18:29:49 2010 +0100
@@ -159,6 +159,18 @@
   editor =	 {A. Robinson and A. Voronkov}
 }
 
+@inproceedings{cvc3,
+  author    = {Clark Barrett and Cesare Tinelli},
+  title     = {{CVC3}},
+  booktitle = {CAV},
+  editor    = {Werner Damm and Holger Hermanns},
+  volume    = {4590},
+  series    = LNCS,
+  pages     = {298--302},
+  publisher = {Springer},
+  year      = {2007}
+}
+
 @incollection{basin91,
   author	= {David Basin and Matt Kaufmann},
   title		= {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
@@ -392,6 +404,12 @@
   year		= 1977,
   publisher	= {Oxford University Press}}
 
+@misc{yices,
+  author    = {Bruno Dutertre and Leonardo de Moura},
+  title     = {The {Yices} {SMT} Solver},
+  publisher = "\url{http://yices.csl.sri.com/tool-paper.pdf}",
+  year = 2006}
+
 @incollection{dybjer91,
   author	= {Peter Dybjer},
   title		= {Inductive Sets and Families in {Martin-L{\"o}f's} Type