Document running 3rd party smt2 solver (with skips)

Author: Joel Allred

regression/smt2_strings/README.md

@@ -7,8 +7,26 @@ backend.
 It can also be used to test the level of string support of any SMT2 solver, by
 using a command such as:
 ```
-../test.pl -p -F -c <path_to_solver_binary>
+../test.pl -p -CKFT -c <path_to_solver_binary>
 ```
 
-(note the `-F` option to consider all tests tagged as "FUTURE").
+(note the `-CKFT` option to consider all testing levels ("CORE", "KNOWNBUG",
+"FUTURE", "THOROUGH"), as these are relevant to CBMC only.
 
+More specifically, tests are tagged according to the expected support by the
+3rd party solver. The commands below will only run the tests where support is
+expected:
+
+CVC4:
+```
+../test.pl -p -CKFT -X cvc4_bug -c <path_to_cvc4_binary>
+```
+Note: Most of the string operations are only supported when cvc4 is passed the
+`--strings-exp` option. For running the tests, suggest creating a script that
+calls cvc4 with `--strings-exp`, and pass the path to that script to the
+command above.
+
+Z3:
+```
+../test.pl -p -CKFT -X z3_bug -c <path_to_z3_binary>
+```