diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 65a4386077b..d8145cad4fe 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -672,6 +672,12 @@ int cbmc_parse_optionst::get_goto_program(
 
     goto_convert(symbol_table, goto_functions, ui_message_handler);
 
+    if(goto_functions.check_internal_invariants(*this))
+    {
+      error() << "GOTO program violates internal invariants" << eom;
+      return 6;
+    }
+
     if(process_goto_program(options, goto_functions))
       return 6;
 
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index 36cc3e49abc..86b61f0e09d 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -127,6 +127,12 @@ int clobber_parse_optionst::doit()
     if(get_goto_program(options, goto_functions))
       return 6;
 
+    if(goto_functions.check_internal_invariants(*this))
+    {
+      error() << "GOTO program violates internal invariants" << eom;
+      return 6;
+    }
+
     label_properties(goto_functions);
 
     if(cmdline.isset("show-properties"))
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index 96b76260e96..cb82118d435 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -129,6 +129,12 @@ bool compilet::doit()
       return true;
   }
 
+  if(compiled_functions.check_internal_invariants(*this))
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    return true;
+  }
+
   return
     warning_is_fatal &&
     get_message_handler().get_message_count(messaget::M_WARNING)!=
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 146fe27eb1c..b1ce4451eca 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -278,6 +278,18 @@ int goto_diff_parse_optionst::doit()
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
 
+  if(goto_model1.goto_functions.check_internal_invariants(*this))
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    return 6;
+  }
+
+  if(goto_model2.goto_functions.check_internal_invariants(*this))
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    return 6;
+  }
+
   if(cmdline.isset("show-goto-functions"))
   {
     show_goto_functions(goto_model1, get_ui());
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 888853c6dc4..a187aad18cc 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -868,6 +868,12 @@ void goto_instrument_parse_optionst::get_goto_program()
 
   config.set(cmdline);
   config.set_from_symbol_table(symbol_table);
+
+  if(goto_functions.check_internal_invariants(*this))
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    throw 0;
+  }
 }
 
 void goto_instrument_parse_optionst::instrument_goto_program()
diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp
index 9c14c8bc6bc..1880c4727fb 100644
--- a/src/goto-programs/goto_functions.cpp
+++ b/src/goto-programs/goto_functions.cpp
@@ -30,3 +30,16 @@ void get_local_identifiers(
       dest.insert(identifier);
   }
 }
+
+/// Ensure that all functions satisfy all assumptions about
+/// consistent goto programs.
+/// \param msg Message output
+/// \return True, iff at least one invariant is violated
+bool goto_functionst::check_internal_invariants(messaget &msg) const
+{
+  forall_goto_functions(it, *this)
+    if(it->second.body.check_internal_invariants(msg))
+      return true;
+
+  return false;
+}
diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h
index 7fc9f70628a..80a4e320928 100644
--- a/src/goto-programs/goto_functions.h
+++ b/src/goto-programs/goto_functions.h
@@ -43,6 +43,8 @@ class goto_functionst:public goto_functions_templatet<goto_programt>
     goto_functions_templatet::operator=(std::move(other));
     return *this;
   }
+
+  bool check_internal_invariants(messaget &msg) const;
 };
 
 #define Forall_goto_functions(it, functions) \
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index 347e156e589..0ca1f921b4c 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <ostream>
 
+#include <util/message.h>
 #include <util/std_expr.h>
 
 #include <langapi/language_util.h>
@@ -483,3 +484,129 @@ std::string as_string(
 
   return "";
 }
+
+/// Ensure the current goto_programt satisfies all assumptions
+/// about consistent goto programs.
+/// \param msg Message output
+/// \return True, iff at least one invariant is violated
+bool goto_programt::check_internal_invariants(messaget &msg) const
+{
+  if(empty())
+    return false;
+
+  unsigned prev_loc_number=0;
+  bool prev_loc_number_set=false;
+
+  forall_goto_program_instructions(it, *this)
+  {
+    const goto_programt::instructiont &ins=*it;
+
+    if(ins.check_internal_invariants(msg))
+      return true;
+
+    if(prev_loc_number_set &&
+       ins.location_number<=prev_loc_number)
+    {
+      msg.error().source_location=ins.source_location;
+      msg.error() << "location number not strictly increasing"
+                  << messaget::eom;
+      return true;
+    }
+    else if(!prev_loc_number_set)
+    {
+      prev_loc_number=ins.location_number;
+      prev_loc_number_set=true;
+    }
+
+    switch(ins.type)
+    {
+      case GOTO:
+      case ASSUME:
+      case ASSERT:
+        if(ins.guard.type()!=bool_typet())
+        {
+          msg.error().source_location=ins.source_location;
+          msg.error() << ins.type << " has non-Boolean guard"
+                      << messaget::eom;
+          return true;
+        }
+        break;
+      case OTHER:
+      case SKIP:
+      case LOCATION:
+      case END_FUNCTION:
+      case START_THREAD:
+      case END_THREAD:
+      case ATOMIC_BEGIN:
+      case ATOMIC_END:
+      case RETURN:
+        break;
+      case ASSIGN:
+        if(ins.code.get_statement()!=ID_assign)
+        {
+          msg.error().source_location=ins.source_location;
+          msg.error() << ins.type << " instruction has code "
+                      << ins.code.get_statement()
+                      << messaget::eom;
+          return true;
+        }
+        return false;
+      case DECL:
+        if(ins.code.get_statement()!=ID_decl)
+        {
+          msg.error().source_location=ins.source_location;
+          msg.error() << ins.type << " instruction has code "
+                      << ins.code.get_statement()
+                      << messaget::eom;
+          return true;
+        }
+        else if(to_code_decl(ins.code).symbol().id()!=ID_symbol)
+        {
+          msg.error().source_location=ins.source_location;
+          msg.error() << "declaration operand is not a symbol"
+                      << messaget::eom;
+          return true;
+        }
+        break;
+      case DEAD:
+        if(ins.code.get_statement()!=ID_dead)
+        {
+          msg.error().source_location=ins.source_location;
+          msg.error() << ins.type << " instruction has code "
+                      << ins.code.get_statement()
+                      << messaget::eom;
+          return true;
+        }
+        break;
+      case FUNCTION_CALL:
+        if(ins.code.get_statement()!=ID_function_call)
+        {
+          msg.error().source_location=ins.source_location;
+          msg.error() << ins.type << " instruction has code "
+                      << ins.code.get_statement()
+                      << messaget::eom;
+          return true;
+        }
+        break;
+      case THROW:
+      case CATCH:
+        break;
+      case NO_INSTRUCTION_TYPE:
+        msg.error().source_location=ins.source_location;
+        msg.error() << ins.type << " not permitted"
+                    << messaget::eom;
+        return true;
+    }
+  }
+
+  // the last instruction must be END_FUNCTION
+  if(!get_end_function()->is_end_function())
+  {
+    msg.error().source_location=get_end_function()->source_location;
+    msg.error() << "end of function is of type "
+                << get_end_function()->type << messaget::eom;
+    return true;
+  }
+
+  return false;
+}
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
index 8e966283953..bc484c32d17 100644
--- a/src/goto-programs/goto_program.h
+++ b/src/goto-programs/goto_program.h
@@ -64,6 +64,8 @@ class goto_programt:public goto_program_templatet<codet, exprt>
   // get the variables in decl statements
   typedef std::set<irep_idt> decl_identifierst;
   void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
+
+  bool check_internal_invariants(messaget &msg) const;
 };
 
 #define forall_goto_program_instructions(it, program) \
diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h
index af121f78444..128a81ad39e 100644
--- a/src/goto-programs/goto_program_template.h
+++ b/src/goto-programs/goto_program_template.h
@@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <sstream>
 #include <string>
 
+#include <util/invariant.h>
+#include <util/message.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 #include <util/source_location.h>
@@ -262,6 +264,84 @@ class goto_program_templatet
       instruction_id_builder << type;
       return instruction_id_builder.str();
     }
+
+    /// Ensure the current instruction satisfies all assumptions
+    /// within consistent goto programs.
+    /// \param msg Message output
+    /// \return True, iff at least one invariant is violated
+    bool check_internal_invariants(messaget &msg) const
+    {
+      if(function.empty())
+      {
+        msg.error().source_location=source_location;
+        msg.error() << "instruction has no function name"
+                    << messaget::eom;
+        return true;
+      }
+
+      switch(type)
+      {
+        case GOTO:
+        case ASSUME:
+        case ASSERT:
+          if(code!=irept() && code.is_not_nil())
+          {
+            msg.error().source_location=source_location;
+            msg.error() << type << " has non-nil code\n"
+                        << code.pretty() << messaget::eom;
+            return true;
+          }
+          else if(guard.is_nil() || guard==irept())
+          {
+            msg.error().source_location=source_location;
+            msg.error() << type << " has nil guard"
+                        << messaget::eom;
+            return true;
+          }
+          return false;
+        case OTHER:
+          return false;
+        case SKIP:
+        case LOCATION:
+        case END_FUNCTION:
+          if(code!=irept() && code.is_not_nil())
+          {
+            msg.error().source_location=source_location;
+            msg.error() << type << " has non-nil code\n"
+                        << code.pretty() << messaget::eom;
+            return true;
+          }
+          return false;
+        case START_THREAD:
+          return false;
+        case END_THREAD:
+          return false;
+        case ATOMIC_BEGIN:
+          return false;
+        case ATOMIC_END:
+          return false;
+        case RETURN:
+          return false;
+        case ASSIGN:
+        case DECL:
+        case DEAD:
+        case FUNCTION_CALL:
+          if(code==irept() || code.is_nil())
+          {
+            msg.error().source_location=source_location;
+            msg.error() << type << " has nil code"
+                        << messaget::eom;
+            return true;
+          }
+          return false;
+        case THROW:
+          return false;
+        case CATCH:
+          return false;
+        default:
+          return true;
+      }
+    }
   };
 
   typedef std::list<instructiont> instructionst;
@@ -466,9 +546,17 @@ class goto_program_templatet
 
   targett get_end_function()
   {
-    assert(!instructions.empty());
+    PRECONDITION(!instructions.empty());
+    const auto end_function=std::prev(instructions.end());
+    DATA_INVARIANT(end_function->is_end_function(), "invalid end_function");
+    return end_function;
+  }
+
+  const_targett get_end_function() const
+  {
+    PRECONDITION(!instructions.empty());
     const auto end_function=std::prev(instructions.end());
-    assert(end_function->is_end_function());
+    DATA_INVARIANT(end_function->is_end_function(), "invalid end_function");
     return end_function;
   }
 
diff --git a/src/musketeer/musketeer_parse_options.cpp b/src/musketeer/musketeer_parse_options.cpp
index ace73687432..3fdb989f4fe 100644
--- a/src/musketeer/musketeer_parse_options.cpp
+++ b/src/musketeer/musketeer_parse_options.cpp
@@ -141,6 +141,12 @@ void goto_fence_inserter_parse_optionst::get_goto_program(
     throw 0;
 
   config.set_from_symbol_table(symbol_table);
+
+  if(goto_functions.check_internal_invariants(*this))
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    throw 0;
+  }
 }
 
 void goto_fence_inserter_parse_optionst::instrument_goto_program(
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 5fc475ee154..06e5d2501f6 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -138,6 +138,12 @@ int symex_parse_optionst::doit()
   if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
     return 6;
 
+  if(goto_model.goto_functions.check_internal_invariants(*this))
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    return 6;
+  }
+
   if(process_goto_program(options))
     return 6;