diff --git a/jbmc/regression/jbmc-generics/constant_propagation/Generic.class b/jbmc/regression/jbmc-generics/constant_propagation/Generic.class
new file mode 100644
index 00000000000..aa709de18f1
Binary files /dev/null and b/jbmc/regression/jbmc-generics/constant_propagation/Generic.class differ
diff --git a/jbmc/regression/jbmc-generics/constant_propagation/GenericSub.class b/jbmc/regression/jbmc-generics/constant_propagation/GenericSub.class
new file mode 100644
index 00000000000..208befc45c1
Binary files /dev/null and b/jbmc/regression/jbmc-generics/constant_propagation/GenericSub.class differ
diff --git a/jbmc/regression/jbmc-generics/constant_propagation/Test.class b/jbmc/regression/jbmc-generics/constant_propagation/Test.class
new file mode 100644
index 00000000000..c339d158cf7
Binary files /dev/null and b/jbmc/regression/jbmc-generics/constant_propagation/Test.class differ
diff --git a/jbmc/regression/jbmc-generics/constant_propagation/Test.java b/jbmc/regression/jbmc-generics/constant_propagation/Test.java
new file mode 100644
index 00000000000..2c71fc754a0
--- /dev/null
+++ b/jbmc/regression/jbmc-generics/constant_propagation/Test.java
@@ -0,0 +1,27 @@
+public class Test {
+  public static void main() {
+    Generic<Integer> g = new GenericSub<Integer>();
+
+    int x = 0;
+    for(int i = 0; i < 1000; ++i)
+      x += g.get();
+
+    assert x == 0;
+  }
+}
+
+class Generic<T> {
+  T key;
+  int x;
+
+  public int get() { return 0; }
+
+  public Generic() {
+    key = null;
+    x = 5;
+  }
+}
+
+class GenericSub<S> extends Generic<S> {
+  public int get() { return x; }
+}
diff --git a/jbmc/regression/jbmc-generics/constant_propagation/test.desc b/jbmc/regression/jbmc-generics/constant_propagation/test.desc
new file mode 100644
index 00000000000..31756c1b722
--- /dev/null
+++ b/jbmc/regression/jbmc-generics/constant_propagation/test.desc
@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.main --show-vcc
+^EXIT=0$
+^SIGNAL=0$
+^\{-\d+\} symex_dynamic::dynamic_object1#3 = \{ \{ \{ "java::GenericSub" \}, NULL, 0 \} \}$
+^\{-\d+\} symex_dynamic::dynamic_object1#4 = \{ \{ \{ "java::GenericSub" \}, NULL, 5 \} \}$
+--
+byte_extract_(big|little)_endian
+--
+The use of generics should not result in any byte_extract operations being
+generated for this test.
diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp
index 09e1381a009..893cfb8dc7b 100644
--- a/jbmc/unit/java-testing-utils/require_type.cpp
+++ b/jbmc/unit/java-testing-utils/require_type.cpp
@@ -9,7 +9,6 @@ Author: Diffblue Ltd.
 #include "require_type.h"
 
 #include <testing-utils/use_catch.h>
-#include <util/base_type.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 
@@ -26,10 +25,8 @@ pointer_typet require_type::require_pointer(
   const pointer_typet &pointer = to_pointer_type(type);
 
   if(subtype)
-  {
-    namespacet ns{symbol_tablet{}};
-    base_type_eq(pointer.subtype(), subtype.value(), ns);
-  }
+    REQUIRE(pointer.subtype() == subtype.value());
+
   return pointer;
 }
 
diff --git a/regression/cbmc/Pointer_byte_extract4/program-only.desc b/regression/cbmc/Pointer_byte_extract4/program-only.desc
new file mode 100644
index 00000000000..7b738a3b40b
--- /dev/null
+++ b/regression/cbmc/Pointer_byte_extract4/program-only.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+: dynamic_object1#\d+\) WITH
+--
+The above pattern makes sure we don't have a conditional choice of objects
+within a "with" expression. We avoid having this by running the simplifier after
+dereferencing.
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 9be0cdf1b51..5771b74a693 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -17,7 +17,6 @@ Author: Peter Schrammel
 #endif
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
@@ -103,7 +102,7 @@ void constant_propagator_domaint::assign_rec(
     if(dest_values.is_constant(tmp))
     {
       DATA_INVARIANT(
-        base_type_eq(ns.lookup(s).type, tmp.type(), ns),
+        ns.lookup(s).type == tmp.type(),
         "type of constant to be replaced should match");
       dest_values.set_to(s, tmp);
     }
@@ -624,7 +623,7 @@ bool constant_propagator_domaint::valuest::meet(
     {
       const typet &m_id_type = ns.lookup(m.first).type;
       DATA_INVARIANT(
-        base_type_eq(m_id_type, m.second.type(), ns),
+        m_id_type == m.second.type(),
         "type of constant to be stored should match");
       set_to(symbol_exprt(m.first, m_id_type), m.second);
       changed=true;
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index 34fae6f31ce..037c3ec8257 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "dump_c.h"
 
-#include <util/base_type.h>
 #include <util/config.h>
 #include <util/find_symbols.h>
 #include <util/invariant.h>
@@ -1277,9 +1276,9 @@ void dump_ct::cleanup_expr(exprt &expr)
       expr.swap(tmp);
     }
   }
-  else if(expr.id()==ID_typecast &&
-      expr.op0().id()==ID_typecast &&
-      base_type_eq(expr.type(), expr.op0().type(), ns))
+  else if(
+    expr.id() == ID_typecast && expr.op0().id() == ID_typecast &&
+    expr.type() == expr.op0().type())
   {
     exprt tmp=expr.op0();
     expr.swap(tmp);
@@ -1309,8 +1308,7 @@ void dump_ct::cleanup_expr(exprt &expr)
           if(type.id()==ID_union &&
              type.get_bool(ID_C_transparent_union))
           {
-            if(it2->id()==ID_typecast &&
-               base_type_eq(it2->type(), type, ns))
+            if(it2->id() == ID_typecast && it2->type() == type)
               *it2=to_typecast_expr(*it2).op();
 
             // add a typecast for NULL or 0
diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp
index fdb8fd9c287..8298e804f62 100644
--- a/src/goto-programs/goto_inline_class.cpp
+++ b/src/goto-programs/goto_inline_class.cpp
@@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #endif
 
-#include <util/base_type.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
@@ -83,7 +82,7 @@ void goto_inlinet::parameter_assignments(
     {
       // it should be the same exact type as the parameter,
       // subject to some exceptions
-      if(!base_type_eq(parameter_type, actual.type(), ns))
+      if(parameter_type != actual.type())
       {
         const typet &f_partype = parameter_type;
         const typet &f_acttype = actual.type();
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index 52976fcc21e..491954821f9 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ostream>
 #include <iomanip>
 
+#include <util/base_type.h>
 #include <util/expr_iterator.h>
 #include <util/find_symbols.h>
 #include <util/invariant.h>
@@ -715,10 +716,9 @@ void goto_programt::instructiont::validate(
             // Return removal sets the return type of a function symbol table
             // entry to 'void', but some callsites still expect the original
             // type (e.g. if a function is passed as a parameter)
-            symbol_expr_type_matches_symbol_table = base_type_eq(
-              goto_symbol_expr.type(),
-              original_return_type(ns.get_symbol_table(), goto_id),
-              ns);
+            symbol_expr_type_matches_symbol_table =
+              goto_symbol_expr.type() ==
+              original_return_type(ns.get_symbol_table(), goto_id);
 
             if(
               !symbol_expr_type_matches_symbol_table &&
@@ -760,8 +760,8 @@ void goto_programt::instructiont::validate(
               auto symbol_table_array_type = to_array_type(table_symbol->type);
               symbol_table_array_type.size() = nil_exprt();
 
-              symbol_expr_type_matches_symbol_table = base_type_eq(
-                goto_symbol_expr.type(), symbol_table_array_type, ns);
+              symbol_expr_type_matches_symbol_table =
+                goto_symbol_expr.type() == symbol_table_array_type;
             }
           }
 
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 0cb93ae8581..4e919938376 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening
 
 #include "graphml_witness.h"
 
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/arith_tools.h>
@@ -75,8 +74,9 @@ std::string graphml_witnesst::convert_assign_rec(
   {
     // dereferencing may have resulted in an lhs that is the first
     // struct member; undo this
-    if(assign.lhs().id()==ID_member &&
-       !base_type_eq(assign.lhs().type(), assign.rhs().type(), ns))
+    if(
+      assign.lhs().id() == ID_member &&
+      assign.lhs().type() != assign.rhs().type())
     {
       code_assignt tmp=assign;
       tmp.lhs()=to_member_expr(assign.lhs()).struct_op();
diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp
index 50f82b912b1..89013c9bafd 100644
--- a/src/goto-programs/wp.cpp
+++ b/src/goto-programs/wp.cpp
@@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_expr.h>
 #include <util/std_code.h>
-#include <util/base_type.h>
 
 #include <util/invariant.h>
 
@@ -79,7 +78,7 @@ aliasingt aliasing(
     return aliasing(e1, e2.op0().op0(), ns);
 
   // fairly radical. Ignores struct prefixes and the like.
-  if(!base_type_eq(e1.type(), e2.type(), ns))
+  if(e1.type() != e2.type())
     return aliasingt::A_MUSTNOT;
 
   // syntactically the same?
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index f9a87afbef8..43dc2d5942d 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -27,8 +27,7 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
   exprt rhs=code.rhs();
 
   DATA_INVARIANT(
-    base_type_eq(lhs.type(), rhs.type(), ns),
-    "assignments must be type consistent");
+    lhs.type() == rhs.type(), "assignments must be type consistent");
 
   clean_expr(lhs, state, true);
   clean_expr(rhs, state, false);
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 05b497e0350..ee764424c66 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
@@ -37,7 +36,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
     process_array_expr(if_expr.true_case(), do_simplify, ns);
     process_array_expr(if_expr.false_case(), do_simplify, ns);
 
-    if(!base_type_eq(if_expr.true_case(), if_expr.false_case(), ns))
+    if(if_expr.true_case() != if_expr.false_case())
     {
       byte_extract_exprt be(
         byte_extract_id(),
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 20f65da8854..0ee52397901 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -12,10 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
 
@@ -60,7 +60,7 @@ exprt goto_symext::address_arithmetic(
 
       // turn &a of type T[i][j] into &(a[0][0])
       for(const typet *t = &(a.type().subtype());
-          t->id() == ID_array && !base_type_eq(expr.type(), *t, ns);
+          t->id() == ID_array && expr.type() != *t;
           t = &(t->subtype()))
         a.object()=index_exprt(a.object(), from_integer(0, index_type()));
     }
@@ -183,9 +183,10 @@ exprt goto_symext::address_arithmetic(
       "goto_symext::address_arithmetic does not handle " + expr.id_string());
 
   const typet &expr_type = expr.type();
-  INVARIANT((expr_type.id()==ID_array && !keep_array) ||
-            base_type_eq(pointer_type(expr_type), result.type(), ns),
-            "either non-persistent array or pointer to result");
+  INVARIANT(
+    (expr_type.id() == ID_array && !keep_array) ||
+      pointer_type(expr_type) == result.type(),
+    "either non-persistent array or pointer to result");
 
   return result;
 }
@@ -285,12 +286,11 @@ void goto_symext::dereference_rec(exprt &expr, statet &state)
     exprt &tc_op=to_typecast_expr(expr).op();
 
     // turn &array into &array[0] when casting to pointer-to-element-type
-    if(tc_op.id()==ID_address_of &&
-       to_address_of_expr(tc_op).object().type().id()==ID_array &&
-       base_type_eq(
-         expr.type(),
-         pointer_type(to_address_of_expr(tc_op).object().type().subtype()),
-         ns))
+    if(
+      tc_op.id() == ID_address_of &&
+      to_address_of_expr(tc_op).object().type().id() == ID_array &&
+      expr.type() ==
+        pointer_type(to_address_of_expr(tc_op).object().type().subtype()))
     {
       expr=
         address_of_exprt(
@@ -363,4 +363,30 @@ void goto_symext::dereference(exprt &expr, statet &state)
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
   expr = state.rename<L1>(std::move(l1_expr), ns);
+
+  // Dereferencing is likely to introduce new member-of-if constructs --
+  // for example, "x->field" may have become "(x == &o1 ? o1 : o2).field."
+  // Run expression simplification, which converts that to
+  // (x == &o1 ? o1.field : o2.field))
+  // before applying field sensitivity. Field sensitivity can then turn such
+  // field-of-symbol expressions into atomic SSA expressions instead of having
+  // to rewrite all of 'o1' otherwise.
+  // Even without field sensitivity this can be beneficial: for example,
+  // "(b ? s1 : s2).member := X" results in
+  // (b ? s1 : s2) := (b ? s1 : s2) with (member := X)
+  // and then
+  // s1 := b ? ((b ? s1 : s2) with (member := X)) : s1
+  // when all we need is
+  // s1 := s1 with (member := X) [and guard b]
+  // s2 := s2 with (member := X) [and guard !b]
+  do_simplify(expr);
+
+  if(symex_config.run_validation_checks)
+  {
+    // make sure simplify has not re-introduced any dereferencing that
+    // had previously been cleaned away
+    INVARIANT(
+      !has_subexpr(expr, ID_dereference),
+      "simplify re-introduced dereferencing");
+  }
 }
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 36a27757a40..a5c4cec57bf 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
@@ -79,7 +78,7 @@ void goto_symext::parameter_assignments(
     else
     {
       // It should be the same exact type.
-      if(!base_type_eq(parameter_type, rhs.type(), ns))
+      if(parameter_type != rhs.type())
       {
         const typet &rhs_type = rhs.type();
 
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 7da7e61ef88..88c1dfdfa42 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
@@ -149,7 +148,7 @@ void goto_symext::symex_other(
     process_array_expr(state, src_array);
 
     // check for size (or type) mismatch and adjust
-    if(!base_type_eq(dest_array.type(), src_array.type(), ns))
+    if(dest_array.type() != src_array.type())
     {
       if(statement==ID_array_copy)
       {
@@ -217,7 +216,7 @@ void goto_symext::symex_other(
 
     const array_typet &array_type = to_array_type(array_expr.type());
 
-    if(!base_type_eq(array_type.subtype(), value.type(), ns))
+    if(array_type.subtype() != value.type())
       value = typecast_exprt(value, array_type.subtype());
 
     code_assignt assignment(array_expr, array_of_exprt(value, array_type));
@@ -250,7 +249,7 @@ void goto_symext::symex_other(
     code_assignt assignment(code.op2(), equal_exprt(array1, array2));
 
     // check for size (or type) mismatch
-    if(!base_type_eq(array1.type(), array2.type(), ns))
+    if(array1.type() != array2.type())
       assignment.lhs() = false_exprt();
 
     symex_assign(state, assignment);
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 8075528bc09..bc03df4f282 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -940,7 +940,7 @@ void symex_target_equationt::SSA_stept::validate(
     validate_full_expr(ssa_rhs, ns, vm);
     DATA_CHECK(
       vm,
-      base_type_eq(ssa_lhs.get_original_expr().type(), ssa_rhs.type(), ns),
+      ssa_lhs.get_original_expr().type() == ssa_rhs.type(),
       "Type inequality in SSA assignment\nlhs-type: " +
         ssa_lhs.get_original_expr().type().id_string() +
         "\nrhs-type: " + ssa_rhs.type().id_string());
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 9ef0478aced..fc10f96bb63 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ostream>
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
 #include <util/prefix.h>
@@ -1155,10 +1154,10 @@ void value_sett::assign(
       }
       else
       {
-        if(!base_type_eq(rhs.type(), type, ns))
+        if(rhs.type() != lhs.type())
           throw "value_sett::assign type mismatch: "
                 "rhs.type():\n"+rhs.type().pretty()+"\n"+
-                "type:\n"+type.pretty();
+                "lhs.type():\n"+lhs.type().pretty();
 
         rhs_member=make_member(rhs, name, ns);
 
@@ -1183,7 +1182,7 @@ void value_sett::assign(
     }
     else
     {
-      if(!base_type_eq(rhs.type(), type, ns))
+      if(rhs.type() != type)
         throw "value_sett::assign type mismatch: "
           "rhs.type():\n"+rhs.type().pretty()+"\n"+
           "type:\n"+type.pretty();
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index fddb2a77568..cd05d712db0 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -18,7 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/array_name.h>
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/config.h>
@@ -208,7 +207,7 @@ bool value_set_dereferencet::dereference_type_compare(
 #endif
   }
 
-  if(base_type_eq(object_type, dereference_type, ns))
+  if(object_type == dereference_type)
     return true; // ok, they just match
 
   // check for struct prefixes
@@ -314,7 +313,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");
     const symbol_exprt symbol_expr(memory_symbol.name, memory_symbol.type);
 
-    if(base_type_eq(memory_symbol.type.subtype(), dereference_type, ns))
+    if(memory_symbol.type.subtype() == dereference_type)
     {
       // Types match already, what a coincidence!
       // We can use an index expression.
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 4a65e3d9729..1325fc9bdb2 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/symbol_table.h>
 #include <util/simplify_expr.h>
-#include <util/base_type.h>
 #include <util/std_expr.h>
 #include <util/prefix.h>
 #include <util/std_code.h>
@@ -990,10 +989,10 @@ void value_set_fit::assign(
       }
       else
       {
-        if(!base_type_eq(rhs.type(), type, ns))
+        if(rhs.type() != lhs.type())
           throw "value_set_fit::assign type mismatch: "
                 "rhs.type():\n"+rhs.type().pretty()+"\n"+
-                "type:\n"+type.pretty();
+                "type:\n"+lhs.type().pretty();
 
         if(rhs.id()==ID_struct ||
            rhs.id()==ID_constant)
@@ -1051,7 +1050,7 @@ void value_set_fit::assign(
     }
     else
     {
-      if(!base_type_eq(rhs.type(), type, ns))
+      if(rhs.type() != type)
         throw "value_set_fit::assign type mismatch: "
               "rhs.type():\n"+rhs.type().pretty()+"\n"+
               "type:\n"+type.pretty();
diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp
index 2deb17e0105..526c3c20112 100644
--- a/src/pointer-analysis/value_set_fivr.cpp
+++ b/src/pointer-analysis/value_set_fivr.cpp
@@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com,
 
 #include <util/symbol_table.h>
 #include <util/simplify_expr.h>
-#include <util/base_type.h>
 #include <util/std_expr.h>
 #include <util/prefix.h>
 #include <util/std_code.h>
@@ -1105,10 +1104,9 @@ void value_set_fivrt::assign(
       }
       else
       {
-        if(!base_type_eq(rhs.type(), type, ns))
-          throw
-            "type mismatch:\nRHS: "+rhs.type().pretty()+"\n"+
-            "LHS: "+type.pretty();
+        if(rhs.type() != lhs.type())
+          throw "type mismatch:\nRHS: " + rhs.type().pretty() + "\n" +
+            "LHS: " + lhs.type().pretty();
 
         if(rhs.id()==ID_struct ||
            rhs.id()==ID_constant)
@@ -1162,7 +1160,7 @@ void value_set_fivrt::assign(
     }
     else
     {
-      assert(base_type_eq(rhs.type(), type, ns));
+      DATA_INVARIANT(rhs.type() == type, "array type mismatch");
 
       if(rhs.id()==ID_array_of)
       {
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
index 1c0bbb93063..654add1b4be 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com,
 
 #include <util/symbol_table.h>
 #include <util/simplify_expr.h>
-#include <util/base_type.h>
 #include <util/std_expr.h>
 #include <util/prefix.h>
 #include <util/std_code.h>
@@ -798,10 +797,9 @@ void value_set_fivrnst::assign(
       }
       else
       {
-        if(!base_type_eq(rhs.type(), type, ns))
-          throw
-            "type mismatch:\nRHS: "+rhs.type().pretty()+"\n"+
-            "LHS: "+type.pretty();
+        if(rhs.type() != lhs.type())
+          throw "type mismatch:\nRHS: " + rhs.type().pretty() + "\n" +
+            "LHS: " + lhs.type().pretty();
 
         if(rhs.id()==ID_struct ||
            rhs.id()==ID_constant)
@@ -855,7 +853,7 @@ void value_set_fivrnst::assign(
     }
     else
     {
-      assert(base_type_eq(rhs.type(), type, ns));
+      DATA_INVARIANT(rhs.type() == type, "array type mismatch");
 
       if(rhs.id()==ID_array_of)
       {
diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index 1848033cb76..fe777e2b4e5 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "arrays.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/format_expr.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
@@ -47,7 +46,7 @@ literalt arrayst::record_array_equality(
   const exprt &op1=equality.op1();
 
   // check types
-  if(!base_type_eq(op0.type(), op1.type(), ns))
+  if(op0.type() != op1.type())
   {
     error() << equality.pretty() << messaget::eom;
     DATA_INVARIANT(
@@ -115,7 +114,7 @@ void arrayst::collect_arrays(const exprt &a)
     const with_exprt &with_expr=to_with_expr(a);
 
     // check types
-    if(!base_type_eq(array_type, with_expr.old().type(), ns))
+    if(array_type != with_expr.old().type())
     {
       error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
@@ -136,7 +135,7 @@ void arrayst::collect_arrays(const exprt &a)
     const update_exprt &update_expr=to_update_expr(a);
 
     // check types
-    if(!base_type_eq(array_type, update_expr.old().type(), ns))
+    if(array_type != update_expr.old().type())
     {
       error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(
@@ -158,14 +157,14 @@ void arrayst::collect_arrays(const exprt &a)
     const if_exprt &if_expr=to_if_expr(a);
 
     // check types
-    if(!base_type_eq(array_type, if_expr.true_case().type(), ns))
+    if(array_type != if_expr.true_case().type())
     {
       error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
     // check types
-    if(!base_type_eq(array_type, if_expr.false_case().type(), ns))
+    if(array_type != if_expr.false_case().type())
     {
       error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got if without matching types");
@@ -655,7 +654,7 @@ void arrayst::add_array_constraints_array_of(
     index_exprt index_expr(expr, index, subtype);
 
     DATA_INVARIANT(
-      base_type_eq(index_expr.type(), expr.what().type(), ns),
+      index_expr.type() == expr.what().type(),
       "array_of operand type should match array element type");
 
     // add constraint
diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp
index a3da6a332bc..1be84441cf2 100644
--- a/src/solvers/flattening/boolbv_equality.cpp
+++ b/src/solvers/flattening/boolbv_equality.cpp
@@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv.h"
 
 #include <util/std_expr.h>
-#include <util/base_type.h>
 #include <util/invariant.h>
 
 #include <solvers/lowering/expr_lowering.h>
@@ -18,10 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 literalt boolbvt::convert_equality(const equal_exprt &expr)
 {
-  const bool is_base_type_eq =
-    base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
+  const bool equality_types_match = expr.lhs().type() == expr.rhs().type();
   DATA_INVARIANT_WITH_DIAGNOSTICS(
-    is_base_type_eq,
+    equality_types_match,
     "types of expressions on each side of equality should match",
     irep_pretty_diagnosticst{expr.lhs()},
     irep_pretty_diagnosticst{expr.rhs()});
@@ -67,10 +65,8 @@ literalt boolbvt::convert_verilog_case_equality(
   // This is 4-valued comparison, i.e., z===z, x===x etc.
   // The result is always Boolean.
 
-  const bool is_base_type_eq =
-    base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
   DATA_INVARIANT_WITH_DIAGNOSTICS(
-    is_base_type_eq,
+    expr.lhs().type() == expr.rhs().type(),
     "lhs and rhs types should match in verilog_case_equality",
     irep_pretty_diagnosticst{expr.lhs()},
     irep_pretty_diagnosticst{expr.rhs()});
diff --git a/src/solvers/flattening/boolbv_member.cpp b/src/solvers/flattening/boolbv_member.cpp
index c1c96c119c7..6a78dda8609 100644
--- a/src/solvers/flattening/boolbv_member.cpp
+++ b/src/solvers/flattening/boolbv_member.cpp
@@ -8,8 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
-#include <util/base_type.h>
-
 bvt boolbvt::convert_member(const member_exprt &expr)
 {
   const exprt &struct_op=expr.struct_op();
@@ -31,7 +29,7 @@ bvt boolbvt::convert_member(const member_exprt &expr)
     if(c.get_name() == component_name)
     {
       DATA_INVARIANT_WITH_DIAGNOSTICS(
-        base_type_eq(subtype, expr.type(), ns),
+        subtype == expr.type(),
         "component type shall match the member expression type",
         subtype.pretty(),
         expr.type().pretty());
diff --git a/src/solvers/flattening/boolbv_struct.cpp b/src/solvers/flattening/boolbv_struct.cpp
index e5a589b915c..9121fcb581a 100644
--- a/src/solvers/flattening/boolbv_struct.cpp
+++ b/src/solvers/flattening/boolbv_struct.cpp
@@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 
 bvt boolbvt::convert_struct(const struct_exprt &expr)
 {
@@ -37,7 +36,7 @@ bvt boolbvt::convert_struct(const struct_exprt &expr)
     const exprt &op=*op_it;
 
     DATA_INVARIANT_WITH_DIAGNOSTICS(
-      base_type_eq(subtype, op.type(), ns),
+      subtype == op.type(),
       "type of a struct expression operand shall equal the type of the "
       "corresponding struct component",
       expr.find_source_location(),
diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp
index 27dd087f554..c068bee37a0 100644
--- a/src/solvers/flattening/boolbv_with.cpp
+++ b/src/solvers/flattening/boolbv_with.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 #include <util/std_expr.h>
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/config.h>
 
 #include "bv_endianness_map.h"
@@ -230,7 +229,7 @@ void boolbvt::convert_with_struct(
 
     if(c.get_name() == component_name)
     {
-      if(!base_type_eq(subtype, op2.type(), ns))
+      if(subtype != op2.type())
       {
         error().source_location=type.source_location();
         error() << "with/struct: component `" << component_name
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 15064214056..67d051b31d0 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "smt2_conv.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_util.h>
@@ -1078,7 +1077,7 @@ void smt2_convt::convert_expr(const exprt &expr)
     const equal_exprt &equal_expr = to_equal_expr(expr);
 
     DATA_INVARIANT(
-      base_type_eq(equal_expr.op0().type(), equal_expr.op1().type(), ns),
+      equal_expr.op0().type() == equal_expr.op1().type(),
       "operands of equal expression shall have same type");
 
     out << "(= ";
@@ -1092,7 +1091,7 @@ void smt2_convt::convert_expr(const exprt &expr)
     const notequal_exprt &notequal_expr = to_notequal_expr(expr);
 
     DATA_INVARIANT(
-      base_type_eq(notequal_expr.op0().type(), notequal_expr.op1().type(), ns),
+      notequal_expr.op0().type() == notequal_expr.op1().type(),
       "operands of not equal expression shall have same type");
 
     out << "(not (= ";
@@ -1110,7 +1109,7 @@ void smt2_convt::convert_expr(const exprt &expr)
       expr.operands().size() == 2,
       "float equal and not equal expressions must have two operands");
     DATA_INVARIANT(
-      base_type_eq(expr.op0().type(), expr.op1().type(), ns),
+      expr.op0().type() == expr.op1().type(),
       "operands of float equal and not equal expressions shall have same type");
 
     // The FPA theory properly treats NaN and negative zero.
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
index 0ee6dd582f4..70cd5b45e6b 100644
--- a/src/solvers/strings/string_refinement.cpp
+++ b/src/solvers/strings/string_refinement.cpp
@@ -330,7 +330,7 @@ static void add_equations_for_symbol_resolution(
       continue;
     }
 
-    if(!base_type_eq(lhs.type(), rhs.type(), ns))
+    if(lhs.type() != rhs.type())
     {
       stream << log_message << "non equal types lhs: " << format(lhs)
              << "\n####################### rhs: " << format(rhs) << eom;
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index fa1f8ac47bb..483b7b8b278 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "pointer_offset_size.h"
 
 #include "arith_tools.h"
-#include "base_type.h"
 #include "byte_operators.h"
 #include "c_types.h"
 #include "invariant.h"
@@ -631,7 +630,7 @@ optionalt<exprt> get_subexpression_at_offset(
   const typet &target_type_raw,
   const namespacet &ns)
 {
-  if(offset_bytes == 0 && base_type_eq(expr.type(), target_type_raw, ns))
+  if(offset_bytes == 0 && expr.type() == target_type_raw)
   {
     exprt result = expr;
 
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 2dbd236218f..8041720736b 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 
 #include "arith_tools.h"
-#include "base_type.h"
 #include "byte_operators.h"
 #include "c_types.h"
 #include "config.h"
@@ -470,8 +469,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
       {
         exprt result=expr.op0();
 
-        if(result.operands().size()>=1 &&
-           base_type_eq(result.op0().type(), result.type(), ns))
+        if(
+          result.operands().size() >= 1 && result.op0().type() == result.type())
         {
           result.type()=expr.type();
 
@@ -844,8 +843,9 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
     const exprt &o=to_address_of_expr(operand).object();
 
     // turn &array into &array[0] when casting to pointer-to-element-type
-    if(o.type().id()==ID_array &&
-       base_type_eq(expr_type, pointer_type(o.type().subtype()), ns))
+    if(
+      o.type().id() == ID_array &&
+      expr_type == pointer_type(o.type().subtype()))
     {
       expr=address_of_exprt(index_exprt(o, from_integer(0, size_type())));
 
@@ -1867,7 +1867,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
   {
     const auto &op_byte_update = to_byte_update_expr(expr.op());
 
-    if(base_type_eq(expr.type(), op_byte_update.value().type(), ns))
+    if(expr.type() == op_byte_update.value().type())
     {
       exprt tmp = op_byte_update.value();
       expr.swap(tmp);
@@ -1897,7 +1897,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
   if(*offset == 0 && byte_extract_id() == expr.id())
   {
     // byte extract of full object is object
-    if(base_type_eq(expr.type(), expr.op().type(), ns))
+    if(expr.type() == expr.op().type())
     {
       exprt tmp = expr.op();
       expr.swap(tmp);
@@ -2023,8 +2023,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
   if(
     expr.id() == expr.op().id() &&
     expr.offset() == to_byte_update_expr(expr.op()).offset() &&
-    base_type_eq(
-      expr.value().type(), to_byte_update_expr(expr.op()).value().type(), ns))
+    expr.value().type() == to_byte_update_expr(expr.op()).value().type())
   {
     expr.op()=expr.op().op0();
     return false;
@@ -2119,7 +2118,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
           simplify_node(index_offset);
 
           // index_offset may need a typecast
-          if(!base_type_eq(offset.type(), index.type(), ns))
+          if(offset.type() != index.type())
           {
             typecast_exprt tmp(index_offset, offset.type());
             simplify_node(tmp);
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index cdf5eff16f9..7e81fe61fac 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 
 #include "arith_tools.h"
-#include "base_type.h"
 #include "bv_arithmetic.h"
 #include "byte_operators.h"
 #include "config.h"
@@ -940,9 +939,7 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
   }
 
   // { x } = x
-  if(
-    expr.operands().size() == 1 &&
-    base_type_eq(expr.op0().type(), expr.type(), ns))
+  if(expr.operands().size() == 1 && expr.op0().type() == expr.type())
   {
     exprt tmp;
     tmp.swap(expr.op0());
@@ -1301,7 +1298,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
   exprt tmp1=expr.op1();
 
   // types must match
-  if(!base_type_eq(tmp0.type(), tmp1.type(), ns))
+  if(tmp0.type() != tmp1.type())
     return true;
 
   // if rhs is ID_if (and lhs is not), swap operands for == and !=
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index f09504d87fd..63544275632 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "simplify_expr_class.h"
 
 #include "arith_tools.h"
-#include "base_type.h"
 #include "byte_operators.h"
 #include "invariant.h"
 #include "namespace.h"
@@ -46,7 +45,7 @@ bool simplify_exprt::simplify_member(exprt &expr)
         {
           // found it!
           DATA_INVARIANT(
-            base_type_eq(op2.type(), expr.type(), ns),
+            op2.type() == expr.type(),
             "member expression type must match component type");
           exprt tmp;
           tmp.swap(op2);
@@ -138,7 +137,7 @@ bool simplify_exprt::simplify_member(exprt &expr)
       {
         std::size_t number=struct_type.component_number(component_name);
         DATA_INVARIANT(
-          base_type_eq(op.operands()[number].type(), expr.type(), ns),
+          op.operands()[number].type() == expr.type(),
           "member expression type must match component type");
         exprt tmp;
         tmp.swap(op.operands()[number]);
@@ -241,7 +240,7 @@ bool simplify_exprt::simplify_member(exprt &expr)
   {
     // Try to look through member(cast(x)) if the cast is between structurally
     // identical types:
-    if(base_type_eq(op_type, op.op0().type(), ns))
+    if(op_type == op.op0().type())
     {
       expr.op0() = op.op0();
       simplify_member(expr);
@@ -263,9 +262,6 @@ bool simplify_exprt::simplify_member(exprt &expr)
 
         // Guess: turning this into a byte-extract operation is not really an
         // optimisation.
-        // The type_eq check is because get_subexpression_at_offset uses
-        // base_type_eq, whereas in the context of a simplifier we should not
-        // change the type of the expression.
         if(
           equivalent_member.has_value() &&
           equivalent_member.value().id() != ID_byte_extract_little_endian &&
diff --git a/src/util/std_code.h b/src/util/std_code.h
index 8f62251aee0..8339c8c3ca2 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <list>
 
-#include "base_type.h"
 #include "expr.h"
 #include "expr_cast.h"
 #include "invariant.h"
@@ -326,14 +325,14 @@ class code_assignt:public codet
 
   static void validate(
     const codet &code,
-    const namespacet &ns,
+    const namespacet &,
     const validation_modet vm = validation_modet::INVARIANT)
   {
     check(code, vm);
 
     DATA_CHECK(
       vm,
-      base_type_eq(code.op0().type(), code.op1().type(), ns),
+      code.op0().type() == code.op1().type(),
       "lhs and rhs of assignment must have same type");
   }
 
@@ -1206,7 +1205,7 @@ class code_function_callt:public codet
 
   static void validate(
     const codet &code,
-    const namespacet &ns,
+    const namespacet &,
     const validation_modet vm = validation_modet::INVARIANT)
   {
     check(code, vm);
@@ -1214,8 +1213,7 @@ class code_function_callt:public codet
     if(code.op0().id() != ID_nil)
       DATA_CHECK(
         vm,
-        base_type_eq(
-          code.op0().type(), to_code_type(code.op1().type()).return_type(), ns),
+        code.op0().type() == to_code_type(code.op1().type()).return_type(),
         "function returns expression of wrong type");
   }
 
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index e2790ae3a67..ce911b25c2e 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file util/std_expr.h
 /// API to expression classes
 
-#include "base_type.h"
 #include "expr_cast.h"
 #include "invariant.h"
 #include "std_types.h"
@@ -868,7 +867,7 @@ class binary_relation_exprt:public binary_predicate_exprt
     // check types
     DATA_CHECK(
       vm,
-      base_type_eq(expr.op0().type(), expr.op1().type(), ns),
+      expr.op0().type() == expr.op1().type(),
       "lhs and rhs of binary relation expression should have same type");
   }