diff --git a/CODING_STANDARD.md b/CODING_STANDARD.md
index 4d57b09da31..06c6bf53666 100644
--- a/CODING_STANDARD.md
+++ b/CODING_STANDARD.md
@@ -107,6 +107,9 @@ Here a few minimalistic coding rules for the CPROVER source tree.
   include in the source file. For example, given `foo.h` and `foo.cpp`, the
   line `#include "foo.h"` should precede all other include statements in
   `foo.cpp`.
+- Use the C++ versions of C headers (e.g. `cmath` instead of `math.h`).
+  Some of the C headers use macros instead of functions which can have
+  unexpected consequences.
 
 # Makefiles
 - Each source file should appear on a separate line
diff --git a/regression/ansi-c/Struct_Initialization1/main.c b/regression/ansi-c/Struct_Initialization1/main.c
index b497a0b60dd..f2e75463d6c 100644
--- a/regression/ansi-c/Struct_Initialization1/main.c
+++ b/regression/ansi-c/Struct_Initialization1/main.c
@@ -1,13 +1,19 @@
 #define STATIC_ASSERT(condition) \
   int some_array##__LINE__[(condition) ? 1 : -1]
 
+struct A {
+  int x;
+  int y;
+};
+
 struct _classinfo {
   char a;
+  struct A s;
   int *interfaces[];
 };
 
-struct _classinfo nullclass1 = { 42, 0, 0 };
-struct _classinfo nullclass2 = { 42, { 0, 0 } };
+struct _classinfo nullclass1 = { 42, 1, 2, 3, 4 };
+struct _classinfo nullclass2 = { 42, { 1, 2 }, { 3, 4 } };
 
 STATIC_ASSERT(sizeof(nullclass1)==sizeof(struct _classinfo));
 STATIC_ASSERT(sizeof(nullclass2)==sizeof(struct _classinfo));
diff --git a/regression/ansi-c/Struct_Initialization1/test.desc b/regression/ansi-c/Struct_Initialization1/test.desc
index fc2b1874059..466da18b2b5 100644
--- a/regression/ansi-c/Struct_Initialization1/test.desc
+++ b/regression/ansi-c/Struct_Initialization1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/ansi-c/Struct_Initialization2/main.c b/regression/ansi-c/Struct_Initialization2/main.c
new file mode 100644
index 00000000000..98cce21ebc8
--- /dev/null
+++ b/regression/ansi-c/Struct_Initialization2/main.c
@@ -0,0 +1,24 @@
+#define STATIC_ASSERT(condition) \
+  int some_array##__LINE__[(condition) ? 1 : -1]
+
+struct A {
+  int x;
+  int y;
+  int arr[];
+};
+
+struct _classinfo {
+  char a;
+  struct A s;
+  int *interfaces[];
+};
+
+struct _classinfo nullclass1 = { 42, 1, 2, 0, 3, 4 };
+struct _classinfo nullclass2 = { 42, { 1, 2, 0 }, { 3, 4 } };
+
+STATIC_ASSERT(sizeof(nullclass1)==sizeof(struct _classinfo));
+STATIC_ASSERT(sizeof(nullclass2)==sizeof(struct _classinfo));
+
+int main()
+{
+}
diff --git a/regression/ansi-c/Struct_Initialization2/test.desc b/regression/ansi-c/Struct_Initialization2/test.desc
new file mode 100644
index 00000000000..73c2caa52cd
--- /dev/null
+++ b/regression/ansi-c/Struct_Initialization2/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=(64|1)$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+^warning: ignoring
+--
+variable-length arrays in the middle of a struct are not permitted
diff --git a/regression/cbmc/dynamic_size1/main.c b/regression/cbmc/dynamic_size1/main.c
new file mode 100644
index 00000000000..6cf9465f50f
--- /dev/null
+++ b/regression/cbmc/dynamic_size1/main.c
@@ -0,0 +1,14 @@
+#include <stdlib.h>
+
+int main()
+{
+  unsigned x;
+
+  int *A=malloc(x*sizeof(int));
+
+  char *p=&A[1];
+
+  char c=*p;
+
+  return c;
+}
diff --git a/regression/cbmc/dynamic_size1/test.desc b/regression/cbmc/dynamic_size1/test.desc
new file mode 100644
index 00000000000..d110065a9cf
--- /dev/null
+++ b/regression/cbmc/dynamic_size1/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^unknown or invalid type size:
diff --git a/regression/cbmc/fgets1/main.c b/regression/cbmc/fgets1/main.c
new file mode 100644
index 00000000000..8c4e418885b
--- /dev/null
+++ b/regression/cbmc/fgets1/main.c
@@ -0,0 +1,22 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main()
+{
+  char buffer[3]={'a', 'b', '\0'};
+  FILE *f=fdopen(0, "r");
+  if(!f)
+    return 1;
+
+  char *p=fgets(buffer, 3, f);
+  if(p)
+  {
+    assert(buffer[1]==p[1]);
+    assert(buffer[2]=='\0');
+    assert(p[1]=='b'); // expected to fail
+  }
+
+  fclose(f);
+
+  return 0;
+}
diff --git a/regression/cbmc/fgets1/test.desc b/regression/cbmc/fgets1/test.desc
new file mode 100644
index 00000000000..3a8c4e6a733
--- /dev/null
+++ b/regression/cbmc/fgets1/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--bounds-check --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[main.assertion.3\] assertion p\[1\]=='b': FAILURE
+\*\* 1 of 38 failed \(2 iterations\)
+--
+^warning: ignoring
diff --git a/regression/cbmc/union9/main.c b/regression/cbmc/union9/main.c
new file mode 100644
index 00000000000..676048e49c8
--- /dev/null
+++ b/regression/cbmc/union9/main.c
@@ -0,0 +1,35 @@
+#include <stdlib.h>
+#include <stdint.h>
+
+typedef union {
+  struct {
+    uint8_t x;
+    uint8_t z;
+  } b;
+} union_t;
+
+typedef struct {
+    uint32_t magic;
+    union_t unions[];
+} flex;
+
+int flex_init(flex * flex, size_t num)
+{
+    if (num == 0 || num >= 200) {
+        return -1;
+    }
+    flex->unions[num - 1].b.z = 255;
+    return 0;
+}
+
+int main() {
+    uint8_t num = nondet_size();
+    flex * pool = (flex *) malloc(sizeof(flex) + num * sizeof(union_t));
+    int ret = flex_init(pool, num);
+    if (num > 0 && num < 200) {
+        __CPROVER_assert(ret == 0, "Accept inside range");
+    } else {
+        __CPROVER_assert(ret != 0, "Reject outside range");
+    }
+}
+
diff --git a/regression/cbmc/union9/test.desc b/regression/cbmc/union9/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/union9/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index 521ae29aa4a..eec934736d5 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -89,10 +89,11 @@ class c_typecheck_baset:
     const typet &type,
     bool force_constant);
 
-  virtual void do_designated_initializer(
+  virtual exprt::operandst::const_iterator do_designated_initializer(
     exprt &result,
     designatort &designator,
-    const exprt &value,
+    const exprt &initializer_list,
+    exprt::operandst::const_iterator init_it,
     bool force_constant);
 
   designatort make_designator(const typet &type, const exprt &src);
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index fd098259796..1bc494c8d4a 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -256,9 +256,7 @@ void c_typecheck_baset::designator_enter(
   const typet &type,
   designatort &designator)
 {
-  designatort::entryt entry;
-  entry.type=type;
-  entry.index=0;
+  designatort::entryt entry(type);
 
   const typet &full_type=follow(type);
 
@@ -268,6 +266,8 @@ void c_typecheck_baset::designator_enter(
 
     entry.size=struct_type.components().size();
     entry.subtype.make_nil();
+    // only a top-level struct may end with a variable-length array
+    entry.vla_permitted=designator.empty();
 
     for(struct_typet::componentst::const_iterator
         it=struct_type.components().begin();
@@ -351,12 +351,16 @@ void c_typecheck_baset::designator_enter(
 
 /// \param pre:initialized result, designator
 /// \return sets result
-void c_typecheck_baset::do_designated_initializer(
+exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
   exprt &result,
   designatort &designator,
-  const exprt &value,
+  const exprt &initializer_list,
+  exprt::operandst::const_iterator init_it,
   bool force_constant)
 {
+  // copy the value, we may need to adjust it
+  exprt value=*init_it;
+
   assert(!designator.empty());
 
   if(value.id()==ID_designated_initializer)
@@ -370,8 +374,10 @@ void c_typecheck_baset::do_designated_initializer(
 
     assert(!designator.empty());
 
-    return do_designated_initializer(
-      result, designator, value.op0(), force_constant);
+    // discard the return value
+    do_designated_initializer(
+      result, designator, value, value.operands().begin(), force_constant);
+    return ++init_it;
   }
 
   exprt *dest=&result;
@@ -503,7 +509,7 @@ void c_typecheck_baset::do_designated_initializer(
 
       assert(full_type==follow(dest->type()));
 
-      return; // done
+      return ++init_it; // done
     }
 
     // union? The component in the zero initializer might
@@ -537,7 +543,7 @@ void c_typecheck_baset::do_designated_initializer(
     if(value.id()==ID_initializer_list)
     {
       *dest=do_initializer_rec(value, type, force_constant);
-      return; // done
+      return ++init_it; // done
     }
     else if(value.id()==ID_string_constant)
     {
@@ -549,7 +555,7 @@ void c_typecheck_baset::do_designated_initializer(
           follow(full_type.subtype()).id()==ID_unsignedbv))
       {
         *dest=do_initializer_rec(value, type, force_constant);
-        return; // done
+        return ++init_it; // done
       }
     }
     else if(follow(value.type())==full_type)
@@ -562,7 +568,7 @@ void c_typecheck_baset::do_designated_initializer(
          full_type.id()==ID_vector)
       {
         *dest=value;
-        return; // done
+        return ++init_it; // done
       }
     }
 
@@ -574,21 +580,49 @@ void c_typecheck_baset::do_designated_initializer(
     // we are initializing a compound type, and enter it!
     // this may change the type, full_type might not be valid any more
     const typet dest_type=full_type;
+    const bool vla_permitted=designator.back().vla_permitted;
     designator_enter(type, designator);
 
+    // GCC permits (though issuing a warning with -Wall) composite
+    // types built from flat initializer lists
     if(dest->operands().empty())
     {
-      err_location(value);
-      error() << "cannot initialize type `"
-              << to_string(dest_type) << "' using value `"
-              << to_string(value) << "'" << eom;
-      throw 0;
+      warning().source_location=value.find_source_location();
+      warning() << "initialisation of " << full_type.id()
+                << " requires initializer list, found "
+                << value.id() << " instead" << eom;
+
+      // in case of a variable-length array consume all remaining
+      // initializer elements
+      if(vla_permitted &&
+         dest_type.id()==ID_array &&
+         (to_array_type(dest_type).size().is_zero() ||
+          to_array_type(dest_type).size().is_nil()))
+      {
+        value.id(ID_initializer_list);
+        value.operands().clear();
+        for( ; init_it!=initializer_list.operands().end(); ++init_it)
+          value.copy_to_operands(*init_it);
+        *dest=do_initializer_rec(value, dest_type, force_constant);
+
+        return init_it;
+      }
+      else
+      {
+        err_location(value);
+        error() << "cannot initialize type `"
+          << to_string(dest_type) << "' using value `"
+          << to_string(value) << "'" << eom;
+        throw 0;
+      }
     }
 
     dest=&(dest->op0());
 
     // we run into another loop iteration
   }
+
+  return ++init_it;
 }
 
 void c_typecheck_baset::increment_designator(designatort &designator)
@@ -651,8 +685,7 @@ designatort c_typecheck_baset::make_designator(
   forall_operands(it, src)
   {
     const exprt &d_op=*it;
-    designatort::entryt entry;
-    entry.type=type;
+    designatort::entryt entry(type);
     const typet &full_type=follow(entry.type);
 
     if(full_type.id()==ID_array)
@@ -856,10 +889,12 @@ exprt c_typecheck_baset::do_initializer_list(
 
   designator_enter(type, current_designator);
 
-  forall_operands(it, value)
+  const exprt::operandst &operands=value.operands();
+  for(exprt::operandst::const_iterator it=operands.begin();
+      it!=operands.end(); ) // no ++it
   {
-    do_designated_initializer(
-      result, current_designator, *it, force_constant);
+    it=do_designated_initializer(
+      result, current_designator, value, it, force_constant);
 
     // increase designator -- might go up
     increment_designator(current_designator);
diff --git a/src/ansi-c/designator.h b/src/ansi-c/designator.h
index d31d3bb3e66..957bbbb6821 100644
--- a/src/ansi-c/designator.h
+++ b/src/ansi-c/designator.h
@@ -24,9 +24,11 @@ class designatort
   {
     size_t index;
     size_t size;
+    bool vla_permitted;
     typet type, subtype;
 
-    entryt():index(0), size(0)
+    explicit entryt(const typet &type):
+      index(0), size(0), vla_permitted(false), type(type)
     {
     }
   };
diff --git a/src/ansi-c/library/getopt.c b/src/ansi-c/library/getopt.c
index d3eedda9814..458f9d2e414 100644
--- a/src/ansi-c/library/getopt.c
+++ b/src/ansi-c/library/getopt.c
@@ -3,22 +3,67 @@
 extern char *optarg;
 extern int optind;
 
+#ifndef __CPROVER_STRING_H_INCLUDED
+#include <string.h>
+#define __CPROVER_STRING_H_INCLUDED
+#endif
+
 inline int getopt(int argc, char * const argv[],
                   const char *optstring)
 {
   __CPROVER_HIDE:;
-  int result_index;
-  __CPROVER_assume(result_index>=0);
-  (void)*optstring;
-  if(optind>=argc)
+  int result=-1;
+
+  if(optind==0)
+    optind=1;
+
+  if(optind>=argc || argv[optind][0]!='-')
     return -1;
-  __CPROVER_assume(result_index<argc && result_index>=optind);
+
+  size_t result_index;
+  __CPROVER_assume(
+    result_index<strlen(optstring) && optstring[result_index]!=':');
   #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(optstring),
     "getopt zero-termination of 3rd argument");
   #endif
-  optarg = argv[result_index];
-  optind = result_index+1;
-  int retval;
-  return retval;
+
+  _Bool found;
+  if(found)
+  {
+    result=optstring[result_index];
+    if(skipped)
+      ++optind;
+  }
+
+  if(result!=-1 && optind<argc && optstring[result_index+1]==':')
+  {
+    _Bool has_no_arg;
+    if(has_no_arg)
+    {
+      optarg=argv[optind];
+      ++optind;
+    }
+    else
+      optarg=NULL;
+  }
+
+  return result;
+}
+
+/* FUNCTION: getopt_long */
+
+int getopt(int argc, char * const argv[], const char *optstring);
+
+inline int getopt_long(int argc, char * const argv[], const char *optstring,
+                const struct option *longopts, int *longindex)
+{
+  // trigger valid-pointer checks (if enabled), even though we don't
+  // use the parameter in this model
+  (void)*longopts;
+  // avoid unused-parameter warnings when compiling using GCC (for
+  // internal library syntax checks)
+  (void)longindex;
+
+  return getopt(argc, argv, optstring);
 }
diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c
index 5a9ab1e9d57..0472908d744 100644
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -65,7 +65,14 @@ inline FILE *fopen(const char *filename, const char *mode)
   FILE *fopen_result;
 
   _Bool fopen_error;
+
+  #if !defined(__linux__) || defined(__GLIBC__)
   fopen_result=fopen_error?NULL:malloc(sizeof(FILE));
+  #else
+  // libraries need to expose the definition of FILE; this is the
+  // case for musl
+  fopen_result=fopen_error?NULL:malloc(sizeof(int));
+  #endif
 
   #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_set_must(fopen_result, "open");
@@ -99,6 +106,11 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#ifndef __CPROVER_STDLIB_H_INCLUDED
+#include <stdlib.h>
+#define __CPROVER_STDLIB_H_INCLUDED
+#endif
+
 inline int fclose(FILE *stream)
 {
   __CPROVER_HIDE:;
@@ -135,11 +147,48 @@ inline FILE *fdopen(int handle, const char *mode)
     "fdopen zero-termination of 2nd argument");
   #endif
 
+  #if !defined(__linux__) || defined(__GLIBC__)
   FILE *f=malloc(sizeof(FILE));
+  #else
+  // libraries need to expose the definition of FILE; this is the
+  // case for musl
+  FILE *f=malloc(sizeof(int));
+  #endif
 
   return f;
 }
 
+/* FUNCTION: _fdopen */
+
+// This is for Apple
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#include <stdio.h>
+#define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDLIB_H_INCLUDED
+#include <stdlib.h>
+#define __CPROVER_STDLIB_H_INCLUDED
+#endif
+
+#ifdef __APPLE__
+inline FILE *_fdopen(int handle, const char *mode)
+{
+  __CPROVER_HIDE:;
+  (void)handle;
+  (void)*mode;
+  #ifdef __CPROVER_STRING_ABSTRACTION
+  __CPROVER_assert(__CPROVER_is_zero_string(mode),
+    "fdopen zero-termination of 2nd argument");
+  #endif
+
+  FILE *f=malloc(sizeof(FILE));
+
+  return f;
+}
+#endif
+
 /* FUNCTION: fgets */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
@@ -147,7 +196,7 @@ inline FILE *fdopen(int handle, const char *mode)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-inline char *fgets(char *str, int size, FILE *stream)
+char *fgets(char *str, int size, FILE *stream)
 {
   __CPROVER_HIDE:;
   __CPROVER_bool error;
@@ -169,6 +218,16 @@ inline char *fgets(char *str, int size, FILE *stream)
     __CPROVER_is_zero_string(str)=!error;
     __CPROVER_zero_string_length(str)=resulting_size;
   }
+  #else
+  if(size>0)
+  {
+    int str_length;
+    __CPROVER_assume(str_length>=0 && str_length<size);
+    char contents_nondet[str_length];
+    __CPROVER_array_replace(str, contents_nondet);
+    if(!error)
+      str[str_length]='\0';
+  }
   #endif
 
   return error?0:str;
@@ -735,3 +794,43 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg)
 
   return result;
 }
+
+/* FUNCTION: vasprintf */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#include <stdio.h>
+#define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#include <stdarg.h>
+#define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDLIB_H_INCLUDED
+#include <stdlib.h>
+#define __CPROVER_STDLIB_H_INCLUDED
+#endif
+
+inline int vasprintf(char **ptr, const char *fmt, va_list ap)
+{
+  (void)*fmt;
+  (void)ap;
+
+  int result_buffer_size;
+  if(result_buffer_size<=0)
+    return -1;
+
+  *ptr=malloc(result_buffer_size);
+  for(int i=0; i<result_buffer_size; ++i)
+  {
+    char c;
+    (*ptr)[i]=c;
+    if(c=='\0')
+      break;
+  }
+
+  __CPROVER_assume(i<result_buffer_size);
+
+  return i;
+}
diff --git a/src/cbmc/version.h b/src/cbmc/version.h
index 017ded44272..58bdccf0018 100644
--- a/src/cbmc/version.h
+++ b/src/cbmc/version.h
@@ -1,6 +1,6 @@
 #ifndef CPROVER_CBMC_VERSION_H
 #define CPROVER_CBMC_VERSION_H
 
-#define CBMC_VERSION "5.7"
+#define CBMC_VERSION "5.8"
 
 #endif // CPROVER_CBMC_VERSION_H
diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile
index da9e1c50d7d..07d8afa2050 100644
--- a/src/goto-analyzer/Makefile
+++ b/src/goto-analyzer/Makefile
@@ -18,7 +18,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../json/json$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../util/util$(LIBEXT) \
-      ../miniz/miniz$(OBJEXT)
+      ../miniz/miniz$(OBJEXT) \
+      ../solvers/solvers$(LIBEXT)
 
 INCLUDES= -I ..
 
diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile
index 576a5e39505..c9b5fa4b732 100644
--- a/src/goto-cc/Makefile
+++ b/src/goto-cc/Makefile
@@ -28,7 +28,8 @@ OBJ += ../big-int/big-int$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../miniz/miniz$(OBJEXT) \
-      ../json/json$(LIBEXT)
+      ../json/json$(LIBEXT) \
+      ../solvers/solvers$(LIBEXT)
 
 INCLUDES= -I ..
 
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 6402923c4cf..c210f6bb327 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -575,7 +575,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
           // that implies the current one
           return false;
 
-        write_guard|=*it;
+        write_guard.logical_or(*it, ns);
       }
     }
 
@@ -600,7 +600,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
         // that implies the current one
         return false;
 
-      read_guard|=*it;
+      read_guard.logical_or(*it, ns);
     }
 
     exprt cond=read_guard.as_expr();
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index d62d4a66af9..bfe52a44779 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -193,6 +193,7 @@ class goto_symex_statet
     value_sett value_set;
     guardt guard;
     symex_targett::sourcet source;
+    guardt guard_before_branch;
     propagationt propagation;
     unsigned atomic_section_id;
 
diff --git a/src/goto-symex/symex_atomic_section.cpp b/src/goto-symex/symex_atomic_section.cpp
index c243cafbcd4..1922ffb8e76 100644
--- a/src/goto-symex/symex_atomic_section.cpp
+++ b/src/goto-symex/symex_atomic_section.cpp
@@ -57,7 +57,7 @@ void goto_symext::symex_atomic_end(statet &state)
         it=++(r_it->second.second.begin());
         it!=r_it->second.second.end();
         ++it)
-      read_guard|=*it;
+      read_guard.logical_or(*it, ns);
     exprt read_guard_expr=read_guard.as_expr();
     do_simplify(read_guard_expr);
 
@@ -83,7 +83,7 @@ void goto_symext::symex_atomic_end(statet &state)
         it=++(w_it->second.begin());
         it!=w_it->second.end();
         ++it)
-      write_guard|=*it;
+      write_guard.logical_or(*it, ns);
     exprt write_guard_expr=write_guard.as_expr();
     do_simplify(write_guard_expr);
 
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index a86efc0815e..0784a408e54 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -175,6 +175,7 @@ void goto_symext::symex_goto(statet &state)
       state.rename(guard_expr, ns);
     }
 
+    new_state.guard_before_branch=state.guard;
     if(forward)
     {
       new_state.guard.add(guard_expr);
@@ -235,9 +236,11 @@ void goto_symext::merge_goto(
   const statet::goto_statet &goto_state,
   statet &state)
 {
+  statet::goto_statet &goto_state=*list_it;
+
   // check atomic section
   if(state.atomic_section_id!=goto_state.atomic_section_id)
-    throw "atomic sections differ across branches";
+    throw "Atomic sections differ across branches";
 
   // do SSA phi functions
   phi_function(goto_state, state);
@@ -245,7 +248,7 @@ void goto_symext::merge_goto(
   merge_value_sets(goto_state, state);
 
   // adjust guard
-  state.guard|=goto_state.guard;
+  state.guard.logical_or(goto_state.guard, ns);
 
   // adjust depth
   state.depth=std::min(state.depth, goto_state.depth);
@@ -278,10 +281,38 @@ void goto_symext::phi_function(
 
   if(!variables.empty())
   {
-    diff_guard=goto_state.guard;
+    guardt tmp_guard(goto_state.guard);
+    guardt tmp_guard2(goto_state.guard);
 
     // this gets the diff between the guards
-    diff_guard-=dest_state.guard;
+    // tmp_guard-=dest_state.guard;
+    if(!goto_state.guard_before_branch.is_constant())
+    {
+      assert(tmp_guard2.id()==ID_and);
+
+      if(goto_state.guard_before_branch.id()==ID_and)
+      {
+        assert(tmp_guard2.operands().size()>
+               goto_state.guard_before_branch.operands().size());
+        for(const auto & op : goto_state.guard_before_branch.operands())
+        {
+          // assert(tmp_guard2.operands().front()==op);
+          (void)op;
+          tmp_guard2.operands().erase(tmp_guard2.operands().begin());
+        }
+      }
+      else
+      {
+        assert(tmp_guard2.operands().front()==
+               goto_state.guard_before_branch);
+        tmp_guard2.operands().erase(tmp_guard2.operands().begin());
+      }
+
+      if(tmp_guard2.operands().size()==1)
+        tmp_guard2=tmp_guard2.op0();
+    }
+    // assert(tmp_guard==tmp_guard2);
+    diff_guard=tmp_guard2;
   }
 
   for(std::unordered_set<ssa_exprt, irep_hash>::const_iterator
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 5c2135e8afe..d97a769d59f 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/ieee_float.h>
+#include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
@@ -163,9 +164,11 @@ const exprt java_bytecode_convert_methodt::variable(
   size_t address,
   java_bytecode_convert_methodt::variable_cast_argumentt do_cast)
 {
-  irep_idt number=to_constant_expr(arg).get_value();
+  mp_integer number;
+  bool ret=to_integer(to_constant_expr(arg), number);
+  CHECK_RETURN(!ret);
 
-  std::size_t number_int=safe_string2size_t(id2string(number));
+  std::size_t number_int=integer2size_t(number);
   typet t=java_type_from_char(type_char);
   variablest &var_list=variables[number_int];
 
@@ -176,7 +179,7 @@ const exprt java_bytecode_convert_methodt::variable(
   if(var.symbol_expr.get_identifier().empty())
   {
     // an unnamed local variable
-    irep_idt base_name="anonlocal::"+id2string(number)+type_char;
+    irep_idt base_name="anonlocal::"+std::to_string(number_int)+type_char;
     irep_idt identifier=id2string(current_method)+"::"+id2string(base_name);
 
     symbol_exprt result(identifier, t);
@@ -848,8 +851,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       assert(!i_it->args.empty());
 
-      const unsigned target=safe_string2unsigned(
-        id2string(to_constant_expr(i_it->args[0]).get_value()));
+      unsigned target;
+      bool ret=to_unsigned_integer(to_constant_expr(i_it->args[0]), target);
+      DATA_INVARIANT(!ret, "target expected to be unsigned integer");
       targets.insert(target);
 
       a_entry.first->second.successors.push_back(target);
@@ -873,8 +877,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
       {
         if(is_label)
         {
-          const unsigned target=safe_string2unsigned(
-            id2string(to_constant_expr(arg).get_value()));
+          unsigned target;
+          bool ret=to_unsigned_integer(to_constant_expr(arg), target);
+          DATA_INVARIANT(!ret, "target expected to be unsigned integer");
           targets.insert(target);
           a_entry.first->second.successors.push_back(target);
         }
@@ -955,9 +960,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
        statement[statement.size()-2]=='_' &&
        isdigit(statement[statement.size()-1]))
     {
-      arg0=constant_exprt(
-        std::string(id2string(statement), statement.size()-1, 1),
-        integer_typet());
+      arg0=
+        from_integer(
+          string2integer(
+            std::string(id2string(statement), statement.size()-1, 1)),
+          java_int_type());
       statement=std::string(id2string(statement), 0, statement.size()-2);
     }
 
@@ -1353,16 +1360,20 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="goto" || statement=="goto_w")
     {
       assert(op.empty() && results.empty());
-      irep_idt number=to_constant_expr(arg0).get_value();
-      code_gotot code_goto(label(number));
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg0), number);
+      INVARIANT(!ret, "goto argument should be an integer");
+      code_gotot code_goto(label(integer2string(number)));
       c=code_goto;
     }
     else if(statement=="jsr" || statement=="jsr_w")
     {
       // As 'goto', except we must also push the subroutine return address:
       assert(op.empty() && results.size()==1);
-      irep_idt number=to_constant_expr(arg0).get_value();
-      code_gotot code_goto(label(number));
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg0), number);
+      INVARIANT(!ret, "jsr argument should be an integer");
+      code_gotot code_goto(label(integer2string(number)));
       c=code_goto;
       results[0]=
         from_integer(
@@ -1422,9 +1433,13 @@ codet java_bytecode_convert_methodt::convert_instructions(
           ieee_float_spect::double_precision());
 
         ieee_floatt value(spec);
-        const typet &arg_type(arg0.type());
-        if(ID_integer==arg_type.id())
-          value.from_integer(arg0.get_int(ID_value));
+        if(arg0.type().id()!=ID_floatbv)
+        {
+          mp_integer number;
+          bool ret=to_integer(to_constant_expr(arg0), number);
+          DATA_INVARIANT(!ret, "failed to convert constant");
+          value.from_integer(number);
+        }
         else
           value.from_expr(to_constant_expr(arg0));
 
@@ -1432,23 +1447,29 @@ codet java_bytecode_convert_methodt::convert_instructions(
       }
       else
       {
-        const unsigned value(arg0.get_unsigned_int(ID_value));
+        mp_integer value;
+        bool ret=to_integer(to_constant_expr(arg0), value);
+        DATA_INVARIANT(!ret, "failed to convert constant");
         const typet type=java_type_from_char(statement[0]);
         results[0]=from_integer(value, type);
       }
     }
     else if(statement==patternt("?ipush"))
     {
-      assert(results.size()==1);
-      mp_integer int_value;
-      bool ret=to_integer(to_constant_expr(arg0), int_value);
-      INVARIANT(!ret, "?ipush argument should be an integer");
-      results[0]=from_integer(int_value, java_int_type());
+      PRECONDITION(results.size()==1);
+      DATA_INVARIANT(
+        arg0.id()==ID_constant,
+        "ipush argument expected to be constant");
+      results[0]=arg0;
+      if(arg0.type()!=java_int_type())
+        results[0].make_typecast(java_int_type());
     }
     else if(statement==patternt("if_?cmp??"))
     {
-      irep_idt number=to_constant_expr(arg0).get_value();
       assert(op.size()==2 && results.empty());
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg0), number);
+      INVARIANT(!ret, "if_?cmp?? argument should be an integer");
 
       code_ifthenelset code_branch;
       const irep_idt cmp_op=get_if_cmp_operator(statement);
@@ -1463,7 +1484,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       code_branch.cond()=condition;
       code_branch.cond().add_source_location()=i_it->source_location;
-      code_branch.then_case()=code_gotot(label(number));
+      code_branch.then_case()=code_gotot(label(integer2string(number)));
       code_branch.then_case().add_source_location()=i_it->source_location;
       code_branch.add_source_location()=i_it->source_location;
 
@@ -1480,15 +1501,17 @@ codet java_bytecode_convert_methodt::convert_instructions(
         statement=="ifle"?ID_le:
         (assert(false), "");
 
-      irep_idt number=to_constant_expr(arg0).get_value();
       assert(op.size()==1 && results.empty());
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg0), number);
+      INVARIANT(!ret, "if?? argument should be an integer");
 
       code_ifthenelset code_branch;
       code_branch.cond()=
         binary_relation_exprt(op[0], id, from_integer(0, op[0].type()));
       code_branch.cond().add_source_location()=i_it->source_location;
       code_branch.cond().add_source_location().set_function(method_id);
-      code_branch.then_case()=code_gotot(label(number));
+      code_branch.then_case()=code_gotot(label(integer2string(number)));
       code_branch.then_case().add_source_location()=i_it->source_location;
       code_branch.then_case().add_source_location().set_function(method_id);
       code_branch.add_source_location()=i_it->source_location;
@@ -1498,13 +1521,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement==patternt("ifnonnull"))
     {
-      irep_idt number=to_constant_expr(arg0).get_value();
       assert(op.size()==1 && results.empty());
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg0), number);
+      INVARIANT(!ret, "ifnonnull argument should be an integer");
       code_ifthenelset code_branch;
       const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
       const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
       code_branch.cond()=binary_relation_exprt(lhs, ID_notequal, rhs);
-      code_branch.then_case()=code_gotot(label(number));
+      code_branch.then_case()=code_gotot(label(integer2string(number)));
       code_branch.then_case().add_source_location()=i_it->source_location;
       code_branch.add_source_location()=i_it->source_location;
 
@@ -1513,12 +1538,14 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("ifnull"))
     {
       assert(op.size()==1 && results.empty());
-      irep_idt number=to_constant_expr(arg0).get_value();
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg0), number);
+      INVARIANT(!ret, "ifnull argument should be an integer");
       code_ifthenelset code_branch;
       const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
       const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
       code_branch.cond()=binary_relation_exprt(lhs, ID_equal, rhs);
-      code_branch.then_case()=code_gotot(label(number));
+      code_branch.then_case()=code_gotot(label(integer2string(number)));
       code_branch.then_case().add_source_location()=i_it->source_location;
       code_branch.add_source_location()=i_it->source_location;
 
@@ -1540,9 +1567,12 @@ codet java_bytecode_convert_methodt::convert_instructions(
       code_assignt code_assign;
       code_assign.lhs()=
         variable(arg0, 'i', i_it->address, NO_CAST);
+      exprt arg1_int_type=arg1;
+      if(arg1.type()!=java_int_type())
+        arg1_int_type.make_typecast(java_int_type());
       code_assign.rhs()=plus_exprt(
         variable(arg0, 'i', i_it->address, CAST_AS_NEEDED),
-        typecast_exprt(arg1, java_int_type()));
+        arg1_int_type);
       block.copy_to_operands(code_assign);
       c=block;
     }
@@ -1579,10 +1609,16 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const std::size_t width=type.get_size_t(ID_width);
       typet target=unsignedbv_typet(width);
 
-      const typecast_exprt lhs(op[0], target);
-      const typecast_exprt rhs(op[1], target);
+      exprt lhs=op[0];
+      if(lhs.type()!=target)
+        lhs.make_typecast(target);
+      exprt rhs=op[1];
+      if(rhs.type()!=target)
+        rhs.make_typecast(target);
 
-      results[0]=typecast_exprt(lshr_exprt(lhs, rhs), op[0].type());
+      results[0]=lshr_exprt(lhs, rhs);
+      if(results[0].type()!=op[0].type())
+        results[0].make_typecast(op[0].type());
     }
     else if(statement==patternt("?add"))
     {
@@ -1815,7 +1851,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("?2?")) // i2c etc.
     {
       assert(op.size()==1 && results.size()==1);
-      results[0]=typecast_exprt(op[0], java_type_from_char(statement[2]));
+      typet type=java_type_from_char(statement[2]);
+      results[0]=op[0];
+      if(results[0].type()!=type)
+        results[0].make_typecast(type);
     }
     else if(statement=="new")
     {
@@ -1901,8 +1940,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       // The first argument is the type, the second argument is the number of
       // dimensions.  The size of each dimension is on the stack.
-      irep_idt number=to_constant_expr(arg1).get_value();
-      std::size_t dimension=safe_string2size_t(id2string(number));
+      mp_integer number;
+      bool ret=to_integer(to_constant_expr(arg1), number);
+      INVARIANT(!ret, "multianewarray argument should be an integer");
+      std::size_t dimension=integer2size_t(number);
 
       op=pop(dimension);
       assert(results.size()==1);
@@ -1976,8 +2017,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
           code_switch_caset code_case;
           code_case.add_source_location()=i_it->source_location;
 
-          irep_idt number=to_constant_expr(*a_it).get_value();
-          code_case.code()=code_gotot(label(number));
+          mp_integer number;
+          bool ret=to_integer(to_constant_expr(*a_it), number);
+          DATA_INVARIANT(!ret, "case label expected to be integer");
+          code_case.code()=code_gotot(label(integer2string(number)));
           code_case.code().add_source_location()=i_it->source_location;
 
           if(a_it==i_it->args.begin())
@@ -1986,7 +2029,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
           {
             instructiont::argst::const_iterator prev=a_it;
             prev--;
-            code_case.case_op()=typecast_exprt(*prev, op[0].type());
+            code_case.case_op()=*prev;
+            if(code_case.case_op().type()!=op[0].type())
+              code_case.case_op().make_typecast(op[0].type());
             code_case.case_op().add_source_location()=i_it->source_location;
           }
 
diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp
index d24141b76da..f93818eb274 100644
--- a/src/java_bytecode/java_bytecode_parser.cpp
+++ b/src/java_bytecode/java_bytecode_parser.cpp
@@ -703,7 +703,7 @@ void java_bytecode_parsert::rbytecode(
     case 'b': // a signed byte
       {
         s1 c=read_u1();
-        instruction.args.push_back(from_integer(c, integer_typet()));
+        instruction.args.push_back(from_integer(c, signedbv_typet(8)));
       }
       address+=1;
 
@@ -712,8 +712,8 @@ void java_bytecode_parsert::rbytecode(
     case 'o': // two byte branch offset, signed
       {
         s2 offset=read_u2();
-        instruction
-          .args.push_back(from_integer(address+offset, integer_typet()));
+        instruction.args.push_back(
+          from_integer(address+offset, signedbv_typet(16)));
       }
       address+=2;
       break;
@@ -721,8 +721,8 @@ void java_bytecode_parsert::rbytecode(
     case 'O': // four byte branch offset, signed
       {
         s4 offset=read_u4();
-        instruction
-          .args.push_back(from_integer(address+offset, integer_typet()));
+        instruction.args.push_back(
+          from_integer(address+offset, signedbv_typet(32)));
       }
       address+=4;
       break;
@@ -730,7 +730,7 @@ void java_bytecode_parsert::rbytecode(
     case 'v': // local variable index (one byte)
       {
         u1 v=read_u1();
-        instruction.args.push_back(from_integer(v, integer_typet()));
+        instruction.args.push_back(from_integer(v, unsignedbv_typet(8)));
       }
       address+=1;
       break;
@@ -740,17 +740,17 @@ void java_bytecode_parsert::rbytecode(
       if(wide_instruction)
       {
         u2 v=read_u2();
-        instruction.args.push_back(from_integer(v, integer_typet()));
+        instruction.args.push_back(from_integer(v, unsignedbv_typet(16)));
         s2 c=read_u2();
-        instruction.args.push_back(from_integer(c, integer_typet()));
+        instruction.args.push_back(from_integer(c, signedbv_typet(16)));
         address+=4;
       }
       else // local variable index (one byte) plus one signed byte
       {
         u1 v=read_u1();
-        instruction.args.push_back(from_integer(v, integer_typet()));
+        instruction.args.push_back(from_integer(v, unsignedbv_typet(8)));
         s1 c=read_u1();
-        instruction.args.push_back(from_integer(c, integer_typet()));
+        instruction.args.push_back(from_integer(c, signedbv_typet(8)));
         address+=2;
       }
       break;
@@ -760,9 +760,9 @@ void java_bytecode_parsert::rbytecode(
         u2 c=read_u2();
         instruction.args.push_back(constant(c));
         u1 b1=read_u1();
-        instruction.args.push_back(from_integer(b1, integer_typet()));
+        instruction.args.push_back(from_integer(b1, unsignedbv_typet(8)));
         u1 b2=read_u1();
-        instruction.args.push_back(from_integer(b2, integer_typet()));
+        instruction.args.push_back(from_integer(b2, unsignedbv_typet(8)));
       }
       address+=4;
       break;
@@ -776,8 +776,8 @@ void java_bytecode_parsert::rbytecode(
 
         // now default value
         s4 default_value=read_u4();
-        instruction.args
-          .push_back(from_integer(base_offset+default_value, integer_typet()));
+        instruction.args.push_back(
+          from_integer(base_offset+default_value, signedbv_typet(32)));
         address+=4;
 
         // number of pairs
@@ -788,9 +788,10 @@ void java_bytecode_parsert::rbytecode(
         {
           s4 match=read_u4();
           s4 offset=read_u4();
-          instruction.args.push_back(from_integer(match, integer_typet()));
-          instruction.args
-            .push_back(from_integer(base_offset+offset, integer_typet()));
+          instruction.args.push_back(
+            from_integer(match, signedbv_typet(32)));
+          instruction.args.push_back(
+            from_integer(base_offset+offset, signedbv_typet(32)));
           address+=8;
         }
       }
@@ -805,8 +806,8 @@ void java_bytecode_parsert::rbytecode(
 
         // now default value
         s4 default_value=read_u4();
-        instruction.args
-          .push_back(from_integer(base_offset+default_value, integer_typet()));
+        instruction.args.push_back(
+          from_integer(base_offset+default_value, signedbv_typet(32)));
         address+=4;
 
         // now low value
@@ -821,9 +822,9 @@ void java_bytecode_parsert::rbytecode(
         for(s4 i=low_value; i<=high_value; i++)
         {
           s4 offset=read_u4();
-          instruction.args.push_back(from_integer(i, integer_typet()));
-          instruction.args
-            .push_back(from_integer(base_offset+offset, integer_typet()));
+          instruction.args.push_back(from_integer(i, signedbv_typet(32)));
+          instruction.args.push_back(
+            from_integer(base_offset+offset, signedbv_typet(32)));
           address+=4;
         }
       }
@@ -834,7 +835,8 @@ void java_bytecode_parsert::rbytecode(
         u2 c=read_u2(); // constant-pool index
         instruction.args.push_back(constant(c));
         u1 dimensions=read_u1(); // number of dimensions
-        instruction.args.push_back(from_integer(dimensions, integer_typet()));
+        instruction.args.push_back(
+          from_integer(dimensions, unsignedbv_typet(8)));
         address+=3;
       }
       break;
@@ -862,7 +864,7 @@ void java_bytecode_parsert::rbytecode(
     case 's': // a signed short
       {
         s2 s=read_u2();
-        instruction.args.push_back(from_integer(s, integer_typet()));
+        instruction.args.push_back(from_integer(s, signedbv_typet(16)));
       }
       address+=2;
       break;
diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp
index 94d5062fb24..70b2568476a 100644
--- a/src/java_bytecode/java_local_variable_table.cpp
+++ b/src/java_bytecode/java_local_variable_table.cpp
@@ -13,6 +13,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 
 #include "java_types.h"
 
+#include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/string2int.h>
 
 #include <climits>
@@ -177,21 +179,22 @@ static bool is_store_to_slot(
   if(!(prevstatement.size()>=1 && prevstatement.substr(1, 5)=="store"))
     return false;
 
-  std::string storeslot;
+  unsigned storeslotidx;
   if(inst.args.size()==1)
   {
     // Store with an argument:
     const auto &arg=inst.args[0];
-    storeslot=id2string(to_constant_expr(arg).get_value());
+    bool ret=to_unsigned_integer(to_constant_expr(arg), storeslotidx);
+    CHECK_RETURN(!ret);
   }
   else
   {
     // Store shorthands, like "store_0", "store_1"
     assert(prevstatement[6]=='_' && prevstatement.size()==8);
-    storeslot=prevstatement[7];
+    std::string storeslot(1, prevstatement[7]);
     assert(isdigit(storeslot[0]));
+    storeslotidx=safe_string2unsigned(storeslot);
   }
-  auto storeslotidx=safe_string2unsigned(storeslot);
   return storeslotidx==slotidx;
 }
 
diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp
index f64071ec617..043ac0fb05c 100644
--- a/src/path-symex/path_symex.cpp
+++ b/src/path-symex/path_symex.cpp
@@ -422,6 +422,14 @@ void path_symext::assign_rec(
       var_state.value=propagate(ssa_rhs)?ssa_rhs:nil_exprt();
     }
   }
+  else if(ssa_lhs.id()==ID_typecast)
+  {
+    // dereferencing might yield a typecast
+    const exprt &new_lhs=to_typecast_expr(ssa_lhs).op();
+    typecast_exprt new_rhs(ssa_rhs, new_lhs.type());
+
+    assign_rec(state, guard, new_lhs, new_rhs);
+  }
   else if(ssa_lhs.id()==ID_member)
   {
     #ifdef DEBUG
@@ -541,14 +549,30 @@ void path_symext::assign_rec(
 
     assert(operands.size()==components.size());
 
-    for(std::size_t i=0; i<components.size(); i++)
+    if(ssa_rhs.id()==ID_struct &&
+       ssa_rhs.operands().size()==components.size())
     {
-      exprt new_rhs=
-        ssa_rhs.is_nil()?ssa_rhs:
-        simplify_expr(
-          member_exprt(ssa_rhs, components[i].get_name(), components[i].type()),
-          state.var_map.ns);
-      assign_rec(state, guard, operands[i], new_rhs);
+      exprt::operandst::const_iterator lhs_it=operands.begin();
+      forall_operands(it, ssa_rhs)
+      {
+        assign_rec(state, guard, *lhs_it, *it);
+        ++lhs_it;
+      }
+    }
+    else
+    {
+      for(std::size_t i=0; i<components.size(); i++)
+      {
+        exprt new_rhs=
+          ssa_rhs.is_nil()?ssa_rhs:
+          simplify_expr(
+            member_exprt(
+              ssa_rhs,
+              components[i].get_name(),
+              components[i].type()),
+            state.var_map.ns);
+        assign_rec(state, guard, operands[i], new_rhs);
+      }
     }
   }
   else if(ssa_lhs.id()==ID_array)
@@ -564,36 +588,30 @@ void path_symext::assign_rec(
     const exprt::operandst &operands=ssa_lhs.operands();
 
     // split up into elements
-    for(std::size_t i=0; i<operands.size(); i++)
+    if(ssa_rhs.id()==ID_array &&
+       ssa_rhs.operands().size()==operands.size())
     {
-      exprt new_rhs=
-        ssa_rhs.is_nil()?ssa_rhs:
-        simplify_expr(
-          index_exprt(
-            ssa_rhs,
-            from_integer(i, index_type()), array_type.subtype()),
-          state.var_map.ns);
-      assign_rec(state, guard, operands[i], new_rhs);
+      exprt::operandst::const_iterator lhs_it=operands.begin();
+      forall_operands(it, ssa_rhs)
+      {
+        assign_rec(state, guard, *lhs_it, *it);
+        ++lhs_it;
+      }
     }
-  }
-  else if(ssa_lhs.id()==ID_vector)
-  {
-    const vector_typet &vector_type=
-      to_vector_type(state.var_map.ns.follow(ssa_lhs.type()));
-
-    const exprt::operandst &operands=ssa_lhs.operands();
-
-    // split up into elements
-    for(std::size_t i=0; i<operands.size(); i++)
+    else
     {
-      exprt new_rhs=
-        ssa_rhs.is_nil()?ssa_rhs:
-        simplify_expr(
-          index_exprt(
-            ssa_rhs,
-            from_integer(i, index_type()), vector_type.subtype()),
-          state.var_map.ns);
-      assign_rec(state, guard, operands[i], new_rhs);
+      for(std::size_t i=0; i<operands.size(); i++)
+      {
+        exprt new_rhs=
+          ssa_rhs.is_nil()?ssa_rhs:
+          simplify_expr(
+            index_exprt(
+              ssa_rhs,
+              from_integer(i, index_type()),
+              array_type.subtype()),
+            state.var_map.ns);
+        assign_rec(state, guard, operands[i], new_rhs);
+      }
     }
   }
   else if(ssa_lhs.id()==ID_string_constant ||
diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp
index 495f598202a..fe663da5b7c 100644
--- a/src/path-symex/path_symex_state.cpp
+++ b/src/path-symex/path_symex_state.cpp
@@ -41,12 +41,6 @@ path_symex_statet initial_state(
   return s;
 }
 
-loc_reft path_symex_statet::get_pc() const
-{
-  assert(current_thread<threads.size());
-  return threads[current_thread].pc;
-}
-
 void path_symex_statet::output(const threadt &thread, std::ostream &out) const
 {
   out << "  PC: " << thread.pc << '\n';
diff --git a/src/path-symex/path_symex_state.h b/src/path-symex/path_symex_state.h
index eb23e891f83..bb6fc91187a 100644
--- a/src/path-symex/path_symex_state.h
+++ b/src/path-symex/path_symex_state.h
@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H
 #define CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H
 
+#include <util/invariant.h>
+
 #include "locs.h"
 #include "var_map.h"
 #include "path_symex_history.h"
@@ -111,11 +113,9 @@ struct path_symex_statet
     current_thread=_thread;
   }
 
-  loc_reft get_pc() const;
-
   goto_programt::const_targett get_instruction() const
   {
-    return locs[get_pc()].target;
+    return locs[pc()].target;
   }
 
   bool is_executable() const
@@ -145,6 +145,7 @@ struct path_symex_statet
 
   loc_reft pc() const
   {
+    PRECONDITION(current_thread<threads.size());
     return threads[current_thread].pc;
   }
 
diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp
index 87dea21be4a..06a7f10f59d 100644
--- a/src/path-symex/path_symex_state_read.cpp
+++ b/src/path-symex/path_symex_state_read.cpp
@@ -247,7 +247,14 @@ exprt path_symex_statet::instantiate_rec(
     {
       irep_idt id="symex::nondet"+std::to_string(var_map.nondet_count);
       var_map.nondet_count++;
-      return symbol_exprt(id, src.type());
+
+      auxiliary_symbolt nondet_symbol;
+      nondet_symbol.name=id;
+      nondet_symbol.base_name=id;
+      nondet_symbol.type=src.type();
+      var_map.new_symbols.add(nondet_symbol);
+
+      return nondet_symbol.symbol_expr();
     }
     else
       throw "instantiate_rec: unexpected side effect "+id2string(statement);
diff --git a/src/path-symex/var_map.h b/src/path-symex/var_map.h
index 7b17169c441..09511174cab 100644
--- a/src/path-symex/var_map.h
+++ b/src/path-symex/var_map.h
@@ -18,12 +18,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/namespace.h>
 #include <util/type.h>
 #include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 class var_mapt
 {
 public:
   explicit var_mapt(const namespacet &_ns):
-    ns(_ns), shared_count(0), local_count(0), nondet_count(0), dynamic_count(0)
+    ns(_ns.get_symbol_table(), new_symbols),
+    shared_count(0),
+    local_count(0),
+    nondet_count(0),
+    dynamic_count(0)
   {
   }
 
@@ -93,7 +98,8 @@ class var_mapt
 
   void init(var_infot &var_info);
 
-  const namespacet &ns;
+  const namespacet ns;
+  symbol_tablet new_symbols;
 
   void output(std::ostream &) const;
 
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index d2098ece102..87712e13bee 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 
+#include <util/invariant.h>
 #include <util/string2int.h>
 #include <util/expr_util.h>
 #include <util/base_type.h>
@@ -858,16 +859,24 @@ bool value_set_dereferencet::memory_model_bytes(
   {
     // upper bound
     {
-      mp_integer from_width=pointer_offset_size(from_type, ns);
-      if(from_width<=0)
-        throw "unknown or invalid type size:\n"+from_type.pretty();
-
-      mp_integer to_width=
-        to_type.id()==ID_empty?0: pointer_offset_size(to_type, ns);
-      if(to_width<0)
-        throw "unknown or invalid type size:\n"+to_type.pretty();
-
-      exprt bound=from_integer(from_width-to_width, offset.type());
+      exprt from_width=size_of_expr(from_type, ns);
+      INVARIANT(
+        from_width.is_not_nil(),
+        "unknown or invalid type size:\n"+from_type.pretty());
+
+      exprt to_width=
+        to_type.id()==ID_empty?
+        from_integer(0, size_type()):size_of_expr(to_type, ns);
+      INVARIANT(
+        to_width.is_not_nil(),
+        "unknown or invalid type size:\n"+to_type.pretty());
+      INVARIANT(
+        from_width.type()==to_width.type(),
+        "type mismatch on result of size_of_expr");
+
+      minus_exprt bound(from_width, to_width);
+      if(bound.type()!=offset.type())
+        bound.make_typecast(offset.type());
 
       binary_relation_exprt
         offset_upper_bound(offset, ID_gt, bound);
diff --git a/src/solvers/flattening/boolbv_extractbits.cpp b/src/solvers/flattening/boolbv_extractbits.cpp
index 3b363a6367d..4f549139feb 100644
--- a/src/solvers/flattening/boolbv_extractbits.cpp
+++ b/src/solvers/flattening/boolbv_extractbits.cpp
@@ -17,15 +17,6 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  const irep_idt &type_id=expr.type().id();
-
-  if(type_id!=ID_signedbv &&
-     type_id!=ID_unsignedbv &&
-     type_id!=ID_c_enum &&
-     type_id!=ID_c_enum_tag &&
-     type_id!=ID_bv)
-    return conversion_failed(expr);
-
   if(expr.operands().size()!=3)
   {
     error().source_location=expr.find_source_location();
diff --git a/src/solvers/flattening/boolbv_member.cpp b/src/solvers/flattening/boolbv_member.cpp
index 448e80f5653..0f01e2be959 100644
--- a/src/solvers/flattening/boolbv_member.cpp
+++ b/src/solvers/flattening/boolbv_member.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 
 bvt boolbvt::convert_member(const member_exprt &expr)
 {
@@ -24,7 +25,7 @@ bvt boolbvt::convert_member(const member_exprt &expr)
     return convert_bv(
       byte_extract_exprt(byte_extract_id(),
                          struct_op,
-                         from_integer(0, integer_typet()),
+                         from_integer(0, index_type()),
                          expr.type()));
   }
   else if(struct_op_type.id()==ID_struct)
diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp
index b5837f3206e..1d431c083c4 100644
--- a/src/solvers/flattening/flatten_byte_operators.cpp
+++ b/src/solvers/flattening/flatten_byte_operators.cpp
@@ -109,8 +109,8 @@ static exprt unpack_rec(
   }
   else if(type.id()!=ID_empty)
   {
-    // a basic type; we turn that into logical right shift and
-    // extractbits while considering endianness
+    // a basic type; we turn that into extractbits while considering
+    // endianness
     mp_integer bits=pointer_offset_bits(type, ns);
     if(bits<0)
     {
@@ -121,17 +121,12 @@ static exprt unpack_rec(
         bits*=8;
     }
 
-    // cast to generic bit-vector
-    typecast_exprt src_tc(src, unsignedbv_typet(integer2size_t(bits)));
-
     for(mp_integer i=0; i<bits; i+=8)
     {
-      lshr_exprt right_shift(src_tc, from_integer(i, index_type()));
-
       extractbits_exprt extractbits(
-        right_shift,
-        from_integer(7, index_type()),
-        from_integer(0, index_type()),
+        src,
+        from_integer(i+7, index_type()),
+        from_integer(i, index_type()),
         unsignedbv_typet(8));
 
       if(little_endian)
@@ -283,6 +278,8 @@ exprt flatten_byte_extract(
       byte_extract_exprt tmp(unpacked);
       tmp.type()=comp.type();
       tmp.offset()=simplify_expr(new_offset, ns);
+
+      s.move_to_operands(tmp);
     }
 
     if(!failed)
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index 3f1ffd47798..1018dfca2b7 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/std_expr.h>
 #include <util/prefix.h>
 #include <util/pointer_offset_size.h>
@@ -87,7 +88,7 @@ exprt pointer_logict::pointer_expr(
       constant_exprt null(type);
       null.set_value(ID_NULL);
       return plus_exprt(null,
-        from_integer(pointer.offset, integer_typet()));
+        from_integer(pointer.offset, pointer_diff_type()));
     }
   }
   else if(pointer.object==invalid_object) // INVALID?
diff --git a/src/solvers/miniBDD/miniBDD.cpp b/src/solvers/miniBDD/miniBDD.cpp
index d32330a0995..4c00b1de85b 100644
--- a/src/solvers/miniBDD/miniBDD.cpp
+++ b/src/solvers/miniBDD/miniBDD.cpp
@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 void mini_bdd_nodet::remove_reference()
 {
+  // NOLINTNEXTLINE(build/deprecated)
   assert(reference_counter!=0);
 
   reference_counter--;
@@ -194,20 +195,23 @@ class mini_bdd_applyt
 
   mini_bddt operator()(const mini_bddt &x, const mini_bddt &y)
   {
-    return APP(x, y);
+    return APP_non_rec(x, y);
   }
 
 protected:
   bool (*fkt)(bool, bool);
-  mini_bddt APP(const mini_bddt &x, const mini_bddt &y);
+  mini_bddt APP_rec(const mini_bddt &x, const mini_bddt &y);
+  mini_bddt APP_non_rec(const mini_bddt &x, const mini_bddt &y);
 
   typedef std::map<std::pair<unsigned, unsigned>, mini_bddt> Gt;
   Gt G;
 };
 
-mini_bddt mini_bdd_applyt::APP(const mini_bddt &x, const mini_bddt &y)
+mini_bddt mini_bdd_applyt::APP_rec(const mini_bddt &x, const mini_bddt &y)
 {
+  // NOLINTNEXTLINE(build/deprecated)
   assert(x.is_initialized() && y.is_initialized());
+  // NOLINTNEXTLINE(build/deprecated)
   assert(x.node->mgr==y.node->mgr);
 
   // dynamic programming
@@ -224,22 +228,134 @@ mini_bddt mini_bdd_applyt::APP(const mini_bddt &x, const mini_bddt &y)
     u=mini_bddt(fkt(x.is_true(), y.is_true())?mgr->True():mgr->False());
   else if(x.var()==y.var())
     u=mgr->mk(x.var(),
-              APP(x.low(), y.low()),
-              APP(x.high(), y.high()));
+              APP_rec(x.low(), y.low()),
+              APP_rec(x.high(), y.high()));
   else if(x.var()<y.var())
     u=mgr->mk(x.var(),
-              APP(x.low(), y),
-              APP(x.high(), y));
+              APP_rec(x.low(), y),
+              APP_rec(x.high(), y));
   else /* x.var() > y.var() */
     u=mgr->mk(y.var(),
-              APP(x, y.low()),
-              APP(x, y.high()));
+              APP_rec(x, y.low()),
+              APP_rec(x, y.high()));
 
   G[key]=u;
 
   return u;
 }
 
+mini_bddt mini_bdd_applyt::APP_non_rec(
+  const mini_bddt &_x,
+  const mini_bddt &_y)
+{
+  struct stack_elementt
+  {
+    stack_elementt(
+      mini_bddt &_result,
+      const mini_bddt &_x,
+      const mini_bddt &_y):
+      result(_result), x(_x), y(_y),
+      key(x.node_number(), y.node_number()),
+      var(0), phase(phaset::INIT) { }
+    mini_bddt &result, x, y, lr, hr;
+    std::pair<unsigned, unsigned> key;
+    unsigned var;
+    enum class phaset { INIT, FINISH } phase;
+  };
+
+  mini_bddt u; // return value
+
+  std::stack<stack_elementt> stack;
+  stack.push(stack_elementt(u, _x, _y));
+
+  while(!stack.empty())
+  {
+    auto &t=stack.top();
+    const mini_bddt &x=t.x;
+    const mini_bddt &y=t.y;
+    // NOLINTNEXTLINE(build/deprecated)
+    assert(x.is_initialized() && y.is_initialized());
+    // NOLINTNEXTLINE(build/deprecated)
+    assert(x.node->mgr==y.node->mgr);
+
+    switch(t.phase)
+    {
+    case stack_elementt::phaset::INIT:
+      {
+        // dynamic programming
+        Gt::const_iterator G_it=G.find(t.key);
+        if(G_it!=G.end())
+        {
+          t.result=G_it->second;
+          stack.pop();
+        }
+        else
+        {
+          if(x.is_constant() && y.is_constant())
+          {
+            bool result_truth=fkt(x.is_true(), y.is_true());
+            const mini_bdd_mgrt &mgr=*x.node->mgr;
+            t.result=result_truth?mgr.True():mgr.False();
+            stack.pop();
+          }
+          else if(x.var()==y.var())
+          {
+            t.var=x.var();
+            t.phase=stack_elementt::phaset::FINISH;
+            // NOLINTNEXTLINE(build/deprecated)
+            assert(x.low().var()>t.var);
+            // NOLINTNEXTLINE(build/deprecated)
+            assert(y.low().var()>t.var);
+            // NOLINTNEXTLINE(build/deprecated)
+            assert(x.high().var()>t.var);
+            // NOLINTNEXTLINE(build/deprecated)
+            assert(y.high().var()>t.var);
+            stack.push(stack_elementt(t.lr, x.low(), y.low()));
+            stack.push(stack_elementt(t.hr, x.high(), y.high()));
+          }
+          else if(x.var()<y.var())
+          {
+            t.var=x.var();
+            t.phase=stack_elementt::phaset::FINISH;
+            // NOLINTNEXTLINE(build/deprecated)
+            assert(x.low().var()>t.var);
+            // NOLINTNEXTLINE(build/deprecated)
+            assert(x.high().var()>t.var);
+            stack.push(stack_elementt(t.lr, x.low(), y));
+            stack.push(stack_elementt(t.hr, x.high(), y));
+          }
+          else /* x.var() > y.var() */
+          {
+            t.var=y.var();
+            t.phase=stack_elementt::phaset::FINISH;
+            // NOLINTNEXTLINE(build/deprecated)
+            assert(y.low().var()>t.var);
+            // NOLINTNEXTLINE(build/deprecated)
+            assert(y.high().var()>t.var);
+            stack.push(stack_elementt(t.lr, x, y.low()));
+            stack.push(stack_elementt(t.hr, x, y.high()));
+          }
+        }
+      }
+      break;
+
+    case stack_elementt::phaset::FINISH:
+      {
+        mini_bdd_mgrt *mgr=x.node->mgr;
+        t.result=mgr->mk(t.var, t.lr, t.hr);
+        G[t.key]=t.result;
+        stack.pop();
+      }
+      break;
+    }
+  }
+
+  // NOLINTNEXTLINE(build/deprecated)
+  assert(u.is_initialized());
+
+  return u;
+}
+
 bool equal_fkt(bool x, bool y)
 {
   return x==y;
@@ -262,6 +378,7 @@ mini_bddt mini_bddt::operator^(const mini_bddt &other) const
 
 mini_bddt mini_bddt::operator!() const
 {
+  // NOLINTNEXTLINE(build/deprecated)
   assert(is_initialized());
   return node->mgr->True()^*this;
 }
@@ -304,8 +421,11 @@ mini_bddt mini_bdd_mgrt::mk(
   const mini_bddt &low,
   const mini_bddt &high)
 {
+  // NOLINTNEXTLINE(build/deprecated)
   assert(var<=var_table.size());
+  // NOLINTNEXTLINE(build/deprecated)
   assert(low.var()>var);
+  // NOLINTNEXTLINE(build/deprecated)
   assert(high.var()>var);
 
   if(low.node_number()==high.node_number())
@@ -343,14 +463,20 @@ mini_bddt mini_bdd_mgrt::mk(
 }
 
 bool mini_bdd_mgrt::reverse_keyt::operator<(
-  const mini_bdd_mgrt::reverse_keyt &other) const
+  const mini_bdd_mgrt::reverse_keyt &y) const
 {
-  if(var<other.var || low<other.low)
+  const reverse_keyt &x=*this;
+
+  if(x.var<y.var)
     return true;
-  if(var>other.var || low>other.low)
+  else if(x.var>y.var)
     return false;
-
-  return high<other.high;
+  else if(x.low<y.low)
+    return true;
+  else if(x.low>y.low)
+    return false;
+  else
+    return x.high<y.high;
 }
 
 void mini_bdd_mgrt::DumpTable(std::ostream &out) const
@@ -399,6 +525,7 @@ mini_bddt restrictt::RES(const mini_bddt &u)
 {
   // replace 'var' in 'u' by constant 'value'
 
+  // NOLINTNEXTLINE(build/deprecated)
   assert(u.is_initialized());
   mini_bdd_mgrt *mgr=u.node->mgr;
 
diff --git a/src/solvers/miniBDD/miniBDD.h b/src/solvers/miniBDD/miniBDD.h
index 9b994b88ff6..2187ceb5979 100644
--- a/src/solvers/miniBDD/miniBDD.h
+++ b/src/solvers/miniBDD/miniBDD.h
@@ -124,7 +124,7 @@ class mini_bdd_mgrt
     reverse_keyt(
       unsigned _var, const mini_bddt &_low, const mini_bddt &_high);
 
-    bool operator<(const reverse_keyt &other) const;
+    bool operator<(const reverse_keyt &) const;
   };
 
   typedef std::map<reverse_keyt, mini_bdd_nodet *> reverse_mapt;
diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp
index 2a5b4ffa786..251a70ef97e 100644
--- a/src/solvers/prop/bdd_expr.cpp
+++ b/src/solvers/prop/bdd_expr.cpp
@@ -122,7 +122,7 @@ exprt bdd_exprt::as_expr(const mini_bddt &r) const
   }
   else if(r.high().is_false())
   {
-    if(r.high().is_true())
+    if(r.low().is_true())
       return not_exprt(n_expr);
     else
       return and_exprt(not_exprt(n_expr), as_expr(r.low()));
@@ -132,7 +132,14 @@ exprt bdd_exprt::as_expr(const mini_bddt &r) const
   else if(r.high().is_true())
     return or_exprt(n_expr, as_expr(r.low()));
   else
+    #if 0
+    return
+      and_exprt(
+        or_exprt(not_exprt(n_expr), as_expr(r.high())),
+        or_exprt(n_expr, as_expr(r.low())));
+    #else
     return if_exprt(n_expr, as_expr(r.high()), as_expr(r.low()));
+    #endif
 }
 
 exprt bdd_exprt::as_expr() const
diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp
index 6b03b163fa5..54f15543430 100644
--- a/src/symex/path_search.cpp
+++ b/src/symex/path_search.cpp
@@ -68,9 +68,9 @@ path_searcht::resultt path_searcht::operator()(
       statet &state=tmp_queue.front();
 
       // record we have seen it
-      loc_data[state.get_pc().loc_number].visited=true;
+      loc_data[state.pc().loc_number].visited=true;
 
-      debug() << "Loc: #" << state.get_pc().loc_number
+      debug() << "Loc: #" << state.pc().loc_number
               << ", queue: " << queue.size()
               << ", depth: " << state.get_depth();
       for(const auto &s : queue)
@@ -102,10 +102,13 @@ path_searcht::resultt path_searcht::operator()(
 
       if(number_of_steps%1000==0)
       {
+        time_periodt running_time=current_time()-start_time;
         status() << "Queue " << queue.size()
-                 << " thread " << state.get_current_thread()
+                 << " thread " << state.get_current_thread()+1
                  << '/' << state.threads.size()
-                 << " PC " << state.pc() << messaget::eom;
+                 << " PC " << state.pc()
+                 << " [" << number_of_steps << " steps, "
+                 << running_time << "s]" << messaget::eom;
       }
 
       // an error, possibly?
@@ -264,34 +267,92 @@ bool path_searcht::drop_state(const statet &state)
 {
   goto_programt::const_targett pc=state.get_instruction();
 
+  const source_locationt &source_location=pc->source_location;
+
+  if(!source_location.is_nil() &&
+     last_source_location!=source_location)
+  {
+    debug() << "SYMEX at file " << source_location.get_file()
+            << " line " << source_location.get_line()
+            << " function " << source_location.get_function()
+            << eom;
+
+    last_source_location=source_location;
+  }
+
   // depth limit
-  if(depth_limit_set && state.get_depth()>depth_limit)
+  if(state.get_depth()>=depth_limit)
     return true;
 
   // context bound
-  if(context_bound_set && state.get_no_thread_interleavings()>context_bound)
+  if(state.get_no_thread_interleavings()>=context_bound)
     return true;
 
   // branch bound
-  if(branch_bound_set && state.get_no_branches()>branch_bound)
+  if(state.get_no_branches()>=branch_bound)
     return true;
 
   // unwinding limit -- loops
-  if(unwind_limit_set && state.get_instruction()->is_backwards_goto())
+  if(unwind_limit!=std::numeric_limits<unsigned>::max() && 
+     pc->is_backwards_goto())
   {
+    bool stop=false;
+
     for(const auto &loop_info : state.unwinding_map)
-      if(loop_info.second>unwind_limit)
-        return true;
+      if(loop_info.second>=unwind_limit)
+      {
+        stop=true;
+        break;
+      }
+
+    const irep_idt id=goto_programt::loop_id(pc);
+    path_symex_statet::unwinding_mapt::const_iterator entry=
+      state.unwinding_map.find(state.pc());
+    debug() << (stop?"Not unwinding":"Unwinding")
+      << " loop " << id << " iteration "
+      << (entry==state.unwinding_map.end()?-1:entry->second)
+      << " (" << unwind_limit << " max)"
+      << " " << source_location
+      << " thread " << state.get_current_thread() << eom;
+
+    if(stop)
+      return true;
   }
 
   // unwinding limit -- recursion
-  if(unwind_limit_set && state.get_instruction()->is_function_call())
+  if(unwind_limit!=std::numeric_limits<unsigned>::max() &&
+     pc->is_function_call())
   {
+    bool stop=false;
+
     for(const auto &rec_info : state.recursion_map)
-      if(rec_info.second>unwind_limit)
-        return true;
+      if(rec_info.second>=unwind_limit)
+      {
+        stop=true;
+        break;
+      }
+
+    exprt function=to_code_function_call(pc->code).function();
+    const irep_idt id=function.get(ID_identifier); // could be nil
+    path_symex_statet::recursion_mapt::const_iterator entry=
+      state.recursion_map.find(id);
+    if(entry!=state.recursion_map.end())
+      debug() << (stop?"Not unwinding":"Unwinding")
+        << " recursion " << id << " iteration "
+        << entry->second
+        << " (" << unwind_limit << " max)"
+        << " " << source_location
+        << " thread " << state.get_current_thread() << eom;
+
+    if(stop)
+      return true;
   }
 
+  // search time limit (--max-search-time)
+  if(time_limit!=std::numeric_limits<unsigned>::max() &&
+     current_time().get_t()>start_time.get_t()+time_limit*1000)
+    return true;
+
   if(pc->is_assume() &&
      simplify_expr(pc->guard, ns).is_false())
   {
diff --git a/src/symex/path_search.h b/src/symex/path_search.h
index ca570819cc8..f02b617ee40 100644
--- a/src/symex/path_search.h
+++ b/src/symex/path_search.h
@@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <path-symex/path_symex_state.h>
 
+#include <limits>
+
 class path_searcht:public safety_checkert
 {
 public:
@@ -26,10 +28,11 @@ class path_searcht:public safety_checkert
     safety_checkert(_ns),
     show_vcc(false),
     eager_infeasibility(false),
-    depth_limit_set(false), // no limit
-    context_bound_set(false),
-    unwind_limit_set(false),
-    branch_bound_set(false),
+    depth_limit(std::numeric_limits<unsigned>::max()),
+    context_bound(std::numeric_limits<unsigned>::max()),
+    branch_bound(std::numeric_limits<unsigned>::max()),
+    unwind_limit(std::numeric_limits<unsigned>::max()),
+    time_limit(std::numeric_limits<unsigned>::max()),
     search_heuristic(search_heuristict::DFS)
   {
   }
@@ -37,42 +40,43 @@ class path_searcht:public safety_checkert
   virtual resultt operator()(
     const goto_functionst &goto_functions);
 
-  void set_depth_limit(unsigned limit)
+  void set_depth_limit(int limit)
   {
-    depth_limit_set=true;
     depth_limit=limit;
   }
 
-  void set_context_bound(unsigned limit)
+  void set_context_bound(int limit)
   {
-    context_bound_set=true;
     context_bound=limit;
   }
 
-  void set_branch_bound(unsigned limit)
+  void set_branch_bound(int limit)
   {
-    branch_bound_set=true;
     branch_bound=limit;
   }
 
-  void set_unwind_limit(unsigned limit)
+  void set_unwind_limit(int limit)
   {
-    unwind_limit_set=true;
     unwind_limit=limit;
   }
 
+  void set_time_limit(int limit)
+  {
+    time_limit=limit;
+  }
+
   bool show_vcc;
   bool eager_infeasibility;
 
   // statistics
-  unsigned number_of_dropped_states;
-  unsigned number_of_paths;
-  unsigned number_of_steps;
-  unsigned number_of_feasible_paths;
-  unsigned number_of_infeasible_paths;
-  unsigned number_of_VCCs;
-  unsigned number_of_VCCs_after_simplification;
-  unsigned number_of_failed_properties;
+  std::size_t number_of_dropped_states;
+  std::size_t number_of_paths;
+  std::size_t number_of_steps;
+  std::size_t number_of_feasible_paths;
+  std::size_t number_of_infeasible_paths;
+  std::size_t number_of_VCCs;
+  std::size_t number_of_VCCs_after_simplification;
+  std::size_t number_of_failed_properties;
   std::size_t number_of_locs;
   absolute_timet start_time;
   time_periodt sat_time;
@@ -134,9 +138,11 @@ class path_searcht:public safety_checkert
   unsigned context_bound;
   unsigned branch_bound;
   unsigned unwind_limit;
-  bool depth_limit_set, context_bound_set, unwind_limit_set, branch_bound_set;
+  unsigned time_limit;
 
   enum class search_heuristict { DFS, BFS, LOCS } search_heuristic;
+
+  source_locationt last_source_location;
 };
 
 #endif // CPROVER_SYMEX_PATH_SEARCH_H
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 5fc475ee154..c2e567cc643 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -36,6 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/xml_goto_trace.h>
 #include <goto-programs/remove_complex.h>
+#include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_exceptions.h>
@@ -186,6 +187,10 @@ int symex_parse_optionst::doit()
       path_search.set_unwind_limit(
         unsafe_string2unsigned(cmdline.get_value("unwind")));
 
+    if(cmdline.isset("max-search-time"))
+      path_search.set_time_limit(
+        safe_string2unsigned(cmdline.get_value("max-search-time")));
+
     if(cmdline.isset("dfs"))
       path_search.set_dfs();
 
@@ -300,6 +305,12 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     // remove stuff
     remove_complex(goto_model);
     remove_vector(goto_model);
+    // remove function pointers
+    status() << "Removal of function pointers and virtual functions" << eom;
+    remove_function_pointers(
+      get_message_handler(),
+      goto_model,
+      cmdline.isset("pointer-check"));
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
     // Java throw and catch -> explicit exceptional return variables:
@@ -607,6 +618,7 @@ void symex_parse_optionst::help()
     " --depth nr                   limit search depth\n"
     " --context-bound nr           limit number of context switches\n"
     " --branch-bound nr            limit number of branches taken\n"
+    " --max-search-time s          limit search to approximately s seconds\n"
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index b4fc6fe2e1c..a9f3d9e3e83 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -30,7 +30,7 @@ class optionst;
 #define SYMEX_OPTIONS \
   "(function):" \
   "D:I:" \
-  "(depth):(context-bound):(branch-bound):(unwind):" \
+  "(depth):(context-bound):(branch-bound):(unwind):(max-search-time):" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
diff --git a/src/util/guard.cpp b/src/util/guard.cpp
index 693b48602c9..220684914f8 100644
--- a/src/util/guard.cpp
+++ b/src/util/guard.cpp
@@ -13,8 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <ostream>
 
+#include <solvers/prop/bdd_expr.h>
+
+#include "namespace.h"
 #include "std_expr.h"
 #include "simplify_utils.h"
+#include "symbol_table.h"
 
 void guardt::guard_expr(exprt &dest) const
 {
@@ -90,8 +94,10 @@ void guardt::add(const exprt &expr)
     op.push_back(expr);
 }
 
-guardt &operator -= (guardt &g1, const guardt &g2)
+guardt& guardt::operator -= (const guardt &g2)
 {
+  guardt &g1=*this;
+
   if(g1.id()!=ID_and || g2.id()!=ID_and)
     return g1;
 
@@ -119,13 +125,26 @@ guardt &operator -= (guardt &g1, const guardt &g2)
   return g1;
 }
 
-guardt &operator |= (guardt &g1, const guardt &g2)
+guardt& guardt::logical_or(const guardt &g2, const namespacet &ns)
 {
-  if(g2.is_false() || g1.is_true())
-    return g1;
-  if(g1.is_false() || g2.is_true())
+  guardt &g1=*this;
+
+  if(g2.is_false() || g1.is_true()) return g1;
+  if(g1.is_false() || g2.is_true()) { g1=g2; return g1; }
+
   {
-    g1=g2;
+    exprt tmp(g2);
+    tmp.make_not();
+
+    if(tmp==g1)
+      g1.make_true();
+    else
+      g1=or_exprt(g1, g2);
+
+    bdd_exprt t(ns);
+    t.from_expr(g1);
+    g1=t.as_expr();
+
     return g1;
   }
 
@@ -139,7 +158,9 @@ guardt &operator |= (guardt &g1, const guardt &g2)
     else
       g1=or_exprt(g1, g2);
 
-    // TODO: make simplify more capable and apply here
+    bdd_exprt t(ns);
+    t.from_expr(g1);
+    g1=t.as_expr();
 
     return g1;
   }
@@ -196,8 +217,13 @@ guardt &operator |= (guardt &g1, const guardt &g2)
     {
     }
     else
-      // TODO: make simplify more capable and apply here
+    {
       g1.add(or_exprt(and_expr1, and_expr2));
+
+      bdd_exprt t(ns);
+      t.from_expr(g1);
+      g1=t.as_expr();
+    }
   }
 
   return g1;
diff --git a/src/util/guard.h b/src/util/guard.h
index a923680e2ad..6cef54f7580 100644
--- a/src/util/guard.h
+++ b/src/util/guard.h
@@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "expr.h"
 
+class namespacet;
+
 class guardt:public exprt
 {
 public:
@@ -60,8 +62,8 @@ class guardt:public exprt
   void make_false();
 #endif
 
-  friend guardt &operator -= (guardt &g1, const guardt &g2);
-  friend guardt &operator |= (guardt &g1, const guardt &g2);
+  guardt& operator -= (const guardt &g2);
+  guardt& logical_or(const guardt &g2, const namespacet &ns);
 
 #if 0
   void swap(guardt &g)
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
index 154ba29c558..ba9fb9ac857 100644
--- a/src/util/ieee_float.cpp
+++ b/src/util/ieee_float.cpp
@@ -8,9 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ieee_float.h"
 
-// <cstdint> is yet to come
-#include <stdint.h>
-
+#include <cstdint>
 #include <ostream>
 #include <cassert>
 #include <cmath>
diff --git a/src/util/invariant.h b/src/util/invariant.h
index 325020a0d6e..a7df274e81d 100644
--- a/src/util/invariant.h
+++ b/src/util/invariant.h
@@ -149,6 +149,9 @@ void report_exception_to_stderr(const invariant_failedt &);
 /// \param params : (variadic) parameters to forward to ET's constructor
 ///  its backtrace member will be set before it is used.
 template<class ET, typename ...Params>
+#ifdef __GNUC__
+__attribute__((noreturn))
+#endif
 typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
 invariant_violated_structured(
   const std::string &file,
@@ -171,6 +174,9 @@ invariant_violated_structured(
 /// \param function : C string giving the name of the function.
 /// \param line : The line number of the invariant
 /// \param reason : brief description of the invariant violation.
+#ifdef __GNUC__
+__attribute__((noreturn))
+#endif
 inline void invariant_violated_string(
   const std::string &file,
   const std::string &function,
diff --git a/src/util/pipe_stream.cpp b/src/util/pipe_stream.cpp
index 44ac29b3eb4..e9fc1887fb5 100644
--- a/src/util/pipe_stream.cpp
+++ b/src/util/pipe_stream.cpp
@@ -23,9 +23,9 @@ Module: A stdin/stdout pipe as STL stream
 #else
 #include <sys/types.h>
 #include <sys/wait.h>
-#include <signal.h>
 #include <unistd.h>
 #include <cstring>
+#include <csignal>
 #endif
 
 #define READ_BUFFER_SIZE 1024
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index 238dfd384c9..bb8579bd3c1 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -11,8 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 #include <unordered_set>
 
+#include <solvers/prop/bdd_expr.h>
+
 #include "expr.h"
 #include "namespace.h"
+#include "simplify_utils.h"
 #include "std_expr.h"
 
 bool simplify_exprt::simplify_boolean(exprt &expr)
@@ -79,6 +82,21 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
     if(operands.empty())
       return true;
 
+    #if 0
+    bdd_exprt t(ns);
+    t.from_expr(expr);
+    exprt tmp=t.as_expr();
+    sort_and_join(tmp);
+
+    if(tmp!=expr)
+    {
+      expr.swap(tmp);
+      return false;
+    }
+
+    return true;
+    #else
+
     bool result=true;
 
     exprt::operandst::const_iterator last;
@@ -183,6 +201,7 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
     }
 
     return result;
+    #endif
   }
 
   return true;
diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
index cef9446e2e1..f57f4979630 100644
--- a/src/util/std_expr.cpp
+++ b/src/util/std_expr.cpp
@@ -135,7 +135,7 @@ void object_descriptor_exprt::build(
   assert(root_object().type().id()!=ID_empty);
 }
 
-constant_exprt constant_exprt::integer_constant(unsigned v)
+static constant_exprt integer_constant(unsigned v)
 {
   return constant_exprt(std::to_string(v), integer_typet());
 }
@@ -144,7 +144,7 @@ shift_exprt::shift_exprt(
   const exprt &_src,
   const irep_idt &_id,
   const std::size_t _distance):
-  binary_exprt(_src, _id, constant_exprt::integer_constant(_distance))
+  binary_exprt(_src, _id, integer_constant(_distance))
 {
 }
 
@@ -152,7 +152,7 @@ extractbit_exprt::extractbit_exprt(
   const exprt &_src,
   const std::size_t _index):
   binary_predicate_exprt(
-    _src, ID_extractbit, constant_exprt::integer_constant(_index))
+    _src, ID_extractbit, integer_constant(_index))
 {
 }
 
@@ -166,8 +166,8 @@ extractbits_exprt::extractbits_exprt(
   assert(_upper>=_lower);
   operands().resize(3);
   src()=_src;
-  upper()=constant_exprt::integer_constant(_upper);
-  lower()=constant_exprt::integer_constant(_lower);
+  upper()=integer_constant(_upper);
+  lower()=integer_constant(_lower);
 }
 
 /*******************************************************************\
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index c4837be001a..a47c3afd684 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -3710,8 +3710,6 @@ class constant_exprt:public exprt
   }
 
   bool value_is_zero_string() const;
-
-  static constant_exprt integer_constant(unsigned);
 };
 
 /*! \brief Cast a generic exprt to a \ref constant_exprt
diff --git a/unit/Makefile b/unit/Makefile
index 3e5bb48afbe..409402af1f1 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -11,6 +11,7 @@ SRC += unit_tests.cpp \
        analyses/does_remove_const/does_expr_lose_const.cpp \
        analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
+       miniBDD_new.cpp \
        catch_example.cpp \
        # Empty last line
 
diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp
index 2d276fdbbd8..d161df0bffb 100644
--- a/unit/analyses/ai/ai_simplify_lhs.cpp
+++ b/unit/analyses/ai/ai_simplify_lhs.cpp
@@ -16,6 +16,7 @@
 #include <ansi-c/ansi_c_language.h>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/namespace.h>
 #include <util/ui_message.h>
@@ -73,7 +74,7 @@ SCENARIO("ai_domain_baset::ai_simplify_lhs",
 
     const unsigned int array_size=5;
     array_typet array_type(
-      signedbv_typet(32), constant_exprt::integer_constant(array_size));
+      signedbv_typet(32), from_integer(array_size, size_type()));
 
     // Verify the results of the setup
     REQUIRE_FALSE(compile_failed);\
@@ -137,7 +138,7 @@ SCENARIO("ai_domain_baset::ai_simplify_lhs",
       {
         REQUIRE(constant_array.operands().size()==i);
         constant_array.operands().push_back(
-          constant_exprt::integer_constant(i));
+          from_integer(i, signedbv_typet(32)));
       }
 
       const index_exprt &index_expr=
diff --git a/unit/miniBDD_new.cpp b/unit/miniBDD_new.cpp
new file mode 100644
index 00000000000..0c176c7f82e
--- /dev/null
+++ b/unit/miniBDD_new.cpp
@@ -0,0 +1,277 @@
+/*******************************************************************\
+
+ Module: Unit tests for miniBDD
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+/// \file
+/// Unit tests for miniBDD
+
+#include <catch.hpp>
+
+#include <solvers/miniBDD/miniBDD.h>
+#include <solvers/flattening/boolbv.h>
+
+#include <util/symbol_table.h>
+#include <util/arith_tools.h>
+#include <util/expanding_vector.h>
+
+#include <iostream>
+
+class bdd_propt:public propt
+{
+public:
+  mini_bdd_mgrt &mgr;
+
+  explicit bdd_propt(mini_bdd_mgrt &_mgr):mgr(_mgr)
+  {
+    // True and False
+    bdd_map.push_back(mgr.False());
+    bdd_map.push_back(mgr.True());
+  }
+
+  mini_bddt to_bdd(literalt a)
+  {
+    if(a.is_true())
+      return mgr.True();
+    if(a.is_false())
+      return mgr.False();
+    INVARIANT(a.var_no()<bdd_map.size(), "literal in map");
+    mini_bddt bdd=bdd_map[a.var_no()];
+    INVARIANT(bdd.is_initialized(), "initialized");
+    if(a.sign())
+      return !bdd;
+    else
+      return bdd;
+  }
+
+  literalt to_literal(const mini_bddt &bdd)
+  {
+    if(bdd.is_constant())
+      return const_literal(bdd.is_true());
+    std::size_t index=bdd.node_number();
+    bdd_map[index]=bdd;
+    return literalt(index, false);
+  }
+
+  literalt land(literalt a, literalt b) override
+  {
+    return to_literal(to_bdd(a) & to_bdd(b));
+  }
+
+  literalt lor(literalt a, literalt b) override
+  {
+    UNREACHABLE;
+  }
+
+  literalt land(const bvt &bv) override
+  {
+    mini_bddt result=mgr.True();
+
+    for(const auto &l : bv)
+      result=result&to_bdd(l);
+
+    return to_literal(result);
+  }
+
+  literalt lor(const bvt &bv) override
+  {
+    mini_bddt result=mgr.False();
+
+    for(const auto &l : bv)
+      result=result|to_bdd(l);
+
+    return to_literal(result);
+  }
+
+  literalt lxor(literalt a, literalt b) override
+  {
+    return to_literal(to_bdd(a) ^ to_bdd(b));
+  }
+
+  literalt lxor(const bvt &bv) override
+  {
+    UNREACHABLE;
+  }
+
+  literalt lnand(literalt a, literalt b) override
+  {
+    UNREACHABLE;
+  }
+
+  literalt lnor(literalt a, literalt b) override
+  {
+    UNREACHABLE;
+  }
+
+  literalt lequal(literalt a, literalt b) override
+  {
+    return to_literal(to_bdd(a)==to_bdd(b));
+  }
+
+  literalt limplies(literalt a, literalt b) override
+  {
+    UNREACHABLE;
+  }
+
+  literalt lselect(literalt a, literalt b, literalt c) override
+  {
+    UNREACHABLE;
+  }
+
+  void lcnf(const bvt &bv) override
+  {
+    UNREACHABLE;
+  }
+
+  literalt new_variable() override
+  {
+    return to_literal(mgr.Var(""));
+  }
+
+  size_t no_variables() const override
+  {
+    return bdd_map.size();
+  }
+
+  const std::string solver_text() override
+  {
+    return "BDDs";
+  }
+
+  resultt prop_solve() override
+  {
+    UNREACHABLE;
+  }
+
+  tvt l_get(literalt a) const override
+  {
+    UNREACHABLE;
+  }
+
+  expanding_vectort<mini_bddt> bdd_map;
+
+  bool has_set_to() const override { return false; }
+  bool cnf_handled_well() const override { return false; }
+};
+
+SCENARIO("miniBDD", "[core][solver][miniBDD]")
+{
+  GIVEN("A bdd for x&!x")
+  {
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    mini_bdd_mgrt bdd_mgr;
+    bdd_propt bdd_prop(bdd_mgr);
+    prop_conv_solvert solver(ns, bdd_prop);
+
+    symbol_exprt var("x", bool_typet());
+    literalt result=
+      solver.convert(and_exprt(var, not_exprt(var)));
+
+    REQUIRE(result.is_false());
+  }
+
+  GIVEN("A bdd for x&!x==0")
+  {
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    mini_bdd_mgrt bdd_mgr;
+    bdd_propt bdd_prop(bdd_mgr);
+    boolbvt boolbv(ns, bdd_prop);
+
+    unsignedbv_typet type(2);
+    symbol_exprt var("x", type);
+    equal_exprt equality(
+      bitand_exprt(var, bitnot_exprt(var)),
+      from_integer(0, type));
+
+    literalt result=
+      boolbv.convert(equality);
+
+    REQUIRE(result.is_true());
+  }
+
+  GIVEN("A bdd for x+x==1")
+  {
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    mini_bdd_mgrt bdd_mgr;
+    bdd_propt bdd_prop(bdd_mgr);
+    boolbvt boolbv(ns, bdd_prop);
+
+    unsignedbv_typet type(32);
+    symbol_exprt var("x", type);
+    equal_exprt equality(
+      plus_exprt(var, var),
+      from_integer(1, type));
+
+    literalt result=
+      boolbv.convert(equality);
+
+    REQUIRE(result.is_false());
+  }
+
+  GIVEN("A bdd for x*y==y*x")
+  {
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    mini_bdd_mgrt bdd_mgr;
+    bdd_propt bdd_prop(bdd_mgr);
+    boolbvt boolbv(ns, bdd_prop);
+
+    unsignedbv_typet type(4);
+    symbol_exprt var_x("x", type);
+    symbol_exprt var_y("y", type);
+    equal_exprt equality(
+      mult_exprt(var_x, var_y),
+      mult_exprt(var_y, var_x));
+
+    literalt result=
+      boolbv.convert(equality);
+
+    REQUIRE(result.is_true());
+  }
+
+  GIVEN("A bdd for x*x==2")
+  {
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    mini_bdd_mgrt bdd_mgr;
+    bdd_propt bdd_prop(bdd_mgr);
+    boolbvt boolbv(ns, bdd_prop);
+
+    unsignedbv_typet type(8);
+    symbol_exprt var_x("x", type);
+    equal_exprt equality(
+      mult_exprt(var_x, var_x),
+      from_integer(2, type));
+
+    literalt result=
+      boolbv.convert(equality);
+
+    REQUIRE(result.is_false());
+  }
+
+  GIVEN("A bdd for x*x==4")
+  {
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    mini_bdd_mgrt bdd_mgr;
+    bdd_propt bdd_prop(bdd_mgr);
+    boolbvt boolbv(ns, bdd_prop);
+
+    unsignedbv_typet type(8);
+    symbol_exprt var_x("x", type);
+    equal_exprt equality(
+      mult_exprt(var_x, var_x),
+      from_integer(4, type));
+
+    literalt result=
+      boolbv.convert(equality);
+
+    REQUIRE(!result.is_constant());
+  }
+}