diff --git a/regression/cbmc-with-incr/Malloc17/main.c b/regression/cbmc-with-incr/Malloc17/main.c
index bf13b054b2e..192ed892ef7 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_malloc(1);
+  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_malloc(1*sizeof(unsigned char));
+  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_malloc(sizeof(unsigned char)*1);
+  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 dc8d60bac01..e993e4e457c 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_malloc(size);
+  unsigned char* buffer=__CPROVER_allocate(size, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
diff --git a/regression/cbmc-with-incr/Malloc19/main.c b/regression/cbmc-with-incr/Malloc19/main.c
index 6d5d041c541..d14a014f03a 100644
--- a/regression/cbmc-with-incr/Malloc19/main.c
+++ b/regression/cbmc-with-incr/Malloc19/main.c
@@ -22,7 +22,7 @@ int main()
 {
     // Create node
     struct node *nd;
-    nd = (struct node *)__CPROVER_malloc(sizeof(struct node));
+    nd = (struct node *)__CPROVER_allocate(sizeof(struct node), 0);
 
     // Link node
     struct list_head *hd = &(nd->linkage);
diff --git a/regression/cbmc/Calloc1/main.c b/regression/cbmc/Calloc1/main.c
new file mode 100644
index 00000000000..75ea31a41bd
--- /dev/null
+++ b/regression/cbmc/Calloc1/main.c
@@ -0,0 +1,9 @@
+#include <stdlib.h>
+#include <assert.h>
+
+int main()
+{
+  int *x=calloc(sizeof(int), 1);
+  assert(*x==0);
+  return 0;
+}
diff --git a/regression/cbmc/Calloc1/test.desc b/regression/cbmc/Calloc1/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/Calloc1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Malloc17/main.c b/regression/cbmc/Malloc17/main.c
index bf13b054b2e..192ed892ef7 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_malloc(1);
+  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_malloc(1*sizeof(unsigned char));
+  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_malloc(sizeof(unsigned char)*1);
+  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 047ada2b009..88dd8de1e25 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_malloc(buffer_size);
+  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/Malloc19/main.c b/regression/cbmc/Malloc19/main.c
index 6d5d041c541..d14a014f03a 100644
--- a/regression/cbmc/Malloc19/main.c
+++ b/regression/cbmc/Malloc19/main.c
@@ -22,7 +22,7 @@ int main()
 {
     // Create node
     struct node *nd;
-    nd = (struct node *)__CPROVER_malloc(sizeof(struct node));
+    nd = (struct node *)__CPROVER_allocate(sizeof(struct node), 0);
 
     // Link node
     struct list_head *hd = &(nd->linkage);
diff --git a/regression/cbmc/Malloc24/main.c b/regression/cbmc/Malloc24/main.c
new file mode 100644
index 00000000000..b7e5975d680
--- /dev/null
+++ b/regression/cbmc/Malloc24/main.c
@@ -0,0 +1,47 @@
+#include <stdlib.h>
+
+struct node
+{
+    int value;
+    struct node *next;
+};
+
+struct list
+{
+  int size;
+  struct node *head;
+};
+
+void removeLast(struct list * l)
+{
+  int index = l->size - 1;
+  struct node **current;
+  for(current = &(l->head); index && *current; index--)
+    current = &(*current)->next;
+  *current = (*current)->next;
+  l->size--;
+}
+
+int main () {
+  //build a 2-nodes list
+  struct node *n0 = malloc(sizeof(struct node));
+  struct node *n1 = malloc(sizeof(struct node));
+  struct list *l = malloc(sizeof(struct list));
+  l->size = 2;
+  l->head = n0;
+
+  n0->next=n1;
+  n1->next=NULL;
+
+  //remove last node from list
+
+  //this passes
+  // struct node **current = &(l->head);
+  // current = &(*current)->next;
+  // *current = (*current)->next;
+  // l->size--;
+  //this doesn't
+  removeLast(l);
+
+  __CPROVER_assert(n0->next == NULL , "not NULL");
+}
diff --git a/regression/cbmc/Malloc24/test.desc b/regression/cbmc/Malloc24/test.desc
new file mode 100644
index 00000000000..cf64d363c65
--- /dev/null
+++ b/regression/cbmc/Malloc24/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 4 --pointer-check --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 19f684d681f..e95417f4934 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -277,7 +277,7 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
     return false;
 
   if(expr.id()==ID_side_effect &&
-     to_side_effect_expr(expr).get_statement()==ID_malloc)
+     to_side_effect_expr(expr).get_statement()==ID_allocate)
     return false;
 
   if(expr.id()==ID_symbol)
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index c45a4c90f79..41700caccb7 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_malloc)
+    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 9e0751f9da9..69728c66e59 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_malloc)
+    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 676c033968e..401ff940ce6 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -160,7 +160,7 @@ void ansi_c_internal_additions(std::string &code)
     "void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);\n"
 
     // malloc
-    "void *__CPROVER_malloc(__CPROVER_size_t size);\n"
+    "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n"
     "const void *__CPROVER_deallocated=0;\n"
     "const void *__CPROVER_dead_object=0;\n"
     "const void *__CPROVER_malloc_object=0;\n"
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 00d68f46c35..6fe03a3cfa0 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 "malloc")
+  else if(identifier==CPROVER_PREFIX "allocate")
   {
-    if(expr.arguments().size()!=1)
+    if(expr.arguments().size()!=2)
     {
       err_location(f_op);
-      error() << "malloc expects one operand" << eom;
+      error() << "allocate expects two operands" << eom;
       throw 0;
     }
 
-    exprt malloc_expr=side_effect_exprt(ID_malloc);
+    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 b889476a73f..b175ecee994 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -1115,18 +1115,19 @@ std::string expr2ct::convert_pointer_object_has_type(
   return dest;
 }
 
-std::string expr2ct::convert_malloc(
-  const exprt &src,
-  unsigned &precedence)
+std::string expr2ct::convert_allocate(const exprt &src, unsigned &precedence)
 {
-  if(src.operands().size()!=1)
+  if(src.operands().size() != 2)
     return convert_norep(src, precedence);
 
   unsigned p0;
-  std::string op0=convert_with_precedence(src.op0(), p0);
+  std::string op0 = convert_with_precedence(src.op0(), p0);
 
-  std::string dest="MALLOC";
-  dest+='(';
+  unsigned p1;
+  std::string op1 = convert_with_precedence(src.op1(), p1);
+
+  std::string dest = "ALLOCATE";
+  dest += '(';
 
   if(src.type().id()==ID_pointer &&
      src.type().subtype().id()!=ID_empty)
@@ -1135,8 +1136,8 @@ std::string expr2ct::convert_malloc(
     dest+=", ";
   }
 
-  dest+=op0;
-  dest+=')';
+  dest += op0 + ", " + op1;
+  dest += ')';
 
   return dest;
 }
@@ -3656,8 +3657,8 @@ std::string expr2ct::convert_with_precedence(
       return
         convert_side_effect_expr_function_call(
           to_side_effect_expr_function_call(src), precedence);
-    else if(statement==ID_malloc)
-      return convert_malloc(src, precedence=15);
+    else if(statement == ID_allocate)
+      return convert_allocate(src, precedence = 15);
     else if(statement==ID_printf)
       return convert_function(src, "printf", precedence=16);
     else if(statement==ID_nondet)
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
index a6c027c7735..43371c0ef94 100644
--- a/src/ansi-c/expr2c_class.h
+++ b/src/ansi-c/expr2c_class.h
@@ -214,7 +214,7 @@ class expr2ct
   std::string convert_function_application(const function_application_exprt &src, unsigned &precedence);
   // NOLINTNEXTLINE(whitespace/line_length)
   std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence);
-  std::string convert_malloc(const exprt &src, unsigned &precedence);
+  std::string convert_allocate(const exprt &src, unsigned &precedence);
   std::string convert_nondet(const exprt &src, unsigned &precedence);
   std::string convert_prob_coin(const exprt &src, unsigned &precedence);
   std::string convert_prob_uniform(const exprt &src, unsigned &precedence);
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
index 94da717f33d..7fce070860a 100644
--- a/src/ansi-c/library/cprover.h
+++ b/src/ansi-c/library/cprover.h
@@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_ANSI_C_LIBRARY_CPROVER_H
 
 typedef __typeof__(sizeof(int)) __CPROVER_size_t;
-void *__CPROVER_malloc(__CPROVER_size_t size);
+void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 extern const void *__CPROVER_deallocated;
 extern const void *__CPROVER_malloc_object;
 extern __CPROVER_size_t __CPROVER_malloc_size;
diff --git a/src/ansi-c/library/new.c b/src/ansi-c/library/new.c
index 81bd62b2093..f4d8ac039b7 100644
--- a/src/ansi-c/library/new.c
+++ b/src/ansi-c/library/new.c
@@ -8,7 +8,7 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
   // This just does memory allocation.
   __CPROVER_HIDE:;
   void *res;
-  res=__CPROVER_malloc(malloc_size);
+  res = __CPROVER_allocate(malloc_size, 0);
 
   // ensure it's not recorded as deallocated
   __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
@@ -36,7 +36,7 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
   // This just does memory allocation.
   __CPROVER_HIDE:;
   void *res;
-  res=__CPROVER_malloc(size*count);
+  res = __CPROVER_allocate(size*count, 0);
 
   // ensure it's not recorded as deallocated
   __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index b0c9c1f3e6c..20b98db7378 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -60,27 +60,39 @@ inline void abort(void)
 /* FUNCTION: calloc */
 
 #undef calloc
-#undef malloc
 
-inline void *malloc(__CPROVER_size_t malloc_size);
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
 inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
 {
+  // realistically, calloc may return NULL,
+  // and __CPROVER_allocate doesn't, but no one cares
   __CPROVER_HIDE:;
-  void *res;
-  res=malloc(nmemb*size);
-  #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_is_zero_string(res)=1;
-  __CPROVER_zero_string_length(res)=0;
-  //for(int i=0; i<nmemb*size; i++) res[i]=0;
-  #else
-  if(nmemb>1)
-    __CPROVER_array_set(res, 0);
-  else if(nmemb==1)
-    for(__CPROVER_size_t i=0; i<size; ++i)
-      ((char*)res)[i]=0;
-  #endif
-  return res;
+  void *malloc_res;
+  malloc_res = __CPROVER_allocate(nmemb * size, 1);
+
+  // make sure it's not recorded as deallocated
+  __CPROVER_deallocated =
+    (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
+
+  // record the object size for non-determistic bounds checking
+  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
+  __CPROVER_malloc_object =
+    record_malloc ? malloc_res : __CPROVER_malloc_object;
+  __CPROVER_malloc_size = record_malloc ? nmemb * size : __CPROVER_malloc_size;
+  __CPROVER_malloc_is_new_array =
+    record_malloc ? 0 : __CPROVER_malloc_is_new_array;
+
+  // detect memory leaks
+  __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
+  __CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak;
+
+#ifdef __CPROVER_STRING_ABSTRACTION
+  __CPROVER_is_zero_string(malloc_res) = 1;
+  __CPROVER_zero_string_length(malloc_res) = 0;
+#endif
+
+  return malloc_res;
 }
 
 /* FUNCTION: malloc */
@@ -92,10 +104,10 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 inline void *malloc(__CPROVER_size_t malloc_size)
 {
   // realistically, malloc may return NULL,
-  // and __CPROVER_malloc doesn't, but no one cares
+  // and __CPROVER_allocate doesn't, but no one cares
   __CPROVER_HIDE:;
   void *malloc_res;
-  malloc_res=__CPROVER_malloc(malloc_size);
+  malloc_res = __CPROVER_allocate(malloc_size, 0);
 
   // make sure it's not recorded as deallocated
   __CPROVER_deallocated=(malloc_res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
@@ -121,7 +133,7 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
 {
   __CPROVER_HIDE:;
   void *res;
-  res=__CPROVER_malloc(alloca_size);
+  res = __CPROVER_allocate(alloca_size, 0);
 
   // make sure it's not recorded as deallocated
   __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
index a193742643e..0417ed9c3e9 100644
--- a/src/cpp/cpp_internal_additions.cpp
+++ b/src/cpp/cpp_internal_additions.cpp
@@ -91,7 +91,8 @@ void cpp_internal_additions(std::ostream &out)
   out << "extern \"C\" const void *__CPROVER_dead_object=0;" << '\n';
 
   // malloc
-  out << "extern \"C\" void *__CPROVER_malloc(__CPROVER::size_t size);" << '\n';
+  out << "extern \"C\" void *__CPROVER_allocate(__CPROVER_size_t size,"
+      << " __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/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index bf5b6cf3a3d..5f28a25e150 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -580,8 +580,10 @@ void goto_convertt::do_java_new(
   CHECK_RETURN(object_size.is_not_nil());
 
   // we produce a malloc side-effect, which stays
-  side_effect_exprt malloc_expr(ID_malloc);
+  side_effect_exprt malloc_expr(ID_allocate);
   malloc_expr.copy_to_operands(object_size);
+  // could use true and get rid of the code below
+  malloc_expr.copy_to_operands(false_exprt());
   malloc_expr.type()=rhs.type();
 
   goto_programt::targett t_n=dest.add_instruction(ASSIGN);
@@ -618,8 +620,10 @@ void goto_convertt::do_java_new_array(
   CHECK_RETURN(!object_size.is_nil());
 
   // we produce a malloc side-effect, which stays
-  side_effect_exprt malloc_expr(ID_malloc);
+  side_effect_exprt malloc_expr(ID_allocate);
   malloc_expr.copy_to_operands(object_size);
+  // code use true and get rid of the code below
+  malloc_expr.copy_to_operands(false_exprt());
   malloc_expr.type()=rhs.type();
 
   goto_programt::targett t_n=dest.add_instruction(ASSIGN);
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index c96e3941cf3..96532adfa84 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -762,7 +762,7 @@ void goto_convertt::convert_assign(
   }
   else if(
     rhs.id() == ID_side_effect &&
-    (rhs.get(ID_statement) == ID_malloc ||
+    (rhs.get(ID_statement) == ID_allocate ||
      rhs.get(ID_statement) == ID_java_new_array_data))
   {
     // just preserve
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index ac12c64be41..898c7fdace2 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_malloc)
+  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/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 5a379a880f5..0a2a7ec6e72 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -448,18 +448,19 @@ void interpretert::evaluate(
         error() << "nondet not implemented" << eom;
       return;
     }
-    else if(side_effect.get_statement()==ID_malloc)
+    else if(side_effect.get_statement()==ID_allocate)
     {
       if(show)
-        error() << "malloc not fully implemented "
+        error() << "heap memory allocation not fully implemented "
                 << expr.type().subtype().pretty()
                 << eom;
       std::stringstream buffer;
       num_dynamic_objects++;
-      buffer << "interpreter::malloc_object" << num_dynamic_objects;
+      buffer << "interpreter::dynamic_object" << num_dynamic_objects;
       irep_idt id(buffer.str().c_str());
       mp_integer address=build_memory_map(id, expr.type().subtype());
       // TODO: check array of type
+      // TODO: interpret zero-initialization argument
       dest.push_back(address);
       return;
     }
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index afe372664d1..096c4766377 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -321,7 +321,7 @@ class goto_symext
 
   virtual void symex_gcc_builtin_va_arg_next(
     statet &state, const exprt &lhs, const side_effect_exprt &code);
-  virtual void symex_malloc(
+  virtual void symex_allocate(
     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(
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index f8db5a92442..8369ef5db2f 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -63,8 +63,8 @@ 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_malloc)
-      symex_malloc(state, lhs, side_effect_expr);
+    else if(statement==ID_allocate)
+      symex_allocate(state, lhs, side_effect_expr);
     else if(statement==ID_printf)
       symex_printf(state, lhs, side_effect_expr);
     else if(statement==ID_gcc_builtin_va_arg_next)
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index abd1b23729c..9bf02bf1e2e 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 
+#include <util/expr_util.h>
+#include <util/message.h>
 #include <util/arith_tools.h>
 #include <util/cprover_prefix.h>
 #include <util/std_types.h>
@@ -51,13 +53,13 @@ inline static typet c_sizeof_type_rec(const exprt &expr)
   return nil_typet();
 }
 
-void goto_symext::symex_malloc(
+void goto_symext::symex_allocate(
   statet &state,
   const exprt &lhs,
   const side_effect_exprt &code)
 {
-  if(code.operands().size()!=1)
-    throw "malloc expected to have one operand";
+  if(code.operands().size()!=2)
+    throw "allocate expected to have two operands";
 
   if(lhs.is_nil())
     return; // ignore
@@ -165,6 +167,32 @@ void goto_symext::symex_malloc(
 
   new_symbol_table.add(value_symbol);
 
+  exprt zero_init=code.op1();
+  state.rename(zero_init, ns); // to allow constant propagation
+  simplify(zero_init, ns);
+
+  if(!zero_init.is_constant())
+    throw "allocate expects constant as second argument";
+
+  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);
+
+    if(zero_value.is_not_nil())
+    {
+      code_assignt assignment(value_symbol.symbol_expr(), zero_value);
+      symex_assign_rec(state, assignment);
+    }
+    else
+      throw "failed to zero initialize dynamic object";
+  }
+
   exprt rhs;
 
   if(object_type.id()==ID_array)
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 60460ffcb21..910c9e29692 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -195,8 +195,9 @@ 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_malloc);
+    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);
     malloc_expr.type()=result_type;
     // create a symbol for the malloc expression so we can initialize
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 032ab702f16..333c07158dd 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -631,8 +631,8 @@ void value_sett::get_value_set_rec(
       objectt object=it->second;
 
       // adjust by offset
-      if(object.offset_is_zero() && i_is_set)
-        object.offset=i;
+      if(object.offset_is_set && i_is_set)
+        object.offset+=i;
       else
         object.offset_is_set=false;
 
@@ -678,7 +678,7 @@ void value_sett::get_value_set_rec(
       // these should be gone
       throw "unexpected function_call sideeffect";
     }
-    else if(statement==ID_malloc)
+    else if(statement==ID_allocate)
     {
       assert(suffix=="");
 
@@ -1005,7 +1005,7 @@ void value_sett::get_reference_set_rec(
         {
         }
         else if(!to_integer(offset, i) &&
-                o.offset_is_zero())
+                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 1323ee31b59..0e4c966817e 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -559,7 +559,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       result.value=o.root_object();
 
       // this is relative to the root object
-      const exprt offset=pointer_offset(pointer_expr);
+      exprt offset;
+      if(o.offset().id()==ID_unknown)
+        offset=pointer_offset(pointer_expr);
+      else
+        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 8b38d975d0d..7e661711c39 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_malloc)
+    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 b3c5a53726c..8ab9ff2c117 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_malloc)
+    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 ae7ec38a526..a405e2d2242 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_malloc)
+    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 c430c44ff06..9cbe9309647 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
 #include <util/pointer_offset_size.h>
@@ -135,7 +136,7 @@ bool bv_pointerst::convert_address_of_rec(
     {
       // this should be gone
       bv=convert_pointer_type(array);
-      assert(bv.size()==bits);
+      POSTCONDITION(bv.size()==bits);
     }
     else if(array_type.id()==ID_array ||
             array_type.id()==ID_incomplete_array ||
@@ -143,18 +144,18 @@ bool bv_pointerst::convert_address_of_rec(
     {
       if(convert_address_of_rec(array, bv))
         return true;
-      assert(bv.size()==bits);
+      POSTCONDITION(bv.size()==bits);
     }
     else
-      assert(false);
+      UNREACHABLE;
 
     // get size
     mp_integer size=
       pointer_offset_size(array_type.subtype(), ns);
-    assert(size>0);
+    DATA_INVARIANT(size>0, "array subtype expected to have non-zero size");
 
     offset_arithmetic(bv, size, index);
-    assert(bv.size()==bits);
+    POSTCONDITION(bv.size()==bits);
     return false;
   }
   else if(expr.id()==ID_member)
@@ -172,7 +173,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);
-      assert(offset>=0);
+      DATA_INVARIANT(offset>=0, "member offset expected to be positive");
 
       // add offset
       offset_arithmetic(bv, offset);
@@ -295,7 +296,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       return bv;
     }
 
-    assert(bv.size()==bits);
+    POSTCONDITION(bv.size()==bits);
     return bv;
   }
   else if(expr.id()==ID_constant)
@@ -333,13 +334,13 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       {
         count++;
         bv=convert_bv(*it);
-        assert(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);
-        assert(size>0);
+        POSTCONDITION(size>0);
       }
     }
 
@@ -413,7 +414,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 
     mp_integer element_size=
       pointer_offset_size(expr.op0().type().subtype(), ns);
-    assert(element_size>0);
+    DATA_INVARIANT(element_size>0, "object size expected to be non-zero");
 
     offset_arithmetic(bv, element_size, neg_op1);
 
@@ -470,7 +471,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
 
     mp_integer element_size=
       pointer_offset_size(expr.op0().type().subtype(), ns);
-    assert(element_size>0);
+    DATA_INVARIANT(element_size>0, "object size expected to be non-zero");
 
     if(element_size!=1)
     {
@@ -570,7 +571,7 @@ exprt bv_pointerst::bv_get_rec(
 
   for(std::size_t i=0; i<bits; i++)
   {
-    char ch;
+    char ch=0;
     std::size_t bit_nr=i+offset;
 
     if(unknown[bit_nr])
@@ -720,8 +721,8 @@ void bv_pointerst::do_postponed(
       bvt saved_bv=postponed.op;
       saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
 
-      assert(bv.size()==saved_bv.size());
-      assert(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();
@@ -773,8 +774,8 @@ void bv_pointerst::do_postponed(
       bvt saved_bv=postponed.op;
       saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
 
-      assert(bv.size()==saved_bv.size());
-      assert(postponed.bv.size()>=1);
+      POSTCONDITION(bv.size()==saved_bv.size());
+      PRECONDITION(postponed.bv.size()>=1);
 
       literalt l1=bv_utils.equal(bv, saved_bv);
 
@@ -785,7 +786,7 @@ void bv_pointerst::do_postponed(
     }
   }
   else
-    assert(false);
+    UNREACHABLE;
 }
 
 void bv_pointerst::post_process()
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 9a999737c30..005124d0ea7 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -209,7 +209,7 @@ IREP_ID_ONE(destination)
 IREP_ID_ONE(main)
 IREP_ID_ONE(expression)
 IREP_ID_ONE(free)
-IREP_ID_ONE(malloc)
+IREP_ID_ONE(allocate)
 IREP_ID_TWO(C_cxx_alloc_type, #cxx_alloc_type)
 IREP_ID_ONE(cpp_new)
 IREP_ID_ONE(cpp_delete)