diff --git a/regression/cbmc-concurrency/thread_chain_posix2/test.desc b/regression/cbmc-concurrency/thread_chain_posix2/test.desc
index 19fca26941b..144bf7efe01 100644
--- a/regression/cbmc-concurrency/thread_chain_posix2/test.desc
+++ b/regression/cbmc-concurrency/thread_chain_posix2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 -D_ENABLE_CHAIN_ --unwind 2
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/thread_chain_posix3/test.desc b/regression/cbmc-concurrency/thread_chain_posix3/test.desc
index 8c70666b904..a2481a984ad 100644
--- a/regression/cbmc-concurrency/thread_chain_posix3/test.desc
+++ b/regression/cbmc-concurrency/thread_chain_posix3/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 -D_ENABLE_CHAIN_ -D_SANITY_CHECK_ --unwind 2
 ^EXIT=10$
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/Local_out_of_scope3/main.c b/regression/cbmc/Local_out_of_scope3/main.c
new file mode 100644
index 00000000000..fc5fc46f07e
--- /dev/null
+++ b/regression/cbmc/Local_out_of_scope3/main.c
@@ -0,0 +1,15 @@
+int main()
+{
+  int *p=0;
+
+  for(int i=0; i<3; ++i)
+  {
+    {
+      int x=42;
+      p=&x;
+      *p=1;
+    }
+  }
+
+  return 0;
+}
diff --git a/regression/cbmc/Local_out_of_scope3/test.desc b/regression/cbmc/Local_out_of_scope3/test.desc
new file mode 100644
index 00000000000..39c491ba8bb
--- /dev/null
+++ b/regression/cbmc/Local_out_of_scope3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^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/realloc3/test.desc b/regression/cbmc/realloc3/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/realloc3/test.desc
+++ b/regression/cbmc/realloc3/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 15cda33e864..08fcd46765d 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -296,7 +296,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/goto_check.cpp b/src/analyses/goto_check.cpp
index 354d12503ec..913797067ed 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1654,6 +1654,34 @@ void goto_checkt::goto_check(
         }
       }
     }
+    else if(i.is_decl())
+    {
+      if(enable_pointer_check)
+      {
+        assert(i.code.operands().size()==1);
+        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 219d446eea2..eca647bb74d 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -234,7 +234,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 02a5c698186..a7023001814 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 a29419961a0..4022bc467ce 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -158,7 +158,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"
@@ -197,6 +197,18 @@ void ansi_c_internal_additions(std::string &code)
     "long double __CPROVER_infl(void);\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"
+    "int __CPROVER_isgreaterequald(double f, double g);\n"
+    "int __CPROVER_islessf(float f, float g);\n"
+    "int __CPROVER_islessd(double f, double g);\n"
+    "int __CPROVER_islessequalf(float f, float g);\n"
+    "int __CPROVER_islessequald(double f, double g);\n"
+    "int __CPROVER_islessgreaterf(float f, float g);\n"
+    "int __CPROVER_islessgreaterd(double f, double g);\n"
+    "int __CPROVER_isunorderedf(float f, float g);\n"
+    "int __CPROVER_isunorderedd(double f, double g);\n"
 
     // absolute value
     "int __CPROVER_abs(int x);\n"
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 58806f5f6b1..e02b34d1ca0 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2258,16 +2258,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 c50d075abaa..cffd7ab2cf1 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -679,6 +679,7 @@ std::string expr2ct::convert_struct_type(
   if(tag!="")
     dest+=" "+id2string(tag);
 
+#if 0
   if(inc_struct_body)
   {
     dest+=" {";
@@ -702,6 +703,7 @@ std::string expr2ct::convert_struct_type(
 
     dest+=" }";
   }
+#endif
 
   dest+=declarator;
 
@@ -1095,17 +1097,20 @@ std::string expr2ct::convert_pointer_object_has_type(
   return dest;
 }
 
-std::string expr2ct::convert_malloc(
+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 dest="MALLOC";
+  unsigned p1;
+  std::string op1=convert_with_precedence(src.op0(), p1);
+
+  std::string dest="ALLOCATE";
   dest+='(';
 
   if(src.type().id()==ID_pointer &&
@@ -1115,7 +1120,7 @@ std::string expr2ct::convert_malloc(
     dest+=", ";
   }
 
-  dest+=op0;
+  dest+=op0+", "+op1;
   dest+=')';
 
   return dest;
@@ -3629,8 +3634,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 ac9c529145a..34be13ba37c 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;
@@ -92,6 +92,7 @@ double __CPROVER_inf(void);
 float __CPROVER_inff(void);
 long double __CPROVER_infl(void);
 //extern int __CPROVER_thread_local __CPROVER_rounding_mode;
+int __CPROVER_isgreaterd(double f, double g);
 
 // absolute value
 int __CPROVER_abs(int);
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index 7312708fb8c..1af12148d83 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -22,8 +22,69 @@ inline long double __builtin_fabsl(long double d) { return __CPROVER_fabsl(d); }
 
 inline float __builtin_fabsf(float f) { return __CPROVER_fabsf(f); }
 
+/* FUNCTION: __CPROVER_isgreaterf */
+
+int __CPROVER_isgreaterf(float f, float g) { return f > g; }
+
+/* FUNCTION: __CPROVER_isgreaterd */
+
+int __CPROVER_isgreaterd(double f, double g) { return f > g; }
+
+/* FUNCTION: __CPROVER_isgreaterequalf */
+
+int __CPROVER_isgreaterequalf(float f, float g) { return f >= g; }
+
+/* FUNCTION: __CPROVER_isgreaterequald */
+
+int __CPROVER_isgreaterequald(double f, double g) { return f >= g; }
+
+/* FUNCTION: __CPROVER_islessf */
+
+int __CPROVER_islessf(float f, float g) { return f < g;}
+
+/* FUNCTION: __CPROVER_islessd */
+
+int __CPROVER_islessd(double f, double g) { return f < g;}
+
+/* FUNCTION: __CPROVER_islessequalf */
+
+int __CPROVER_islessequalf(float f, float g) { return f <= g; }
+
+/* FUNCTION: __CPROVER_islessequald */
+
+int __CPROVER_islessequald(double f, double g) { return f <= g; }
+
+/* FUNCTION: __CPROVER_islessgreaterf */
+
+int __CPROVER_islessgreaterf(float f, float g) { return (f < g) || (f > g); }
+
+/* FUNCTION: __CPROVER_islessgreaterd */
+
+int __CPROVER_islessgreaterd(double f, double g) { return (f < g) || (f > g); }
+
+/* FUNCTION: __CPROVER_isunorderedf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+int __CPROVER_isunorderedf(float f, float g) { return isnanf(f) || isnanf(g); }
+
+/* FUNCTION: __CPROVER_isunorderedd */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+int __CPROVER_isunorderedd(double f, double g) { return isnan(f) || isnan(g); }
+
+
 /* FUNCTION: isfinite */
 
+#undef isfinite
+
 int isfinite(double d) { return __CPROVER_isfinited(d); }
 
 /* FUNCTION: __finite */
@@ -40,6 +101,8 @@ int __finitel(long double ld) { return __CPROVER_isfiniteld(ld); }
 
 /* FUNCTION: isinf */
 
+#undef isinf
+
 inline int isinf(double d) { return __CPROVER_isinfd(d); }
 
 /* FUNCTION: __isinf */
@@ -64,6 +127,8 @@ inline int __isinfl(long double ld) { return __CPROVER_isinfld(ld); }
 
 /* FUNCTION: isnan */
 
+#undef isnan
+
 inline int isnan(double d) { return __CPROVER_isnand(d); }
 
 /* FUNCTION: __isnan */
@@ -88,6 +153,8 @@ inline int __isnanl(long double ld) { return __CPROVER_isnanld(ld); }
 
 /* FUNCTION: isnormal */
 
+#undef isnormal
+
 inline int isnormal(double d) { return __CPROVER_isnormald(d); }
 
 /* FUNCTION: __isnormalf */
@@ -152,6 +219,8 @@ inline int _fdsign(float f) { return __CPROVER_signf(f); }
 
 /* FUNCTION: signbit */
 
+#undef signbit
+
 inline int signbit(double d) { return __CPROVER_signd(d); }
 
 /* FUNCTION: __signbitd */
@@ -423,10 +492,70 @@ float __builtin_nanf(const char *str)
 {
   // the 'str' argument is not yet used
 __CPROVER_hide:;
+  (void)*str;
+  return 0.0f/0.0f;
+}
+
+
+/* ISO 9899:2011
+ * The call nan("n-char-sequence") is equivalent to
+ * strtod("NAN(n-char-sequence)", (char**) NULL); the call nan("") is
+ * equivalent to strtod("NAN()", (char**) NULL). If tagp does not
+ * point to an n-char sequence or an empty string, the call is
+ * equivalent to strtod("NAN", (char**) NULL). Calls to nanf and nanl
+ * are equivalent to the corresponding calls to strtof and strtold.
+ *
+ * The nan functions return a quiet NaN, if available, with content
+ * indicated through tagp. If the implementation does not support
+ * quiet NaNs, the functions return zero.
+ */
+
+/* FUNCTION: nan */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+double nan(const char *str) {
+  // the 'str' argument is not yet used
+ __CPROVER_hide:;
+  (void)*str;
+  return 0.0/0.0;
+}
+
+/* FUNCTION: nanf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+float nanf(const char *str) {
+  // the 'str' argument is not yet used
+ __CPROVER_hide:;
+  (void)*str;
+  return 0.0f/0.0f;
+}
+
+/* FUNCTION: nanl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+long double nanl(const char *str) {
+  // the 'str' argument is not yet used
+ __CPROVER_hide:;
   (void)*str;
   return 0.0/0.0;
 }
 
+
+
+
+
 /* FUNCTION: nextUpf */
 
 #ifndef __CPROVER_LIMITS_H_INCLUDED
@@ -575,6 +704,7 @@ __CPROVER_hide:;
     --m.bv;
     return m.f;
   }
+  
 }
 
 
@@ -608,8 +738,6 @@ __CPROVER_hide:;
 
 float nextUpf(float f);
 
-extern int __CPROVER_rounding_mode;
-
 float sqrtf(float f)
 {
  __CPROVER_hide:;
@@ -645,7 +773,7 @@ float sqrtf(float f)
     __CPROVER_assume(f < upperSquare);
 
     // Select between them to work out which to return
-    switch(__CPROVER_rounding_mode)
+    switch(fegetround())
     {
     case FE_TONEAREST :
       return (f - lowerSquare < upperSquare - f) ? lower : upper; break;
@@ -720,7 +848,7 @@ double sqrt(double d)
     __CPROVER_assume(lowerSquare <= d);
     __CPROVER_assume(d < upperSquare);
 
-    switch(__CPROVER_rounding_mode)
+    switch(fegetround())
     {
     case FE_TONEAREST:
       return (d - lowerSquare < upperSquare - d) ? lower : upper; break;
@@ -789,7 +917,7 @@ long double sqrtl(long double d)
     __CPROVER_assume(lowerSquare <= d);
     __CPROVER_assume(d < upperSquare);
 
-    switch(__CPROVER_rounding_mode)
+    switch(fegetround())
     {
     case FE_TONEAREST:
       return (d - lowerSquare < upperSquare - d) ? lower : upper; break;
@@ -816,3 +944,1381 @@ long double sqrtl(long double d)
     return root;
   }
 }
+
+
+/* ISO 9899:2011
+ * The fmax functions determine the maximum numeric value of their
+ * arguments. 242)
+ *
+ * 242) NaN arguments are treated as missing data: if one argument is
+ * a NaN and the other numeric, then the fmax functions choose the
+ * numeric value. See F.10.9.2.
+ *
+ * - If just one argument is a NaN, the fmax functions return the other
+ *   argument (if both arguments are NaNs, the functions return a NaN).
+ * - The returned value is exact and is independent of the current
+ *   rounding direction mode.
+ * - The body of the fmax function might be 374)
+ *       { return (isgreaterequal(x, y) || isnan(y)) ? x : y; }
+ *
+ * 374) Ideally, fmax would be sensitive to the sign of zero, for
+ * example fmax(-0.0, +0.0) would return +0; however, implementation
+ * in software might be impractical.
+ */
+
+/* FUNCTION: fmax */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+// TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB
+double fmax(double f, double g) { return ((f >= g) || isnan(g)) ? f : g; }
+
+/* FUNCTION : fmaxf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+// TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB
+float fmaxf(float f, float g) { return ((f >= g) || isnan(g)) ? f : g; }
+
+
+/* FUNCTION : fmaxl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+// TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB
+long double fmaxl(long double f, long double g) { return ((f >= g) || isnan(g)) ? f : g; }
+
+
+/* ISO 9899:2011
+ * The fmin functions determine the minimum numeric value of their
+ * arguments.243)
+ *
+ * 243) The fmin functions are analogous to the fmax functions in
+ * their treatment of NaNs.
+ *
+ * - The fmin functions are analogous to the fmax functions (see F.10.9.2).
+ * - The returned value is exact and is independent of the current
+ *   rounding direction mode.
+ */
+
+/* FUNCTION: fmin */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+ 
+// TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB
+double fmin(double f, double g) { return ((f <= g) || isnan(g)) ? f : g; }
+
+/* FUNCTION: fminf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+// TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB 
+float fminf(float f, float g) { return ((f <= g) || isnan(g)) ? f : g; }
+
+/* FUNCTION: fminl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+// TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB 
+long double fminl(long double f, long double g) { return ((f <= g) || isnan(g)) ? f : g; }
+
+
+/* ISO 9899:2011
+ * The fdim functions determine the positive difference between their
+ * arguments:
+ *     x - y if x > y
+ *     +0    if x <= y
+ * A range error may occur.
+ */
+
+/* FUNCTION: fdim */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+double fdim(double f, double g) { return ((f > g) ? f - g : +0.0); }
+
+
+/* FUNCTION: fdimf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+float fdimf(float f, float g) { return ((f > g) ? f - g : +0.0f); }
+
+
+/* FUNCTION: fdiml */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+long double fdiml(long double f, long double g) { return ((f > g) ? f - g : +0.0); }
+
+
+
+/* FUNCTION: __sort_of_CPROVER_round_to_integral */
+// TODO : Should be a real __CPROVER function to convert to SMT-LIB
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d)
+{
+  double magicConst = 0x1.0p+52;
+  double return_value;
+  int saved_rounding_mode = fegetround();
+  fesetround(rounding_mode);
+  
+  if (fabs(d) >= magicConst || d == 0.0)
+  {
+    return_value = d;
+  }
+  else
+  {
+    if (!signbit(d)) {
+      double tmp = d + magicConst;
+      return_value = tmp - magicConst;
+    } else {
+      double tmp = d - magicConst;
+      return_value = tmp + magicConst;    
+    }
+  }
+
+  fesetround(saved_rounding_mode);
+  return return_value;
+}
+
+/* FUNCTION: __sort_of_CPROVER_round_to_integralf */
+// TODO : Should be a real __CPROVER function to convert to SMT-LIB
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d)
+{
+  float magicConst = 0x1.0p+23f;  // 23 is significant
+  float return_value;
+  int saved_rounding_mode = fegetround();
+  fesetround(rounding_mode);
+  
+  if (fabsf(d) >= magicConst || d == 0.0)
+  {
+    return_value = d;
+  }
+  else
+  {
+    if (!signbit(d)) {
+      float tmp = d + magicConst;
+      return_value = tmp - magicConst;    
+    } else {
+      float tmp = d - magicConst;
+      return_value = tmp + magicConst;    
+    }
+  }
+
+  fesetround(saved_rounding_mode);
+  return return_value;
+}
+
+
+/* FUNCTION: __sort_of_CPROVER_round_to_integrall */
+// TODO : Should be a real __CPROVER function to convert to SMT-LIB
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d)
+{
+  long double magicConst = 0x1.0p+64;
+  long double return_value;
+  int saved_rounding_mode = fegetround();
+  fesetround(rounding_mode);
+  
+  if (fabsl(d) >= magicConst || d == 0.0)
+  {
+    return_value = d;
+  }
+  else
+  {
+    if (!signbit(d)) {
+      long double tmp = d + magicConst;
+      return_value = tmp - magicConst;    
+    } else {
+      long double tmp = d - magicConst;
+      return_value = tmp + magicConst;    
+    }
+  }
+
+  fesetround(saved_rounding_mode);
+  return return_value;
+}
+
+/* ISO 9899:2011
+ *
+ * The ceil functions compute the smallest integer value not less than
+ * x.
+ */
+
+/* FUNCTION: ceil */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+
+double ceil(double x)
+{
+  return __sort_of_CPROVER_round_to_integral(FE_UPWARD, x);
+}
+
+/* FUNCTION: ceilf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+
+float ceilf(float x)
+{
+  return __sort_of_CPROVER_round_to_integralf(FE_UPWARD, x);
+}
+
+
+/* FUNCTION: ceill */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+
+long double ceill(long double x)
+{
+  return __sort_of_CPROVER_round_to_integrall(FE_UPWARD, x);
+}
+
+
+/* ISO 9899:2011
+ *
+ * The floor functions compute the largest integer value not greater than x.
+ */
+
+/* FUNCTION: floor */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+
+double floor(double x)
+{
+  return __sort_of_CPROVER_round_to_integral(FE_DOWNWARD, x);
+}
+
+/* FUNCTION: floorf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+
+float floorf(float x)
+{
+  return __sort_of_CPROVER_round_to_integralf(FE_DOWNWARD, x);
+}
+
+
+/* FUNCTION: floorl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+
+long double floorl(long double x)
+{
+  return __sort_of_CPROVER_round_to_integrall(FE_DOWNWARD, x);
+}
+
+
+/* ISO 9899:2011
+ *
+ * The trunc functions round their argument to the integer value, in
+ * floating format, nearest to but no larger in magnitude than the argument.
+ */
+
+/* FUNCTION: trunc */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+
+double trunc(double x)
+{
+  return __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, x);
+}
+
+/* FUNCTION: truncf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+
+float truncf(float x)
+{
+  return __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, x);
+}
+
+
+/* FUNCTION: truncl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+
+long double truncl(long double x)
+{
+  return __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, x);
+}
+
+
+/* ISO 9899:2011
+ *
+ * The round functions round their argument to the integer value, in
+ * floating format, nearest to but no larger in magnitude than the argument.
+ */
+
+/* FUNCTION: round */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+
+double round(double x)
+{
+  // Tempting but RNE not RNA
+  // return __sort_of_CPROVER_round_to_integral(FE_TONEAREST, x);
+
+  int saved_rounding_mode = fegetround();
+  fesetround(FE_TOWARDZERO);
+
+  double xp;
+  if (x > 0.0) {
+    xp = x + 0.5;
+  } else if (x < 0.0) {
+    xp = x - 0.5;
+  } else {
+    xp = x;
+  }
+
+  fesetround(saved_rounding_mode);
+  
+  return __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, xp);
+}
+
+/* FUNCTION: roundf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+
+float roundf(float x)
+{
+  // Tempting but RNE not RNA
+  // return __sort_of_CPROVER_round_to_integralf(FE_TONEAREST, x);
+
+  int saved_rounding_mode = fegetround();
+  fesetround(FE_TOWARDZERO);
+
+  float xp;
+  if (x > 0.0f) {
+    xp = x + 0.5f;
+  } else if (x < 0.0f) {
+    xp = x - 0.5f;
+  } else {
+    xp = x;
+  }
+
+  fesetround(saved_rounding_mode);
+  
+  return __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, xp);
+}
+
+
+/* FUNCTION: roundl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+
+long double roundl(long double x)
+{
+  // Tempting but RNE not RNA
+  // return __sort_of_CPROVER_round_to_integrall(FE_TONEAREST, x);
+
+  int saved_rounding_mode = fegetround();
+  fesetround(FE_TOWARDZERO);
+
+  long double xp;
+  if (x > 0.0) {
+    xp = x + 0.5;
+  } else if (x < 0.0) {
+    xp = x - 0.5;
+  } else {
+    xp = x;
+  }
+
+  fesetround(saved_rounding_mode);
+  
+  return __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, xp);
+}
+
+
+
+/* ISO 9899:2011
+ *
+ * The nearbyint functions round their argument to an integer value in
+ * floating-point format, using the current rounding direction and
+ * without raising the inexact floating-point exception.
+ */
+
+/* FUNCTION: nearbyint */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+
+double nearbyint(double x)
+{
+  return __sort_of_CPROVER_round_to_integral(fegetround(), x);
+}
+
+/* FUNCTION: nearbyintf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+
+float nearbyintf(float x)
+{
+  return __sort_of_CPROVER_round_to_integralf(fegetround(), x);
+}
+
+
+/* FUNCTION: nearbyintl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+
+long double nearbyintl(long double x)
+{
+  return __sort_of_CPROVER_round_to_integrall(fegetround(), x);
+}
+
+
+
+/* ISO 9899:2011
+ *
+ * The rint functions differ from the nearbyint functions (7.12.9.3)
+ * only in that the rint functions may raise the inexact
+ * floating-point exception if the result differs in value from the argument.
+ */
+
+/* FUNCTION: rint */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+
+double rint(double x)
+{
+  return __sort_of_CPROVER_round_to_integral(fegetround(), x);
+}
+
+/* FUNCTION: rintf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+
+float rintf(float x)
+{
+  return __sort_of_CPROVER_round_to_integralf(fegetround(), x);
+}
+
+/* FUNCTION: rintl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+
+long double rintl(long double x)
+{
+  return __sort_of_CPROVER_round_to_integrall(fegetround(), x);
+}
+
+
+
+/* ISO 9899:2011
+ *
+ * The lrint and llrint functions round their argument to the nearest
+ * integer value, rounding according to the current rounding
+ * direction. If the rounded value is outside the range of the return
+ * type, the numeric result is unspecified and a domain error or range
+ * error may occur.
+ */
+
+/* FUNCTION: lrint */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+
+long int lrint(double x)
+{
+  // TODO : should be an all-in-one __CPROVER function to allow
+  // conversion to SMT
+  double rti = __sort_of_CPROVER_round_to_integral(fegetround(), x);
+  return (long int)rti;
+}
+
+/* FUNCTION: lrintf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+
+long int lrintf(float x)
+{
+  // TODO : should be an all-in-one __CPROVER function to allow
+  // conversion to SMT
+  float rti = __sort_of_CPROVER_round_to_integralf(fegetround(), x);
+  return (long int)rti;
+}
+
+
+/* FUNCTION: lrintl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+
+long int lrintl(long double x)
+{
+  // TODO : should be an all-in-one __CPROVER function to allow
+  // conversion to SMT
+  long double rti = __sort_of_CPROVER_round_to_integrall(fegetround(), x);
+  return (long int)rti;
+}
+
+
+/* FUNCTION: llrint */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+
+long long int llrint(double x)
+{
+  // TODO : should be an all-in-one __CPROVER function to allow
+  // conversion to SMT
+  double rti = __sort_of_CPROVER_round_to_integral(fegetround(), x);
+  return (long long int)rti;
+}
+
+/* FUNCTION: llrintf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+
+long long int llrintf(float x)
+{
+  // TODO : should be an all-in-one __CPROVER function to allow
+  // conversion to SMT
+  float rti = __sort_of_CPROVER_round_to_integralf(fegetround(), x);
+  return (long long int)rti;
+}
+
+
+/* FUNCTION: llrintl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+
+long long int llrintl(long double x)
+{
+  // TODO : should be an all-in-one __CPROVER function to allow
+  // conversion to SMT
+  long double rti = __sort_of_CPROVER_round_to_integrall(fegetround(), x);
+  return (long long int)rti;
+}
+
+
+/* ISO 9899:2011
+ *
+ * The lround and llround functions round their argument to the
+ * nearest integer value, rounding halfway cases away from zero,
+ * regardless of the current rounding direction. If the rounded value
+ * is outside the range of the return type, the numeric result is
+ * unspecified and a domain error or range error may occur.
+ */
+
+/* FUNCTION: lround */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+
+long int lround(double x)
+{
+  // TODO : should be an all-in-one __CPROVER function to allow
+  // conversion to SMT, plus should use RNA
+
+  int saved_rounding_mode = fegetround();
+  fesetround(FE_TOWARDZERO);
+
+  double xp;
+  if (x > 0.0) {
+    xp = x + 0.5;
+  } else if (x < 0.0) {
+    xp = x - 0.5;
+  } else {
+    xp = x;
+  }
+
+  fesetround(saved_rounding_mode);
+  
+  double rti = __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, xp);
+  return (long int)rti;
+}
+
+/* FUNCTION: lroundf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+
+long int lroundf(float x)
+{
+  // TODO : should be an all-in-one __CPROVER function to allow
+  // conversion to SMT, plus should use RNA
+  int saved_rounding_mode = fegetround();
+  fesetround(FE_TOWARDZERO);
+
+  float xp;
+  if (x > 0.0f) {
+    xp = x + 0.5f;
+  } else if (x < 0.0f) {
+    xp = x - 0.5f;
+  } else {
+    xp = x;
+  }
+
+  fesetround(saved_rounding_mode);
+  
+  float rti = __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, xp);
+  return (long int)rti;
+}
+
+
+/* FUNCTION: lroundl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+
+long int lroundl(long double x)
+{
+  int saved_rounding_mode = fegetround();
+  fesetround(FE_TOWARDZERO);
+
+  // TODO : should be an all-in-one __CPROVER function to allow
+  // conversion to SMT, plus should use RNA
+  long double xp;
+  if (x > 0.0) {
+    xp = x + 0.5;
+  } else if (x < 0.0) {
+    xp = x - 0.5;
+  } else {
+    xp = x;
+  }
+
+  fesetround(saved_rounding_mode);
+  
+  long double rti = __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, xp);
+  return (long int)rti;
+}
+
+
+/* FUNCTION: llround */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+
+long long int llround(double x)
+{
+  // TODO : should be an all-in-one __CPROVER function to allow
+  // conversion to SMT, plus should use RNA
+  int saved_rounding_mode = fegetround();
+  fesetround(FE_TOWARDZERO);
+
+  double xp;
+  if (x > 0.0) {
+    xp = x + 0.5;
+  } else if (x < 0.0) {
+    xp = x - 0.5;
+  } else {
+    xp = x;
+  }
+
+  fesetround(saved_rounding_mode);
+  
+  double rti = __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, xp);
+  return (long long int)rti;
+}
+
+/* FUNCTION: llroundf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+
+long long int llroundf(float x)
+{
+  // TODO : should be an all-in-one __CPROVER function to allow
+  // conversion to SMT, plus should use RNA
+  int saved_rounding_mode = fegetround();
+  fesetround(FE_TOWARDZERO);
+
+  float xp;
+  if (x > 0.0f) {
+    xp = x + 0.5f;
+  } else if (x < 0.0f) {
+    xp = x - 0.5f;
+  } else {
+    xp = x;
+  }
+
+  fesetround(saved_rounding_mode);
+  
+  float rti = __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, xp);
+  return (long long int)rti;
+}
+
+
+/* FUNCTION: llroundl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+
+long long int llroundl(long double x)
+{
+  // TODO : should be an all-in-one __CPROVER function to allow
+  // conversion to SMT, plus should use RNA
+  int saved_rounding_mode = fegetround();
+  fesetround(FE_TOWARDZERO);
+
+  long double xp;
+  if (x > 0.0) {
+    xp = x + 0.5;
+  } else if (x < 0.0) {
+    xp = x - 0.5;
+  } else {
+    xp = x;
+  }
+
+  fesetround(saved_rounding_mode);
+  
+  long double rti = __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, xp);
+  return (long long int)rti;
+}
+
+
+/* ISO 9899:2011
+ *
+ * The modf functions break the argument value into integral and
+ * fractional parts, each of which has the same type and sign as the
+ * argument. They store the integral part (in floating-point format)
+ * in the object pointed to by iptr.
+ */
+
+/* FUNCTION: modf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+
+double modf(double x, double *iptr)
+{
+  *iptr = __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, x);
+  return (x - *iptr);
+}
+
+/* FUNCTION: modff */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+
+  float modff(float x, float *iptr)
+{
+  *iptr = __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, x);
+  return (x - *iptr);
+}
+
+
+/* FUNCTION: modfl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+
+  long double modfl(long double x, long double *iptr)
+{
+  *iptr = __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, x);
+  return (x - *iptr);
+}
+
+
+
+/* FUNCTION: __sort_of_CPROVER_remainder */
+// TODO : Should be a real __CPROVER function to convert to SMT-LIB
+double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+  
+double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y)
+{
+  if (x == 0.0 || __CPROVER_isinfd(y))
+    return x;
+
+  // Extended precision helps... a bit...
+  long double div = x/y;
+  long double n = __sort_of_CPROVER_round_to_integral(rounding_mode,div);
+  long double res = (-y * n) + x;   // TODO : FMA would be an improvement
+  return res;
+}
+
+/* FUNCTION: __sort_of_CPROVER_remainderf */
+// TODO : Should be a real __CPROVER function to convert to SMT-LIB
+
+float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+
+float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y)
+{
+  if (x == 0.0f || __CPROVER_isinff(y))
+    return x;
+
+  // Extended precision helps... a bit...
+  long double div = x/y;
+  long double n = __sort_of_CPROVER_round_to_integral(rounding_mode,div);
+  long double res = (-y * n) + x;   // TODO : FMA would be an improvement
+  return res;
+}
+
+/* FUNCTION: __sort_of_CPROVER_remainderl */
+// TODO : Should be a real __CPROVER function to convert to SMT-LIB
+
+long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+
+long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y)
+{
+  if (x == 0.0 || __CPROVER_isinfld(y))
+    return x;
+
+  // Extended precision helps... a bit...
+  long double div = x/y;
+  long double n = __sort_of_CPROVER_round_to_integral(rounding_mode,div);
+  long double res = (-y * n) + x;   // TODO : FMA would be an improvement
+  return res;
+}
+
+
+
+/* ISO 9899:2011
+ *
+ * The fmod functions return the value x - ny, for some
+ * integer n such that, if y is nonzero, the result has the same sign
+ * as x and magnitude less than the magnitude of y. If y is zero,
+ * whether a domain error occurs or the fmod functions return zero is
+ * implementation-defined.
+ */
+
+/* FUNCTION: fmod */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y);
+
+double fmod(double x, double y) { return __sort_of_CPROVER_remainder(FE_TOWARDZERO, x, y); }
+
+
+/* FUNCTION: fmodf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y);
+
+float fmodf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TOWARDZERO, x, y); }
+
+
+/* FUNCTION: fmodl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y);
+
+long double fmodl(long double x, long double y) { return __sort_of_CPROVER_remainderl(FE_TOWARDZERO, x, y); }
+
+
+
+/* ISO 9899:2011
+ *
+ * The remainder functions compute the remainder x REM y required by
+ * IEC 60559.239)
+ *
+ * 239) "When y != 0, the remainder r = x REM y is defined regardless
+ *      of the rounding mode by the  mathematical relation r = x - n
+ *      y, where n is the integer nearest the exact value of x/y;
+ *      whenever | n -  x/y | = 1/2, then n is even. If r = 0, its
+ *      sign shall be that of x." This definition is applicable for
+ *      all implementations.
+ */
+
+/* FUNCTION: remainder */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y);
+
+double remainder(double x, double y) { return __sort_of_CPROVER_remainder(FE_TONEAREST, x, y); }
+
+
+/* FUNCTION: remainderf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y);
+
+float remainderf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TONEAREST, x, y); }
+
+
+/* FUNCTION: remainderl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#include <fenv.h>
+#define __CPROVER_FENV_H_INCLUDED
+#endif
+
+long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y);
+
+long double remainderl(long double x, long double y) { return __sort_of_CPROVER_remainderl(FE_TONEAREST, x, y); }
+
+
+
+
+/* ISO 9899:2011
+ * The copysign functions produce a value with the magnitude of x and
+ * the sign of y. They produce a NaN (with the sign of y) if x is a
+ * NaN. On implementations that represent a signed zero but do not
+ * treat negative zero consistently in arithmetic operations, the
+ * copysign functions regard the sign of zero as positive.
+ */
+
+/* FUNCTION: copysign */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+double fabs (double d);
+
+double copysign(double x, double y)
+{
+  double abs = fabs(x);
+  return (signbit(y)) ? -abs : abs;
+}
+
+/* FUNCTION: copysignf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+float fabsf (float d);
+
+float copysignf(float x, float y)
+{
+  float abs = fabs(x);
+  return (signbit(y)) ? -abs : abs;
+}
+
+/* FUNCTION: copysignl */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+long double fabsl (long double d);
+
+long double copysignl(long double x, long double y)
+{
+  long double abs = fabs(x);
+  return (signbit(y)) ? -abs : abs;
+}
+
+
+
diff --git a/src/ansi-c/library/new.c b/src/ansi-c/library/new.c
index beb4e70e1bf..3ed70ec46e6 100644
--- a/src/ansi-c/library/new.c
+++ b/src/ansi-c/library/new.c
@@ -6,7 +6,13 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
   // This just does memory allocation.
   __CPROVER_HIDE:;
   void *res;
-  res=__CPROVER_malloc(malloc_size);
+  // ensure that all bytes in the allocated memory can be addressed
+  // using our object:offset encoding as specified in
+  // flattening/pointer_logic.h; also avoid sign-extension issues
+  // for 32-bit systems that yields a maximum allocation of 2^23-1,
+  // i.e., just under 8MB
+  __CPROVER_assume(malloc_size<(1UL<<((sizeof(char*)-1)*8-1)));
+  res=__CPROVER_allocate(malloc_size, 0);
 
   // ensure it's not recorded as deallocated
   __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
@@ -31,8 +37,14 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
   // The constructor call is done by the front-end.
   // This just does memory allocation.
   __CPROVER_HIDE:;
+  // ensure that all bytes in the allocated memory can be addressed
+  // using our object:offset encoding as specified in
+  // flattening/pointer_logic.h; also avoid sign-extension issues
+  // for 32-bit systems that yields a maximum allocation of 2^23-1,
+  // i.e., just under 8MB
+  __CPROVER_assume(size*count<(1UL<<((sizeof(char*)-1)*8-1)));
   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;
@@ -87,6 +99,9 @@ inline void __delete(void *ptr)
     // non-deterministically record as deallocated
     __CPROVER_bool record;
     __CPROVER_deallocated=record?ptr:__CPROVER_deallocated;
+
+    // detect memory leaks
+    if(__CPROVER_memory_leak==ptr) __CPROVER_memory_leak=0;
   }
 }
 
@@ -116,5 +131,8 @@ inline void __delete_array(void *ptr)
     // non-deterministically record as deallocated
     __CPROVER_bool record;
     __CPROVER_deallocated=record?ptr:__CPROVER_deallocated;
+
+    // detect memory leaks
+    if(__CPROVER_memory_leak==ptr) __CPROVER_memory_leak=0;
   }
 }
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index 3b85223320e..b2e2b7b7e97 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -60,27 +60,40 @@ inline void abort(void)
 /* FUNCTION: calloc */
 
 #undef calloc
-#undef malloc
-
-inline void *malloc(__CPROVER_size_t malloc_size);
 
 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);
+  // ensure that all bytes in the allocated memory can be addressed
+  // using our object:offset encoding as specified in
+  // flattening/pointer_logic.h; also avoid sign-extension issues
+  // for 32-bit systems that yields a maximum allocation of 2^23-1,
+  // i.e., just under 8MB
+  __CPROVER_assume(nmemb*size<(1UL<<((sizeof(char*)-1)*8-1)));
+  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;
+  __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;
+  __CPROVER_memory_leak=record_may_leak?malloc_res:__CPROVER_memory_leak;
+
   #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;
+  __CPROVER_is_zero_string(malloc_res)=1;
+  __CPROVER_zero_string_length(malloc_res)=0;
   #endif
-  return res;
+
+  return malloc_res;
 }
 
 /* FUNCTION: malloc */
@@ -90,10 +103,16 @@ inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
 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:;
+  // ensure that all bytes in the allocated memory can be addressed
+  // using our object:offset encoding as specified in
+  // flattening/pointer_logic.h; also avoid sign-extension issues
+  // for 32-bit systems that yields a maximum allocation of 2^23-1,
+  // i.e., just under 8MB
+  __CPROVER_assume(malloc_size<(1UL<<((sizeof(char*)-1)*8-1)));
   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;
@@ -116,8 +135,14 @@ inline void *malloc(__CPROVER_size_t malloc_size)
 inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
 {
   __CPROVER_HIDE:;
+  // ensure that all bytes in the allocated memory can be addressed
+  // using our object:offset encoding as specified in
+  // flattening/pointer_logic.h; also avoid sign-extension issues
+  // for 32-bit systems that yields a maximum allocation of 2^23-1,
+  // i.e., just under 8MB
+  __CPROVER_assume(alloca_size<(1UL<<((sizeof(char*)-1)*8-1)));
   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;
@@ -301,6 +326,8 @@ inline long atol(const char *nptr)
 #define __CPROVER_LIMITS_H_INCLUDED
 #endif
 
+inline void *__builtin_alloca(__CPROVER_size_t alloca_size);
+
 inline char *getenv(const char *name)
 {
   __CPROVER_HIDE:;
@@ -330,7 +357,7 @@ inline char *getenv(const char *name)
   // the range.
 
   __CPROVER_assume(1<=buf_size && buf_size<=SSIZE_MAX);
-  buffer=(char *)__CPROVER_malloc(buf_size);
+  buffer=(char *)__builtin_alloca(buf_size);
   buffer[buf_size-1]=0;
 
   return buffer;
diff --git a/src/config.inc b/src/config.inc
index dc2c8f6a47c..d464495fe4d 100644
--- a/src/config.inc
+++ b/src/config.inc
@@ -5,7 +5,7 @@ BUILD_ENV = AUTO
 ifeq ($(BUILD_ENV),MSVC)
   #CXXFLAGS += /Wall /WX
 else
-  CXXFLAGS += -Wall -pedantic -Werror
+  CXXFLAGS += -Wall -Werror -Wno-parentheses
 endif
 
 # Select optimisation or debug info
@@ -22,8 +22,8 @@ endif
 #CHAFF = ../../zChaff
 #BOOLEFORCE = ../../booleforce-0.4
 #MINISAT = ../../MiniSat-p_v1.14
-MINISAT2 = ../../minisat-2.2.1
-#GLUCOSE = ../../glucose-syrup
+#MINISAT2 = ../../minisat-2.2.1
+GLUCOSE = ../../glucose-syrup
 #SMVSAT =
 
 # Signing identity for MacOS Gatekeeper
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
index cd80ac8f298..fa0b7ef99c7 100644
--- a/src/cpp/cpp_internal_additions.cpp
+++ b/src/cpp/cpp_internal_additions.cpp
@@ -92,7 +92,7 @@ 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 3de38da7b8e..60d746dee27 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -599,8 +599,10 @@ void goto_convertt::do_java_new(
   }
 
   // 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 git rid of the code below
+  malloc_expr.copy_to_operands(false_exprt());
   malloc_expr.type()=pointer_typet(object_type);
 
   goto_programt::targett t_n=dest.add_instruction(ASSIGN);
@@ -655,8 +657,10 @@ void goto_convertt::do_java_new_array(
   }
 
   // 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()=pointer_typet(object_type);
 
   goto_programt::targett t_n=dest.add_instruction(ASSIGN);
@@ -1767,6 +1771,77 @@ void goto_convertt::do_function_call_symbol(
 
     // void __sync_lock_release (type *ptr, ...)
   }
+  else if(identifier=="__builtin_isgreater" ||
+          identifier=="__builtin_isgreater" ||
+          identifier=="__builtin_isgreaterequal" ||
+          identifier=="__builtin_isless" ||
+          identifier=="__builtin_islessequal" ||
+          identifier=="__builtin_islessgreater" ||
+          identifier=="__builtin_isunordered")
+  {
+    // these support two double or two float arguments; we call the
+    // appropriate internal version
+    if(arguments.size()!=2 ||
+       (arguments[0].type()!=double_type() &&
+        arguments[0].type()!=float_type()) ||
+       (arguments[1].type()!=double_type() &&
+        arguments[1].type()!=float_type()))
+    {
+      error().source_location=function.find_source_location();
+      error() << "`" << identifier
+              << "' expected to have two float/double arguments"
+              << eom;
+      throw 0;
+    }
+
+    exprt::operandst new_arguments=arguments;
+
+    bool use_double=arguments[0].type()==double_type();
+    if(arguments[0].type()!=arguments[1].type())
+    {
+      if(use_double)
+        new_arguments[1].make_typecast(arguments[0].type());
+      else
+      {
+        new_arguments[0].make_typecast(arguments[1].type());
+        use_double=true;
+      }
+    }
+
+    code_typet f_type=to_code_type(function.type());
+    f_type.remove_ellipsis();
+    const typet &a_t=new_arguments[0].type();
+    f_type.parameters()=
+      code_typet::parameterst(2, code_typet::parametert(a_t));
+
+    // replace __builtin_ by CPROVER_PREFIX
+    std::string name=CPROVER_PREFIX+id2string(identifier).substr(10);
+    // append d or f for double/float
+    name+=use_double?'d':'f';
+
+    symbol_exprt new_function=function;
+    new_function.set_identifier(name);
+    new_function.type()=f_type;
+
+    code_function_callt function_call;
+    function_call.lhs()=lhs;
+    function_call.function()=new_function;
+    function_call.arguments()=new_arguments;
+    function_call.add_source_location()=function.source_location();
+
+    if(!symbol_table.has_symbol(name))
+    {
+      code_typet();
+      symbolt new_symbol;
+      new_symbol.base_name=name;
+      new_symbol.name=name;
+      new_symbol.type=f_type;
+      new_symbol.location=function.source_location();
+      symbol_table.add(new_symbol);
+    }
+
+    copy(function_call, FUNCTION_CALL, dest);
+  }
   else
   {
     do_function_call_symbol(*symbol);
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index 6b3f5d68d66..eeefe80dfcb 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -777,7 +777,7 @@ void goto_convertt::convert_assign(
     do_java_new_array(lhs, to_side_effect_expr(rhs), dest);
   }
   else if(rhs.id()==ID_side_effect &&
-          rhs.get(ID_statement)==ID_malloc)
+          rhs.get(ID_statement)==ID_allocate)
   {
     // just preserve
     Forall_operands(it, rhs)
diff --git a/src/goto-programs/goto_convert_new_switch_case.cpp b/src/goto-programs/goto_convert_new_switch_case.cpp
index 315d9ae810f..39dde2f9c2a 100644
--- a/src/goto-programs/goto_convert_new_switch_case.cpp
+++ b/src/goto-programs/goto_convert_new_switch_case.cpp
@@ -620,7 +620,7 @@ void goto_convertt::convert_assign(
     do_java_new_array(lhs, to_side_effect_expr(rhs), dest);
   }
   else if(rhs.id()==ID_side_effect &&
-          rhs.get(ID_statement)==ID_malloc)
+          rhs.get(ID_statement)==ID_allocate)
   {
     // just preserve
     Forall_operands(it, rhs)
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index 3119cc252d7..d0a08663a45 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -681,7 +681,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-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index f45d722ebf7..878a240e487 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -311,7 +311,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/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index d88e9c68bac..a8dd9d675e1 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -209,7 +209,7 @@ bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
   return false;
 }
 
-/// write to a variable
+#if 0
 static bool check_renaming(const exprt &expr);
 
 static bool check_renaming(const typet &type)
@@ -290,10 +290,11 @@ static bool check_renaming(const exprt &expr)
 
   return false;
 }
+#endif
 
 static void assert_l1_renaming(const exprt &expr)
 {
-  #if 1
+  #if 0
   if(check_renaming_l1(expr))
   {
     std::cerr << expr.pretty() << '\n';
@@ -306,7 +307,7 @@ static void assert_l1_renaming(const exprt &expr)
 
 static void assert_l2_renaming(const exprt &expr)
 {
-  #if 1
+  #if 0
   if(check_renaming(expr))
   {
     std::cerr << expr.pretty() << '\n';
@@ -317,6 +318,7 @@ static void assert_l2_renaming(const exprt &expr)
   #endif
 }
 
+/// write to a variable
 void goto_symex_statet::assignment(
   ssa_exprt &lhs, // L0/L1
   const exprt &rhs,  // L2
@@ -353,6 +355,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 047f3be8325..99969c2ddfa 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -61,8 +61,8 @@ void goto_symext::symex_assign(
     else if(statement==ID_cpp_new ||
             statement==ID_cpp_new_array)
       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 44e7d532c42..9b4566fc64c 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -11,6 +11,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>
@@ -50,18 +52,21 @@ 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
 
   dynamic_counter++;
+  // we can only encode 254 fresh objects + invalid + null in 8 bits
+  if(dynamic_counter>254)
+    throw "at most 254 distinct dynamic objects are supported";
 
   exprt size=code.op0();
   typet object_type=nil_typet();
@@ -164,19 +169,43 @@ 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() && !zero_init.is_zero())
+  {
+    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);
+    }
+  }
+
   address_of_exprt rhs;
 
+  symbol_exprt v=value_symbol.symbol_expr();
+  v.add("#dynamic_guard", state.guard);
+
   if(object_type.id()==ID_array)
   {
     rhs.type()=pointer_typet(value_symbol.type.subtype());
     index_exprt index_expr(value_symbol.type.subtype());
-    index_expr.array()=value_symbol.symbol_expr();
+    index_expr.array()=v;
     index_expr.index()=from_integer(0, index_type());
     rhs.op0()=index_expr;
   }
   else
   {
-    rhs.op0()=value_symbol.symbol_expr();
+    rhs.op0()=v;
     rhs.type()=pointer_typet(value_symbol.type);
   }
 
@@ -373,6 +402,9 @@ void goto_symext::symex_cpp_new(
   do_array=(code.get(ID_statement)==ID_cpp_new_array);
 
   dynamic_counter++;
+  // we can only encode 254 fresh objects + invalid + null in 8 bits
+  if(dynamic_counter>254)
+    throw "at most 254 distinct dynamic objects are supported";
 
   const std::string count_string(std::to_string(dynamic_counter));
 
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index 436a2d6e55c..a4e9e3fc290 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -45,7 +45,39 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
 
   ssa_exprt ssa(expr);
   state.rename(ssa, ns, goto_symex_statet::L1);
-  const irep_idt &l1_identifier=ssa.get_identifier();
+  irep_idt l1_identifier=ssa.get_identifier();
+
+  // inlining may yield multiple declarations of the same identifier
+  // within the same L1 context
+#if 0
+  if(state.level2.current_names.find(l1_identifier)!=
+     state.level2.current_names.end())
+  {
+    // remove the previous one
+    state.level2.current_names.erase(l1_identifier);
+
+    // get L0 name
+    state.get_original_name(ssa);
+    state.rename(ssa, ns, goto_symex_statet::L0);
+    const irep_idt l0_name=ssa.get_identifier();
+
+    unsigned new_l1=state.level1.current_count(l0_name);
+
+    while(state.l1_history.find(l1_identifier)!=state.l1_history.end())
+    {
+      state.level1.increase_counter(l0_name);
+      ++new_l1;
+      ssa.set_level_1(new_l1);
+      l1_identifier=ssa.get_identifier();
+    }
+
+    // now unique -- store
+    state.top().local_objects.insert(l1_identifier);
+    state.l1_history.insert(l1_identifier);
+
+    state.rename(ssa, ns, goto_symex_statet::L1);
+  }
+#endif
 
   // rename type to L2
   state.rename(ssa.type(), l1_identifier, ns);
@@ -77,11 +109,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 5f97bbfa529..900bd813378 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -149,8 +149,9 @@ exprt java_object_factoryt::allocate_object(
     {
       assert(!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_typet(allocate_type);
       malloc_expr.type()=result_type;
       // Create a symbol for the malloc expression so we can initialize
diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp
index 356474cc294..50df3e6d040 100644
--- a/src/path-symex/path_symex.cpp
+++ b/src/path-symex/path_symex.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 /// Concrete Symbolic Transformer
 
 #include <util/arith_tools.h>
+#include <util/message.h>
 #include <util/simplify_expr.h>
 #include <util/string2int.h>
 #include <util/byte_operators.h>
@@ -98,9 +99,9 @@ void path_symext::assign(
     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)
     {
-      symex_malloc(state, lhs, side_effect_expr);
+      symex_allocate(state, lhs, side_effect_expr);
       return;
     }
     else if(statement==ID_nondet)
@@ -152,13 +153,13 @@ inline static typet c_sizeof_type_rec(const exprt &expr)
   return nil_typet();
 }
 
-void path_symext::symex_malloc(
+void path_symext::symex_allocate(
   path_symex_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";
 
   // increment dynamic object counter
   unsigned dynamic_count=++state.var_map.dynamic_count;
@@ -244,6 +245,23 @@ void path_symext::symex_malloc(
   value_symbol.type.set("#dynamic", true);
   value_symbol.mode=ID_C;
 
+  exprt zero_init=code.op1();
+  exprt zero_init_val=state.read(zero_init);
+
+  if(zero_init_val.is_constant() && !zero_init_val.is_zero())
+  {
+    null_message_handlert null_message;
+    exprt zero_value=
+      zero_initializer(
+        object_type,
+        code.source_location(),
+        state.var_map.ns,
+        null_message);
+
+    if(zero_value.is_not_nil())
+      assign(state, value_symbol.symbol_expr(), zero_value);
+  }
+
   address_of_exprt rhs;
 
   if(object_type.id()==ID_array)
diff --git a/src/path-symex/path_symex_class.h b/src/path-symex/path_symex_class.h
index 933b871e9fa..a0d57df66a1 100644
--- a/src/path-symex/path_symex_class.h
+++ b/src/path-symex/path_symex_class.h
@@ -68,7 +68,7 @@ class path_symext
 
   void set_return_value(path_symex_statet &, const exprt &);
 
-  void symex_malloc(
+  void symex_allocate(
     path_symex_statet &state,
     const exprt &lhs,
     const side_effect_exprt &code);
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 9c30fbe3ca7..5503fdf10fb 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -628,8 +628,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;
 
@@ -675,7 +675,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=="");
 
@@ -1002,7 +1002,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 9efd87c5793..28f27413f6b 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -557,7 +557,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 149af498760..02a5524563e 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -610,7 +610,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 2acb06ad601..7370c5430fc 100644
--- a/src/pointer-analysis/value_set_fivr.cpp
+++ b/src/pointer-analysis/value_set_fivr.cpp
@@ -728,7 +728,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 034b0839da0..bad8235ebc6 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -514,7 +514,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 aeecd21e2bc..880ba00a74a 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/config.h>
 #include <util/arith_tools.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 &&
        is_ptr(operands[0].type()))
     {
-      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)
@@ -439,6 +424,9 @@ 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);
 }
@@ -780,6 +768,78 @@ 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);
+      assert(bv.size()==saved_bv.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);
+      assert(guard_bv.size()==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);
+    assert(bv.size()==saved_bv.size());
+
+    disj.push_back(
+      bv_utils.rel(saved_bv, ID_ge, bv, bv_utilst::representationt::UNSIGNED));
+
+    assert(postponed.bv.size()==1);
+    literalt l=postponed.bv.front();
+    prop.l_set_to(prop.lequal(prop.lor(disj), l), true);
+  }
   else
     assert(false);
 }
diff --git a/src/solvers/sat/satcheck.h b/src/solvers/sat/satcheck.h
index ada65d253e8..a918203c607 100644
--- a/src/solvers/sat/satcheck.h
+++ b/src/solvers/sat/satcheck.h
@@ -14,8 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 // #define SATCHECK_ZCHAFF
 // #define SATCHECK_MINISAT1
-#define SATCHECK_MINISAT2
-// #define SATCHECK_GLUCOSE
+// #define SATCHECK_MINISAT2
+#define SATCHECK_GLUCOSE
 // #define SATCHECK_BOOLEFORCE
 // #define SATCHECK_PRECOSAT
 // #define SATCHECK_PICOSAT
diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp
index adcfbded617..7a129ede03d 100644
--- a/src/solvers/sat/satcheck_glucose.cpp
+++ b/src/solvers/sat/satcheck_glucose.cpp
@@ -115,7 +115,7 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
 template<typename T>
 propt::resultt satcheck_glucose_baset<T>::prop_solve()
 {
-  assert(status!=ERROR);
+  assert(status!=statust::ERROR);
 
   // We start counting at 1, thus there is one variable fewer.
   {
@@ -155,8 +155,8 @@ propt::resultt satcheck_glucose_baset<T>::prop_solve()
         messaget::status() <<
           "SAT checker: instance is SATISFIABLE" << eom;
         assert(solver->model.size()!=0);
-        status=SAT;
-        return P_SATISFIABLE;
+        status=statust::SAT;
+        return resultt::P_SATISFIABLE;
       }
       else
       {
@@ -166,8 +166,8 @@ propt::resultt satcheck_glucose_baset<T>::prop_solve()
     }
   }
 
-  status=UNSAT;
-  return P_UNSATISFIABLE;
+  status=statust::UNSAT;
+  return resultt::P_UNSATISFIABLE;
 }
 
 template<typename T>
diff --git a/src/util/guard.cpp b/src/util/guard.cpp
index 6bad260f84f..1d70c0abc43 100644
--- a/src/util/guard.cpp
+++ b/src/util/guard.cpp
@@ -94,9 +94,9 @@ guardt &operator -= (guardt &g1, const guardt &g2)
   if(g1.id()!=ID_and || g2.id()!=ID_and)
     return g1;
 
-  sort_and_join(g1);
+  // sort_and_join(g1);
   guardt g2_sorted=g2;
-  sort_and_join(g2_sorted);
+  // sort_and_join(g2_sorted);
 
   exprt::operandst &op1=g1.operands();
   const exprt::operandst &op2=g2_sorted.operands();
@@ -107,10 +107,12 @@ guardt &operator -= (guardt &g1, const guardt &g2)
       it2!=op2.end();
       ++it2)
   {
-    while(it1!=op1.end() && *it1<*it2)
-      ++it1;
+    /*while(it1!=op1.end() && *it1<*it2)
+      ++it1;*/
     if(it1!=op1.end() && *it1==*it2)
       it1=op1.erase(it1);
+    else
+      break;
   }
 
   g1=conjunction(op1);
@@ -144,9 +146,9 @@ guardt &operator |= (guardt &g1, const guardt &g2)
   }
 
   // find common prefix
-  sort_and_join(g1);
+  // sort_and_join(g1);
   guardt g2_sorted=g2;
-  sort_and_join(g2_sorted);
+  // sort_and_join(g2_sorted);
 
   exprt::operandst &op1=g1.operands();
   const exprt::operandst &op2=g2_sorted.operands();
diff --git a/src/util/irep.h b/src/util/irep.h
index f0f42abda20..c045bedeca9 100644
--- a/src/util/irep.h
+++ b/src/util/irep.h
@@ -18,9 +18,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "irep_ids.h"
 
 #define SHARING
-// #define HASH_CODE
+#define HASH_CODE
 #define USE_MOVE
-// #define SUB_IS_LIST
+#define SUB_IS_LIST
 
 #ifdef SUB_IS_LIST
 #include <list>
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index e31eceb1e98..fe82b1c7324 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -207,7 +207,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)
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index d8d62fee483..2dfa234b144 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1806,6 +1806,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
             index_exprt(
               result,
               from_integer(offset, expr.offset().type()));
+          result.make_typecast(expr.type());
 
           if(!base_type_eq(expr.type(), op_type_ptr->subtype(), ns))
              result.make_typecast(expr.type());
@@ -1866,7 +1867,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
         simplify_member(expr.op());
         expr.offset()=
           from_integer(offset-m_offset_bits/8, expr.offset().type());
-        simplify_rec(expr.offset());
+        simplify_rec(expr);
 
         return false;
       }
@@ -2188,7 +2189,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
 
   bool result=true;
 
-  result=sort_and_join(expr) && result;
+  result=sort_and_join(expr, false) && result;
 
   if(expr.id()==ID_typecast)
     result=simplify_typecast(expr) && result;
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index f50c9b61b19..8a5723f5b33 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -72,21 +72,59 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
       return false;
     }
   }
-  else if(expr.id()==ID_or ||
-          expr.id()==ID_and ||
-          expr.id()==ID_xor)
+  else if(expr.id()==ID_xor)
   {
-    if(operands.empty())
-      return true;
-
     bool result=true;
 
-    exprt::operandst::const_iterator last;
-    bool last_set=false;
-
     bool negate=false;
 
-    for(exprt::operandst::iterator it=operands.begin();
+    for(exprt::operandst::const_iterator it=operands.begin();
+        it!=operands.end();)
+    {
+      if(it->type().id()!=ID_bool) return true;
+
+      bool erase;
+
+      if(it->is_true())
+      {
+        erase=true;
+        negate=!negate;
+      }
+      else
+        erase=it->is_false();
+
+      if(erase)
+      {
+        it=operands.erase(it);
+        result=false;
+      }
+      else
+        it++;
+    }
+
+    if(operands.empty())
+    {
+      expr.make_bool(negate);
+      return false;
+    }
+    else if(operands.size()==1)
+    {
+      if(negate)
+        expr.op0().make_not();
+      exprt tmp(operands.front());
+      expr.swap(tmp);
+      return false;
+    }
+
+    return result;
+  }
+  else if(expr.id()==ID_and || expr.id()==ID_or)
+  {
+    std::unordered_set<exprt, irep_hash> expr_set;
+
+    bool result=true;
+
+    for(exprt::operandst::const_iterator it=operands.begin();
         it!=operands.end();)
     {
       if(it->type().id()!=ID_bool)
@@ -106,21 +144,9 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
         return false;
       }
 
-      bool erase;
-
-      if(expr.id()==ID_and)
-        erase=is_true;
-      else if(is_true && expr.id()==ID_xor)
-      {
-        erase=true;
-        negate=!negate;
-      }
-      else
-        erase=is_false;
-
-      if(last_set && *it==*last &&
-         (expr.id()==ID_or || expr.id()==ID_and))
-        erase=true; // erase duplicate operands
+      bool erase=
+        (expr.id()==ID_and ? is_true : is_false) ||
+        !expr_set.insert(*it).second;
 
       if(erase)
       {
@@ -128,55 +154,27 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
         result=false;
       }
       else
-      {
-        last=it;
-        last_set=true;
         it++;
-      }
     }
 
     // search for a and !a
-    if(expr.id()==ID_and || expr.id()==ID_or)
-    {
-      // first gather all the a's with !a
-
-      std::unordered_set<exprt, irep_hash> expr_set;
-
-      forall_operands(it, expr)
-        if(it->id()==ID_not &&
-           it->operands().size()==1 &&
-           it->type().id()==ID_bool)
-          expr_set.insert(it->op0());
-
-      // now search for a
-
-      if(!expr_set.empty())
+    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())
       {
-        forall_operands(it, expr)
-        {
-          if(it->id()!=ID_not &&
-             expr_set.find(*it)!=expr_set.end())
-          {
-            expr.make_bool(expr.id()==ID_or);
-            return false;
-          }
-        }
+        expr.make_bool(expr.id()==ID_or);
+        return false;
       }
-    }
 
     if(operands.empty())
     {
-      if(expr.id()==ID_and || negate)
-        expr=true_exprt();
-      else
-        expr=false_exprt();
-
+      expr.make_bool(expr.id()==ID_and);
       return false;
     }
     else if(operands.size()==1)
     {
-      if(negate)
-        expr.op0().make_not();
       exprt tmp(operands.front());
       expr.swap(tmp);
       return false;
diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp
index d5583226f71..a7309f7a4f2 100644
--- a/src/util/simplify_utils.cpp
+++ b/src/util/simplify_utils.cpp
@@ -120,7 +120,7 @@ static const struct saj_tablet &sort_and_join(
   return saj_table[i];
 }
 
-bool sort_and_join(exprt &expr)
+bool sort_and_join(exprt &expr, bool do_sort)
 {
   bool result=true;
 
@@ -160,7 +160,8 @@ bool sort_and_join(exprt &expr)
 
   // sort it
 
-  result=sort_operands(new_ops) && result;
+  if(do_sort)
+    result=sort_operands(new_ops) && result;
   expr.operands().swap(new_ops);
 
   return result;
diff --git a/src/util/simplify_utils.h b/src/util/simplify_utils.h
index 33e294f4e96..6f0af7865b9 100644
--- a/src/util/simplify_utils.h
+++ b/src/util/simplify_utils.h
@@ -14,6 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bool sort_operands(exprt::operandst &operands);
 
-bool sort_and_join(exprt &expr);
+bool sort_and_join(exprt &expr, bool do_sort=true);
 
 #endif // CPROVER_UTIL_SIMPLIFY_UTILS_H