diff --git a/README.md b/README.md
index 2e5fb83ea..20c8b858f 100644
--- a/README.md
+++ b/README.md
@@ -1,9 +1,10 @@
 JKind
 =====
 
-JKind is a Java implementation of the [KIND model
-checker](http://clc.cs.uiowa.edu/Kind/). KIND is a parallel
-multi-property k-induction model checker for Lustre programs.
+JKind is a Java implementation of the [Kind 2 model
+checker](http://kind2-mc.github.io/kind2/). Kind 2 is a multi-engine
+SMT-based automatic model checker for safety properties of Lustre
+programs.
 
 Downloads
 ---------
@@ -18,12 +19,8 @@ Design Goals
 
 JKind is designed to be cross-platform, reliable, and easy to extend.
 Power and performance are secondary goals. Additionally, JKind
-attempts to be mostly compatible with pkind, the standard
-implementation of KIND. Differences between JKind and pkind are
-described on the
-[wiki](https://github.com/agacek/jkind/wiki/Differences-with-pkind).
-JKind also attempts to be compatible with Kind 2, though this varies
-over time due to developments in both systems.
+attempts to be mostly compatible with pkind and Kind 2, though this
+varies over time due to developments in both systems.
 
 
 Installation Notes
@@ -32,5 +29,7 @@ Installation Notes
 By default, JKind requires [Yices (version
 1)](http://yices.csl.sri.com/download-yices1.shtml) to be installed on
 your PATH. Alternatively, one can use
-[CVC4](http://cvc4.cs.nyu.edu/web/), [Z3](http://z3.codeplex.com/), or
-[Yices 2](http://yices.csl.sri.com/index.shtml).
+[CVC4](http://cvc4.cs.nyu.edu/web/), [Z3](http://z3.codeplex.com/),
+[Yices 2](http://yices.csl.sri.com/index.shtml),
+[MathSAT](http://mathsat.fbk.eu/), or
+[SMTInterpol](http://ultimate.informatik.uni-freiburg.de/smtinterpol/).