diff --git a/README.md b/README.md
index 912394b6d..08a532f25 100644
--- a/README.md
+++ b/README.md
@@ -7,7 +7,7 @@ SMACK is both a *modular software verification toolchain* and a
 *self-contained software verifier*. It can be used to verify the assertions
 in its input programs. In its default mode, assertions are verified up to a
 given bound on loop iterations and recursion depth; it contains experimental
-support for unbounded verification as well. SMACK handles complicated feature
+support for unbounded verification as well (REMOVE THIS). SMACK handles complicated feature
 of the C language, including dynamic memory allocation, pointer arithmetic, and
 bitwise operations.
 
diff --git a/docs/running.md b/docs/running.md
index 984d7b47e..be668e6db 100644
--- a/docs/running.md
+++ b/docs/running.md
@@ -3,7 +3,7 @@
 
 SMACK software verifier is run using the `smack` tool in the bin directory.
 For a given input C/C++ program, the tool checks for violations of user-provided
-assertions. SMACK has a number of command line options that can be used
+assertions (MENTION GENERATED ASSERTIONS IN MEMORY SAFETY/OVERFLOW CHECKING). SMACK has a number of command line options that can be used
 to fine-tune the toolchain. Type `smack -h` for a full list of supported command
 line options.
 
@@ -99,6 +99,8 @@ directory. SMACK defines a number of functions (one for each basic type)
 for introducing nondeterministic (i.e., unconstrained) values, such as
 `__VERIFIER_nondet_int` used in this example.
 
+MENTION ASSERT/ASSUME
+
 Simply run the SMACK verifier on your input C file:
 ```Shell
 smack simple.c
@@ -114,5 +116,9 @@ verifier leverages to generate more informative error traces. Then, the generate
 file is translated into Boogie code, which is in turn passed to the chosen back-end
 verifier.
 
+EXAMPLE ON MEMORY SAFETY
+EXAMPLE ON INTEGER OVERFLOW CHECKING
+EXAMPLE ON USING WHOLE-PROGRAM-LLVM
+
 For mode advanced usage scenarios, please refer to our [usage notes](usage-notes.md).