diff --git a/CMakeLists.txt b/CMakeLists.txt
index a5c0ef6893d..99a97066cde 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -3,6 +3,7 @@ cmake_minimum_required(VERSION 3.2)
 find_program(CCACHE_PROGRAM ccache)
 if(CCACHE_PROGRAM)
     set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "${CCACHE_PROGRAM}")
+    message(STATUS "Rule launch compile: ${CCACHE_PROGRAM}")
  endif()
 
 set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
@@ -19,7 +20,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
     #   Ensure NDEBUG is not set for release builds
     set(CMAKE_CXX_FLAGS_RELEASE "-O2")
     #   Enable lots of warnings
-    set(CMAKE_CXX_FLAGS "-Wall -Wpedantic -Werror")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror")
 elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
     #   This would be the place to enable warnings for Windows builds, although
     #   config.inc doesn't seem to do that currently
diff --git a/regression/ansi-c/arch_flags_mcpu_bad/object.intel b/regression/ansi-c/arch_flags_mcpu_bad/object.intel
index cc6ea40a25e..e32d04e4c56 100644
Binary files a/regression/ansi-c/arch_flags_mcpu_bad/object.intel and b/regression/ansi-c/arch_flags_mcpu_bad/object.intel differ
diff --git a/regression/ansi-c/arch_flags_mcpu_good/object.arm b/regression/ansi-c/arch_flags_mcpu_good/object.arm
index 7c14d169f62..f0a1397b8d6 100644
Binary files a/regression/ansi-c/arch_flags_mcpu_good/object.arm and b/regression/ansi-c/arch_flags_mcpu_good/object.arm differ
diff --git a/regression/ansi-c/arch_flags_mcpu_good/test.desc b/regression/ansi-c/arch_flags_mcpu_good/test.desc
index c02992dcb8d..c7daf68b878 100644
--- a/regression/ansi-c/arch_flags_mcpu_good/test.desc
+++ b/regression/ansi-c/arch_flags_mcpu_good/test.desc
@@ -14,6 +14,10 @@ command line:
 
   goto-cc --native-compiler=arm-none-eabi-gcc -mcpu=cortex-a15 -c source.c
 
+On Ubuntu, you can get a suitable compiler using:
+
+  sudo apt install gcc-arm-none-eabi
+
 preproc.i is already pre-processed so that it can be linked in without
 needing to invoke a pre-processor from a cross-compile toolchain on your
 local machine. Linking it together with the ARM object file, while
diff --git a/regression/ansi-c/arch_flags_mthumb_bad/object.intel b/regression/ansi-c/arch_flags_mthumb_bad/object.intel
index cc6ea40a25e..72136c8ae3c 100644
Binary files a/regression/ansi-c/arch_flags_mthumb_bad/object.intel and b/regression/ansi-c/arch_flags_mthumb_bad/object.intel differ
diff --git a/regression/ansi-c/arch_flags_mthumb_good/object.arm b/regression/ansi-c/arch_flags_mthumb_good/object.arm
index 7c14d169f62..eb41c683911 100644
Binary files a/regression/ansi-c/arch_flags_mthumb_good/object.arm and b/regression/ansi-c/arch_flags_mthumb_good/object.arm differ
diff --git a/regression/ansi-c/arch_flags_mthumb_good/test.desc b/regression/ansi-c/arch_flags_mthumb_good/test.desc
index 02a5c7389e3..9f56b40997e 100644
--- a/regression/ansi-c/arch_flags_mthumb_good/test.desc
+++ b/regression/ansi-c/arch_flags_mthumb_good/test.desc
@@ -14,6 +14,10 @@ line:
 
   goto-cc --native-compiler=arm-none-eabi-gcc -mthumb -c source.c
 
+On Ubuntu, you can get a suitable compiler using:
+
+  sudo apt install gcc-arm-none-eabi
+
 preproc.i is already pre-processed so that it can be linked in without
 needing to invoke a pre-processor from a cross-compile toolchain on your
 local machine. Linking it together with the ARM object file, while
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index a7be2e0fd31..13c6d0045b5 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -165,7 +165,6 @@ add_subdirectory(util)
 add_subdirectory(xmllang)
 add_subdirectory(java_bytecode)
 add_subdirectory(miniz)
-add_subdirectory(musketeer)
 add_subdirectory(clobber)
 add_subdirectory(cbmc)
 add_subdirectory(goto-cc)
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index edf95e5379e..0be52dae81c 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -372,8 +372,7 @@ void c_typecastt::implicit_typecast_arithmetic(
   case PTR:
     if(expr_type.id()==ID_array)
     {
-      new_type.id(ID_pointer);
-      new_type.subtype()=expr_type.subtype();
+      new_type=pointer_type(expr_type.subtype());
       break;
     }
     return;
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index e45dc1a4d89..59c684de00b 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -1594,8 +1594,7 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr)
     {
       // Make it void *.
       // gcc and clang issue a warning for this.
-      expr.type()=typet(ID_pointer);
-      expr.type().subtype()=typet(ID_empty);
+      expr.type()=pointer_type(empty_typet());
       implicit_typecast(operands[1], expr.type());
       implicit_typecast(operands[2], expr.type());
     }
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 1a6bf27adad..88ca770c4bf 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -1492,7 +1492,7 @@ void c_typecheck_baset::adjust_function_parameter(typet &type) const
 {
   if(type.id()==ID_array)
   {
-    type.id(ID_pointer);
+    type=pointer_type(type.subtype());
     type.remove(ID_size);
     type.remove(ID_C_constant);
   }
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index bddccced310..ba7ab7a0bb1 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -3065,8 +3065,7 @@ unary_identifier_declarator:
         {
           // the type_qualifier_list is for the pointer,
           // and not the identifier_declarator
-          stack_type($1).id(ID_pointer);
-          stack_type($1).subtype()=typet(ID_abstract);
+          stack_type($1)=pointer_type(typet(ID_abstract));
           $2=merge($2, $1); // dest=$2
           make_subtype($3, $2); // dest=$3
           $$=$3;
@@ -3250,15 +3249,13 @@ unary_abstract_declarator:
           '*'
         {
           $$=$1;
-          set($$, ID_pointer);
-          stack_type($$).subtype()=typet(ID_abstract);
+          stack_type($$)=pointer_type(typet(ID_abstract));
         }
         | '*' attribute_type_qualifier_list
         {
           // The type_qualifier_list belongs to the pointer,
           // not to the (missing) abstract declarator.
-          set($1, ID_pointer);
-          stack_type($1).subtype()=typet(ID_abstract);
+          stack_type($1)=pointer_type(typet(ID_abstract));
           $$=merge($2, $1);
         }
         | '*' abstract_declarator
@@ -3270,8 +3267,7 @@ unary_abstract_declarator:
         {
           // The type_qualifier_list belongs to the pointer,
           // not to the abstract declarator.
-          stack_type($1).id(ID_pointer);
-          stack_type($1).subtype()=typet(ID_abstract);
+          stack_type($1)=pointer_type(typet(ID_abstract));
           $2=merge($2, $1); // dest=$2
           make_subtype($3, $2); // dest=$3
           $$=$3;
@@ -3290,15 +3286,13 @@ parameter_unary_abstract_declarator:
           '*'
         {
           $$=$1;
-          set($$, ID_pointer);
-          stack_type($$).subtype()=typet(ID_abstract);
+          stack_type($$)=pointer_type(typet(ID_abstract));
         }
         | '*' attribute_type_qualifier_list
         {
           // The type_qualifier_list belongs to the pointer,
           // not to the (missing) abstract declarator.
-          set($1, ID_pointer);
-          stack_type($1).subtype()=typet(ID_abstract);
+          stack_type($1)=pointer_type(typet(ID_abstract));
           $$=merge($2, $1);
         }
         | '*' parameter_abstract_declarator
@@ -3310,8 +3304,7 @@ parameter_unary_abstract_declarator:
         {
           // The type_qualifier_list belongs to the pointer,
           // not to the (missing) abstract declarator.
-          stack($1).id(ID_pointer);
-          stack_type($1).subtype()=typet(ID_abstract);
+          stack_type($1)=pointer_type(typet(ID_abstract));
           $2=merge($2, $1); // dest=$2
           make_subtype($3, $2); // dest=$3
           $$=$3;
diff --git a/src/ansi-c/parser_static.inc b/src/ansi-c/parser_static.inc
index e0c8385998d..6f0b3f41b1d 100644
--- a/src/ansi-c/parser_static.inc
+++ b/src/ansi-c/parser_static.inc
@@ -290,8 +290,7 @@ Function: make_pointer
 
 static void make_pointer(const YYSTYPE dest)
 {
-  set(dest, ID_pointer);
-  stack_type(dest).subtype()=typet(ID_abstract);
+  stack_type(dest)=pointer_type(typet(ID_abstract));
 }
 
 /*******************************************************************\
diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp
index 40b0fe18afd..2ec3a686c2d 100644
--- a/src/cpp/cpp_typecheck_constructor.cpp
+++ b/src/cpp/cpp_typecheck_constructor.cpp
@@ -41,17 +41,17 @@ static void copy_parent(
   exprt &op0=code.op0().op0();
 
   op0.operands().push_back(exprt("cpp-this"));
-  op0.type().id(ID_pointer);
-  op0.type().subtype()=cpp_namet(parent_base_name, source_location).as_type();
+  op0.type()=
+    pointer_type(cpp_namet(parent_base_name, source_location).as_type());
   op0.add_source_location()=source_location;
 
   code.operands().push_back(exprt("explicit-typecast"));
   exprt &op1=code.op1();
 
-  op1.type().id(ID_pointer);
+  op0.type()=
+    pointer_type(cpp_namet(parent_base_name, source_location).as_type());
   op1.type().set(ID_C_reference, true);
   op1.type().subtype().set(ID_C_constant, true);
-  op1.type().subtype()=cpp_namet(parent_base_name, source_location).as_type();
 
   op1.operands().push_back(exprt(ID_cpp_name));
   op1.op0().get_sub().push_back(irept(ID_name));
@@ -420,9 +420,8 @@ void cpp_typecheckt::default_assignop(
   args_decl_declor.name().get_sub().back().add(ID_identifier).id(arg_name);
   args_decl_declor.add_source_location()=source_location;
 
-  args_decl_declor.type().id(ID_pointer);
+  args_decl_declor.type()=pointer_type(typet(ID_nil));
   args_decl_declor.type().set(ID_C_reference, true);
-  args_decl_declor.type().subtype().make_nil();
   args_decl_declor.value().make_nil();
 }
 
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index ee399b8af8d..1cb4bfbe651 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
+#include <util/c_types.h>
 
 #include <ansi-c/ansi_c_y.tab.h>
 
@@ -3015,7 +3016,7 @@ bool Parser::optPtrOperator(typet &ptrs)
 
     if(t=='*')
     {
-      typet op(ID_pointer);
+      typet op=pointer_type(typet(ID_nil));
       cpp_tokent tk;
       lex.get_token(tk);
       set_location(op, tk);
@@ -3078,7 +3079,7 @@ bool Parser::optPtrOperator(typet &ptrs)
     {
       cpp_tokent tk;
       lex.get_token(tk);
-      typet op(ID_pointer);
+      typet op=pointer_type(typet(ID_nil));
       op.set(ID_C_reference, true);
       set_location(op, tk);
       t_list.push_front(op);
@@ -3087,7 +3088,7 @@ bool Parser::optPtrOperator(typet &ptrs)
     {
       cpp_tokent tk;
       lex.get_token(tk);
-      typet op(ID_pointer);
+      typet op=pointer_type(typet(ID_nil));
       op.set(ID_C_rvalue_reference, true);
       set_location(op, tk);
       t_list.push_front(op);
@@ -3530,7 +3531,7 @@ bool Parser::rPtrToMember(irept &ptr_to_mem)
   std::cout << std::string(__indent, ' ') << "Parser::rPtrToMember 0\n";
   #endif
 
-  irept ptm(ID_pointer);
+  typet ptm=pointer_type(typet(ID_nil));
   irept &name = ptm.add("to-member");
   name=cpp_namet();
   irept::subt &components=name.get_sub();
@@ -6477,7 +6478,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
 
   case TOK_NULLPTR:
     lex.get_token(tk);
-    exp=constant_exprt(ID_NULL, typet(ID_pointer, typet(ID_nullptr)));
+    exp=constant_exprt(ID_NULL, pointer_type(typet(ID_nullptr)));
     set_location(exp, tk);
     #ifdef DEBUG
     std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 6\n";
diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp
index 0c9a922367d..d437ddf622b 100644
--- a/src/goto-programs/remove_exceptions.cpp
+++ b/src/goto-programs/remove_exceptions.cpp
@@ -213,7 +213,7 @@ void remove_exceptionst::add_exceptional_returns(
       new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX;
       new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX;
       new_symbol.mode=function_symbol.mode;
-      new_symbol.type=typet(ID_pointer, empty_typet());
+      new_symbol.type=pointer_type(empty_typet());
       symbol_table.add(new_symbol);
 
       // initialize the exceptional return with NULL
diff --git a/src/musketeer/CMakeLists.txt b/src/musketeer/CMakeLists.txt
deleted file mode 100644
index 6265183ee0b..00000000000
--- a/src/musketeer/CMakeLists.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-# Library
-file(GLOB_RECURSE sources "*.cpp")
-file(GLOB_RECURSE headers "*.h")
-list(REMOVE_ITEM sources
-    ${CMAKE_CURRENT_SOURCE_DIR}/musketeer_main.cpp
-)
-add_library(musketeer-lib ${sources} ${headers})
-
-generic_includes(musketeer-lib)
-
-target_link_libraries(musketeer-lib
-    ansi-c
-    linking
-    big-int
-    goto-programs
-    goto-symex
-    assembler
-    pointer-analysis
-    analyses
-    langapi
-    util
-    solvers
-    goto-instrument-lib
-)
-
-add_if_library(musketeer-lib glpk)
-
-# Executable
-add_executable(musketeer musketeer_main.cpp)
-target_link_libraries(musketeer musketeer-lib)
diff --git a/src/util/std_types.h b/src/util/std_types.h
index 4d4a0763ca8..726c210e52e 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -17,10 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com
  * \date   Sun Jul 31 21:54:44 BST 2011
 */
 
-#include <cassert>
-
 #include "expr.h"
 #include "mp_arith.h"
+#include "invariant.h"
 
 class constant_exprt;
 
@@ -141,7 +140,7 @@ class symbol_typet:public typet
 */
 inline const symbol_typet &to_symbol_type(const typet &type)
 {
-  assert(type.id()==ID_symbol);
+  PRECONDITION(type.id()==ID_symbol);
   return static_cast<const symbol_typet &>(type);
 }
 
@@ -150,7 +149,7 @@ inline const symbol_typet &to_symbol_type(const typet &type)
 */
 inline symbol_typet &to_symbol_type(typet &type)
 {
-  assert(type.id()==ID_symbol);
+  PRECONDITION(type.id()==ID_symbol);
   return static_cast<symbol_typet &>(type);
 }
 
@@ -276,8 +275,7 @@ class struct_union_typet:public typet
 */
 inline const struct_union_typet &to_struct_union_type(const typet &type)
 {
-  assert(type.id()==ID_struct ||
-         type.id()==ID_union);
+  PRECONDITION(type.id()==ID_struct || type.id()==ID_union);
   return static_cast<const struct_union_typet &>(type);
 }
 
@@ -286,8 +284,7 @@ inline const struct_union_typet &to_struct_union_type(const typet &type)
 */
 inline struct_union_typet &to_struct_union_type(typet &type)
 {
-  assert(type.id()==ID_struct ||
-         type.id()==ID_union);
+  PRECONDITION(type.id()==ID_struct || type.id()==ID_union);
   return static_cast<struct_union_typet &>(type);
 }
 
@@ -316,7 +313,7 @@ class struct_typet:public struct_union_typet
 */
 inline const struct_typet &to_struct_type(const typet &type)
 {
-  assert(type.id()==ID_struct);
+  PRECONDITION(type.id()==ID_struct);
   return static_cast<const struct_typet &>(type);
 }
 
@@ -325,7 +322,7 @@ inline const struct_typet &to_struct_type(const typet &type)
 */
 inline struct_typet &to_struct_type(typet &type)
 {
-  assert(type.id()==ID_struct);
+  PRECONDITION(type.id()==ID_struct);
   return static_cast<struct_typet &>(type);
 }
 
@@ -420,7 +417,7 @@ class class_typet:public struct_typet
 */
 inline const class_typet &to_class_type(const typet &type)
 {
-  assert(type.id()==ID_struct);
+  PRECONDITION(type.id()==ID_struct);
   return static_cast<const class_typet &>(type);
 }
 
@@ -429,7 +426,7 @@ inline const class_typet &to_class_type(const typet &type)
 */
 inline class_typet &to_class_type(typet &type)
 {
-  assert(type.id()==ID_struct);
+  PRECONDITION(type.id()==ID_struct);
   return static_cast<class_typet &>(type);
 }
 
@@ -455,7 +452,7 @@ class union_typet:public struct_union_typet
 */
 inline const union_typet &to_union_type(const typet &type)
 {
-  assert(type.id()==ID_union);
+  PRECONDITION(type.id()==ID_union);
   return static_cast<const union_typet &>(type);
 }
 
@@ -464,7 +461,7 @@ inline const union_typet &to_union_type(const typet &type)
 */
 inline union_typet &to_union_type(typet &type)
 {
-  assert(type.id()==ID_union);
+  PRECONDITION(type.id()==ID_union);
   return static_cast<union_typet &>(type);
 }
 
@@ -508,9 +505,9 @@ class tag_typet:public typet
 */
 inline const tag_typet &to_tag_type(const typet &type)
 {
-  assert(type.id()==ID_c_enum_tag ||
-         type.id()==ID_struct_tag ||
-         type.id()==ID_union_tag);
+  PRECONDITION(type.id()==ID_c_enum_tag ||
+               type.id()==ID_struct_tag ||
+               type.id()==ID_union_tag);
   return static_cast<const tag_typet &>(type);
 }
 
@@ -519,9 +516,9 @@ inline const tag_typet &to_tag_type(const typet &type)
 */
 inline tag_typet &to_tag_type(typet &type)
 {
-  assert(type.id()==ID_c_enum_tag ||
-         type.id()==ID_struct_tag ||
-         type.id()==ID_union_tag);
+  PRECONDITION(type.id()==ID_c_enum_tag ||
+               type.id()==ID_struct_tag ||
+               type.id()==ID_union_tag);
   return static_cast<tag_typet &>(type);
 }
 
@@ -549,7 +546,7 @@ class struct_tag_typet:public tag_typet
 */
 inline const struct_tag_typet &to_struct_tag_type(const typet &type)
 {
-  assert(type.id()==ID_struct_tag);
+  PRECONDITION(type.id()==ID_struct_tag);
   return static_cast<const struct_tag_typet &>(type);
 }
 
@@ -558,7 +555,7 @@ inline const struct_tag_typet &to_struct_tag_type(const typet &type)
 */
 inline struct_tag_typet &to_struct_tag_type(typet &type)
 {
-  assert(type.id()==ID_struct_tag);
+  PRECONDITION(type.id()==ID_struct_tag);
   return static_cast<struct_tag_typet &>(type);
 }
 
@@ -586,7 +583,7 @@ class union_tag_typet:public tag_typet
 */
 inline const union_tag_typet &to_union_tag_type(const typet &type)
 {
-  assert(type.id()==ID_union_tag);
+  PRECONDITION(type.id()==ID_union_tag);
   return static_cast<const union_tag_typet &>(type);
 }
 
@@ -595,7 +592,7 @@ inline const union_tag_typet &to_union_tag_type(const typet &type)
 */
 inline union_tag_typet &to_union_tag_type(typet &type)
 {
-  assert(type.id()==ID_union_tag);
+  PRECONDITION(type.id()==ID_union_tag);
   return static_cast<union_tag_typet &>(type);
 }
 
@@ -632,7 +629,7 @@ class enumeration_typet:public typet
 */
 inline const enumeration_typet &to_enumeration_type(const typet &type)
 {
-  assert(type.id()==ID_enumeration);
+  PRECONDITION(type.id()==ID_enumeration);
   return static_cast<const enumeration_typet &>(type);
 }
 
@@ -641,7 +638,7 @@ inline const enumeration_typet &to_enumeration_type(const typet &type)
 */
 inline enumeration_typet &to_enumeration_type(typet &type)
 {
-  assert(type.id()==ID_enumeration);
+  PRECONDITION(type.id()==ID_enumeration);
   return static_cast<enumeration_typet &>(type);
 }
 
@@ -693,7 +690,7 @@ class c_enum_typet:public type_with_subtypet
 */
 inline const c_enum_typet &to_c_enum_type(const typet &type)
 {
-  assert(type.id()==ID_c_enum);
+  PRECONDITION(type.id()==ID_c_enum);
   return static_cast<const c_enum_typet &>(type);
 }
 
@@ -702,7 +699,7 @@ inline const c_enum_typet &to_c_enum_type(const typet &type)
 */
 inline c_enum_typet &to_c_enum_type(typet &type)
 {
-  assert(type.id()==ID_c_enum);
+  PRECONDITION(type.id()==ID_c_enum);
   return static_cast<c_enum_typet &>(type);
 }
 
@@ -730,7 +727,7 @@ class c_enum_tag_typet:public tag_typet
 */
 inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type)
 {
-  assert(type.id()==ID_c_enum_tag);
+  PRECONDITION(type.id()==ID_c_enum_tag);
   return static_cast<const c_enum_tag_typet &>(type);
 }
 
@@ -739,7 +736,7 @@ inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type)
 */
 inline c_enum_tag_typet &to_c_enum_tag_type(typet &type)
 {
-  assert(type.id()==ID_c_enum_tag);
+  PRECONDITION(type.id()==ID_c_enum_tag);
   return static_cast<c_enum_tag_typet &>(type);
 }
 
@@ -907,7 +904,7 @@ class code_typet:public typet
 */
 inline const code_typet &to_code_type(const typet &type)
 {
-  assert(type.id()==ID_code);
+  PRECONDITION(type.id()==ID_code);
   return static_cast<const code_typet &>(type);
 }
 
@@ -916,7 +913,7 @@ inline const code_typet &to_code_type(const typet &type)
 */
 inline code_typet &to_code_type(typet &type)
 {
-  assert(type.id()==ID_code);
+  PRECONDITION(type.id()==ID_code);
   return static_cast<code_typet &>(type);
 }
 
@@ -969,7 +966,7 @@ class array_typet:public type_with_subtypet
 */
 inline const array_typet &to_array_type(const typet &type)
 {
-  assert(type.id()==ID_array);
+  PRECONDITION(type.id()==ID_array);
   return static_cast<const array_typet &>(type);
 }
 
@@ -978,7 +975,7 @@ inline const array_typet &to_array_type(const typet &type)
 */
 inline array_typet &to_array_type(typet &type)
 {
-  assert(type.id()==ID_array);
+  PRECONDITION(type.id()==ID_array);
   return static_cast<array_typet &>(type);
 }
 
@@ -1009,7 +1006,7 @@ class incomplete_array_typet:public type_with_subtypet
 */
 inline const incomplete_array_typet &to_incomplete_array_type(const typet &type)
 {
-  assert(type.id()==ID_array);
+  PRECONDITION(type.id()==ID_array);
   return static_cast<const incomplete_array_typet &>(type);
 }
 
@@ -1018,7 +1015,7 @@ inline const incomplete_array_typet &to_incomplete_array_type(const typet &type)
 */
 inline incomplete_array_typet &to_incomplete_array_type(typet &type)
 {
-  assert(type.id()==ID_array);
+  PRECONDITION(type.id()==ID_array);
   return static_cast<incomplete_array_typet &>(type);
 }
 
@@ -1074,32 +1071,32 @@ class bitvector_typet:public type_with_subtypet
 */
 inline const bitvector_typet &to_bitvector_type(const typet &type)
 {
-  assert(type.id()==ID_signedbv ||
-         type.id()==ID_unsignedbv ||
-         type.id()==ID_fixedbv ||
-         type.id()==ID_floatbv ||
-         type.id()==ID_verilog_signedbv ||
-         type.id()==ID_verilog_unsignedbv ||
-         type.id()==ID_bv ||
-         type.id()==ID_pointer ||
-         type.id()==ID_c_bit_field ||
-         type.id()==ID_c_bool);
+  PRECONDITION(type.id()==ID_signedbv ||
+               type.id()==ID_unsignedbv ||
+               type.id()==ID_fixedbv ||
+               type.id()==ID_floatbv ||
+               type.id()==ID_verilog_signedbv ||
+               type.id()==ID_verilog_unsignedbv ||
+               type.id()==ID_bv ||
+               type.id()==ID_pointer ||
+               type.id()==ID_c_bit_field ||
+               type.id()==ID_c_bool);
 
   return static_cast<const bitvector_typet &>(type);
 }
 
 inline bitvector_typet &to_bitvector_type(typet &type)
 {
-  assert(type.id()==ID_signedbv ||
-         type.id()==ID_unsignedbv ||
-         type.id()==ID_fixedbv ||
-         type.id()==ID_floatbv ||
-         type.id()==ID_verilog_signedbv ||
-         type.id()==ID_verilog_unsignedbv ||
-         type.id()==ID_bv ||
-         type.id()==ID_pointer ||
-         type.id()==ID_c_bit_field ||
-         type.id()==ID_c_bool);
+  PRECONDITION(type.id()==ID_signedbv ||
+               type.id()==ID_unsignedbv ||
+               type.id()==ID_fixedbv ||
+               type.id()==ID_floatbv ||
+               type.id()==ID_verilog_signedbv ||
+               type.id()==ID_verilog_unsignedbv ||
+               type.id()==ID_bv ||
+               type.id()==ID_pointer ||
+               type.id()==ID_c_bit_field ||
+               type.id()==ID_c_bool);
 
   return static_cast<bitvector_typet &>(type);
 }
@@ -1131,7 +1128,7 @@ class bv_typet:public bitvector_typet
 */
 inline const bv_typet &to_bv_type(const typet &type)
 {
-  assert(type.id()==ID_bv);
+  PRECONDITION(type.id()==ID_bv);
   return static_cast<const bv_typet &>(type);
 }
 
@@ -1140,7 +1137,7 @@ inline const bv_typet &to_bv_type(const typet &type)
 */
 inline bv_typet &to_bv_type(typet &type)
 {
-  assert(type.id()==ID_bv);
+  PRECONDITION(type.id()==ID_bv);
   return static_cast<bv_typet &>(type);
 }
 
@@ -1177,7 +1174,7 @@ class unsignedbv_typet:public bitvector_typet
 */
 inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
 {
-  assert(type.id()==ID_unsignedbv);
+  PRECONDITION(type.id()==ID_unsignedbv);
   return static_cast<const unsignedbv_typet &>(type);
 }
 
@@ -1186,7 +1183,7 @@ inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
 */
 inline unsignedbv_typet &to_unsignedbv_type(typet &type)
 {
-  assert(type.id()==ID_unsignedbv);
+  PRECONDITION(type.id()==ID_unsignedbv);
   return static_cast<unsignedbv_typet &>(type);
 }
 
@@ -1223,7 +1220,7 @@ class signedbv_typet:public bitvector_typet
 */
 inline const signedbv_typet &to_signedbv_type(const typet &type)
 {
-  assert(type.id()==ID_signedbv);
+  PRECONDITION(type.id()==ID_signedbv);
   return static_cast<const signedbv_typet &>(type);
 }
 
@@ -1232,7 +1229,7 @@ inline const signedbv_typet &to_signedbv_type(const typet &type)
 */
 inline signedbv_typet &to_signedbv_type(typet &type)
 {
-  assert(type.id()==ID_signedbv);
+  PRECONDITION(type.id()==ID_signedbv);
   return static_cast<signedbv_typet &>(type);
 }
 
@@ -1270,7 +1267,7 @@ class fixedbv_typet:public bitvector_typet
 */
 inline const fixedbv_typet &to_fixedbv_type(const typet &type)
 {
-  assert(type.id()==ID_fixedbv);
+  PRECONDITION(type.id()==ID_fixedbv);
   return static_cast<const fixedbv_typet &>(type);
 }
 
@@ -1309,7 +1306,7 @@ class floatbv_typet:public bitvector_typet
 */
 inline const floatbv_typet &to_floatbv_type(const typet &type)
 {
-  assert(type.id()==ID_floatbv);
+  PRECONDITION(type.id()==ID_floatbv);
   return static_cast<const floatbv_typet &>(type);
 }
 
@@ -1342,7 +1339,7 @@ class c_bit_field_typet:public bitvector_typet
 */
 inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
 {
-  assert(type.id()==ID_c_bit_field);
+  PRECONDITION(type.id()==ID_c_bit_field);
   return static_cast<const c_bit_field_typet &>(type);
 }
 
@@ -1358,7 +1355,7 @@ inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
 */
 inline c_bit_field_typet &to_c_bit_field_type(typet &type)
 {
-  assert(type.id()==ID_c_bit_field);
+  PRECONDITION(type.id()==ID_c_bit_field);
   return static_cast<c_bit_field_typet &>(type);
 }
 
@@ -1390,7 +1387,8 @@ class pointer_typet:public bitvector_typet
 */
 inline const pointer_typet &to_pointer_type(const typet &type)
 {
-  assert(type.id()==ID_pointer);
+  PRECONDITION(type.id()==ID_pointer);
+  PRECONDITION(!type.get(ID_width).empty());
   return static_cast<const pointer_typet &>(type);
 }
 
@@ -1399,7 +1397,8 @@ inline const pointer_typet &to_pointer_type(const typet &type)
 */
 inline pointer_typet &to_pointer_type(typet &type)
 {
-  assert(type.id()==ID_pointer);
+  PRECONDITION(type.id()==ID_pointer);
+  PRECONDITION(!type.get(ID_width).empty());
   return static_cast<pointer_typet &>(type);
 }
 
@@ -1427,7 +1426,8 @@ class reference_typet:public pointer_typet
 */
 inline const reference_typet &to_reference_type(const typet &type)
 {
-  assert(type.id()==ID_pointer && type.get_bool(ID_C_reference));
+  PRECONDITION(type.id()==ID_pointer && type.get_bool(ID_C_reference));
+  PRECONDITION(!type.get(ID_width).empty());
   return static_cast<const reference_typet &>(type);
 }
 
@@ -1436,7 +1436,8 @@ inline const reference_typet &to_reference_type(const typet &type)
 */
 inline reference_typet &to_reference_type(typet &type)
 {
-  assert(type.id()==ID_pointer && type.get_bool(ID_C_reference));
+  PRECONDITION(type.id()==ID_pointer && type.get_bool(ID_C_reference));
+  PRECONDITION(!type.get(ID_width).empty());
   return static_cast<reference_typet &>(type);
 }
 
@@ -1474,7 +1475,7 @@ class c_bool_typet:public bitvector_typet
 */
 inline const c_bool_typet &to_c_bool_type(const typet &type)
 {
-  assert(type.id()==ID_c_bool);
+  PRECONDITION(type.id()==ID_c_bool);
   return static_cast<const c_bool_typet &>(type);
 }
 
@@ -1483,7 +1484,7 @@ inline const c_bool_typet &to_c_bool_type(const typet &type)
 */
 inline c_bool_typet &to_c_bool_type(typet &type)
 {
-  assert(type.id()==ID_c_bool);
+  PRECONDITION(type.id()==ID_c_bool);
   return static_cast<c_bool_typet &>(type);
 }
 
@@ -1509,7 +1510,7 @@ class string_typet:public typet
 */
 inline const string_typet &to_string_type(const typet &type)
 {
-  assert(type.id()==ID_string);
+  PRECONDITION(type.id()==ID_string);
   return static_cast<const string_typet &>(type);
 }
 
@@ -1547,7 +1548,7 @@ class range_typet:public typet
 */
 inline const range_typet &to_range_type(const typet &type)
 {
-  assert(type.id()==ID_range);
+  PRECONDITION(type.id()==ID_range);
   return static_cast<const range_typet &>(type);
 }
 
@@ -1590,7 +1591,7 @@ class vector_typet:public type_with_subtypet
 */
 inline const vector_typet &to_vector_type(const typet &type)
 {
-  assert(type.id()==ID_vector);
+  PRECONDITION(type.id()==ID_vector);
   return static_cast<const vector_typet &>(type);
 }
 
@@ -1599,7 +1600,7 @@ inline const vector_typet &to_vector_type(const typet &type)
 */
 inline vector_typet &to_vector_type(typet &type)
 {
-  assert(type.id()==ID_vector);
+  PRECONDITION(type.id()==ID_vector);
   return static_cast<vector_typet &>(type);
 }
 
@@ -1630,7 +1631,7 @@ class complex_typet:public type_with_subtypet
 */
 inline const complex_typet &to_complex_type(const typet &type)
 {
-  assert(type.id()==ID_complex);
+  PRECONDITION(type.id()==ID_complex);
   return static_cast<const complex_typet &>(type);
 }
 
@@ -1639,7 +1640,7 @@ inline const complex_typet &to_complex_type(const typet &type)
 */
 inline complex_typet &to_complex_type(typet &type)
 {
-  assert(type.id()==ID_complex);
+  PRECONDITION(type.id()==ID_complex);
   return static_cast<complex_typet &>(type);
 }