diff --git a/jbmc/unit/java-testing-utils/load_java_class.cpp b/jbmc/unit/java-testing-utils/load_java_class.cpp
index 6288f2cdd7a..e5cd0bf5e4c 100644
--- a/jbmc/unit/java-testing-utils/load_java_class.cpp
+++ b/jbmc/unit/java-testing-utils/load_java_class.cpp
@@ -9,9 +9,9 @@ Author: Diffblue Ltd.
 #include "load_java_class.h"
 
 #include <iostream>
-#include <testing-utils/catch.hpp>
 #include <testing-utils/free_form_cmdline.h>
 #include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 
 #include <util/config.h>
 #include <util/options.h>
diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp
index cc611b0ebf1..aa8d93e513d 100644
--- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp
+++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp
@@ -8,7 +8,7 @@ Author: Diffblue Ltd.
 
 #include "require_goto_statements.h"
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <algorithm>
 #include <util/expr_iterator.h>
diff --git a/jbmc/unit/java-testing-utils/require_parse_tree.h b/jbmc/unit/java-testing-utils/require_parse_tree.h
index 45b37aeb577..1bb1a546e05 100644
--- a/jbmc/unit/java-testing-utils/require_parse_tree.h
+++ b/jbmc/unit/java-testing-utils/require_parse_tree.h
@@ -14,7 +14,7 @@ Author: Diffblue Ltd.
 
 #include <java_bytecode/java_bytecode_parse_tree.h>
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 // NOLINTNEXTLINE(readability/namespace)
 namespace require_parse_tree
diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp
index 75fd11f1cf2..818299aafaa 100644
--- a/jbmc/unit/java-testing-utils/require_type.cpp
+++ b/jbmc/unit/java-testing-utils/require_type.cpp
@@ -8,7 +8,7 @@ Author: Diffblue Ltd.
 
 #include "require_type.h"
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/base_type.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
diff --git a/jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp b/jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp
index 92def24e99f..229eac0f772 100644
--- a/jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp
+++ b/jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp
@@ -6,9 +6,9 @@ Author: Diffblue Limited.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <testing-utils/require_symbol.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "Lazy load lambda methods",
diff --git a/jbmc/unit/java_bytecode/expr2java.cpp b/jbmc/unit/java_bytecode/expr2java.cpp
index df93aa40ead..8329412c708 100644
--- a/jbmc/unit/java_bytecode/expr2java.cpp
+++ b/jbmc/unit/java_bytecode/expr2java.cpp
@@ -6,8 +6,8 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java_bytecode/expr2java.h>
+#include <testing-utils/use_catch.h>
 
 TEST_CASE(
   "expr2java tests",
diff --git a/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_graph.cpp b/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_graph.cpp
index e3f74db7546..13fc2aed898 100644
--- a/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_graph.cpp
+++ b/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_graph.cpp
@@ -6,8 +6,8 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
+#include <testing-utils/use_catch.h>
 
 #include <goto-programs/class_hierarchy.h>
 
diff --git a/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp b/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp
index 003414870a8..00f09c31871 100644
--- a/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp
+++ b/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp
@@ -6,8 +6,8 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
+#include <testing-utils/use_catch.h>
 
 #include <goto-programs/class_hierarchy.h>
 
diff --git a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp
index 6ef5e7d527a..4c15e0976ca 100644
--- a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp
+++ b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp
@@ -7,8 +7,8 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
+#include <testing-utils/use_catch.h>
 
 #include <util/simplify_expr.h>
 #include <goto-programs/remove_virtual_functions.h>
diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp
index 66b58dbd02f..769edb50a13 100644
--- a/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp
+++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp
@@ -5,12 +5,12 @@ Module: Unit tests for instantiating generic superclasses and interfaces.
 Author: Diffblue Ltd.
 
 \*******************************************************************/
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_goto_statements.h>
-#include <util/config.h>
 #include <java-testing-utils/require_type.h>
 #include <testing-utils/require_symbol.h>
+#include <testing-utils/use_catch.h>
+#include <util/config.h>
 
 // NOTE: To inspect these tests at any point, use expr2java.
 // A good way to verify the validity of a test is to iterate
diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp
index fe407a23a55..5d803a770d8 100644
--- a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp
+++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp
@@ -5,12 +5,12 @@ Module: Unit tests for instantiating generic classes.
 Author: Diffblue Ltd.
 
 \*******************************************************************/
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_goto_statements.h>
-#include <util/config.h>
 #include <java-testing-utils/require_type.h>
 #include <testing-utils/require_symbol.h>
+#include <testing-utils/use_catch.h>
+#include <util/config.h>
 
 // NOTE: To inspect these tests at any point, use expr2java.
 // A good way to verify the validity of a test is to iterate
diff --git a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
index f1b1f0b3820..163bbb7ad77 100644
--- a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
+++ b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
@@ -9,7 +9,7 @@ Author: Diffblue Ltd.
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_goto_statements.h>
 #include <java-testing-utils/require_type.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "Generics class with mutually recursive_generic parameters",
diff --git a/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp b/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp
index 10ae09a556c..fe32f90b8bf 100644
--- a/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp
+++ b/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp
@@ -6,8 +6,8 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
+#include <testing-utils/use_catch.h>
 
 #include <algorithm>
 
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp
index 21652ebcefe..b7522944cb1 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp
@@ -6,7 +6,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <istream>
 #include <memory>
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp
index 9ffeb38a94b..f72e0fbc409 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp
@@ -10,7 +10,7 @@ Author: Diffblue Ltd.
 #include <java_bytecode/java_bytecode_convert_class.h>
 #include <java_bytecode/java_bytecode_parse_tree.h>
 #include <java_bytecode/java_types.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "java_bytecode_convert_annotations",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp
index e1359046da6..3ff951bb18d 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp
@@ -6,7 +6,7 @@ Author: Diffblue Limited.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <memory>
 
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp
index c1e9b392f4c..6dbc812870f 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp
@@ -6,15 +6,15 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <goto-programs/class_hierarchy.h>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_goto_statements.h>
-#include <testing-utils/require_expr.h>
 #include <java-testing-utils/require_type.h>
-#include <testing-utils/run_test_with_compilers.h>
+#include <testing-utils/require_expr.h>
 #include <testing-utils/require_symbol.h>
+#include <testing-utils/run_test_with_compilers.h>
+#include <testing-utils/use_catch.h>
 #include <util/expr_iterator.h>
-#include <goto-programs/class_hierarchy.h>
 
 struct lambda_assignment_test_datat
 {
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp
index 603425686d9..b4539c8f0e1 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp
@@ -6,7 +6,7 @@ Author: Diffblue Limited.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/symbol_table.h>
 
diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp
index 80752b41d8c..0211ee72acf 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp
@@ -7,9 +7,9 @@ Author: Diffblue Limited.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
-#include <testing-utils/message.h>
 #include <java-testing-utils/load_java_class.h>
+#include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 
 #include <analyses/local_safe_pointers.h>
 #include <goto-programs/goto_convert_functions.h>
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp
index ca1aebec508..04d6973e69c 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp
@@ -6,9 +6,9 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_bounded_generic_inner_classes",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp
index 58a54521b4a..b0a57720564 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp
@@ -6,9 +6,9 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_derived_generic_class",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp
index 06f49410a9a..425a8abe974 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp
@@ -6,9 +6,9 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_functions_with_generics",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp
index 324acf2b3dd..1e733b6dc79 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp
@@ -6,9 +6,9 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_generic_array_class",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp
index 6310f06b8e2..374e2b34031 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp
@@ -6,9 +6,9 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_generic_class_one_param",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp
index 78b92e45ad8..22cd28c16c8 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp
@@ -6,9 +6,9 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_generic_class_with_generic_inner_classes_fields",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp
index 68fa862d318..13a34cdcaa2 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp
@@ -6,9 +6,9 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_generic_class_with_inner_classes",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp
index 90de48f8e90..c4416f4817f 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp
@@ -6,9 +6,9 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_generic_fields",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp
index 0a944c69c77..134eb3a17d6 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp
@@ -6,9 +6,9 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_generic_functions",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp
index 763aedb8af8..052508f10c8 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp
@@ -8,9 +8,9 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse generic superclass signature",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp
index 2db7851dab7..5b415a1e1b5 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp
@@ -6,8 +6,8 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_generic_wildcard",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_lvtt_generic_local_vars.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_lvtt_generic_local_vars.cpp
index 4d277ab56a0..65d9224b11d 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_lvtt_generic_local_vars.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_lvtt_generic_local_vars.cpp
@@ -8,7 +8,7 @@ Author: Diffblue Ltd.
 
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_lvtt_generic_local_vars",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp
index 97b035a0cc7..05032fab72c 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp
@@ -6,9 +6,9 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_nested_generics_fields",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp
index 3445191e0ea..afc2cfd22b5 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp
@@ -6,8 +6,8 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_recursive_generic_class",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp
index 95bca1fd0ba..c437bb8a807 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp
@@ -6,9 +6,9 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "parse_signature_descriptor_mismatch",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp
index 8f4bfb2a624..0c63e4c4010 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp
@@ -8,10 +8,10 @@ Author: Diffblue Ltd.
 
 #include <algorithm>
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
-#include <testing-utils/run_test_with_compilers.h>
 #include <java-testing-utils/require_type.h>
+#include <testing-utils/run_test_with_compilers.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "Static lambdas in class symbol",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp
index 9ac9effb61a..9857994f76d 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp
@@ -13,8 +13,8 @@ Author: Diffblue Ltd.
 #include <java-testing-utils/require_parse_tree.h>
 
 #include <java_bytecode/java_bytecode_parser.h>
-#include <testing-utils/catch.hpp>
 #include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 
 #include <java_bytecode/java_bytecode_parse_tree.h>
 #include <java_bytecode/java_types.h>
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp
index 24c00bdafba..69841c6bbbe 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp
@@ -12,7 +12,7 @@ Author: Diffblue Ltd.
 #include <testing-utils/message.h>
 #include <util/message.h>
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 static void check_class_structure(
   const java_bytecode_parse_treet::classt &loaded_class)
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp
index ecc1b878fde..5c2032175a2 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp
@@ -6,9 +6,10 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
+#include <testing-utils/use_catch.h>
+
 #include <java-testing-utils/load_java_class.h>
 #include <java_bytecode/java_types.h>
-#include <testing-utils/catch.hpp>
 
 #include <string>
 #include <vector>
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
index 9a6690d8b48..d1ddc46c754 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
@@ -11,9 +11,9 @@ Author: Diffblue Ltd.
 #include <java_bytecode/java_bytecode_convert_class.h>
 #include <java_bytecode/java_bytecode_parse_tree.h>
 #include <java_bytecode/java_types.h>
-#include <testing-utils/catch.hpp>
 #include <testing-utils/free_form_cmdline.h>
 #include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 #include <util/options.h>
 
 class test_java_bytecode_languaget : public java_bytecode_languaget
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp
index dd3c2ab6bc9..7a927171f32 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp
@@ -11,7 +11,7 @@ Author: Diffblue Ltd.
 #include <java_bytecode/java_bytecode_convert_method.h>
 #include <java_bytecode/java_bytecode_parse_tree.h>
 #include <java_bytecode/java_types.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "java_bytecode_parse_attributes",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_class.cpp
index 4ebf03e03db..dc73a645601 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_class.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_class.cpp
@@ -10,7 +10,7 @@ Author: Diffblue Ltd.
 #include <java_bytecode/java_bytecode_convert_class.h>
 #include <java_bytecode/java_bytecode_parse_tree.h>
 #include <java_bytecode/java_types.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "java_bytecode_parse_class",
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_field.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_field.cpp
index 9c8df771f3c..5cc06efc643 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_field.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_field.cpp
@@ -10,7 +10,7 @@ Author: Diffblue Ltd.
 #include <java_bytecode/java_bytecode_convert_class.h>
 #include <java_bytecode/java_bytecode_parse_tree.h>
 #include <java_bytecode/java_types.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "java_bytecode_parse_field",
diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
index 4196c2ed83c..888a37514db 100644
--- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
+++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
@@ -7,16 +7,16 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
-#include <util/expr.h>
-#include <util/std_code.h>
-#include <util/namespace.h>
-#include <java_bytecode/java_object_factory.h>
+#include <iostream>
 #include <java_bytecode/java_bytecode_language.h>
+#include <java_bytecode/java_object_factory.h>
 #include <java_bytecode/java_root_class.h>
 #include <langapi/language_util.h>
 #include <langapi/mode.h>
-#include <iostream>
+#include <testing-utils/use_catch.h>
+#include <util/expr.h>
+#include <util/namespace.h>
+#include <util/std_code.h>
 
 SCENARIO(
   "Generate string object",
diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
index f1042aaabc2..872066ded25 100644
--- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
+++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
@@ -8,8 +8,8 @@ Author: Diffblue Ltd.
 \*******************************************************************/
 
 #include <java-testing-utils/load_java_class.h>
-#include <testing-utils/catch.hpp>
 #include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
diff --git a/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
index 5989553d109..283c81f0c37 100644
--- a/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
+++ b/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
@@ -7,15 +7,15 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
-#include <util/c_types.h>
-#include <util/fresh_symbol.h>
-#include <util/std_code.h>
+#include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_string_library_preprocess.h>
 #include <langapi/language_util.h>
-#include <java_bytecode/java_bytecode_language.h>
-#include <util/namespace.h>
 #include <langapi/mode.h>
+#include <testing-utils/use_catch.h>
+#include <util/c_types.h>
+#include <util/fresh_symbol.h>
+#include <util/namespace.h>
+#include <util/std_code.h>
 
 refined_string_exprt convert_exprt_to_string_exprt_unit_test(
   java_string_library_preprocesst &preprocess,
diff --git a/jbmc/unit/java_bytecode/java_types/erase_type_arguments.cpp b/jbmc/unit/java_bytecode/java_types/erase_type_arguments.cpp
index f4b95bfda86..88efe491516 100644
--- a/jbmc/unit/java_bytecode/java_types/erase_type_arguments.cpp
+++ b/jbmc/unit/java_bytecode/java_types/erase_type_arguments.cpp
@@ -6,8 +6,8 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java_bytecode/java_types.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO("erase_type_arguments", "[core][java_types]")
 {
diff --git a/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp b/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp
index d88add0f23e..4c5e42a06fb 100644
--- a/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp
+++ b/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp
@@ -6,8 +6,8 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java_bytecode/java_types.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO("generic_type_index", "[core][java_types]")
 {
diff --git a/jbmc/unit/java_bytecode/java_types/java_generic_symbol_type.cpp b/jbmc/unit/java_bytecode/java_types/java_generic_symbol_type.cpp
index 4cb751b52f8..a78cfaa266b 100644
--- a/jbmc/unit/java_bytecode/java_types/java_generic_symbol_type.cpp
+++ b/jbmc/unit/java_bytecode/java_types/java_generic_symbol_type.cpp
@@ -6,8 +6,8 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java_bytecode/java_types.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO("java_generic_struct_tag_type", "[core][java_types]")
 {
diff --git a/jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp b/jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp
index 8ff05c906af..0ee79226a39 100644
--- a/jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp
+++ b/jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp
@@ -6,8 +6,8 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <java_bytecode/java_types.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO("java_type_from_string", "[core][java_types]")
 {
diff --git a/jbmc/unit/java_bytecode/java_utils_test.cpp b/jbmc/unit/java_bytecode/java_utils_test.cpp
index b238de43eda..d56a08323fd 100644
--- a/jbmc/unit/java_bytecode/java_utils_test.cpp
+++ b/jbmc/unit/java_bytecode/java_utils_test.cpp
@@ -11,7 +11,7 @@ Author: Diffblue Ltd.
 #include <string>
 #include <vector>
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <java_bytecode/java_types.h>
 #include <java_bytecode/java_utils.h>
diff --git a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp
index f1723fbc9d8..8886d986d69 100644
--- a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp
+++ b/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp
@@ -7,8 +7,8 @@ Author: Diffblue Ltd.
 \*******************************************************************/
 
 #include <java-testing-utils/load_java_class.h>
-#include <testing-utils/catch.hpp>
 #include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
diff --git a/jbmc/unit/java_bytecode/load_method_by_regex.cpp b/jbmc/unit/java_bytecode/load_method_by_regex.cpp
index 53d4140765c..ffc4cb1e600 100644
--- a/jbmc/unit/java_bytecode/load_method_by_regex.cpp
+++ b/jbmc/unit/java_bytecode/load_method_by_regex.cpp
@@ -7,8 +7,8 @@ Author: Diffblue Limited
 \*******************************************************************/
 
 #include <java_bytecode/load_method_by_regex.h>
-#include <testing-utils/catch.hpp>
 #include <testing-utils/require_vectors_equal_unordered.h>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "load_method_by_regex::does_pattern_miss_descriptor",
diff --git a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp
index c4785c8347c..82bb8083d56 100644
--- a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp
+++ b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp
@@ -6,8 +6,8 @@ Author: Chris Smowton, chris@smowton.net
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/initialize_goto_model.h>
diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
index 4a673595f5d..36a450bdac0 100644
--- a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -6,7 +6,7 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_types.h>
diff --git a/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp b/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp
index 4bbf21c5d22..49998dd1bc5 100644
--- a/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp
+++ b/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp
@@ -7,7 +7,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <java_bytecode/java_types.h>
 #include <solvers/strings/string_refinement_util.h>
diff --git a/jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp b/jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp
index 352bd3d4eb9..8b718baf192 100644
--- a/jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp
+++ b/jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp
@@ -7,7 +7,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <solvers/strings/string_refinement.h>
 
diff --git a/jbmc/unit/util/expr_iterator.cpp b/jbmc/unit/util/expr_iterator.cpp
index c45cb325799..b3d37b1f9c0 100644
--- a/jbmc/unit/util/expr_iterator.cpp
+++ b/jbmc/unit/util/expr_iterator.cpp
@@ -2,7 +2,7 @@
 
 /// \file Tests for depth_iteratort and friends
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/expr.h>
 #include <util/expr_iterator.h>
 
diff --git a/jbmc/unit/util/has_subtype.cpp b/jbmc/unit/util/has_subtype.cpp
index 65ebd875c23..45dea2cec76 100644
--- a/jbmc/unit/util/has_subtype.cpp
+++ b/jbmc/unit/util/has_subtype.cpp
@@ -6,7 +6,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/c_types.h>
 #include <util/expr_util.h>
diff --git a/jbmc/unit/util/parameter_indices.cpp b/jbmc/unit/util/parameter_indices.cpp
index 4befc93714b..ed1ab753143 100644
--- a/jbmc/unit/util/parameter_indices.cpp
+++ b/jbmc/unit/util/parameter_indices.cpp
@@ -8,8 +8,8 @@ Author: Diffblue Ltd.
 
 #include <java_bytecode/java_types.h>
 
-#include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
+#include <testing-utils/use_catch.h>
 
 void check_consistency(const symbolt &symbol)
 {
diff --git a/jbmc/unit/util/simplify_expr.cpp b/jbmc/unit/util/simplify_expr.cpp
index c3c963d8012..4d2cebe0907 100644
--- a/jbmc/unit/util/simplify_expr.cpp
+++ b/jbmc/unit/util/simplify_expr.cpp
@@ -6,7 +6,7 @@ Author: Michael Tautschnig
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <java_bytecode/java_types.h>
 #include <util/config.h>
diff --git a/unit/analyses/ai/ai.cpp b/unit/analyses/ai/ai.cpp
index 109fe50616f..58cfa0ccac3 100644
--- a/unit/analyses/ai/ai.cpp
+++ b/unit/analyses/ai/ai.cpp
@@ -9,8 +9,8 @@ Author: Diffblue Ltd.
 /// \file
 /// Unit tests for ait
 
-#include <testing-utils/catch.hpp>
 #include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 
 #include <analyses/ai.h>
 
diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp
index 6b4442174c5..bb081a6523a 100644
--- a/unit/analyses/ai/ai_simplify_lhs.cpp
+++ b/unit/analyses/ai/ai_simplify_lhs.cpp
@@ -9,8 +9,8 @@ Author: Diffblue Ltd.
 /// \file
 /// Unit tests for ai_domain_baset::ai_simplify_lhs
 
-#include <testing-utils/catch.hpp>
 #include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 
 #include <analyses/ai.h>
 
diff --git a/unit/analyses/call_graph.cpp b/unit/analyses/call_graph.cpp
index d893c7e8ab4..65dcfa9ac31 100644
--- a/unit/analyses/call_graph.cpp
+++ b/unit/analyses/call_graph.cpp
@@ -9,7 +9,7 @@ Module: Unit test for call graph generation
 #include <iostream>
 
 #include <testing-utils/call_graph_test_utils.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <analyses/call_graph.h>
 #include <analyses/call_graph_helpers.h>
diff --git a/unit/analyses/constant_propagator.cpp b/unit/analyses/constant_propagator.cpp
index 46972e42974..59a2411bb6d 100644
--- a/unit/analyses/constant_propagator.cpp
+++ b/unit/analyses/constant_propagator.cpp
@@ -6,8 +6,8 @@ Author: Diffblue Ltd
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 
 #include <analyses/constant_propagator.h>
 
diff --git a/unit/analyses/dependence_graph.cpp b/unit/analyses/dependence_graph.cpp
index d8cbcd0cc4e..6a673d8ed9c 100644
--- a/unit/analyses/dependence_graph.cpp
+++ b/unit/analyses/dependence_graph.cpp
@@ -13,7 +13,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #include <goto-programs/goto_convert_functions.h>
 #include <langapi/mode.h>
 #include <testing-utils/call_graph_test_utils.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/std_code.h>
diff --git a/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp b/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp
index 195280f6ac7..0411200ffac 100644
--- a/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp
+++ b/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp
@@ -9,7 +9,7 @@ Module: Unit test for graph class functions
 #include <iostream>
 
 #include <testing-utils/call_graph_test_utils.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <analyses/call_graph_helpers.h>
 
diff --git a/unit/analyses/does_remove_const/does_expr_lose_const.cpp b/unit/analyses/does_remove_const/does_expr_lose_const.cpp
index 09f1a62e280..cf21ef0cf3c 100644
--- a/unit/analyses/does_remove_const/does_expr_lose_const.cpp
+++ b/unit/analyses/does_remove_const/does_expr_lose_const.cpp
@@ -9,7 +9,7 @@ Author: Diffblue Ltd.
 /// \file
 /// Does Remove Const Unit Tests
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/std_expr.h>
 #include <util/std_code.h>
diff --git a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp
index e74392b4da0..4b6c6c3e028 100644
--- a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp
+++ b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp
@@ -9,7 +9,7 @@ Author: Diffblue Ltd.
 /// \file
 /// Does Remove Const Unit Tests
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/c_types.h>
 #include <util/namespace.h>
diff --git a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp
index ebb51e92fc9..2e54032bd21 100644
--- a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp
+++ b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp
@@ -9,7 +9,7 @@ Author: Diffblue Ltd.
 /// \file
 /// Does Remove Const Unit Tests
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/c_types.h>
 #include <util/namespace.h>
diff --git a/unit/big-int/big-int.cpp b/unit/big-int/big-int.cpp
index 580fdc2b871..7220484a2ba 100644
--- a/unit/big-int/big-int.cpp
+++ b/unit/big-int/big-int.cpp
@@ -6,7 +6,7 @@ Author: Daniel Kroening
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <string>
 
diff --git a/unit/catch/CMakeLists.txt b/unit/catch/CMakeLists.txt
new file mode 100644
index 00000000000..d9113dc9290
--- /dev/null
+++ b/unit/catch/CMakeLists.txt
@@ -0,0 +1,4 @@
+target_include_directories(catch
+    PUBLIC
+    ${CMAKE_CURRENT_SOURCE_DIR}/..
+)
diff --git a/unit/testing-utils/catch.hpp b/unit/catch/catch.hpp
similarity index 99%
rename from unit/testing-utils/catch.hpp
rename to unit/catch/catch.hpp
index fa9110ca0ce..7c54383bf4e 100644
--- a/unit/testing-utils/catch.hpp
+++ b/unit/catch/catch.hpp
@@ -8,6 +8,14 @@
  *  Distributed under the Boost Software License, Version 1.0. (See accompanying
  *  file LICENSE_1_0.txt or copy at http://www.boost.org/LICENSE_1_0.txt)
  */
+
+#ifndef INCLUDED_VIA_USE_CATCH_H
+#error Do not include this file directly, use use_catch.h instead
+#endif
+
+// this is imported code, don't impose formatting rules
+// clang-format off
+
 #ifndef TWOBLUECUBES_SINGLE_INCLUDE_CATCH_HPP_INCLUDED
 #define TWOBLUECUBES_SINGLE_INCLUDE_CATCH_HPP_INCLUDED
 
@@ -11418,3 +11426,4 @@ using Catch::Detail::Approx;
 
 #endif // TWOBLUECUBES_SINGLE_INCLUDE_CATCH_HPP_INCLUDED
 
+// clang-format on
diff --git a/unit/compound_block_locations.cpp b/unit/compound_block_locations.cpp
index 2e9d2f9be0a..1b1ce3e8e12 100644
--- a/unit/compound_block_locations.cpp
+++ b/unit/compound_block_locations.cpp
@@ -8,7 +8,7 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>, 2018
 
 #include "compound_block_locations.h"
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <fstream>
 #include <utility>
diff --git a/unit/goto-programs/goto_model_function_type_consistency.cpp b/unit/goto-programs/goto_model_function_type_consistency.cpp
index c426d139d9d..e5ee11fd696 100644
--- a/unit/goto-programs/goto_model_function_type_consistency.cpp
+++ b/unit/goto-programs/goto_model_function_type_consistency.cpp
@@ -6,10 +6,12 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <goto-programs/goto_model.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
+
 #include <util/arith_tools.h>
 
+#include <goto-programs/goto_model.h>
+
 SCENARIO(
   "Validation of consistent program/table pair (function type)",
   "[core][goto-programs][validate]")
diff --git a/unit/goto-programs/goto_program_assume.cpp b/unit/goto-programs/goto_program_assume.cpp
index 068621fd6a3..aa4ef524fd8 100644
--- a/unit/goto-programs/goto_program_assume.cpp
+++ b/unit/goto-programs/goto_program_assume.cpp
@@ -6,10 +6,12 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <goto-programs/goto_function.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
+
 #include <util/arith_tools.h>
 
+#include <goto-programs/goto_function.h>
+
 SCENARIO(
   "Validation of well-formed assert/assume codes",
   "[core][goto-programs][validate]")
diff --git a/unit/goto-programs/goto_program_dead.cpp b/unit/goto-programs/goto_program_dead.cpp
index d5ce994675c..b57ad6ca7c6 100644
--- a/unit/goto-programs/goto_program_dead.cpp
+++ b/unit/goto-programs/goto_program_dead.cpp
@@ -6,10 +6,12 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <goto-programs/goto_function.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
+
 #include <util/arith_tools.h>
 
+#include <goto-programs/goto_function.h>
+
 SCENARIO(
   "Validation of well-formed symbol removing codes",
   "[core][goto-programs][validate]")
diff --git a/unit/goto-programs/goto_program_declaration.cpp b/unit/goto-programs/goto_program_declaration.cpp
index d7bb25c3fe4..e273ffd3129 100644
--- a/unit/goto-programs/goto_program_declaration.cpp
+++ b/unit/goto-programs/goto_program_declaration.cpp
@@ -6,8 +6,10 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
+#include <testing-utils/use_catch.h>
+
 #include <goto-programs/goto_function.h>
-#include <testing-utils/catch.hpp>
+
 #include <util/arith_tools.h>
 
 SCENARIO(
diff --git a/unit/goto-programs/goto_program_function_call.cpp b/unit/goto-programs/goto_program_function_call.cpp
index ea1d5c40de0..3407fc0f069 100644
--- a/unit/goto-programs/goto_program_function_call.cpp
+++ b/unit/goto-programs/goto_program_function_call.cpp
@@ -6,10 +6,12 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <goto-programs/goto_function.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
+
 #include <util/arith_tools.h>
 
+#include <goto-programs/goto_function.h>
+
 SCENARIO(
   "Validation of well-formed function call codes",
   "[core][goto-programs][validate]")
diff --git a/unit/goto-programs/goto_program_goto_target.cpp b/unit/goto-programs/goto_program_goto_target.cpp
index 7078ff32846..bc0349fe200 100644
--- a/unit/goto-programs/goto_program_goto_target.cpp
+++ b/unit/goto-programs/goto_program_goto_target.cpp
@@ -6,10 +6,12 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <goto-programs/goto_function.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
+
 #include <util/arith_tools.h>
 
+#include <goto-programs/goto_function.h>
+
 SCENARIO(
   "Validation of well-formed goto codes",
   "[core][goto-programs][validate]")
diff --git a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp
index 58d84d5194c..07090357cfd 100644
--- a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp
+++ b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp
@@ -6,10 +6,12 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <goto-programs/goto_function.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
+
 #include <util/arith_tools.h>
 
+#include <goto-programs/goto_function.h>
+
 SCENARIO(
   "Validation of consistent program/table pair (type-wise)",
   "[core][goto-programs][validate]")
diff --git a/unit/goto-programs/goto_program_table_consistency.cpp b/unit/goto-programs/goto_program_table_consistency.cpp
index 73907d027f1..d33ea824671 100644
--- a/unit/goto-programs/goto_program_table_consistency.cpp
+++ b/unit/goto-programs/goto_program_table_consistency.cpp
@@ -6,10 +6,12 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <goto-programs/goto_function.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
+
 #include <util/arith_tools.h>
 
+#include <goto-programs/goto_function.h>
+
 SCENARIO(
   "Validation of consistent program/table pair",
   "[core][goto-programs][validate]")
diff --git a/unit/goto-programs/goto_trace_output.cpp b/unit/goto-programs/goto_trace_output.cpp
index afd0c21d5fd..5e7604ad19f 100644
--- a/unit/goto-programs/goto_trace_output.cpp
+++ b/unit/goto-programs/goto_trace_output.cpp
@@ -6,10 +6,10 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
 #include <goto-programs/goto_program.h>
 #include <goto-programs/goto_trace.h>
 #include <sstream>
+#include <testing-utils/use_catch.h>
 
 SCENARIO(
   "Output trace with nil lhs object",
diff --git a/unit/goto-programs/xml_expr.cpp b/unit/goto-programs/xml_expr.cpp
index 67a41648d14..0f531f6f352 100644
--- a/unit/goto-programs/xml_expr.cpp
+++ b/unit/goto-programs/xml_expr.cpp
@@ -6,7 +6,7 @@ Author: Michael Tautschnig
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/arith_tools.h>
 #include <util/config.h>
diff --git a/unit/goto-symex/ssa_equation.cpp b/unit/goto-symex/ssa_equation.cpp
index 9bfe4bc7c12..3c387d43395 100644
--- a/unit/goto-symex/ssa_equation.cpp
+++ b/unit/goto-symex/ssa_equation.cpp
@@ -6,10 +6,12 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <goto-symex/symex_target_equation.h>
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
+
 #include <util/arith_tools.h>
 
+#include <goto-symex/symex_target_equation.h>
+
 SCENARIO("Validation of well-formed SSA steps", "[core][goto-symex][validate]")
 {
   GIVEN("A program with one function return")
diff --git a/unit/interpreter/interpreter.cpp b/unit/interpreter/interpreter.cpp
index bba0341b933..6e125acbebb 100644
--- a/unit/interpreter/interpreter.cpp
+++ b/unit/interpreter/interpreter.cpp
@@ -6,7 +6,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/interpreter_class.h>
diff --git a/unit/json/json_parser.cpp b/unit/json/json_parser.cpp
index 6c89b52286a..d91828a3dfe 100644
--- a/unit/json/json_parser.cpp
+++ b/unit/json/json_parser.cpp
@@ -8,8 +8,8 @@ Author: Diffblue Ltd.
 
 #include <fstream>
 #include <json/json_parser.h>
-#include <testing-utils/catch.hpp>
 #include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 #include <util/tempfile.h>
 
 SCENARIO("Loading JSON files")
diff --git a/unit/json_symbol_table.cpp b/unit/json_symbol_table.cpp
index 5163a65dc3f..6a5ba528aee 100644
--- a/unit/json_symbol_table.cpp
+++ b/unit/json_symbol_table.cpp
@@ -23,8 +23,8 @@
 #include <util/options.h>
 #include <util/symbol_table.h>
 
-#include <testing-utils/catch.hpp>
 #include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 
 #include <iosfwd>
 
diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp
index 37582b2e610..3c37bdc60c0 100644
--- a/unit/path_strategies.cpp
+++ b/unit/path_strategies.cpp
@@ -6,7 +6,7 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>, 2018
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <path_strategies.h>
 
diff --git a/unit/pointer-analysis/value_set.cpp b/unit/pointer-analysis/value_set.cpp
index 8926205f956..36d684e65cd 100644
--- a/unit/pointer-analysis/value_set.cpp
+++ b/unit/pointer-analysis/value_set.cpp
@@ -9,7 +9,7 @@ Author: Diffblue Ltd.
 /// \file
 /// Unit tests for value_sett
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <pointer-analysis/value_set.h>
 #include <util/arith_tools.h>
diff --git a/unit/solvers/floatbv/float_utils.cpp b/unit/solvers/floatbv/float_utils.cpp
index aec2b35eb5a..be7bbf4bea9 100644
--- a/unit/solvers/floatbv/float_utils.cpp
+++ b/unit/solvers/floatbv/float_utils.cpp
@@ -6,7 +6,7 @@ Author: Daniel Kroening
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 // for debug output in case of failure
 #include <iostream>
diff --git a/unit/solvers/miniBDD/miniBDD.cpp b/unit/solvers/miniBDD/miniBDD.cpp
index 6bd48326dbe..0d1d7df143f 100644
--- a/unit/solvers/miniBDD/miniBDD.cpp
+++ b/unit/solvers/miniBDD/miniBDD.cpp
@@ -9,7 +9,7 @@ Author: Diffblue Ltd.
 /// \file
 /// Unit tests for miniBDD
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <solvers/flattening/boolbv.h>
 #include <solvers/miniBDD/miniBDD.h>
diff --git a/unit/solvers/strings/array_pool/array_pool.cpp b/unit/solvers/strings/array_pool/array_pool.cpp
index bb6a286cd68..3b938682c63 100644
--- a/unit/solvers/strings/array_pool/array_pool.cpp
+++ b/unit/solvers/strings/array_pool/array_pool.cpp
@@ -7,7 +7,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <solvers/strings/string_constraint_generator.h>
 
diff --git a/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp b/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp
index fd93101a534..ef0d3dcfeaa 100644
--- a/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp
+++ b/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp
@@ -7,7 +7,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <solvers/strings/string_constraint_generator.h>
 #include <util/std_types.h>
diff --git a/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp b/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp
index faf2a032a33..de145800006 100644
--- a/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp
+++ b/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp
@@ -7,7 +7,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <solvers/strings/string_constraint_generator.h>
 
diff --git a/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp b/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp
index 42d5db8d4fa..3edd7886b8c 100644
--- a/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp
+++ b/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp
@@ -7,7 +7,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <solvers/strings/string_constraint_generator.h>
 
diff --git a/unit/solvers/strings/string_refinement/concretize_array.cpp b/unit/solvers/strings/string_refinement/concretize_array.cpp
index 0d7f27b615a..216a5c42c36 100644
--- a/unit/solvers/strings/string_refinement/concretize_array.cpp
+++ b/unit/solvers/strings/string_refinement/concretize_array.cpp
@@ -7,7 +7,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
diff --git a/unit/solvers/strings/string_refinement/sparse_array.cpp b/unit/solvers/strings/string_refinement/sparse_array.cpp
index fd460e104ec..9c5088c56db 100644
--- a/unit/solvers/strings/string_refinement/sparse_array.cpp
+++ b/unit/solvers/strings/string_refinement/sparse_array.cpp
@@ -7,7 +7,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <solvers/strings/string_refinement.h>
 
diff --git a/unit/solvers/strings/string_refinement/substitute_array_list.cpp b/unit/solvers/strings/string_refinement/substitute_array_list.cpp
index aa98a14f73a..8d7e91b291b 100644
--- a/unit/solvers/strings/string_refinement/substitute_array_list.cpp
+++ b/unit/solvers/strings/string_refinement/substitute_array_list.cpp
@@ -7,7 +7,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <iostream>
 #include <solvers/strings/string_refinement.h>
diff --git a/unit/solvers/strings/string_refinement/union_find_replace.cpp b/unit/solvers/strings/string_refinement/union_find_replace.cpp
index 564ec973bcf..8c5b93b6e39 100644
--- a/unit/solvers/strings/string_refinement/union_find_replace.cpp
+++ b/unit/solvers/strings/string_refinement/union_find_replace.cpp
@@ -7,7 +7,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <solvers/strings/string_refinement.h>
 
diff --git a/unit/testing-utils/module_dependencies.txt b/unit/testing-utils/module_dependencies.txt
index dc09d4d3f95..636163352dd 100644
--- a/unit/testing-utils/module_dependencies.txt
+++ b/unit/testing-utils/module_dependencies.txt
@@ -1,4 +1,5 @@
 ansi-c
+catch
 testing-utils
 util
 analyses
diff --git a/unit/testing-utils/require_expr.cpp b/unit/testing-utils/require_expr.cpp
index 04e06d8943f..2147aeed587 100644
--- a/unit/testing-utils/require_expr.cpp
+++ b/unit/testing-utils/require_expr.cpp
@@ -14,7 +14,7 @@ Author: Diffblue Ltd.
 
 #include "require_expr.h"
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/arith_tools.h>
 #include <util/std_code.h>
 
diff --git a/unit/testing-utils/require_symbol.cpp b/unit/testing-utils/require_symbol.cpp
index 9b727853af8..c9659a99153 100644
--- a/unit/testing-utils/require_symbol.cpp
+++ b/unit/testing-utils/require_symbol.cpp
@@ -7,7 +7,7 @@ Author: Diffblue Limited.
 \*******************************************************************/
 
 #include "require_symbol.h"
-#include "catch.hpp"
+#include "use_catch.h"
 
 /// Verify whether a given identifier is found in the symbol table and return it
 /// \param symbol_table: The symbol table to look in
diff --git a/unit/testing-utils/require_vectors_equal_unordered.h b/unit/testing-utils/require_vectors_equal_unordered.h
index 87fa47b9801..7032930fbbe 100644
--- a/unit/testing-utils/require_vectors_equal_unordered.h
+++ b/unit/testing-utils/require_vectors_equal_unordered.h
@@ -9,7 +9,7 @@ Author: Diffblue Limited.
 #ifndef CPROVER_TESTING_UTILS_REQUIRE_VECTORS_EQUAL_UNORDERED_H
 #define CPROVER_TESTING_UTILS_REQUIRE_VECTORS_EQUAL_UNORDERED_H
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <vector>
 
 /// Checks whether two vectors are equal, ignoring ordering
diff --git a/unit/testing-utils/use_catch.h b/unit/testing-utils/use_catch.h
new file mode 100644
index 00000000000..4055b62a8c3
--- /dev/null
+++ b/unit/testing-utils/use_catch.h
@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module: Wrapper around CATCH to disable selected compiler warnings
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#ifndef CPROVER_TESTING_UTILS_USE_CATCH_H
+#define CPROVER_TESTING_UTILS_USE_CATCH_H
+
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable : 4061)
+// enumerator not explicitly handled by case label
+#pragma warning(disable : 4388)
+// signed/unsigned mismatch
+#pragma warning(disable : 4668)
+// using #if/#elif on undefined macro
+#pragma warning(disable : 4628)
+// digraphs not supported with -Ze
+#pragma warning(disable : 4583)
+// destructor is not implicitly called
+#pragma warning(disable : 4868)
+// compiler may not enforce left-to-right evaluation order in braced initializer
+// list
+#pragma warning(disable : 4365)
+// signed/unsigned mismatch
+#endif
+
+#define INCLUDED_VIA_USE_CATCH_H
+
+#include <catch/catch.hpp>
+
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
+
+#endif // CPROVER_TESTING_UTILS_USE_CATCH_H
diff --git a/unit/unit_tests.cpp b/unit/unit_tests.cpp
index 45c3dd1a1e6..ed75b917507 100644
--- a/unit/unit_tests.cpp
+++ b/unit/unit_tests.cpp
@@ -7,7 +7,7 @@ Author: Diffblue Ltd.
 \*******************************************************************/
 
 #define CATCH_CONFIG_MAIN
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/irep.h>
 
 // Debug printer for irept
diff --git a/unit/util/cmdline.cpp b/unit/util/cmdline.cpp
index 90d5a8ab4b1..633f45eac4b 100644
--- a/unit/util/cmdline.cpp
+++ b/unit/util/cmdline.cpp
@@ -6,7 +6,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/cmdline.h>
 
 TEST_CASE("cmdlinet::has_option", "[core][util][cmdline]")
diff --git a/unit/util/expr.cpp b/unit/util/expr.cpp
index 2f6d172fa70..39b49a639b8 100644
--- a/unit/util/expr.cpp
+++ b/unit/util/expr.cpp
@@ -6,7 +6,7 @@ Author: Diffblue Ltd
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/arith_tools.h>
 #include <util/expr.h>
diff --git a/unit/util/expr_cast/expr_cast.cpp b/unit/util/expr_cast/expr_cast.cpp
index 0f88b4936f4..031d3d7325b 100644
--- a/unit/util/expr_cast/expr_cast.cpp
+++ b/unit/util/expr_cast/expr_cast.cpp
@@ -9,12 +9,11 @@ Author: Nathan Phillips <Nathan.Phillips@diffblue.com>
 /// \file
 /// expr_dynamic_cast Unit Tests
 
-#include <testing-utils/catch.hpp>
-#include <util/std_expr.h>
+#include <testing-utils/use_catch.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
 #include <util/std_types.h>
 
-
 SCENARIO("expr_dynamic_cast",
   "[core][utils][expr_cast][expr_dynamic_cast]")
 {
diff --git a/unit/util/expr_cast/expr_undefined_casts.cpp b/unit/util/expr_cast/expr_undefined_casts.cpp
index ebc215d0ce0..4974f16aede 100644
--- a/unit/util/expr_cast/expr_undefined_casts.cpp
+++ b/unit/util/expr_cast/expr_undefined_casts.cpp
@@ -12,12 +12,11 @@ Author: Nathan Phillips <Nathan.Phillips@diffblue.com>
 // This could have a unit test that consisted of trying to compile the file
 // and checking that the compiler gave the right error messages.
 
-#include <catch.hpp>
-#include <util/std_expr.h>
+#include <testing-utils/use_catch.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
 #include <util/std_types.h>
 
-
 SCENARIO("expr_dynamic_cast",
   "[core][utils][expr_cast][expr_dynamic_cast]")
 {
diff --git a/unit/util/file_util.cpp b/unit/util/file_util.cpp
index 897c2a47db0..102ad69ce3e 100644
--- a/unit/util/file_util.cpp
+++ b/unit/util/file_util.cpp
@@ -6,7 +6,7 @@ Author: Daniel Kroening
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/exception_utils.h>
 #include <util/file_util.h>
diff --git a/unit/util/format_number_range.cpp b/unit/util/format_number_range.cpp
index 7268d8a4685..22cf1465611 100644
--- a/unit/util/format_number_range.cpp
+++ b/unit/util/format_number_range.cpp
@@ -6,7 +6,7 @@ Author: Michael Tautschnig
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/format_number_range.h>
 
diff --git a/unit/util/get_base_name.cpp b/unit/util/get_base_name.cpp
index 43c40c3c03c..71552bdd914 100644
--- a/unit/util/get_base_name.cpp
+++ b/unit/util/get_base_name.cpp
@@ -6,7 +6,7 @@ Author: Daniel Kroening
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/get_base_name.h>
 
diff --git a/unit/util/graph.cpp b/unit/util/graph.cpp
index 25ac3bf020b..aef27d2250b 100644
--- a/unit/util/graph.cpp
+++ b/unit/util/graph.cpp
@@ -6,7 +6,7 @@ Author: Diffblue Ltd
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/graph.h>
 
diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp
index e5ac9c61b30..9e3dfcd8aa0 100644
--- a/unit/util/irep.cpp
+++ b/unit/util/irep.cpp
@@ -2,7 +2,7 @@
 
 /// \file Tests that irept memory consumption is fixed
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/irep.h>
 
 SCENARIO("irept_memory", "[core][utils][irept]")
diff --git a/unit/util/irep_sharing.cpp b/unit/util/irep_sharing.cpp
index 8d92f66855c..7f4b8f47681 100644
--- a/unit/util/irep_sharing.cpp
+++ b/unit/util/irep_sharing.cpp
@@ -2,7 +2,7 @@
 
 /// \file Tests that irep sharing works correctly
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/irep.h>
 
 #ifdef SHARING
diff --git a/unit/util/json_object.cpp b/unit/util/json_object.cpp
index 7307b795278..9ea4c393207 100644
--- a/unit/util/json_object.cpp
+++ b/unit/util/json_object.cpp
@@ -6,7 +6,8 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
+
 #include <util/json.h>
 #include <util/optional.h>
 #include <util/optional_utils.h>
diff --git a/unit/util/memory_info.cpp b/unit/util/memory_info.cpp
index 0b3cd067732..df7c82a742d 100644
--- a/unit/util/memory_info.cpp
+++ b/unit/util/memory_info.cpp
@@ -6,7 +6,7 @@ Author: Michael Tautschnig
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/memory_info.h>
 
diff --git a/unit/util/message.cpp b/unit/util/message.cpp
index 0e287576b0e..520515555fb 100644
--- a/unit/util/message.cpp
+++ b/unit/util/message.cpp
@@ -6,10 +6,10 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
-#include <util/message.h>
 #include <sstream>
 #include <string.h>
+#include <testing-utils/use_catch.h>
+#include <util/message.h>
 
 TEST_CASE("Copy a messaget")
 {
diff --git a/unit/util/optional.cpp b/unit/util/optional.cpp
index de0b0cbca14..bbaf6c6a97e 100644
--- a/unit/util/optional.cpp
+++ b/unit/util/optional.cpp
@@ -6,7 +6,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/optional.h>
 
 TEST_CASE("Optional without a value", "[core][util][optional]")
diff --git a/unit/util/optional_utils.cpp b/unit/util/optional_utils.cpp
index 80e3428bb59..cbe306fbe9f 100644
--- a/unit/util/optional_utils.cpp
+++ b/unit/util/optional_utils.cpp
@@ -6,7 +6,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/optional_utils.h>
 
diff --git a/unit/util/pointer_offset_size.cpp b/unit/util/pointer_offset_size.cpp
index 186a07864cc..98621681667 100644
--- a/unit/util/pointer_offset_size.cpp
+++ b/unit/util/pointer_offset_size.cpp
@@ -6,7 +6,7 @@ Author: Michael Tautschnig
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
diff --git a/unit/util/range.cpp b/unit/util/range.cpp
index f8bc6d7c299..2483071beea 100644
--- a/unit/util/range.cpp
+++ b/unit/util/range.cpp
@@ -8,7 +8,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 #include <vector>
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/range.h>
 
 /// Trivial example template function requiring a container to have a
diff --git a/unit/util/replace_symbol.cpp b/unit/util/replace_symbol.cpp
index 6e7523c4fbb..7dec445f130 100644
--- a/unit/util/replace_symbol.cpp
+++ b/unit/util/replace_symbol.cpp
@@ -6,7 +6,7 @@ Author: Michael Tautschnig
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/replace_symbol.h>
 #include <util/std_expr.h>
diff --git a/unit/util/sharing_map.cpp b/unit/util/sharing_map.cpp
index e1bfda93e0b..907aa9aa9e0 100644
--- a/unit/util/sharing_map.cpp
+++ b/unit/util/sharing_map.cpp
@@ -13,7 +13,7 @@ Author: Daniel Poetzl
 #include <random>
 #include <set>
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/sharing_map.h>
 
 class smt : public sharing_mapt<irep_idt, std::string, irep_id_hash>
diff --git a/unit/util/sharing_node.cpp b/unit/util/sharing_node.cpp
index 7a5e81d9e42..2626ccf5fb0 100644
--- a/unit/util/sharing_node.cpp
+++ b/unit/util/sharing_node.cpp
@@ -4,7 +4,7 @@
 
 #define SN_INTERNAL_CHECKS
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/sharing_node.h>
 
 void sharing_node_test()
diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index e77c4997729..1c0ab7b035c 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -6,7 +6,7 @@ Author: Michael Tautschnig
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
diff --git a/unit/util/small_map.cpp b/unit/util/small_map.cpp
index eabcfb107f8..cdb69bb98b8 100644
--- a/unit/util/small_map.cpp
+++ b/unit/util/small_map.cpp
@@ -2,7 +2,7 @@
 
 /// \file Tests for small map
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/small_map.h>
 
 // This method is a friend of small_map
diff --git a/unit/util/small_shared_two_way_ptr.cpp b/unit/util/small_shared_two_way_ptr.cpp
index 7ca44c94e2c..efdf3f62106 100644
--- a/unit/util/small_shared_two_way_ptr.cpp
+++ b/unit/util/small_shared_two_way_ptr.cpp
@@ -2,8 +2,8 @@
 
 /// \file Tests for small shared two-way pointer
 
+#include <testing-utils/use_catch.h>
 #include <util/small_shared_two_way_ptr.h>
-#include <testing-utils/catch.hpp>
 
 class d1t : public small_shared_two_way_pointeet<unsigned>
 {
diff --git a/unit/util/std_expr.cpp b/unit/util/std_expr.cpp
index 52679b8533e..359bc53d8c9 100644
--- a/unit/util/std_expr.cpp
+++ b/unit/util/std_expr.cpp
@@ -6,7 +6,7 @@ Author: Diffblue Ltd
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
diff --git a/unit/util/string_utils/split_string.cpp b/unit/util/string_utils/split_string.cpp
index 11ada1444cb..bc7ef28cf95 100644
--- a/unit/util/string_utils/split_string.cpp
+++ b/unit/util/string_utils/split_string.cpp
@@ -9,7 +9,7 @@ Author: Diffblue Ltd.
 /// \file
 /// split_string Unit Tests
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/string_utils.h>
 
 struct expected_resultst
diff --git a/unit/util/string_utils/strip_string.cpp b/unit/util/string_utils/strip_string.cpp
index 31ba6a1912d..6a414ea174e 100644
--- a/unit/util/string_utils/strip_string.cpp
+++ b/unit/util/string_utils/strip_string.cpp
@@ -9,7 +9,7 @@ Author: Diffblue Ltd.
 /// \file
 /// strip_string Unit Tests
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/string_utils.h>
 
 SCENARIO("strip_string", "[core][utils][string_utils][strip_string]")
diff --git a/unit/util/symbol.cpp b/unit/util/symbol.cpp
index 8ea897506bb..6ed1baf152a 100644
--- a/unit/util/symbol.cpp
+++ b/unit/util/symbol.cpp
@@ -8,7 +8,8 @@ Author: Diffblue Ltd.
 
 /// \file Tests for symbol_tablet
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
+
 #include <util/exception_utils.h>
 #include <util/symbol.h>
 
diff --git a/unit/util/symbol_table.cpp b/unit/util/symbol_table.cpp
index 260dc460603..e8f984bb753 100644
--- a/unit/util/symbol_table.cpp
+++ b/unit/util/symbol_table.cpp
@@ -2,7 +2,7 @@
 
 /// \file Tests for symbol_tablet
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 #include <util/exception_utils.h>
 #include <util/journalling_symbol_table.h>
 
diff --git a/unit/util/unicode.cpp b/unit/util/unicode.cpp
index ff4901f2e45..5e2349eaa59 100644
--- a/unit/util/unicode.cpp
+++ b/unit/util/unicode.cpp
@@ -6,7 +6,7 @@ Author: Vojtech Forejt, forejtv@diffblue.com
 
 \*******************************************************************/
 
-#include <testing-utils/catch.hpp>
+#include <testing-utils/use_catch.h>
 
 #include <vector>
 #include <string>