diff --git a/src/aa-symex/symex_parseoptions.cpp b/src/aa-symex/symex_parseoptions.cpp
index a83ce22223f..e9099b1d568 100644
--- a/src/aa-symex/symex_parseoptions.cpp
+++ b/src/aa-symex/symex_parseoptions.cpp
@@ -28,8 +28,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/xml_goto_trace.h>
 
-#include <analyses/goto_check.h>
-
 #include <langapi/mode.h>
 
 #include <cbmc/version.h>
@@ -112,47 +110,8 @@ void symex_parseoptionst::get_command_line_options(optionst &options)
   if(cmdline.isset("unwindset"))
     options.set_option("unwindset", cmdline.getval("unwindset"));
 
-  // check array bounds
-  if(cmdline.isset("bounds-check"))
-    options.set_option("bounds-check", true);
-  else
-    options.set_option("bounds-check", false);
-
-  // check division by zero
-  if(cmdline.isset("div-by-zero-check"))
-    options.set_option("div-by-zero-check", true);
-  else
-    options.set_option("div-by-zero-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("signed-overflow-check"))
-    options.set_option("signed-overflow-check", true);
-  else
-    options.set_option("signed-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("unsigned-overflow-check"))
-    options.set_option("unsigned-overflow-check", true);
-  else
-    options.set_option("unsigned-overflow-check", false);
-
-  // check for NaN (not a number)
-  if(cmdline.isset("nan-check"))
-    options.set_option("nan-check", true);
-  else
-    options.set_option("nan-check", false);
-
-  // check pointers
-  if(cmdline.isset("pointer-check"))
-    options.set_option("pointer-check", true);
-  else
-    options.set_option("pointer-check", false);
-
-  // check for memory leaks
-  if(cmdline.isset("memory-leak-check"))
-    options.set_option("memory-leak-check", true);
-  else
-    options.set_option("memory-leak-check", false);
+  // all checks supported by goto_check
+  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -811,13 +770,7 @@ void symex_parseoptionst::help()
     " --round-to-zero              IEEE floating point rounding mode\n"
     "\n"
     "Program instrumentation options:\n"
-    " --bounds-check               enable array bounds checks\n"
-    " --div-by-zero-check          enable division by zero checks\n"
-    " --pointer-check              enable pointer checks\n"
-    " --memory-leak-check          enable memory leak checks\n"
-    " --signed-overflow-check      enable arithmetic over- and underflow checks\n"
-    " --unsigned-overflow-check    enable arithmetic over- and underflow checks\n"
-    " --nan-check                  check floating-point for NaN\n"
+    GOTO_CHECK_HELP
     " --show-properties            show the properties\n"
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
diff --git a/src/aa-symex/symex_parseoptions.h b/src/aa-symex/symex_parseoptions.h
index 4c2ba908088..f70da76dbfe 100644
--- a/src/aa-symex/symex_parseoptions.h
+++ b/src/aa-symex/symex_parseoptions.h
@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/language_ui.h>
 
+#include <analyses/goto_check.h>
+
 #include "path_search.h"
 
 class goto_functionst;
@@ -23,8 +25,7 @@ class optionst;
   "(function):" \
   "D:I:" \
   "(depth):(context-bound):(unwind):" \
-  "(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \
-  "(signed-overflow-check)(unsigned-overflow-check)(nan-check)" \
+  GOTO_CHECK_OPTIONS \
   "(no-assertions)(no-assumptions)" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 8aa43ba9769..0bc3a1c7826 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/base_type.h>
 #include <util/pointer_predicates.h>
 #include <util/cprover_prefix.h>
+#include <util/options.h>
 
 #include "local_bitvector_analysis.h"
 #include "goto_check.h"
@@ -39,6 +40,8 @@ class goto_checkt
     enable_div_by_zero_check=_options.get_bool_option("div-by-zero-check");
     enable_signed_overflow_check=_options.get_bool_option("signed-overflow-check");
     enable_unsigned_overflow_check=_options.get_bool_option("unsigned-overflow-check");
+    enable_pointer_overflow_check=_options.get_bool_option("pointer-overflow-check");
+    enable_conversion_check=_options.get_bool_option("conversion-check");
     enable_undefined_shift_check=_options.get_bool_option("undefined-shift-check");
     enable_float_overflow_check=_options.get_bool_option("float-overflow-check");
     enable_simplify=_options.get_bool_option("simplify");
@@ -72,6 +75,7 @@ class goto_checkt
   void pointer_overflow_check(const exprt &expr, const guardt &guard);
   void pointer_validity_check(const dereference_exprt &expr, const guardt &guard);
   void integer_overflow_check(const exprt &expr, const guardt &guard);
+  void conversion_check(const exprt &expr, const guardt &guard);
   void float_overflow_check(const exprt &expr, const guardt &guard);
   void nan_check(const exprt &expr, const guardt &guard);
 
@@ -102,6 +106,8 @@ class goto_checkt
   bool enable_div_by_zero_check;
   bool enable_signed_overflow_check;
   bool enable_unsigned_overflow_check;
+  bool enable_pointer_overflow_check;
+  bool enable_conversion_check;
   bool enable_undefined_shift_check;
   bool enable_float_overflow_check;
   bool enable_simplify;
@@ -302,7 +308,7 @@ void goto_checkt::mod_by_zero_check(
 
 /*******************************************************************\
 
-Function: goto_checkt::integer_overflow_check
+Function: goto_checkt::conversion_check
 
   Inputs:
 
@@ -312,25 +318,20 @@ Function: goto_checkt::integer_overflow_check
 
 \*******************************************************************/
 
-void goto_checkt::integer_overflow_check(
+void goto_checkt::conversion_check(
   const exprt &expr,
   const guardt &guard)
 {
-  if(!enable_signed_overflow_check &&
-     !enable_unsigned_overflow_check)
+  if(!enable_conversion_check)
     return;
 
   // First, check type.
   const typet &type=ns.follow(expr.type());
 
-  if(type.id()==ID_signedbv && !enable_signed_overflow_check)
-    return;
-
-  if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check)
+  if(type.id()!=ID_signedbv &&
+     type.id()!=ID_unsignedbv)
     return;
 
-  // add overflow subgoal
-
   if(expr.id()==ID_typecast)
   {
     // conversion to signed int may overflow
@@ -490,10 +491,41 @@ void goto_checkt::integer_overflow_check(
           guard);
       }
     }
+  }
+}
+
+/*******************************************************************\
+
+Function: goto_checkt::integer_overflow_check
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
 
+void goto_checkt::integer_overflow_check(
+  const exprt &expr,
+  const guardt &guard)
+{
+  if(!enable_signed_overflow_check &&
+     !enable_unsigned_overflow_check)
     return;
-  }
-  else if(expr.id()==ID_div)
+
+  // First, check type.
+  const typet &type=ns.follow(expr.type());
+
+  if(type.id()==ID_signedbv && !enable_signed_overflow_check)
+    return;
+
+  if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check)
+    return;
+
+  // add overflow subgoal
+
+  if(expr.id()==ID_div)
   {
     assert(expr.operands().size()==2);
 
@@ -898,7 +930,7 @@ void goto_checkt::pointer_overflow_check(
   const exprt &expr,
   const guardt &guard)
 {
-  if(!enable_pointer_check)
+  if(!enable_pointer_overflow_check)
     return;
 
   if(expr.id()==ID_plus ||
@@ -1429,8 +1461,7 @@ void goto_checkt::check_rec(
   }
   else if(expr.id()==ID_plus || expr.id()==ID_minus ||
           expr.id()==ID_mult ||
-          expr.id()==ID_unary_minus ||
-          expr.id()==ID_typecast)
+          expr.id()==ID_unary_minus)
   {
     if(expr.type().id()==ID_signedbv ||
        expr.type().id()==ID_unsignedbv)
@@ -1451,6 +1482,8 @@ void goto_checkt::check_rec(
       pointer_overflow_check(expr, guard);
     }
   }
+  else if(expr.id()==ID_typecast)
+    conversion_check(expr, guard);
   else if(expr.id()==ID_le || expr.id()==ID_lt ||
           expr.id()==ID_ge || expr.id()==ID_gt)
     pointer_rel_check(expr, guard);
diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h
index 0620ce1560d..8aaddcc3e68 100644
--- a/src/analyses/goto_check.h
+++ b/src/analyses/goto_check.h
@@ -9,12 +9,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H
 
-#include <util/namespace.h>
-#include <util/options.h>
-
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
 
+class namespacet;
+class optionst;
+
 void goto_check(
   const namespacet &ns,
   const optionst &options,
@@ -29,4 +29,36 @@ void goto_check(
   const optionst &options,
   goto_modelt &goto_model);
 
+#define GOTO_CHECK_OPTIONS \
+  "(bounds-check)(pointer-check)(memory-leak-check)" \
+  "(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \
+  "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
+  "(float-overflow-check)(nan-check)"
+
+#define GOTO_CHECK_HELP \
+  " --bounds-check               enable array bounds checks\n" \
+  " --pointer-check              enable pointer checks\n" \
+  " --memory-leak-check          enable memory leak checks\n" \
+  " --div-by-zero-check          enable division by zero checks\n" \
+  " --signed-overflow-check      enable signed arithmetic over- and underflow checks\n" \
+  " --unsigned-overflow-check    enable arithmetic over- and underflow checks\n" \
+  " --pointer-overflow-check     enable pointer arithmetic over- and underflow checks\n" \
+  " --conversion-check           check whether values can be represented after type cast\n" \
+  " --undefined-shift-check      check shift greater than bit-width\n" \
+  " --float-overflow-check       check floating-point for +/-Inf\n" \
+  " --nan-check                  check floating-point for NaN\n" \
+
+#define GOTO_CHECK_PARSE_OPTIONS(cmdline, options) \
+  options.set_option("bounds-check", cmdline.isset("bounds-check")); \
+  options.set_option("pointer-check", cmdline.isset("pointer-check")); \
+  options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
+  options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
+  options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); \
+  options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); \
+  options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); \
+  options.set_option("conversion-check", cmdline.isset("conversion-check")); \
+  options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); \
+  options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); \
+  options.set_option("nan-check", cmdline.isset("nan-check"))
+
 #endif
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 09f2f17812d..0c7027e0dea 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -46,8 +46,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <pointer-analysis/add_failed_symbols.h>
 
-#include <analyses/goto_check.h>
-
 #include <langapi/mode.h>
 
 #include "cbmc_solvers.h"
@@ -218,53 +216,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   else
     options.set_option("propagation", true);
 
-  // check array bounds
-  if(cmdline.isset("bounds-check"))
-    options.set_option("bounds-check", true);
-  else
-    options.set_option("bounds-check", false);
-
-  // check division by zero
-  if(cmdline.isset("div-by-zero-check"))
-    options.set_option("div-by-zero-check", true);
-  else
-    options.set_option("div-by-zero-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("signed-overflow-check"))
-    options.set_option("signed-overflow-check", true);
-  else
-    options.set_option("signed-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("unsigned-overflow-check"))
-    options.set_option("unsigned-overflow-check", true);
-  else
-    options.set_option("unsigned-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("float-overflow-check"))
-    options.set_option("float-overflow-check", true);
-  else
-    options.set_option("float-overflow-check", false);
-
-  // check for NaN (not a number)
-  if(cmdline.isset("nan-check"))
-    options.set_option("nan-check", true);
-  else
-    options.set_option("nan-check", false);
-
-  // check pointers
-  if(cmdline.isset("pointer-check"))
-    options.set_option("pointer-check", true);
-  else
-    options.set_option("pointer-check", false);
-
-  // check for memory leaks
-  if(cmdline.isset("memory-leak-check"))
-    options.set_option("memory-leak-check", true);
-  else
-    options.set_option("memory-leak-check", false);
+  // all checks supported by goto_check
+  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -1137,14 +1090,7 @@ void cbmc_parse_optionst::help()
     " --show-goto-functions        show goto program\n"
     "\n"
     "Program instrumentation options:\n"
-    " --bounds-check               enable array bounds checks\n"
-    " --div-by-zero-check          enable division by zero checks\n"
-    " --pointer-check              enable pointer checks\n"
-    " --memory-leak-check          enable memory leak checks\n"
-    " --signed-overflow-check      enable arithmetic over- and underflow checks\n"
-    " --unsigned-overflow-check    enable arithmetic over- and underflow checks\n"
-    " --float-overflow-check       check floating-point for +/-Inf\n"
-    " --nan-check                  check floating-point for NaN\n"
+    GOTO_CHECK_HELP
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 1a4b9477cfd..8f0269d4cb6 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/language_ui.h>
 
+#include <analyses/goto_check.h>
+
 #include "xml_interface.h"
 
 class bmct;
@@ -28,8 +30,7 @@ class optionst;
   "D:I:(c89)(c99)(c11)(cpp89)(cpp99)(cpp11)" \
   "(classpath):(cp):(main-class):" \
   "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
-  "(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \
-  "(signed-overflow-check)(unsigned-overflow-check)(float-overflow-check)(nan-check)" \
+  GOTO_CHECK_OPTIONS \
   "(no-assertions)(no-assumptions)" \
   "(xml-ui)(xml-interface)(json-ui)" \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index 8c9fb178dad..ab94bc84cfb 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -30,8 +30,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-instrument/dump_c.h>
 
-#include <analyses/goto_check.h>
-
 #include <langapi/mode.h>
 
 #include <cbmc/version.h>
@@ -112,53 +110,8 @@ void clobber_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("unwindset"))
     options.set_option("unwindset", cmdline.getval("unwindset"));
 
-  // check array bounds
-  if(cmdline.isset("bounds-check"))
-    options.set_option("bounds-check", true);
-  else
-    options.set_option("bounds-check", false);
-
-  // check division by zero
-  if(cmdline.isset("div-by-zero-check"))
-    options.set_option("div-by-zero-check", true);
-  else
-    options.set_option("div-by-zero-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("signed-overflow-check"))
-    options.set_option("signed-overflow-check", true);
-  else
-    options.set_option("signed-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("unsigned-overflow-check"))
-    options.set_option("unsigned-overflow-check", true);
-  else
-    options.set_option("unsigned-overflow-check", false);
-
-  // check overflow
-  if(cmdline.isset("float-overflow-check"))
-    options.set_option("float-overflow-check", true);
-  else
-    options.set_option("float-overflow-check", false);
-
-  // check for NaN (not a number)
-  if(cmdline.isset("nan-check"))
-    options.set_option("nan-check", true);
-  else
-    options.set_option("nan-check", false);
-
-  // check pointers
-  if(cmdline.isset("pointer-check"))
-    options.set_option("pointer-check", true);
-  else
-    options.set_option("pointer-check", false);
-
-  // check for memory leaks
-  if(cmdline.isset("memory-leak-check"))
-    options.set_option("memory-leak-check", true);
-  else
-    options.set_option("memory-leak-check", false);
+  // all checks supported by goto_check
+  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -788,13 +741,7 @@ void clobber_parse_optionst::help()
     " --round-to-zero              IEEE floating point rounding mode\n"
     "\n"
     "Program instrumentation options:\n"
-    " --bounds-check               enable array bounds checks\n"
-    " --div-by-zero-check          enable division by zero checks\n"
-    " --pointer-check              enable pointer checks\n"
-    " --memory-leak-check          enable memory leak checks\n"
-    " --signed-overflow-check      enable arithmetic over- and underflow checks\n"
-    " --unsigned-overflow-check    enable arithmetic over- and underflow checks\n"
-    " --nan-check                  check floating-point for NaN\n"
+    GOTO_CHECK_HELP
     " --show-properties            show the properties\n"
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
diff --git a/src/clobber/clobber_parse_options.h b/src/clobber/clobber_parse_options.h
index d00db917084..de74b73ff20 100644
--- a/src/clobber/clobber_parse_options.h
+++ b/src/clobber/clobber_parse_options.h
@@ -14,14 +14,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/language_ui.h>
 
+#include <analyses/goto_check.h>
+
 class goto_functionst;
 class optionst;
 
 #define CLOBBER_OPTIONS \
   "(depth):(context-bound):(unwind):" \
-  "(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \
-  "(signed-overflow-check)(unsigned-overflow-check)(nan-check)" \
-  "(float-overflow-check)" \
+  GOTO_CHECK_OPTIONS \
   "(no-assertions)(no-assumptions)" \
   "(error-label):(verbosity):(no-library)" \
   "(version)" \
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 50622b4d2a5..4b29d4b8548 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -30,7 +30,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/link_to_library.h>
 
-#include <analyses/goto_check.h>
 #include <analyses/local_may_alias.h>
 
 #include <langapi/mode.h>
@@ -154,54 +153,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   #endif
 
   #if 0
-  // check array bounds
-  if(cmdline.isset("bounds-check"))
-    options.set_option("bounds-check", true);
-  else
-    options.set_option("bounds-check", false);
-
-  // check division by zero
-  if(cmdline.isset("div-by-zero-check"))
-    options.set_option("div-by-zero-check", true);
-  else
-    options.set_option("div-by-zero-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("signed-overflow-check"))
-    options.set_option("signed-overflow-check", true);
-  else
-    options.set_option("signed-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("unsigned-overflow-check"))
-    options.set_option("unsigned-overflow-check", true);
-  else
-    options.set_option("unsigned-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("float-overflow-check"))
-    options.set_option("float-overflow-check", true);
-  else
-    options.set_option("float-overflow-check", false);
-
-  // check for NaN (not a number)
-  if(cmdline.isset("nan-check"))
-    options.set_option("nan-check", true);
-  else
-    options.set_option("nan-check", false);
-
-  // check pointers
-  if(cmdline.isset("pointer-check"))
-    options.set_option("pointer-check", true);
-  else
-    options.set_option("pointer-check", false);
-
-  // check for memory leaks
-  if(cmdline.isset("memory-leak-check"))
-    options.set_option("memory-leak-check", true);
-  else
-    options.set_option("memory-leak-check", false);
-
   // check assertions
   if(cmdline.isset("no-assertions"))
     options.set_option("assertions", false);
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 317da4bf32b..1943c7c5ced 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -16,6 +16,7 @@ Author: Peter Schrammel
 #include <util/expr_util.h>
 #include <util/language.h>
 #include <util/i2string.h>
+#include <util/options.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_function_pointers.h>
@@ -36,8 +37,6 @@ Author: Peter Schrammel
 
 #include <pointer-analysis/add_failed_symbols.h>
 
-#include <analyses/goto_check.h>
-
 #include <langapi/mode.h>
 
 #include <cbmc/version.h>
@@ -495,10 +494,6 @@ bool goto_diff_parse_optionst::process_goto_program(
     remove_vector(symbol_table, goto_functions);
     remove_complex(symbol_table, goto_functions);
 
-    // add generic checks
-    status() << "Generic Property Instrumentation" << eom;
-    goto_check(ns, options, goto_functions);
-
     // add failed symbols
     // needs to be done before pointer analysis
     add_failed_symbols(symbol_table);
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 8fd60ad0fb3..4f1d49e74ca 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -43,7 +43,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <analyses/local_bitvector_analysis.h>
 #include <analyses/custom_bitvector_analysis.h>
 #include <analyses/escape_analysis.h>
-#include <analyses/goto_check.h>
 #include <analyses/call_graph.h>
 #include <analyses/interval_analysis.h>
 #include <analyses/interval_domain.h>
@@ -783,59 +782,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   else
     options.set_option("assert-to-assume", false);
 
-  // check array bounds
-  if(cmdline.isset("bounds-check"))
-    options.set_option("bounds-check", true);
-  else
-    options.set_option("bounds-check", false);
-
-  // check division by zero
-  if(cmdline.isset("div-by-zero-check"))
-    options.set_option("div-by-zero-check", true);
-  else
-    options.set_option("div-by-zero-check", false);
-
-  // check undefined shifts
-  if(cmdline.isset("undefined-shift-check"))
-    options.set_option("undefined-shift-check", true);
-  else
-    options.set_option("undefined-shift-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("signed-overflow-check"))
-    options.set_option("signed-overflow-check", true);
-  else
-    options.set_option("signed-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("unsigned-overflow-check"))
-    options.set_option("unsigned-overflow-check", true);
-  else
-    options.set_option("unsigned-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("float-overflow-check"))
-    options.set_option("float-overflow-check", true);
-  else
-    options.set_option("float-overflow-check", false);
-
-  // check for NaN (not a number)
-  if(cmdline.isset("nan-check"))
-    options.set_option("nan-check", true);
-  else
-    options.set_option("nan-check", false);
-
-  // check pointers
-  if(cmdline.isset("pointer-check"))
-    options.set_option("pointer-check", true);
-  else
-    options.set_option("pointer-check", false);
-
-  // check pointers
-  if(cmdline.isset("memory-leak-check"))
-    options.set_option("memory-leak-check", true);
-  else
-    options.set_option("memory-leak-check", false);
+  // all checks supported by goto_check
+  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -1308,14 +1256,7 @@ void goto_instrument_parse_optionst::help()
     "\n"
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"
-    " --bounds-check               add array bounds checks\n"
-    " --div-by-zero-check          add division by zero checks\n"
-    " --pointer-check              add pointer checks\n"
-    " --memory-leak-check          add memory leak checks\n"
-    " --signed-overflow-check      add arithmetic over- and underflow checks\n"
-    " --unsigned-overflow-check    add arithmetic over- and underflow checks\n"
-    " --undefined-shift-check      add range checks for shift distances\n"
-    " --nan-check                  add floating-point NaN checks\n"
+    GOTO_CHECK_HELP
     " --uninitialized-check        add checks for uninitialized locals (experimental)\n"
     " --error-label label          check that label is unreachable\n"
     " --stack-depth n              add check that call stack size of non-inlined functions never exceeds n\n"
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index 1123a1ec6e9..da9c266bf86 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -15,20 +15,21 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language_ui.h>
 #include <goto-programs/goto_functions.h>
 
+#include <analyses/goto_check.h>
+
 #define GOTO_INSTRUMENT_OPTIONS \
   "(all)" \
   "(document-claims-latex)(document-claims-html)" \
   "(document-properties-latex)(document-properties-html)" \
   "(dump-c)(dump-cpp)(use-system-headers)(dot)(xml)" \
-  "(bounds-check)(no-bounds-check)" \
-  "(pointer-check)(memory-leak-check)(no-pointer-check)" \
+  GOTO_CHECK_OPTIONS \
+  /* no-X-check are deprecated and ignored */ \
+  "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
+  "(no-nan-check)" \
   "(remove-pointers)" \
   "(no-simplify)" \
   "(assert-to-assume)" \
-  "(div-by-zero-check)(no-div-by-zero-check)" \
-  "(undefined-shift-check)" \
   "(no-assertions)(no-assumptions)(uninitialized-check)" \
-  "(nan-check)(no-nan-check)" \
   "(race-check)(scc)(one-event-per-cycle)" \
   "(minimum-interference)" \
   "(mm):(my-events)(unwind):" \
@@ -39,7 +40,6 @@ Author: Daniel Kroening, kroening@kroening.com
   "(nondet-volatile)(isr):" \
   "(stack-depth):(nondet-static)" \
   "(function-enter):(function-exit):(branch):" \
-  "(signed-overflow-check)(unsigned-overflow-check)(float-overflow-check)" \
   "(show-goto-functions)(show-value-sets)" \
   "(show-global-may-alias)" \
   "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
diff --git a/src/musketeer/musketeer_parse_options.cpp b/src/musketeer/musketeer_parse_options.cpp
index 3ac2ba56b37..28accf23fa2 100644
--- a/src/musketeer/musketeer_parse_options.cpp
+++ b/src/musketeer/musketeer_parse_options.cpp
@@ -32,7 +32,6 @@ Module: Main Module
 #include <pointer-analysis/add_failed_symbols.h>
 
 #include <analyses/local_may_alias.h>
-#include <analyses/goto_check.h>
 
 #include <goto-instrument/rw_set.h>
 #include <goto-instrument/wmm/weak_memory.h>
@@ -204,9 +203,6 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program(
 
   namespacet ns(symbol_table);
 
-  // add generic checks, if needed
-  goto_check(ns, options, goto_functions);
-
   if( cmdline.isset("mm")
       || cmdline.isset("all-shared")
       || cmdline.isset("volatile")
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index bfd6a24cae5..7a9227e6f58 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -35,8 +35,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-instrument/cover.h>
 
-#include <analyses/goto_check.h>
-
 #include <langapi/mode.h>
 
 #include <cbmc/version.h>
@@ -120,53 +118,8 @@ void symex_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("unwindset"))
     options.set_option("unwindset", cmdline.get_value("unwindset"));
 
-  // check array bounds
-  if(cmdline.isset("bounds-check"))
-    options.set_option("bounds-check", true);
-  else
-    options.set_option("bounds-check", false);
-
-  // check division by zero
-  if(cmdline.isset("div-by-zero-check"))
-    options.set_option("div-by-zero-check", true);
-  else
-    options.set_option("div-by-zero-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("signed-overflow-check"))
-    options.set_option("signed-overflow-check", true);
-  else
-    options.set_option("signed-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("unsigned-overflow-check"))
-    options.set_option("unsigned-overflow-check", true);
-  else
-    options.set_option("unsigned-overflow-check", false);
-
-  // check overflow
-  if(cmdline.isset("float-overflow-check"))
-    options.set_option("float-overflow-check", true);
-  else
-    options.set_option("float-overflow-check", false);
-
-  // check for NaN (not a number)
-  if(cmdline.isset("nan-check"))
-    options.set_option("nan-check", true);
-  else
-    options.set_option("nan-check", false);
-
-  // check pointers
-  if(cmdline.isset("pointer-check"))
-    options.set_option("pointer-check", true);
-  else
-    options.set_option("pointer-check", false);
-
-  // check for memory leaks
-  if(cmdline.isset("memory-leak-check"))
-    options.set_option("memory-leak-check", true);
-  else
-    options.set_option("memory-leak-check", false);
+  // all checks supported by goto_check
+  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -743,13 +696,7 @@ void symex_parse_optionst::help()
     " --function name              set main function name\n"
     "\n"
     "Program instrumentation options:\n"
-    " --bounds-check               enable array bounds checks\n"
-    " --div-by-zero-check          enable division by zero checks\n"
-    " --pointer-check              enable pointer checks\n"
-    " --memory-leak-check          enable memory leak checks\n"
-    " --signed-overflow-check      enable arithmetic over- and underflow checks\n"
-    " --unsigned-overflow-check    enable arithmetic over- and underflow checks\n"
-    " --nan-check                  check floating-point for NaN\n"
+    GOTO_CHECK_HELP
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index b93c937515e..0a84fa98b32 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/language_ui.h>
 
+#include <analyses/goto_check.h>
+
 #include "path_search.h"
 
 class goto_functionst;
@@ -25,9 +27,7 @@ class optionst;
   "(function):" \
   "D:I:" \
   "(depth):(context-bound):(branch-bound):(unwind):" \
-  "(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \
-  "(signed-overflow-check)(unsigned-overflow-check)(nan-check)" \
-  "(float-overflow-check)" \
+  GOTO_CHECK_OPTIONS \
   "(no-assertions)(no-assumptions)" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \