diff --git a/regression/cbmc-with-incr/Malloc17/main.c b/regression/cbmc-with-incr/Malloc17/main.c
index 192ed892ef7..77836c85203 100644
--- a/regression/cbmc-with-incr/Malloc17/main.c
+++ b/regression/cbmc-with-incr/Malloc17/main.c
@@ -4,7 +4,7 @@ unsigned char* init1()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(1, 0);
+  unsigned char *buffer = __CPROVER_allocate(1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -18,7 +18,7 @@ unsigned char* init2()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(1*sizeof(unsigned char), 0);
+  unsigned char *buffer = __CPROVER_allocate(1 * sizeof(unsigned char), 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -32,7 +32,7 @@ unsigned char* init3()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(sizeof(unsigned char)*1, 0);
+  unsigned char *buffer = __CPROVER_allocate(sizeof(unsigned char) * 1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
diff --git a/regression/cbmc-with-incr/Malloc18/main.c b/regression/cbmc-with-incr/Malloc18/main.c
index e993e4e457c..a80662e73d3 100644
--- a/regression/cbmc-with-incr/Malloc18/main.c
+++ b/regression/cbmc-with-incr/Malloc18/main.c
@@ -4,7 +4,7 @@ unsigned char* init()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(size, 0);
+  unsigned char *buffer = __CPROVER_allocate(size, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
diff --git a/regression/cbmc/Calloc1/main.c b/regression/cbmc/Calloc1/main.c
index 75ea31a41bd..0a006b14056 100644
--- a/regression/cbmc/Calloc1/main.c
+++ b/regression/cbmc/Calloc1/main.c
@@ -3,7 +3,7 @@
 
 int main()
 {
-  int *x=calloc(sizeof(int), 1);
-  assert(*x==0);
+  int *x = calloc(sizeof(int), 1);
+  assert(*x == 0);
   return 0;
 }
diff --git a/regression/cbmc/Malloc17/main.c b/regression/cbmc/Malloc17/main.c
index 192ed892ef7..77836c85203 100644
--- a/regression/cbmc/Malloc17/main.c
+++ b/regression/cbmc/Malloc17/main.c
@@ -4,7 +4,7 @@ unsigned char* init1()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(1, 0);
+  unsigned char *buffer = __CPROVER_allocate(1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -18,7 +18,7 @@ unsigned char* init2()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(1*sizeof(unsigned char), 0);
+  unsigned char *buffer = __CPROVER_allocate(1 * sizeof(unsigned char), 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -32,7 +32,7 @@ unsigned char* init3()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(sizeof(unsigned char)*1, 0);
+  unsigned char *buffer = __CPROVER_allocate(sizeof(unsigned char) * 1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
diff --git a/regression/cbmc/Malloc18/main.c b/regression/cbmc/Malloc18/main.c
index 88dd8de1e25..f5428a1387b 100644
--- a/regression/cbmc/Malloc18/main.c
+++ b/regression/cbmc/Malloc18/main.c
@@ -3,7 +3,7 @@ unsigned char* init()
   unsigned long buffer_size;
   if(buffer_size!=1) return 0;
 
-  unsigned char* buffer=__CPROVER_allocate(buffer_size, 0);
+  unsigned char *buffer = __CPROVER_allocate(buffer_size, 0);
   __CPROVER_assert(buffer!=0, "malloc did not return NULL");
 
   buffer[0]=10;
diff --git a/regression/cbmc/Malloc24/main.c b/regression/cbmc/Malloc24/main.c
index b7e5975d680..231ae323439 100644
--- a/regression/cbmc/Malloc24/main.c
+++ b/regression/cbmc/Malloc24/main.c
@@ -2,8 +2,8 @@
 
 struct node
 {
-    int value;
-    struct node *next;
+  int value;
+  struct node *next;
 };
 
 struct list
@@ -12,7 +12,7 @@ struct list
   struct node *head;
 };
 
-void removeLast(struct list * l)
+void removeLast(struct list *l)
 {
   int index = l->size - 1;
   struct node **current;
@@ -22,7 +22,8 @@ void removeLast(struct list * l)
   l->size--;
 }
 
-int main () {
+int main()
+{
   //build a 2-nodes list
   struct node *n0 = malloc(sizeof(struct node));
   struct node *n1 = malloc(sizeof(struct node));
@@ -30,8 +31,8 @@ int main () {
   l->size = 2;
   l->head = n0;
 
-  n0->next=n1;
-  n1->next=NULL;
+  n0->next = n1;
+  n1->next = NULL;
 
   //remove last node from list
 
@@ -43,5 +44,5 @@ int main () {
   //this doesn't
   removeLast(l);
 
-  __CPROVER_assert(n0->next == NULL , "not NULL");
+  __CPROVER_assert(n0->next == NULL, "not NULL");
 }
diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc
index d0d0ed3c04e..2012b1e9828 100644
--- a/regression/cbmc/address_space_size_limit1/test.desc
+++ b/regression/cbmc/address_space_size_limit1/test.desc
@@ -1,5 +1,7 @@
 CORE
 test.c
 --no-simplify --unwind 300 --object-bits 8
+^EXIT=6$
+^SIGNAL=0$
 too many addressed objects
---
+--
\ No newline at end of file
diff --git a/regression/cbmc/realloc3/test.desc b/regression/cbmc/realloc3/test.desc
index 9efefbc7362..11abbc90b12 100644
--- a/regression/cbmc/realloc3/test.desc
+++ b/regression/cbmc/realloc3/test.desc
@@ -1,8 +1,12 @@
 CORE
 main.c
 
-^EXIT=0$
+^EXIT=6$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+pointer handling for concurrency is unsound
 --
 ^warning: ignoring
+--
+The test uses "__CPROVER_ASYNC_1:" and the async-called function foo
+does pointer operations over allocated memory - which is not handled sound
+way in CBMC.
diff --git a/regression/strings-smoke-tests/java_format/test.desc b/regression/strings-smoke-tests/java_format/test.desc
index 8999b5b27ec..de7ffe3c754 100644
--- a/regression/strings-smoke-tests/java_format/test.desc
+++ b/regression/strings-smoke-tests/java_format/test.desc
@@ -5,5 +5,4 @@ test.class
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$
 ^\[.*assertion.2\].* line 7.* FAILURE$
---
-^ignoring
+--
\ No newline at end of file
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index e95417f4934..80c8c058fdb 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -276,9 +276,12 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
      to_side_effect_expr(expr).get_statement()==ID_nondet)
     return false;
 
-  if(expr.id()==ID_side_effect &&
-     to_side_effect_expr(expr).get_statement()==ID_allocate)
+  if(
+    expr.id() == ID_side_effect &&
+    to_side_effect_expr(expr).get_statement() == ID_allocate)
+  {
     return false;
+  }
 
   if(expr.id()==ID_symbol)
     if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier())==
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index c36c8b189dc..cc4126b93a3 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_predicates.h>
 #include <util/cprover_prefix.h>
 #include <util/options.h>
+#include <util/invariant.h>
 
 #include "local_bitvector_analysis.h"
 
@@ -1658,7 +1659,7 @@ void goto_checkt::goto_check(
     {
       if(enable_pointer_check)
       {
-        assert(i.code.operands().size()==1);
+        INVARIANT(i.code.operands().size() == 1, "The num-operands must be 1.");
         const symbol_exprt &variable=to_symbol_expr(i.code.op0());
 
         // is it dirty?
@@ -1666,22 +1667,48 @@ void goto_checkt::goto_check(
         {
           // need to mark the dead variable as dead
           goto_programt::targett t=new_code.add_instruction(ASSIGN);
-          exprt address_of_expr=address_of_exprt(variable);
+          address_of_exprt address_of_expr = address_of_exprt(variable);
           exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
           if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
             address_of_expr.make_typecast(lhs.type());
-          exprt rhs=
-            if_exprt(
-              side_effect_expr_nondett(bool_typet()),
-              address_of_expr,
-              lhs,
-              lhs.type());
+          if_exprt rhs = if_exprt(
+            side_effect_expr_nondett(bool_typet()),
+            address_of_expr,
+            lhs,
+            lhs.type());
           t->source_location=i.source_location;
           t->code=code_assignt(lhs, rhs);
           t->code.add_source_location()=i.source_location;
         }
       }
     }
+    else if(i.is_decl())
+    {
+      if(enable_pointer_check)
+      {
+        INVARIANT(i.code.operands().size() == 1, "There must be 1 operand.");
+        const symbol_exprt &variable = to_symbol_expr(i.code.op0());
+
+        // is it dirty?
+        if(local_bitvector_analysis->dirty(variable))
+        {
+          // reset the dead marker
+          goto_programt::targett t = new_code.add_instruction(ASSIGN);
+          exprt address_of_expr = address_of_exprt(variable);
+          exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+          if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
+            address_of_expr.make_typecast(lhs.type());
+          exprt rhs = if_exprt(
+            equal_exprt(lhs, address_of_expr),
+            null_pointer_exprt(to_pointer_type(address_of_expr.type())),
+            lhs,
+            lhs.type());
+          t->source_location = i.source_location;
+          t->code = code_assignt(lhs, rhs);
+          t->code.add_source_location() = i.source_location;
+        }
+      }
+    }
     else if(i.is_end_function())
     {
       if(i.function==goto_functionst::entry_point() &&
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index 41700caccb7..8d3a64a53d0 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -232,7 +232,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
     const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
     const irep_idt &statement=side_effect_expr.get_statement();
 
-    if(statement==ID_allocate)
+    if(statement == ID_allocate)
       return flagst::mk_dynamic_heap();
     else
       return flagst::mk_unknown();
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index 69728c66e59..459abac4725 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -298,7 +298,7 @@ void local_may_aliast::get_rec(
     const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
     const irep_idt &statement=side_effect_expr.get_statement();
 
-    if(statement==ID_allocate)
+    if(statement == ID_allocate)
     {
       dest.insert(objects.number(exprt(ID_dynamic_object)));
     }
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 401ff940ce6..5ce9d786714 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -105,15 +105,17 @@ static std::string architecture_string(int value, const char *s)
 
 void ansi_c_internal_additions(std::string &code)
 {
-  code+=
+  code +=
     "# 1 \"<built-in-additions>\"\n"
     "typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n"
     "void __CPROVER_assume(__CPROVER_bool assumption);\n"
     "void __VERIFIER_assume(__CPROVER_bool assumption);\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "void __CPROVER_assert(__CPROVER_bool assertion, const char *description);\n"
+    "void __CPROVER_assert(__CPROVER_bool assertion, const char "
+    "*description);\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);\n"
+    "void __CPROVER_precondition(__CPROVER_bool precondition, const char "
+    "*description);\n"
     "void __CPROVER_havoc_object(void *);\n"
     "__CPROVER_bool __CPROVER_equal();\n"
     "__CPROVER_bool __CPROVER_same_object(const void *, const void *);\n"
@@ -145,7 +147,8 @@ void ansi_c_internal_additions(std::string &code)
     "void __CPROVER_fence(const char *kind, ...);\n"
     "__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n"
+    "__CPROVER_bool "
+    "__CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n"
     "unsigned long __CPROVER_next_thread_id=0;\n"
 
     // traces
@@ -157,7 +160,8 @@ void ansi_c_internal_additions(std::string &code)
     "__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);\n"
     "extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);\n"
+    "void __CPROVER_allocated_memory(__CPROVER_size_t address, "
+    "__CPROVER_size_t extent);\n"
 
     // malloc
     "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n"
@@ -170,13 +174,16 @@ void ansi_c_internal_additions(std::string &code)
 
     // this is ANSI-C
     // NOLINTNEXTLINE(whitespace/line_length)
-    "extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];\n"
+    "extern __CPROVER_thread_local const char "
+    "__func__[__CPROVER_constant_infinity_uint];\n"
 
     // this is GCC
     // NOLINTNEXTLINE(whitespace/line_length)
-    "extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];\n"
+    "extern __CPROVER_thread_local const char "
+    "__FUNCTION__[__CPROVER_constant_infinity_uint];\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n"
+    "extern __CPROVER_thread_local const char "
+    "__PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n"
 
     // float stuff
     "__CPROVER_bool __CPROVER_isnanf(float f);\n"
@@ -197,8 +204,9 @@ void ansi_c_internal_additions(std::string &code)
     "double __CPROVER_inf(void);\n"
     "float __CPROVER_inff(void);\n"
     "long double __CPROVER_infl(void);\n"
-    "int __CPROVER_thread_local __CPROVER_rounding_mode="+
-      std::to_string(config.ansi_c.rounding_mode)+";\n"
+    "int __CPROVER_thread_local __CPROVER_rounding_mode=" +
+    std::to_string(config.ansi_c.rounding_mode) +
+    ";\n"
     "int __CPROVER_isgreaterf(float f, float g);\n"
     "int __CPROVER_isgreaterd(double f, double g);\n"
     "int __CPROVER_isgreaterequalf(float f, float g);\n"
@@ -222,7 +230,8 @@ void ansi_c_internal_additions(std::string &code)
 
     // arrays
     // NOLINTNEXTLINE(whitespace/line_length)
-    "__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);\n"
+    "__CPROVER_bool __CPROVER_array_equal(const void *array1, "
+    "const void *array2);\n"
     // overwrite all of *dest (possibly using nondet values), even
     // if *src is smaller
     "void __CPROVER_array_copy(const void *dest, const void *src);\n"
@@ -232,7 +241,7 @@ void ansi_c_internal_additions(std::string &code)
 
     // k-induction
     "void __CPROVER_k_induction_hint(unsigned min, unsigned max, "
-      "unsigned step, unsigned loop_free);\n"
+    "unsigned step, unsigned loop_free);\n"
 
     // format string-related
     "int __CPROVER_scanf(const char *, ...);\n"
@@ -245,7 +254,8 @@ void ansi_c_internal_additions(std::string &code)
     "  short next_unread;\n"
     "};\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];\n"
+    "extern struct __CPROVER_pipet "
+    "__CPROVER_pipes[__CPROVER_constant_infinity_uint];\n"
     // offset to make sure we don't collide with other fds
     "extern const int __CPROVER_pipe_offset;\n"
     "unsigned __CPROVER_pipe_count=0;\n"
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 6fe03a3cfa0..b911b813a00 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2271,16 +2271,16 @@ exprt c_typecheck_baset::do_special_functions(
 
     return abs_expr;
   }
-  else if(identifier==CPROVER_PREFIX "allocate")
+  else if(identifier == CPROVER_PREFIX "allocate")
   {
-    if(expr.arguments().size()!=2)
+    if(expr.arguments().size() != 2)
     {
       err_location(f_op);
       error() << "allocate expects two operands" << eom;
       throw 0;
     }
 
-    exprt malloc_expr=side_effect_exprt(ID_allocate);
+    exprt malloc_expr = side_effect_exprt(ID_allocate);
     malloc_expr.type()=expr.type();
     malloc_expr.add_source_location()=source_location;
     malloc_expr.operands()=expr.arguments();
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index b175ecee994..755e3ea2ff0 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -1124,7 +1124,7 @@ std::string expr2ct::convert_allocate(const exprt &src, unsigned &precedence)
   std::string op0 = convert_with_precedence(src.op0(), p0);
 
   unsigned p1;
-  std::string op1 = convert_with_precedence(src.op1(), p1);
+  const std::string op1 = convert_with_precedence(src.op1(), p1);
 
   std::string dest = "ALLOCATE";
   dest += '(';
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
index 0417ed9c3e9..bd43ab5221c 100644
--- a/src/cpp/cpp_internal_additions.cpp
+++ b/src/cpp/cpp_internal_additions.cpp
@@ -91,8 +91,10 @@ void cpp_internal_additions(std::ostream &out)
   out << "extern \"C\" const void *__CPROVER_dead_object=0;" << '\n';
 
   // malloc
+  // NOLINTNEXTLINE(whitespace/line_length)
   out << "extern \"C\" void *__CPROVER_allocate(__CPROVER_size_t size,"
-      << " __CPROVER_bool zero);" << '\n';
+         " __CPROVER_bool zero);"
+      << '\n';
   out << "extern \"C\" const void *__CPROVER_deallocated=0;" << '\n';
   out << "extern \"C\" const void *__CPROVER_malloc_object=0;" << '\n';
   out << "extern \"C\" __CPROVER::size_t __CPROVER_malloc_size;" << '\n';
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index 898c7fdace2..ec88c539679 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -670,7 +670,7 @@ void goto_convertt::remove_side_effect(
   else if(statement==ID_cpp_delete ||
           statement==ID_cpp_delete_array)
     remove_cpp_delete(expr, dest, result_is_used);
-  else if(statement==ID_allocate)
+  else if(statement == ID_allocate)
     remove_malloc(expr, dest, result_is_used);
   else if(statement==ID_temporary_object)
     remove_temporary_object(expr, dest, result_is_used);
diff --git a/src/goto-programs/system_library_symbols.h b/src/goto-programs/system_library_symbols.h
index 82146991be1..db03b538ae0 100644
--- a/src/goto-programs/system_library_symbols.h
+++ b/src/goto-programs/system_library_symbols.h
@@ -14,6 +14,7 @@ Author: Thomas Kiley
 
 #include <list>
 #include <set>
+#include <map>
 #include <string>
 #include <util/irep.h>
 #include <util/type.h>
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 096c4766377..55d9f727ebb 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -322,7 +322,9 @@ class goto_symext
   virtual void symex_gcc_builtin_va_arg_next(
     statet &state, const exprt &lhs, const side_effect_exprt &code);
   virtual void symex_allocate(
-    statet &state, const exprt &lhs, const side_effect_exprt &code);
+    statet &state,
+    const exprt &lhs,
+    const side_effect_exprt &code);
   virtual void symex_cpp_delete(statet &state, const codet &code);
   virtual void symex_cpp_new(
     statet &state, const exprt &lhs, const side_effect_exprt &code);
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index f2db40c8b71..c6d20d37a1f 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -345,6 +345,9 @@ void goto_symex_statet::assignment(
   assert_l2_renaming(lhs);
   assert_l2_renaming(rhs);
 
+  if(is_shared && lhs.type().id() == ID_pointer)
+    throw "pointer handling for concurrency is unsound";
+
   // for value propagation -- the RHS is L2
 
   if(!is_shared && record_value && constant_propagation(rhs))
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 8369ef5db2f..a89f20da569 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -63,7 +63,7 @@ void goto_symext::symex_assign(
       statement == ID_cpp_new || statement == ID_cpp_new_array ||
       statement == ID_java_new_array_data)
       symex_cpp_new(state, lhs, side_effect_expr);
-    else if(statement==ID_allocate)
+    else if(statement == ID_allocate)
       symex_allocate(state, lhs, side_effect_expr);
     else if(statement==ID_printf)
       symex_printf(state, lhs, side_effect_expr);
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 9bf02bf1e2e..f631bef6b04 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -58,7 +58,7 @@ void goto_symext::symex_allocate(
   const exprt &lhs,
   const side_effect_exprt &code)
 {
-  if(code.operands().size()!=2)
+  if(code.operands().size() != 2)
     throw "allocate expected to have two operands";
 
   if(lhs.is_nil())
@@ -167,7 +167,7 @@ void goto_symext::symex_allocate(
 
   new_symbol_table.add(value_symbol);
 
-  exprt zero_init=code.op1();
+  exprt zero_init = code.op1();
   state.rename(zero_init, ns); // to allow constant propagation
   simplify(zero_init, ns);
 
@@ -177,12 +177,8 @@ void goto_symext::symex_allocate(
   if(!zero_init.is_zero() && !zero_init.is_false())
   {
     null_message_handlert null_message;
-    exprt zero_value=
-      zero_initializer(
-        object_type,
-        code.source_location(),
-        ns,
-        null_message);
+    exprt zero_value =
+      zero_initializer(object_type, code.source_location(), ns, null_message);
 
     if(zero_value.is_not_nil())
     {
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 5179c5f88f1..367930ce388 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -174,19 +174,23 @@ static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
   Forall_operands(it, expr)
     adjust_byte_extract_rec(*it, ns);
 
-  if(expr.id()==ID_byte_extract_big_endian ||
-     expr.id()==ID_byte_extract_little_endian)
-  {
-    byte_extract_exprt &be=to_byte_extract_expr(expr);
-    if(be.op().id()==ID_symbol &&
-       to_ssa_expr(be.op()).get_original_expr().get_bool(ID_C_invalid_object))
+  if(
+    expr.id() == ID_byte_extract_big_endian ||
+    expr.id() == ID_byte_extract_little_endian)
+  {
+    byte_extract_exprt &be = to_byte_extract_expr(expr);
+    if(
+      be.op().id() == ID_symbol &&
+      to_ssa_expr(be.op()).get_original_expr().get_bool(ID_C_invalid_object))
+    {
       return;
+    }
 
     object_descriptor_exprt ode;
     ode.build(expr, ns);
 
-    be.op()=ode.root_object();
-    be.offset()=ode.offset();
+    be.op() = ode.root_object();
+    be.offset() = ode.offset();
   }
 }
 
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index 3dbdc1e554c..0042f534098 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -72,11 +72,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   state.propagation.remove(l1_identifier);
 
   // L2 renaming
-  // inlining may yield multiple declarations of the same identifier
-  // within the same L1 context
-  if(state.level2.current_names.find(l1_identifier)==
-     state.level2.current_names.end())
-    state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0);
+  state.level2.current_names.insert(
+    std::make_pair(l1_identifier, std::make_pair(ssa, 0)));
   state.level2.increase_counter(l1_identifier);
   const bool record_events=state.record_events;
   state.record_events=false;
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 910c9e29692..180c50d6ec3 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -195,7 +195,7 @@ exprt allocate_dynamic_object(
   {
     INVARIANT(!object_size.is_nil(), "Size of Java objects should be known");
     // malloc expression
-    exprt malloc_expr=side_effect_exprt(ID_allocate);
+    exprt malloc_expr = side_effect_exprt(ID_allocate);
     malloc_expr.copy_to_operands(object_size);
     malloc_expr.copy_to_operands(false_exprt());
     typet result_type=pointer_type(allocate_type);
diff --git a/src/memory-models/mm2cpp.cpp b/src/memory-models/mm2cpp.cpp
index a5be8b35d48..fd409bfd8c8 100644
--- a/src/memory-models/mm2cpp.cpp
+++ b/src/memory-models/mm2cpp.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "mm2cpp.h"
 
 #include <ostream>
+#include <map>
 
 #include <util/std_code.h>
 
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 0f8f5ea18dc..b03499982f7 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -636,7 +636,7 @@ void value_sett::get_value_set_rec(
 
       // adjust by offset
       if(object.offset_is_set && i_is_set)
-        object.offset+=i;
+        object.offset += i;
       else
         object.offset_is_set=false;
 
@@ -682,7 +682,7 @@ void value_sett::get_value_set_rec(
       // these should be gone
       throw "unexpected function_call sideeffect";
     }
-    else if(statement==ID_allocate)
+    else if(statement == ID_allocate)
     {
       assert(suffix=="");
 
@@ -1008,8 +1008,7 @@ void value_sett::get_reference_set_rec(
         if(offset.is_zero())
         {
         }
-        else if(!to_integer(offset, i) &&
-                o.offset_is_set)
+        else if(!to_integer(offset, i) && o.offset_is_set)
         {
           mp_integer size=pointer_offset_size(array_type.subtype(), ns);
 
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 0e4c966817e..63a636841c4 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -560,10 +560,10 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 
       // this is relative to the root object
       exprt offset;
-      if(o.offset().id()==ID_unknown)
-        offset=pointer_offset(pointer_expr);
+      if(o.offset().id() == ID_unknown)
+        offset = pointer_offset(pointer_expr);
       else
-        offset=o.offset();
+        offset = o.offset();
 
       if(memory_model(result.value, dereference_type, tmp_guard, offset))
       {
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 7e661711c39..252253642df 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -613,7 +613,7 @@ void value_set_fit::get_value_set_rec(
       // these should be gone
       throw "unexpected function_call sideeffect";
     }
-    else if(statement==ID_allocate)
+    else if(statement == ID_allocate)
     {
       if(expr.type().id()!=ID_pointer)
         throw "malloc expected to return pointer type";
diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp
index 8ab9ff2c117..e03052029ee 100644
--- a/src/pointer-analysis/value_set_fivr.cpp
+++ b/src/pointer-analysis/value_set_fivr.cpp
@@ -730,7 +730,7 @@ void value_set_fivrt::get_value_set_rec(
       // these should be gone
       throw "unexpected function_call sideeffect";
     }
-    else if(statement==ID_allocate)
+    else if(statement == ID_allocate)
     {
       if(expr.type().id()!=ID_pointer)
         throw "malloc expected to return pointer type";
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
index a405e2d2242..aaf094e7477 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -516,7 +516,7 @@ void value_set_fivrnst::get_value_set_rec(
       // these should be gone
       throw "unexpected function_call sideeffect";
     }
-    else if(statement==ID_allocate)
+    else if(statement == ID_allocate)
     {
       if(expr.type().id()!=ID_pointer)
         throw "malloc expected to return pointer type";
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 9cbe9309647..4a62e16a9fb 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/invariant.h>
 #include <util/prefix.h>
+#include <util/ssa_expr.h>
 #include <util/std_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/threeval.h>
@@ -29,31 +30,15 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
     if(operands.size()==1 &&
        operands[0].type().id()==ID_pointer)
     {
-      const bvt &bv=convert_bv(operands[0]);
+      // we postpone
+      literalt l = prop.new_variable();
 
-      if(!bv.empty())
-      {
-        bvt invalid_bv, null_bv;
-        encode(pointer_logic.get_invalid_object(), invalid_bv);
-        encode(pointer_logic.get_null_object(),    null_bv);
-
-        bvt equal_invalid_bv, equal_null_bv;
-        equal_invalid_bv.resize(object_bits);
-        equal_null_bv.resize(object_bits);
-
-        for(std::size_t i=0; i<object_bits; i++)
-        {
-          equal_invalid_bv[i]=prop.lequal(bv[offset_bits+i],
-                                          invalid_bv[offset_bits+i]);
-          equal_null_bv[i]   =prop.lequal(bv[offset_bits+i],
-                                          null_bv[offset_bits+i]);
-        }
-
-        literalt equal_invalid=prop.land(equal_invalid_bv);
-        literalt equal_null=prop.land(equal_null_bv);
-
-        return prop.lor(equal_invalid, equal_null);
-      }
+      postponed_list.push_back(postponedt());
+      postponed_list.back().op = convert_bv(operands[0]);
+      postponed_list.back().bv.push_back(l);
+      postponed_list.back().expr = expr;
+
+      return l;
     }
   }
   else if(expr.id()==ID_dynamic_object)
@@ -136,7 +121,7 @@ bool bv_pointerst::convert_address_of_rec(
     {
       // this should be gone
       bv=convert_pointer_type(array);
-      POSTCONDITION(bv.size()==bits);
+      POSTCONDITION(bv.size() == bits);
     }
     else if(array_type.id()==ID_array ||
             array_type.id()==ID_incomplete_array ||
@@ -144,7 +129,7 @@ bool bv_pointerst::convert_address_of_rec(
     {
       if(convert_address_of_rec(array, bv))
         return true;
-      POSTCONDITION(bv.size()==bits);
+      POSTCONDITION(bv.size() == bits);
     }
     else
       UNREACHABLE;
@@ -152,10 +137,10 @@ bool bv_pointerst::convert_address_of_rec(
     // get size
     mp_integer size=
       pointer_offset_size(array_type.subtype(), ns);
-    DATA_INVARIANT(size>0, "array subtype expected to have non-zero size");
+    DATA_INVARIANT(size > 0, "array subtype expected to have non-zero size");
 
     offset_arithmetic(bv, size, index);
-    POSTCONDITION(bv.size()==bits);
+    POSTCONDITION(bv.size() == bits);
     return false;
   }
   else if(expr.id()==ID_member)
@@ -173,7 +158,7 @@ bool bv_pointerst::convert_address_of_rec(
       mp_integer offset=member_offset(
         to_struct_type(struct_op_type),
         member_expr.get_component_name(), ns);
-      DATA_INVARIANT(offset>=0, "member offset expected to be positive");
+      DATA_INVARIANT(offset >= 0, "member offset expected to be positive");
 
       // add offset
       offset_arithmetic(bv, offset);
@@ -296,7 +281,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       return bv;
     }
 
-    POSTCONDITION(bv.size()==bits);
+    POSTCONDITION(bv.size() == bits);
     return bv;
   }
   else if(expr.id()==ID_constant)
@@ -334,13 +319,13 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       {
         count++;
         bv=convert_bv(*it);
-        POSTCONDITION(bv.size()==bits);
+        POSTCONDITION(bv.size() == bits);
 
         typet pointer_sub_type=it->type().subtype();
         if(pointer_sub_type.id()==ID_empty)
           pointer_sub_type=char_type();
         size=pointer_offset_size(pointer_sub_type, ns);
-        POSTCONDITION(size>0);
+        POSTCONDITION(size > 0);
       }
     }
 
@@ -414,7 +399,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 
     mp_integer element_size=
       pointer_offset_size(expr.op0().type().subtype(), ns);
-    DATA_INVARIANT(element_size>0, "object size expected to be non-zero");
+    DATA_INVARIANT(element_size > 0, "object size expected to be non-zero");
 
     offset_arithmetic(bv, element_size, neg_op1);
 
@@ -440,6 +425,12 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   {
     return SUB::convert_byte_extract(to_byte_extract_expr(expr));
   }
+  else if(
+    expr.id() == ID_byte_update_little_endian ||
+    expr.id() == ID_byte_update_big_endian)
+  {
+    throw "byte-wise updates of pointers are unsupported";
+  }
 
   return conversion_failed(expr);
 }
@@ -471,7 +462,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
 
     mp_integer element_size=
       pointer_offset_size(expr.op0().type().subtype(), ns);
-    DATA_INVARIANT(element_size>0, "object size expected to be non-zero");
+    DATA_INVARIANT(element_size > 0, "object size expected to be non-zero");
 
     if(element_size!=1)
     {
@@ -571,7 +562,7 @@ exprt bv_pointerst::bv_get_rec(
 
   for(std::size_t i=0; i<bits; i++)
   {
-    char ch=0;
+    char ch = 0;
     std::size_t bit_nr=i+offset;
 
     if(unknown[bit_nr])
@@ -721,8 +712,8 @@ void bv_pointerst::do_postponed(
       bvt saved_bv=postponed.op;
       saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
 
-      POSTCONDITION(bv.size()==saved_bv.size());
-      PRECONDITION(postponed.bv.size()==1);
+      POSTCONDITION(bv.size() == saved_bv.size());
+      PRECONDITION(postponed.bv.size() == 1);
 
       literalt l1=bv_utils.equal(bv, saved_bv);
       literalt l2=postponed.bv.front();
@@ -774,8 +765,8 @@ void bv_pointerst::do_postponed(
       bvt saved_bv=postponed.op;
       saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
 
-      POSTCONDITION(bv.size()==saved_bv.size());
-      PRECONDITION(postponed.bv.size()>=1);
+      POSTCONDITION(bv.size() == saved_bv.size());
+      PRECONDITION(postponed.bv.size() >= 1);
 
       literalt l1=bv_utils.equal(bv, saved_bv);
 
@@ -785,6 +776,75 @@ void bv_pointerst::do_postponed(
       prop.l_set_to(prop.limplies(l1, l2), true);
     }
   }
+  else if(postponed.expr.id() == ID_invalid_pointer)
+  {
+    const pointer_logict::objectst &objects = pointer_logic.objects;
+
+    bvt disj;
+    disj.reserve(objects.size());
+
+    bvt saved_bv = postponed.op;
+    saved_bv.erase(saved_bv.begin(), saved_bv.begin() + offset_bits);
+
+    bvt invalid_bv, null_bv;
+    encode(pointer_logic.get_invalid_object(), invalid_bv);
+    invalid_bv.erase(invalid_bv.begin(), invalid_bv.begin() + offset_bits);
+    encode(pointer_logic.get_null_object(), null_bv);
+    null_bv.erase(null_bv.begin(), null_bv.begin() + offset_bits);
+
+    disj.push_back(bv_utils.equal(saved_bv, invalid_bv));
+    disj.push_back(bv_utils.equal(saved_bv, null_bv));
+
+    // compare object part to non-allocated dynamic objects
+    std::size_t number = 0;
+
+    for(pointer_logict::objectst::const_iterator it = objects.begin();
+        it != objects.end();
+        it++, number++)
+    {
+      const exprt &expr = *it;
+
+      if(!pointer_logic.is_dynamic_object(expr) || !is_ssa_expr(expr))
+        continue;
+
+      // only compare object part
+      bvt bv;
+      encode(number, bv);
+
+      bv.erase(bv.begin(), bv.begin() + offset_bits);
+      INVARIANT(bv.size() == saved_bv.size(), "Must be of the same size.");
+
+      literalt l1 = bv_utils.equal(bv, saved_bv);
+
+      const ssa_exprt &ssa = to_ssa_expr(expr);
+
+      const exprt &guard = static_cast<const exprt &>(
+        ssa.get_original_expr().find("#dynamic_guard"));
+
+      if(guard.is_nil())
+        continue;
+
+      const bvt &guard_bv = convert_bv(guard);
+      INVARIANT(guard_bv.size() == 1, "Size must be 1.");
+      literalt l_guard = guard_bv[0];
+
+      disj.push_back(prop.land(!l_guard, l1));
+    }
+
+    // compare object part to max object number
+    bvt bv;
+    encode(number, bv);
+
+    bv.erase(bv.begin(), bv.begin() + offset_bits);
+    INVARIANT(bv.size() == saved_bv.size(), "Must be of the same size.");
+
+    disj.push_back(
+      bv_utils.rel(saved_bv, ID_ge, bv, bv_utilst::representationt::UNSIGNED));
+
+    INVARIANT(postponed.bv.size() == 1, "Must be of the size 1.");
+    literalt l = postponed.bv.front();
+    prop.l_set_to(prop.lequal(prop.lor(disj), l), true);
+  }
   else
     UNREACHABLE;
 }
diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp
index 896ada763c9..5d64ac81dce 100644
--- a/src/solvers/flattening/flatten_byte_operators.cpp
+++ b/src/solvers/flattening/flatten_byte_operators.cpp
@@ -242,7 +242,7 @@ exprt flatten_byte_extract(
 
         byte_extract_exprt tmp(unpacked);
         tmp.type()=subtype;
-        tmp.offset()=new_offset;
+        tmp.offset() = new_offset;
 
         array.copy_to_operands(flatten_byte_extract(tmp, ns));
       }
@@ -277,7 +277,7 @@ exprt flatten_byte_extract(
 
       byte_extract_exprt tmp(unpacked);
       tmp.type()=comp.type();
-      tmp.offset()=new_offset;
+      tmp.offset() = new_offset;
 
       s.move_to_operands(tmp);
     }
diff --git a/src/util/guard.cpp b/src/util/guard.cpp
index 693b48602c9..2fd6a9a8a31 100644
--- a/src/util/guard.cpp
+++ b/src/util/guard.cpp
@@ -95,9 +95,7 @@ guardt &operator -= (guardt &g1, const guardt &g2)
   if(g1.id()!=ID_and || g2.id()!=ID_and)
     return g1;
 
-  sort_and_join(g1);
   guardt g2_sorted=g2;
-  sort_and_join(g2_sorted);
 
   exprt::operandst &op1=g1.operands();
   const exprt::operandst &op2=g2_sorted.operands();
@@ -108,10 +106,10 @@ guardt &operator -= (guardt &g1, const guardt &g2)
       it2!=op2.end();
       ++it2)
   {
-    while(it1!=op1.end() && *it1<*it2)
-      ++it1;
     if(it1!=op1.end() && *it1==*it2)
       it1=op1.erase(it1);
+    else
+      break;
   }
 
   g1=conjunction(op1);
@@ -145,9 +143,7 @@ guardt &operator |= (guardt &g1, const guardt &g2)
   }
 
   // find common prefix
-  sort_and_join(g1);
   guardt g2_sorted=g2;
-  sort_and_join(g2_sorted);
 
   exprt::operandst &op1=g1.operands();
   const exprt::operandst &op2=g2_sorted.operands();
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 670f933f8f6..8a8defd2ae8 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -316,16 +316,16 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
 
   // mildly more elaborate version of the above:
   // (int)((T*)0 + int) -> (int)(sizeof(T)*(size_t)int) if NULL is zero
-  if(config.ansi_c.NULL_is_zero &&
-     (expr_type.id()==ID_signedbv || expr_type.id()==ID_unsignedbv) &&
-     op_type.id()==ID_pointer &&
-     expr.op0().id()==ID_plus &&
-     expr.op0().operands().size()==2 &&
-     ((expr.op0().op0().id()==ID_typecast &&
-     expr.op0().op0().operands().size()==1 &&
-       expr.op0().op0().op0().is_zero()) ||
-      (expr.op0().op0().is_constant() &&
-       to_constant_expr(expr.op0().op0()).get_value()==ID_NULL)))
+  if(
+    config.ansi_c.NULL_is_zero &&
+    (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv) &&
+    op_type.id() == ID_pointer && expr.op0().id() == ID_plus &&
+    expr.op0().operands().size() == 2 &&
+    ((expr.op0().op0().id() == ID_typecast &&
+      expr.op0().op0().operands().size() == 1 &&
+      expr.op0().op0().op0().is_zero()) ||
+     (expr.op0().op0().is_constant() &&
+      to_constant_expr(expr.op0().op0()).get_value() == ID_NULL)))
   {
     mp_integer sub_size=pointer_offset_size(op_type.subtype(), ns);
     if(sub_size!=-1)
@@ -729,15 +729,16 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
       return false;
     }
   }
-  else if(operand.id()==ID_address_of)
+  else if(operand.id() == ID_address_of)
   {
-    const exprt &o=to_address_of_expr(operand).object();
+    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 &&
+      base_type_eq(expr_type, pointer_type(o.type().subtype()), ns))
     {
-      expr=address_of_exprt(index_exprt(o, from_integer(0, size_type())));
+      expr = address_of_exprt(index_exprt(o, from_integer(0, size_type())));
 
       simplify_rec(expr);
       return false;
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index 99a548927e1..3fc2467ce72 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -72,32 +72,25 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
       return false;
     }
   }
-  else if(expr.id()==ID_xor)
+  else if(expr.id() == ID_xor)
   {
     bool result=true;
 
     bool negate=false;
 
-    for(exprt::operandst::const_iterator it=operands.begin();
-        it!=operands.end();)
+    for(exprt::operandst::const_iterator it = operands.begin();
+        it != operands.end();)
     {
-      if(it->type().id()!=ID_bool)
+      if(it->type().id() != ID_bool)
         return true;
 
-      bool erase;
-
       if(it->is_true())
-      {
-        erase=true;
-        negate=!negate;
-      }
-      else
-        erase=it->is_false();
+        negate = !negate;
 
-      if(erase)
+      if(it->is_constant())
       {
-        it=operands.erase(it);
-        result=false;
+        it = operands.erase(it);
+        result = false;
       }
       else
         it++;
@@ -108,7 +101,7 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
       expr.make_bool(negate);
       return false;
     }
-    else if(operands.size()==1)
+    else if(operands.size() == 1)
     {
       exprt tmp(operands.front());
       if(negate)
@@ -119,14 +112,14 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
 
     return result;
   }
-  else if(expr.id()==ID_and || expr.id()==ID_or)
+  else if(expr.id() == ID_and || expr.id() == ID_or)
   {
     std::unordered_set<exprt, irep_hash> expr_set;
 
-    bool result=true;
+    bool result = true;
 
-    for(exprt::operandst::const_iterator it=operands.begin();
-        it!=operands.end();)
+    for(exprt::operandst::const_iterator it = operands.begin();
+        it != operands.end();)
     {
       if(it->type().id()!=ID_bool)
         return true;
@@ -145,9 +138,8 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
         return false;
       }
 
-      bool erase=
-        (expr.id()==ID_and ? is_true : is_false) ||
-        !expr_set.insert(*it).second;
+      bool erase = (expr.id() == ID_and ? is_true : is_false) ||
+                   !expr_set.insert(*it).second;
 
       if(erase)
       {
@@ -160,18 +152,17 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
 
     // search for a and !a
     for(const exprt &op : operands)
-      if(op.id()==ID_not &&
-         op.operands().size()==1 &&
-         op.type().id()==ID_bool &&
-         expr_set.find(op.op0())!=expr_set.end())
+      if(
+        op.id() == ID_not && op.operands().size() == 1 &&
+        op.type().id() == ID_bool && expr_set.find(op.op0()) != expr_set.end())
       {
-        expr.make_bool(expr.id()==ID_or);
+        expr.make_bool(expr.id() == ID_or);
         return false;
       }
 
     if(operands.empty())
     {
-      expr.make_bool(expr.id()==ID_and);
+      expr.make_bool(expr.id() == ID_and);
       return false;
     }
     else if(operands.size()==1)