diff --git a/doc/architectural/compilation-and-development.md b/doc/architectural/compilation-and-development.md
index 0bce414fd6a..4816d373afa 100644
--- a/doc/architectural/compilation-and-development.md
+++ b/doc/architectural/compilation-and-development.md
@@ -77,6 +77,12 @@ CI, should succeed), `THOROUGH` (takes too long to be run in CI, should
 succeed), `FUTURE` (will succeed when a planned feature is added) or
 `KNOWNBUG` (will succeed when a bug is fixed).
 
+Test descriptions may also include a number of tags. `test.pl -I<tag>` will only
+run tests with a particular `<tag>`, and `test.pl -X<tag>` will run all tests
+except for those with a particular `<tag>`. See
+[regression/README.md](https://github.com/diffblue/cbmc/blob/develop/regression/README.md)
+for the current set of tags and their intended use.
+
 \subsubsection compilation-and-development-subsubsection-running-regression-tests-with-make Running regression tests with make
 
 If you have compiled using `make` then you can run the regression tests
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/lambda_examples/readme.md b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/lambda_examples/README.md
similarity index 100%
rename from jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/lambda_examples/readme.md
rename to jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/lambda_examples/README.md
diff --git a/regression/readme.md b/regression/README.md
similarity index 69%
rename from regression/readme.md
rename to regression/README.md
index 218f51a8763..54baab0cf94 100644
--- a/regression/readme.md
+++ b/regression/README.md
@@ -30,13 +30,6 @@ This folder contains the CProver regression test-suite.
 
 - `winbug`:
   These tests are currently known to be failing on Windows,
-  but passing on other platforms.
-  The reason for this is not known, and it's currently being investigated.
-  This was discovered during work done to port CI from [Travis]
-  and [AWS CodeBuild] to [GitHub Actions].
-  Worth noting that those tests were not being run on Windows before.
-
-
-[AWS CodeBuild]: https://aws.amazon.com/codebuild/
-[GitHub Actions]: https://github.com/features/actions
-[Travis]: https://travis-ci.com/
+  but passing on other platforms. https://github.com/diffblue/cbmc/pull/5572
+  will address one part thereof; the remaining ones are C++ tests that fail on
+  both Windows and MacOS for our lack of C++-11 support.
diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/readme.md b/regression/cbmc-incr-smt2/bitvector-flag-tests/README.md
similarity index 100%
rename from regression/cbmc-incr-smt2/bitvector-flag-tests/readme.md
rename to regression/cbmc-incr-smt2/bitvector-flag-tests/README.md
diff --git a/regression/goto-cc-cbmc-shared-options/readme.md b/regression/goto-cc-cbmc-shared-options/README.md
similarity index 100%
rename from regression/goto-cc-cbmc-shared-options/readme.md
rename to regression/goto-cc-cbmc-shared-options/README.md
diff --git a/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc b/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc
index 77516db1ccb..ac805176c57 100644
--- a/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc
+++ b/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc
@@ -3,9 +3,7 @@ test.c
 --malloc-may-fail --malloc-fail-null
 ^EXIT=10$
 ^SIGNAL=0$
-\[main.assertion.1\] line 7 assertion array != .*: FAILURE
+\[main.assertion.1\] line 7 assertion array != NULL: FAILURE
 --
 --
 Compiling a file with goto-cc should not affect how --malloc-may-fail behaves
-Regex in the assertion because on travis for some reason the preprocessor seems to run
-before cbmc.
diff --git a/regression/symtab2gb-cbmc/readme.md b/regression/symtab2gb-cbmc/README.md
similarity index 100%
rename from regression/symtab2gb-cbmc/readme.md
rename to regression/symtab2gb-cbmc/README.md
diff --git a/regression/symtab2gb/readme.md b/regression/symtab2gb/README.md
similarity index 100%
rename from regression/symtab2gb/readme.md
rename to regression/symtab2gb/README.md
diff --git a/scripts/bash-autocomplete/Readme.md b/scripts/bash-autocomplete/README.md
similarity index 100%
rename from scripts/bash-autocomplete/Readme.md
rename to scripts/bash-autocomplete/README.md