diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index b54831c7962..99a28ebfaad 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -79,6 +79,11 @@ class goto_checkt
     const irep_idt &function_identifier,
     goto_functiont &goto_function);
 
+  /// Fill the list of allocations \ref allocationst with <address, size> for
+  ///   every allocation instruction. Also check that each allocation is
+  ///   well-formed.
+  /// \param goto_functions: goto functions from which the allocations are to be
+  ///   collected
   void collect_allocations(const goto_functionst &goto_functions);
 
 protected:
@@ -87,10 +92,63 @@ class goto_checkt
   goto_programt::const_targett current_target;
   guard_managert guard_manager;
 
-  void check_rec(
-    const exprt &expr,
-    guardt &guard,
-    bool address);
+  /// Check an address-of expression:
+  ///  if it is a dereference then check the pointer
+  ///  if it is an index then address-check the array and then check the index
+  /// \param expr: the expression to be checked
+  /// \param guard: the condition for the check (unmodified here)
+  void check_rec_address(const exprt &expr, guardt &guard);
+
+  /// Check a logical operation: check each operand in separation while
+  /// extending the guarding condition as follows.
+  ///  a /\ b /\ c ==> check(a, TRUE), check(b, a), check (c, a /\ b)
+  ///  a \/ b \/ c ==> check(a, TRUE), check(b, ~a), check (c, ~a /\ ~b)
+  /// \param expr: the expression to be checked
+  /// \param guard: the condition for the check (extended with the previous
+  ///   operands (or their negations) for recursively calls)
+  void check_rec_logical_op(const exprt &expr, guardt &guard);
+
+  /// Check an if expression: check the if-condition alone, and then check the
+  ///   true/false-cases with the guard extended with if-condition and it's
+  ///   negation, respectively.
+  /// \param if_expr: the expression to be checked
+  /// \param guard: the condition for the check (extended with the (negation of
+  ///   the) if-condition for recursively calls)
+  void check_rec_if(const if_exprt &if_expr, guardt &guard);
+
+  /// Check that a member expression is valid:
+  /// - check the structure this expression is a member of (via pointer of its
+  ///   dereference)
+  /// - run pointer-validity check on `*(s+member_offset)' instead of
+  ///   `s->member' to avoid checking safety of `s'
+  /// - check all operands of the expression
+  /// \param member: the expression to be checked
+  /// \param guard: the condition for the check (unmodified here)
+  /// \return true if no more checks are required for \p member or its
+  ///   sub-expressions
+  bool check_rec_member(const member_exprt &member, guardt &guard);
+
+  /// Check that a division is valid: check for division by zero, overflow and
+  ///   NaN (for floating point numbers).
+  /// \param div_expr: the expression to be checked
+  /// \param guard: the condition for the check (unmodified here)
+  void check_rec_div(const div_exprt &div_expr, guardt &guard);
+
+  /// Check that an arithmetic operation is valid: overflow check, NaN-check
+  ///   (for floating point numbers), and pointer overflow check.
+  /// \param expr: the expression to be checked
+  /// \param guard: the condition for the check (unmodified here)
+  void check_rec_arithmetic_op(const exprt &expr, guardt &guard);
+
+  /// Recursively descend into \p expr and run the appropriate check for each
+  ///   sub-expression, while collecting the condition for the check in \p
+  ///   guard.
+  /// \param expr: the expression to be checked
+  /// \param guard: the condition for when the check should be made
+  void check_rec(const exprt &expr, guardt &guard);
+
+  /// Initiate the recursively analysis of \p expr with its `guard' set to TRUE.
+  /// \param expr: the expression to be checked
   void check(const exprt &expr);
 
   struct conditiont
@@ -123,11 +181,19 @@ class goto_checkt
 
   std::string array_name(const exprt &);
 
-  void add_guarded_claim(
-    const exprt &expr,
+  /// Include the \p asserted_expr in the code conditioned by the \p guard.
+  /// \param asserted_expr: expression to be asserted
+  /// \param comment: human readable comment
+  /// \param property_class: classification of the property
+  /// \param source_location: the source location of the original expression
+  /// \param src_expr: the original expression to be included in the comment
+  /// \param guard: the condition under which the asserted expression should be
+  ///   taken into account
+  void add_guarded_property(
+    const exprt &asserted_expr,
     const std::string &comment,
     const std::string &property_class,
-    const source_locationt &,
+    const source_locationt &source_location,
     const exprt &src_expr,
     const guardt &guard);
 
@@ -135,6 +201,10 @@ class goto_checkt
   typedef std::set<exprt> assertionst;
   assertionst assertions;
 
+  /// Remove all assertions containing the symbol in \p lhs as well as all
+  ///   assertions containing dereference.
+  /// \param lhs: the left-hand-side expression whose symbol should be
+  ///   invalidated
   void invalidate(const exprt &lhs);
 
   bool enable_bounds_check;
@@ -208,21 +278,14 @@ void goto_checkt::invalidate(const exprt &lhs)
   else if(lhs.id()==ID_symbol)
   {
     // clear all assertions about 'symbol'
-    find_symbols_sett find_symbols_set;
-    find_symbols_set.insert(to_symbol_expr(lhs).get_identifier());
+    find_symbols_sett find_symbols_set{to_symbol_expr(lhs).get_identifier()};
 
-    for(assertionst::iterator
-        it=assertions.begin();
-        it!=assertions.end();
-        ) // no it++
+    for(auto it = assertions.begin(); it != assertions.end();)
     {
-      assertionst::iterator next=it;
-      next++;
-
       if(has_symbol(*it, find_symbols_set) || has_subexpr(*it, ID_dereference))
-        assertions.erase(it);
-
-      it=next;
+        it = assertions.erase(it);
+      else
+        ++it;
     }
   }
   else
@@ -244,7 +307,7 @@ void goto_checkt::div_by_zero_check(
   exprt zero=from_integer(0, expr.op1().type());
   const notequal_exprt inequality(expr.op1(), std::move(zero));
 
-  add_guarded_claim(
+  add_guarded_property(
     inequality,
     "division by zero",
     "division-by-zero",
@@ -270,7 +333,7 @@ void goto_checkt::undefined_shift_check(
     binary_relation_exprt inequality(
       expr.distance(), ID_ge, from_integer(0, distance_type));
 
-    add_guarded_claim(
+    add_guarded_property(
       inequality,
       "shift distance is negative",
       "undefined-shift",
@@ -286,7 +349,7 @@ void goto_checkt::undefined_shift_check(
     exprt width_expr=
       from_integer(to_bitvector_type(op_type).get_width(), distance_type);
 
-    add_guarded_claim(
+    add_guarded_property(
       binary_relation_exprt(expr.distance(), ID_lt, std::move(width_expr)),
       "shift distance too large",
       "undefined-shift",
@@ -299,7 +362,7 @@ void goto_checkt::undefined_shift_check(
       binary_relation_exprt inequality(
         expr.op(), ID_ge, from_integer(0, op_type));
 
-      add_guarded_claim(
+      add_guarded_property(
         inequality,
         "shift operand is negative",
         "undefined-shift",
@@ -310,7 +373,7 @@ void goto_checkt::undefined_shift_check(
   }
   else
   {
-    add_guarded_claim(
+    add_guarded_property(
       false_exprt(),
       "shift of non-integer type",
       "undefined-shift",
@@ -332,7 +395,7 @@ void goto_checkt::mod_by_zero_check(
   exprt zero=from_integer(0, expr.op1().type());
   const notequal_exprt inequality(expr.op1(), std::move(zero));
 
-  add_guarded_claim(
+  add_guarded_property(
     inequality,
     "division by zero",
     "division-by-zero",
@@ -362,7 +425,7 @@ void goto_checkt::mod_overflow_check(const mod_exprt &expr, const guardt &guard)
     notequal_exprt minus_one_neq(
       expr.op1(), from_integer(-1, expr.op1().type()));
 
-    add_guarded_claim(
+    add_guarded_property(
       or_exprt(int_min_neq, minus_one_neq),
       "result of signed mod is not representable",
       "overflow",
@@ -413,7 +476,7 @@ void goto_checkt::conversion_check(
         const binary_relation_exprt no_overflow_lower(
           expr.op0(), ID_ge, from_integer(-power(2, new_width - 1), old_type));
 
-        add_guarded_claim(
+        add_guarded_property(
           and_exprt(no_overflow_lower, no_overflow_upper),
           "arithmetic overflow on signed type conversion",
           "overflow",
@@ -432,7 +495,7 @@ void goto_checkt::conversion_check(
           ID_le,
           from_integer(power(2, new_width - 1) - 1, old_type));
 
-        add_guarded_claim(
+        add_guarded_property(
           no_overflow_upper,
           "arithmetic overflow on unsigned to signed type conversion",
           "overflow",
@@ -453,7 +516,7 @@ void goto_checkt::conversion_check(
         const binary_relation_exprt no_overflow_lower(
           expr.op0(), ID_gt, lower.to_expr());
 
-        add_guarded_claim(
+        add_guarded_property(
           and_exprt(no_overflow_lower, no_overflow_upper),
           "arithmetic overflow on float to signed integer type conversion",
           "overflow",
@@ -476,7 +539,7 @@ void goto_checkt::conversion_check(
           const binary_relation_exprt no_overflow_lower(
             expr.op0(), ID_ge, from_integer(0, old_type));
 
-          add_guarded_claim(
+          add_guarded_property(
             no_overflow_lower,
             "arithmetic overflow on signed to unsigned type conversion",
             "overflow",
@@ -493,7 +556,7 @@ void goto_checkt::conversion_check(
           const binary_relation_exprt no_overflow_lower(
             expr.op0(), ID_ge, from_integer(0, old_type));
 
-          add_guarded_claim(
+          add_guarded_property(
             and_exprt(no_overflow_lower, no_overflow_upper),
             "arithmetic overflow on signed to unsigned type conversion",
             "overflow",
@@ -511,7 +574,7 @@ void goto_checkt::conversion_check(
         const binary_relation_exprt no_overflow_upper(
           expr.op0(), ID_le, from_integer(power(2, new_width) - 1, old_type));
 
-        add_guarded_claim(
+        add_guarded_property(
           no_overflow_upper,
           "arithmetic overflow on unsigned to unsigned type conversion",
           "overflow",
@@ -532,7 +595,7 @@ void goto_checkt::conversion_check(
         const binary_relation_exprt no_overflow_lower(
           expr.op0(), ID_gt, lower.to_expr());
 
-        add_guarded_claim(
+        add_guarded_property(
           and_exprt(no_overflow_lower, no_overflow_upper),
           "arithmetic overflow on float to unsigned integer type conversion",
           "overflow",
@@ -576,7 +639,7 @@ void goto_checkt::integer_overflow_check(
       equal_exprt minus_one_eq(
         expr.op1(), from_integer(-1, type));
 
-      add_guarded_claim(
+      add_guarded_property(
         not_exprt(and_exprt(int_min_eq, minus_one_eq)),
         "arithmetic overflow on signed division",
         "overflow",
@@ -597,7 +660,7 @@ void goto_checkt::integer_overflow_check(
       equal_exprt int_min_eq(
         expr.op0(), to_signedbv_type(type).smallest_expr());
 
-      add_guarded_claim(
+      add_guarded_property(
         not_exprt(int_min_eq),
         "arithmetic overflow on signed unary minus",
         "overflow",
@@ -696,7 +759,7 @@ void goto_checkt::integer_overflow_check(
       // a shift that's too far isn't an overflow;
       // a shift of zero isn't overflow;
       // else check the top bits
-      add_guarded_claim(
+      add_guarded_property(
         disjunction({neg_value_shift,
                      neg_dist_shift,
                      dist_too_large,
@@ -739,9 +802,9 @@ void goto_checkt::integer_overflow_check(
       std::string kind=
         type.id()==ID_unsignedbv?"unsigned":"signed";
 
-      add_guarded_claim(
+      add_guarded_property(
         not_exprt(overflow),
-        "arithmetic overflow on "+kind+" "+expr.id_string(),
+        "arithmetic overflow on " + kind + " " + expr.id_string(),
         "overflow",
         expr.find_source_location(),
         expr,
@@ -753,9 +816,9 @@ void goto_checkt::integer_overflow_check(
     std::string kind=
       type.id()==ID_unsignedbv?"unsigned":"signed";
 
-    add_guarded_claim(
+    add_guarded_property(
       not_exprt(overflow),
-      "arithmetic overflow on "+kind+" "+expr.id_string(),
+      "arithmetic overflow on " + kind + " " + expr.id_string(),
       "overflow",
       expr.find_source_location(),
       expr,
@@ -792,7 +855,7 @@ void goto_checkt::float_overflow_check(
 
       or_exprt overflow_check(op0_inf, not_exprt(new_inf));
 
-      add_guarded_claim(
+      add_guarded_property(
         overflow_check,
         "arithmetic overflow on floating-point typecast",
         "overflow",
@@ -805,7 +868,7 @@ void goto_checkt::float_overflow_check(
       // non-float-to-float
       const isinf_exprt new_inf(expr);
 
-      add_guarded_claim(
+      add_guarded_property(
         not_exprt(new_inf),
         "arithmetic overflow on floating-point typecast",
         "overflow",
@@ -826,7 +889,7 @@ void goto_checkt::float_overflow_check(
 
     or_exprt overflow_check(op0_inf, not_exprt(new_inf));
 
-    add_guarded_claim(
+    add_guarded_property(
       overflow_check,
       "arithmetic overflow on floating-point division",
       "overflow",
@@ -863,9 +926,9 @@ void goto_checkt::float_overflow_check(
         expr.id()==ID_minus?"subtraction":
         expr.id()==ID_mult?"multiplication":"";
 
-      add_guarded_claim(
+      add_guarded_property(
         overflow_check,
-        "arithmetic overflow on floating-point "+kind,
+        "arithmetic overflow on floating-point " + kind,
         "overflow",
         expr.find_source_location(),
         expr,
@@ -983,7 +1046,7 @@ void goto_checkt::nan_check(
   else
     UNREACHABLE;
 
-  add_guarded_claim(
+  add_guarded_property(
     boolean_negate(isnan),
     "NaN on " + expr.id_string(),
     "NaN",
@@ -1011,7 +1074,7 @@ void goto_checkt::pointer_rel_check(
     {
       exprt same_object=::same_object(expr.op0(), expr.op1());
 
-      add_guarded_claim(
+      add_guarded_property(
         same_object,
         "same object violation",
         "pointer",
@@ -1039,7 +1102,7 @@ void goto_checkt::pointer_overflow_check(
   exprt overflow("overflow-" + expr.id_string(), bool_typet());
   overflow.operands() = expr.operands();
 
-  add_guarded_claim(
+  add_guarded_property(
     not_exprt(overflow),
     "pointer arithmetic overflow on " + expr.id_string(),
     "overflow",
@@ -1064,9 +1127,9 @@ void goto_checkt::pointer_validity_check(
 
   for(const auto &c : conditions)
   {
-    add_guarded_claim(
+    add_guarded_property(
       c.assertion,
-      "dereference failure: "+c.description,
+      "dereference failure: " + c.description,
       "pointer dereference",
       expr.find_source_location(),
       expr,
@@ -1263,9 +1326,9 @@ void goto_checkt::bounds_check(
         binary_relation_exprt inequality(
           effective_offset, ID_ge, std::move(zero));
 
-        add_guarded_claim(
+        add_guarded_property(
           inequality,
-          name+" lower bound",
+          name + " lower bound",
           "array bounds",
           expr.find_source_location(),
           expr,
@@ -1320,9 +1383,9 @@ void goto_checkt::bounds_check(
       and_exprt(dynamic_object(pointer), not_exprt(malloc_object(pointer, ns))),
       inequality);
 
-    add_guarded_claim(
+    add_guarded_property(
       precond,
-      name+" dynamic object upper bound",
+      name + " dynamic object upper bound",
       "array bounds",
       expr.find_source_location(),
       expr,
@@ -1381,7 +1444,7 @@ void goto_checkt::bounds_check(
       ID_lt,
       type_size_opt.value());
 
-    add_guarded_claim(
+    add_guarded_property(
       implies_exprt(type_matches_size, inequality),
       name + " upper bound",
       "array bounds",
@@ -1397,9 +1460,9 @@ void goto_checkt::bounds_check(
     inequality.op1() = typecast_exprt::conditional_cast(
       inequality.op1(), inequality.op0().type());
 
-    add_guarded_claim(
+    add_guarded_property(
       implies_exprt(type_matches_size, inequality),
-      name+" upper bound",
+      name + " upper bound",
       "array bounds",
       expr.find_source_location(),
       expr,
@@ -1407,189 +1470,213 @@ void goto_checkt::bounds_check(
   }
 }
 
-void goto_checkt::add_guarded_claim(
-  const exprt &_expr,
+void goto_checkt::add_guarded_property(
+  const exprt &asserted_expr,
   const std::string &comment,
   const std::string &property_class,
   const source_locationt &source_location,
   const exprt &src_expr,
   const guardt &guard)
 {
-  exprt expr(_expr);
-
   // first try simplifier on it
-  if(enable_simplify)
-    simplify(expr, ns);
+  exprt simplified_expr =
+    enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr;
 
   // throw away trivial properties?
-  if(!retain_trivial && expr.is_true())
+  if(!retain_trivial && simplified_expr.is_true())
     return;
 
   // add the guard
+  exprt guarded_expr =
+    guard.is_true()
+      ? std::move(simplified_expr)
+      : implies_exprt{guard.as_expr(), std::move(simplified_expr)};
 
-  exprt new_expr;
-
-  if(guard.is_true())
-    new_expr.swap(expr);
-  else
-    new_expr = implies_exprt(guard.as_expr(), std::move(expr));
-
-  if(assertions.insert(new_expr).second)
+  if(assertions.insert(guarded_expr).second)
   {
-    goto_program_instruction_typet type=
-      enable_assert_to_assume?ASSUME:ASSERT;
-
-    goto_programt::targett t = new_code.add(goto_programt::instructiont(
-      static_cast<const codet &>(get_nil_irep()),
-      source_location,
-      type,
-      std::move(new_expr),
-      {}));
+    auto t = new_code.add(
+      enable_assert_to_assume ? goto_programt::make_assumption(
+                                  std::move(guarded_expr), source_location)
+                              : goto_programt::make_assertion(
+                                  std::move(guarded_expr), source_location));
 
     std::string source_expr_string;
     get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
 
-    t->source_location.set_comment(comment+" in "+source_expr_string);
+    t->source_location.set_comment(comment + " in " + source_expr_string);
     t->source_location.set_property_class(property_class);
   }
 }
 
-void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
+void goto_checkt::check_rec_address(const exprt &expr, guardt &guard)
 {
   // we don't look into quantifiers
-  if(expr.id()==ID_exists || expr.id()==ID_forall)
+  if(expr.id() == ID_exists || expr.id() == ID_forall)
     return;
 
-  if(address)
+  if(expr.id() == ID_dereference)
   {
-    if(expr.id()==ID_dereference)
-    {
-      assert(expr.operands().size()==1);
-      check_rec(expr.op0(), guard, false);
-    }
-    else if(expr.id()==ID_index)
-    {
-      assert(expr.operands().size()==2);
-      check_rec(expr.op0(), guard, true);
-      check_rec(expr.op1(), guard, false);
-    }
-    else
-    {
-      forall_operands(it, expr)
-        check_rec(*it, guard, true);
-    }
-    return;
+    check_rec(to_dereference_expr(expr).pointer(), guard);
   }
-
-  if(expr.id()==ID_address_of)
+  else if(expr.id() == ID_index)
   {
-    assert(expr.operands().size()==1);
-    check_rec(expr.op0(), guard, true);
-    return;
+    const index_exprt &index_expr = to_index_expr(expr);
+    check_rec_address(index_expr.array(), guard);
+    check_rec(index_expr.index(), guard);
   }
-  else if(expr.id()==ID_and || expr.id()==ID_or)
+  else
   {
-    if(!expr.is_boolean())
-      throw "`"+expr.id_string()+"' must be Boolean, but got "+
-            expr.pretty();
+    for(const auto &operand : expr.operands())
+      check_rec_address(operand, guard);
+  }
+}
 
-    guardt old_guard=guard;
+void goto_checkt::check_rec_logical_op(const exprt &expr, guardt &guard)
+{
+  INVARIANT(
+    expr.is_boolean(),
+    "`" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());
 
-    for(const auto &op : expr.operands())
-    {
-      if(!op.is_boolean())
-        throw "`"+expr.id_string()+"' takes Boolean operands only, but got "+
-              op.pretty();
+  guardt old_guard = guard;
 
-      check_rec(op, guard, false);
+  for(const auto &op : expr.operands())
+  {
+    INVARIANT(
+      op.is_boolean(),
+      "`" + expr.id_string() + "' takes Boolean operands only, but got " +
+        op.pretty());
 
-      if(expr.id()==ID_or)
-        guard.add(not_exprt(op));
-      else
-        guard.add(op);
-    }
+    check_rec(op, guard);
+    guard.add(expr.id() == ID_or ? boolean_negate(op) : op);
+  }
+
+  guard = std::move(old_guard);
+}
+
+void goto_checkt::check_rec_if(const if_exprt &if_expr, guardt &guard)
+{
+  INVARIANT(
+    if_expr.cond().is_boolean(),
+    "first argument of if must be boolean, but got " + if_expr.cond().pretty());
 
+  check_rec(if_expr.cond(), guard);
+
+  {
+    guardt old_guard = guard;
+    guard.add(if_expr.cond());
+    check_rec(if_expr.true_case(), guard);
     guard = std::move(old_guard);
-    return;
   }
-  else if(expr.id()==ID_if)
+
   {
-    if(expr.operands().size()!=3)
-      throw "if takes three arguments";
+    guardt old_guard = guard;
+    guard.add(not_exprt{if_expr.cond()});
+    check_rec(if_expr.false_case(), guard);
+    guard = std::move(old_guard);
+  }
+}
 
-    if(!expr.op0().is_boolean())
-    {
-      std::string msg=
-        "first argument of if must be boolean, but got "
-        +expr.op0().pretty();
-      throw msg;
-    }
+bool goto_checkt::check_rec_member(const member_exprt &member, guardt &guard)
+{
+  const dereference_exprt &deref = to_dereference_expr(member.struct_op());
 
-    check_rec(expr.op0(), guard, false);
+  check_rec(deref.pointer(), guard);
 
-    {
-      guardt old_guard=guard;
-      guard.add(expr.op0());
-      check_rec(expr.op1(), guard, false);
-      guard = std::move(old_guard);
-    }
+  // avoid building the following expressions when pointer_validity_check
+  // would return immediately anyway
+  if(!enable_pointer_check)
+    return true;
 
-    {
-      guardt old_guard=guard;
-      guard.add(not_exprt(expr.op0()));
-      check_rec(expr.op2(), guard, false);
-      guard = std::move(old_guard);
-    }
+  // we rewrite s->member into *(s+member_offset)
+  // to avoid requiring memory safety of the entire struct
+  auto member_offset_opt = member_offset_expr(member, ns);
 
-    return;
-  }
-  else if(expr.id()==ID_member &&
-          to_member_expr(expr).struct_op().id()==ID_dereference)
+  if(member_offset_opt.has_value())
   {
-    const member_exprt &member=to_member_expr(expr);
-    const dereference_exprt &deref=
-      to_dereference_expr(member.struct_op());
+    pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
+    new_pointer_type.subtype() = member.type();
 
-    check_rec(deref.pointer(), guard, false);
+    const exprt char_pointer = typecast_exprt::conditional_cast(
+      deref.pointer(), pointer_type(char_type()));
 
-    // avoid building the following expressions when pointer_validity_check
-    // would return immediately anyway
-    if(!enable_pointer_check)
-      return;
+    const exprt new_address_casted = typecast_exprt::conditional_cast(
+      typecast_exprt{
+        plus_exprt{char_pointer,
+                   typecast_exprt::conditional_cast(
+                     member_offset_opt.value(), pointer_diff_type())},
+        char_pointer.type()},
+      new_pointer_type);
 
-    // we rewrite s->member into *(s+member_offset)
-    // to avoid requiring memory safety of the entire struct
-    auto member_offset_opt = member_offset_expr(member, ns);
+    dereference_exprt new_deref{new_address_casted};
+    new_deref.add_source_location() = deref.source_location();
+    pointer_validity_check(new_deref, guard);
 
-    if(member_offset_opt.has_value())
-    {
-      pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
-      new_pointer_type.subtype() = expr.type();
+    return true;
+  }
+  return false;
+}
 
-      const exprt char_pointer =
-        typecast_exprt::conditional_cast(
-          deref.pointer(), pointer_type(char_type()));
+void goto_checkt::check_rec_div(const div_exprt &div_expr, guardt &guard)
+{
+  div_by_zero_check(to_div_expr(div_expr), guard);
 
-      const exprt new_address = typecast_exprt(
-        plus_exprt(
-          char_pointer,
-          typecast_exprt::conditional_cast(
-            member_offset_opt.value(), pointer_diff_type())),
-        char_pointer.type());
+  if(div_expr.type().id() == ID_signedbv)
+    integer_overflow_check(div_expr, guard);
+  else if(div_expr.type().id() == ID_floatbv)
+  {
+    nan_check(div_expr, guard);
+    float_overflow_check(div_expr, guard);
+  }
+}
 
-      const exprt new_address_casted =
-        typecast_exprt::conditional_cast(new_address, new_pointer_type);
+void goto_checkt::check_rec_arithmetic_op(const exprt &expr, guardt &guard)
+{
+  if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
+  {
+    integer_overflow_check(expr, guard);
+  }
+  else if(expr.type().id() == ID_floatbv)
+  {
+    nan_check(expr, guard);
+    float_overflow_check(expr, guard);
+  }
+  else if(expr.type().id() == ID_pointer)
+  {
+    pointer_overflow_check(expr, guard);
+  }
+}
 
-      dereference_exprt new_deref{new_address_casted};
-      new_deref.add_source_location() = deref.source_location();
-      pointer_validity_check(new_deref, guard);
+void goto_checkt::check_rec(const exprt &expr, guardt &guard)
+{
+  // we don't look into quantifiers
+  if(expr.id() == ID_exists || expr.id() == ID_forall)
+    return;
 
+  if(expr.id() == ID_address_of)
+  {
+    check_rec_address(to_address_of_expr(expr).object(), guard);
+    return;
+  }
+  else if(expr.id() == ID_and || expr.id() == ID_or)
+  {
+    check_rec_logical_op(expr, guard);
+    return;
+  }
+  else if(expr.id() == ID_if)
+  {
+    check_rec_if(to_if_expr(expr), guard);
+    return;
+  }
+  else if(
+    expr.id() == ID_member &&
+    to_member_expr(expr).struct_op().id() == ID_dereference)
+  {
+    if(check_rec_member(to_member_expr(expr), guard))
       return;
-    }
   }
 
   forall_operands(it, expr)
-    check_rec(*it, guard, false);
+    check_rec(*it, guard);
 
   if(expr.id()==ID_index)
   {
@@ -1597,15 +1684,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
   }
   else if(expr.id()==ID_div)
   {
-    div_by_zero_check(to_div_expr(expr), guard);
-
-    if(expr.type().id()==ID_signedbv)
-      integer_overflow_check(expr, guard);
-    else if(expr.type().id()==ID_floatbv)
-    {
-      nan_check(expr, guard);
-      float_overflow_check(expr, guard);
-    }
+    check_rec_div(to_div_expr(expr), guard);
   }
   else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr)
   {
@@ -1623,20 +1702,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
           expr.id()==ID_mult ||
           expr.id()==ID_unary_minus)
   {
-    if(expr.type().id()==ID_signedbv ||
-       expr.type().id()==ID_unsignedbv)
-    {
-      integer_overflow_check(expr, guard);
-    }
-    else if(expr.type().id()==ID_floatbv)
-    {
-      nan_check(expr, guard);
-      float_overflow_check(expr, guard);
-    }
-    else if(expr.type().id()==ID_pointer)
-    {
-      pointer_overflow_check(expr, guard);
-    }
+    check_rec_arithmetic_op(expr, guard);
   }
   else if(expr.id()==ID_typecast)
     conversion_check(expr, guard);
@@ -1652,7 +1718,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
 void goto_checkt::check(const exprt &expr)
 {
   guardt guard{true_exprt{}, guard_manager};
-  check_rec(expr, guard, false);
+  check_rec(expr, guard);
 }
 
 /// expand the r_ok and w_ok predicates
@@ -1798,15 +1864,10 @@ void goto_checkt::goto_check(
     {
       if(std::find(i.labels.begin(), i.labels.end(), label)!=i.labels.end())
       {
-        goto_program_instruction_typet type=
-          enable_assert_to_assume?ASSUME:ASSERT;
-
-        goto_programt::targett t = new_code.add(goto_programt::instructiont(
-          static_cast<const codet &>(get_nil_irep()),
-          i.source_location,
-          type,
-          false_exprt(),
-          {}));
+        auto t = new_code.add(
+          enable_assert_to_assume
+            ? goto_programt::make_assumption(false_exprt{}, i.source_location)
+            : goto_programt::make_assertion(false_exprt{}, i.source_location));
 
         t->source_location.set_property_class("error label");
         t->source_location.set_comment("error label "+label);
@@ -1873,7 +1934,7 @@ void goto_checkt::goto_check(
             pointer,
             null_pointer_exprt(to_pointer_type(pointer.type())));
 
-          add_guarded_claim(
+          add_guarded_property(
             not_eq_null,
             "this is null on method invocation",
             "pointer dereference",
@@ -1922,7 +1983,7 @@ void goto_checkt::goto_check(
         const notequal_exprt not_eq_null(
           pointer, null_pointer_exprt(to_pointer_type(pointer.type())));
 
-        add_guarded_claim(
+        add_guarded_property(
           not_eq_null,
           "throwing null",
           "pointer dereference",
@@ -1997,7 +2058,7 @@ void goto_checkt::goto_check(
         equal_exprt eq(
           leak_expr,
           null_pointer_exprt(to_pointer_type(leak.type)));
-        add_guarded_claim(
+        add_guarded_property(
           eq,
           "dynamically allocated memory never freed",
           "memory-leak",