diff --git a/.travis.yml b/.travis.yml index 2a0d5b00375..8c98d3e8e9b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -77,4 +77,8 @@ script: COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" && eval ${PRE_COMMAND} ${COMMAND} && COMMAND="make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" && + eval ${PRE_COMMAND} ${COMMAND} && + COMMAND="make -C src clean" && + eval ${PRE_COMMAND} ${COMMAND} && + COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O0 -ggdb3 -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DDEBUG\" -j2" && eval ${PRE_COMMAND} ${COMMAND} diff --git a/CHANGELOG b/CHANGELOG index 4052fe87941..0f15c3d5081 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,99 @@ +5.7 +=== + +* General: All tools now support the same set of --*-check options. +* General: Added --conversion-check to catch type casts that cause loss of + information. Previously --(un)signed-overflow-check would report these. +* CBMC: New option --symex-coverage-report to produce a Cobertura-compatible + statement- and branch coverage report. +* CBMC/Java: New options --java-max-vla-length, --java-unwind-enum-static, + --java-cp-include-files, --lazy-methods. +* GOTO-INSTRUMENT: Static loop unwinding via --unwind or via new options + --unwindset, --unwindset-file, --unwinding-assertions, --partial-loops, + --continue-as-loops, --log +* GOTO-INSTRUMENT: New option --slice-global-inits +* GOTO-INSTRUMENT: Inlining via --inline, --partial-inline, --function-inline, + --no-caching +* GOTO-INSTRUMENT: New options --remove-function-pointers, --model-argc-argv, + --show-threaded +* GOTO-CC: Additional drop-in replacement support for bcc, as, as86 +* GOTO-CC: GCC-style error/warning messages +* GOTO-CC: New options --native-compiler and --native-linker to select the + compiler/linker to be used when building combined native/goto object files. +* CBMC, SYMEX, GOTO-INSTRUMENT: New option --drop-unused-functions. Removed + ambiguous --show-reachable-properties. +* CBMC: New option --no-built-in-assertions + + +5.6 +=== + +Bugfixes in the C, C++, Java front-ends. + + +5.5 +=== + +This is a major release, with significant changes. The option +--all-properties is now the default; to restore the previous behaviour, +use --stop-on-fail. The primary area of attention was again the Java +front-end. We have furthermore added test-suite generation for branch +coverage, location coverage, condition coverage, decision coverage and +MC/DC. + + +5.4 +=== + +This is a minor release, focused primarily on maintenance. The primary +area of attention was again the Java front-end. We have also updated to +Minisat 2.2.1. + + +5.3 +=== + +This is a minor release, focused primarily on maintenance. The primary +area of attention is the Java front-end. + + +5.2 +=== + +This is a minor release, focused primarily on maintenance. The primary +areas of attention are the full slicer, the Java frontend, test suite +generation and support for the Glucose solver. + + +5.1 +=== + +This is a minor release, focused primarily on maintenance. Support for solving +floating-point problems using for SMT-LIB2 solvers without support for the +floating-point theory has been added. + + +5.0 +=== + +This is a major release, focused primarily on performance improvements. +Furthermore, the support for the floating-point theory for SMT-LIB2 has been +improved substantially. This release breaks compatibility with the goto-binary +format used by earlier releases; i.e., you will need to rebuild your +goto-binaries. + + +4.9 +=== + +This release is primarily for maintenance purposes and does not add any major +new features. The support for SMT-LIB2 solvers has been improved substantially. + + +4.8 +=== + + 4.7 === diff --git a/COMPILING b/COMPILING index 93fc65c2938..7cbdfcaab13 100644 --- a/COMPILING +++ b/COMPILING @@ -36,7 +36,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. On Red Hat/Fedora or derivates, do - yum install gcc gcc-c++ flex bison perl-libwww-perl patch + yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 Note that you need g++ version 5.2 or newer. @@ -44,10 +44,23 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. git clone https://github.com/diffblue/cbmc cbmc-git -2) Do +2) On Debian, do cd cbmc-git/src make minisat2-download + make CXX=g++-6 + + On Ubuntu, or other distributions with recent g++, do + + cd cbmc-git/src + make minisat2-download + make + + On Redhat/Fedora etc., do + + cd cbmc-git/src + make minisat2-download + scl enable devtoolset-6 bash make @@ -57,7 +70,7 @@ COMPILATION ON SOLARIS 11 1) As root, get the necessary development tools: pkg install system/header developer/lexer/flex developer/parser/bison developer/versioning/git - pkg install --accept developer/gcc-5 + pkg install --accept developer/gcc/gcc-c++-5 2) As a user, get the CBMC source via @@ -79,9 +92,6 @@ COMPILATION ON SOLARIS 11 export LD_LIBRARY_PATH=/usr/gcc/4.9/lib - Do not attempt to compile with gcc-45 that comes with Solaris 11. - It will mis-optimize MiniSat2. - COMPILATION ON FREEBSD 11 ------------------------- @@ -156,23 +166,21 @@ Follow these instructions: The patch removes the dependency on zlib and prevents a problem with a header file that is often unavailable on Windows. -2) Adjust src/config.inc for the paths to item 1). - -3A) To compile with Cygwin, install the mingw compilers, and adjust +2A) To compile with Cygwin, install the mingw compilers, and adjust the second line of config.inc to say BUILD_ENV = MinGW -3B) To compile with Visual Studio, make sure you have at least Visual +2B) To compile with Visual Studio, make sure you have at least Visual Studio version 12 (2013), and adjust the second line of config.inc to say BUILD_ENV = MSVC - Open the Visual Studio Command prompt, and then run the make.exe - from Cygwin from in there. + Open the Visual Studio Command prompt, and then bash.exe -login from + Cygwin from in there. + +3) Type cd src; make - that should do it. -4) Type cd src; make - that should do it. - Note that "nmake" is not expected to work. Use "make". (Optional) A Visual Studio project file can be generated with the script "generate_vcxproj" that is in the subdirectory "scripts". The project file diff --git a/doc/html-manual/cover.shtml b/doc/html-manual/cover.shtml index 45a3fb82143..5e3bfaffad8 100644 --- a/doc/html-manual/cover.shtml +++ b/doc/html-manual/cover.shtml @@ -149,7 +149,7 @@ To demonstrate the automatic test suite generation in CBMC, we call the following command and we are going to explain the command line options one by one.

-
cbmc pid.c --cover mcdc --unwind 6 --trace --xml-ui
+
cbmc pid.c --cover mcdc --unwind 6 --xml-ui
 

 
 

@@ -173,11 +173,11 @@ pprz >= (float)0 && pprz <= (float)(16 * 600)     id="climb_pid_run.coverage.3"
 
 

 The "id" of each coverage goal is automatically assigned by CBMC.  For every
-coverage goal, a trace (if there exists) of the program execution that
-satisfies such a goal is printed out in XML format, as the parameters
---trace --xml-ui are given.  Multiple coverage goals can share a
-trace, when the corresponding execution of the program satisfies all these
-goals at the same time.  Each trace corresponds to a test case. 
+coverage goal, a test suite (if there exists) that 
+satisfies such a goal is printed out in XML format, as the parameter
+--xml-ui is given.  Multiple coverage goals can share a
+test suite, when the corresponding execution of the program satisfies all these
+goals at the same time.  
 

 
 

@@ -185,6 +185,10 @@ In the end, the following test suites are automatically generated for testing th
 A test suite consists of a sequence of input parameters that are
 passed to the PID function climb_pid_run at each loop iteration. 
 For example, Test 1 covers the MC/DC goal with id="climb_pid_run.coverage.1".
+The complete output from CBMC is in
+pid_test_suites.xml, where every test suite and the coverage goals it is for
+are clearly described.
+
 
Test suite:
 Test 1. 
   (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
diff --git a/doc/html-manual/pid_test_suites.xml b/doc/html-manual/pid_test_suites.xml
new file mode 100644
index 00000000000..014fea12294
--- /dev/null
+++ b/doc/html-manual/pid_test_suites.xml
@@ -0,0 +1,500 @@
+
+
+CBMC 5.5
+
+  CBMC version 5.5 64-bit x86_64 macos
+
+
+
+  Parsing pid.c
+
+
+
+  Converting
+
+
+
+  Type-checking pid
+
+
+
+  
+  function `nondet_float' is not declared
+
+
+
+  Generating GOTO Program
+
+
+
+  Adding CPROVER library (x86_64)
+
+
+
+  Removal of function pointers and virtual functions
+
+
+
+  Partial Inlining
+
+
+
+  Generic Property Instrumentation
+
+
+criterion: mcdc
+
+
+  Instrumenting coverage goals
+
+
+
+  Starting Bounded Model Checking
+
+
+
+  Unwinding loop main.0 iteration 1 (6 max) file pid.c line 56 function main thread 0
+
+
+
+  Unwinding loop main.0 iteration 2 (6 max) file pid.c line 56 function main thread 0
+
+
+
+  Unwinding loop main.0 iteration 3 (6 max) file pid.c line 56 function main thread 0
+
+
+
+  Unwinding loop main.0 iteration 4 (6 max) file pid.c line 56 function main thread 0
+
+
+
+  Unwinding loop main.0 iteration 5 (6 max) file pid.c line 56 function main thread 0
+
+
+
+  Not unwinding loop main.0 iteration 6 (6 max) file pid.c line 56 function main thread 0
+
+
+
+  size of program expression: 416 steps
+
+
+
+  Generated 114 VCC(s), 108 remaining after simplification
+
+
+
+  Passing problem to propositional reduction
+
+
+
+  converting SSA
+
+
+
+  Aiming to cover 19 goal(s)
+
+
+
+  Running propositional reduction
+
+
+
+  Post-processing
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 553801 clauses
+
+
+
+  SAT checker: instance is SATISFIABLE
+
+
+
+  Covered decision/condition `1 != 0' true
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 395675 clauses
+
+
+
+  SAT checker: instance is SATISFIABLE
+
+
+
+  Covered MC/DC independence condition `!(pprz >= (float)0) && pprz <= (float)(16 * 600)'
+
+
+
+  Covered decision `pprz >= (float)0 && pprz <= (float)(16 * 600)' false
+
+
+
+  Covered condition `pprz >= (float)0' false
+
+
+
+  Covered decision/condition `pprz > (float)(16 * 600)' false
+
+
+
+  Covered condition `pprz <= (float)(16 * 600)' true
+
+
+
+  Covered decision/condition `desired_climb > (float)0' false
+
+
+
+  Covered decision/condition `climb_sum_err > (float)10' false
+
+
+
+  Covered decision/condition `climb_sum_err < (float)-10' false
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 393279 clauses
+
+
+
+  SAT checker: instance is SATISFIABLE
+
+
+
+  Covered MC/DC independence condition `pprz >= (float)0 && !(pprz <= (float)(16 * 600))'
+
+
+
+  Covered condition `pprz >= (float)0' true
+
+
+
+  Covered decision/condition `pprz > (float)(16 * 600)' true
+
+
+
+  Covered condition `pprz <= (float)(16 * 600)' false
+
+
+
+  Covered decision/condition `desired_climb > (float)0' true
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 391285 clauses
+
+
+
+  SAT checker: instance is SATISFIABLE
+
+
+
+  Covered MC/DC independence condition `pprz >= (float)0 && pprz <= (float)(16 * 600)'
+
+
+
+  Covered decision `pprz >= (float)0 && pprz <= (float)(16 * 600)' true
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 390122 clauses
+
+
+
+  SAT checker: instance is SATISFIABLE
+
+
+
+  Covered decision/condition `climb_sum_err < (float)-10' true
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 390121 clauses
+
+
+
+  SAT checker: instance is SATISFIABLE
+
+
+
+  Covered decision/condition `climb_sum_err > (float)10' true
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 387493 clauses
+
+
+
+  SAT checker inconsistent: instance is UNSATISFIABLE
+
+
+
+  Runtime decision procedure: 3.806s
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+  
+
+
+
+  
+    
+      -1.000000
+    
+    
+      1.000000
+    
+  
+  
+  
+  
+  
+  
+  
+  
+  
+
+
+
+  
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+  
+  
+  
+  
+  
+  
+
+
+
+  
+    
+      0.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+  
+  
+  
+
+
+
+  
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      0.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+  
+  
+
+
+
+  
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+  
+  
+
+
+
+  ** 18 of 19 covered (94.7%)
+
+
+
+  ** Used 7 iterations
+
+
+
diff --git a/regression/ansi-c/function_return1/test.desc b/regression/ansi-c/function_return1/test.desc
index 78396740555..f49480a607f 100644
--- a/regression/ansi-c/function_return1/test.desc
+++ b/regression/ansi-c/function_return1/test.desc
@@ -3,7 +3,6 @@ main.c
 --verbosity 2
 ^main.c:3:1: warning: function has return void but a return statement returning signed int$
 ^SIGNAL=0$
-
 --
 ^warning: ignoring
 ^CONVERSION ERROR$
diff --git a/regression/ansi-c/static_inline1/main.c b/regression/ansi-c/static_inline1/main.c
new file mode 100644
index 00000000000..ba8e8c6fb6b
--- /dev/null
+++ b/regression/ansi-c/static_inline1/main.c
@@ -0,0 +1,11 @@
+inline static int fun(int a)
+{
+    return a+1;
+}
+
+int main(int argc, char *argv[])
+{
+    fun(5);
+    return 0;
+}
+
diff --git a/regression/ansi-c/static_inline1/test.desc b/regression/ansi-c/static_inline1/test.desc
new file mode 100644
index 00000000000..5717777037a
--- /dev/null
+++ b/regression/ansi-c/static_inline1/test.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+
+--
+^warning: ignoring
diff --git a/regression/ansi-c/static_inline2/main.c b/regression/ansi-c/static_inline2/main.c
new file mode 100644
index 00000000000..c67e498b4f5
--- /dev/null
+++ b/regression/ansi-c/static_inline2/main.c
@@ -0,0 +1,4 @@
+inline static int fun(int a)
+{
+    return a+1;
+}
diff --git a/regression/ansi-c/static_inline2/test.desc b/regression/ansi-c/static_inline2/test.desc
new file mode 100644
index 00000000000..c5c5692745d
--- /dev/null
+++ b/regression/ansi-c/static_inline2/test.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+--function fun
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+
+--
+^warning: ignoring
diff --git a/regression/cbmc-concurrency/trace1/main.c b/regression/cbmc-concurrency/trace1/main.c
new file mode 100644
index 00000000000..7e1d3749edd
--- /dev/null
+++ b/regression/cbmc-concurrency/trace1/main.c
@@ -0,0 +1,28 @@
+// #include 
+#include 
+
+volatile unsigned x = 0, y = 0;
+volatile unsigned r1 = 0, r2 = 0;
+
+void* thr1(void* arg) {
+  x = 1;
+  r1 = y + 1;
+  return 0;
+}
+
+void* thr2(void* arg) {
+  y = 1;
+  r2 = x + 1;
+  return 0;
+}
+
+int main(){
+  // pthread_t t1, t2;
+  // pthread_create(&t1, NULL, thr1, NULL);
+  // pthread_create(&t2, NULL, thr2, NULL);
+__CPROVER_ASYNC_1: thr1(0);
+__CPROVER_ASYNC_2: thr2(0);
+  assert(r1 != 1 || r2 != 1);
+  return 0;
+}
+
diff --git a/regression/cbmc-concurrency/trace1/test.desc b/regression/cbmc-concurrency/trace1/test.desc
new file mode 100644
index 00000000000..a6f904e7a86
--- /dev/null
+++ b/regression/cbmc-concurrency/trace1/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--mm tso --trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^[[:space:]]*r2=1u \(.*\)$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/multinewarray/multinewarray.class b/regression/cbmc-java/multinewarray/multinewarray.class
index 09cb7711192..6895eaa962b 100644
Binary files a/regression/cbmc-java/multinewarray/multinewarray.class and b/regression/cbmc-java/multinewarray/multinewarray.class differ
diff --git a/regression/cbmc-java/multinewarray/multinewarray.java b/regression/cbmc-java/multinewarray/multinewarray.java
index ce3219586e4..62df1740671 100644
--- a/regression/cbmc-java/multinewarray/multinewarray.java
+++ b/regression/cbmc-java/multinewarray/multinewarray.java
@@ -12,8 +12,8 @@ public static void main(String[] args)
     assert some_a[0].length==3;
     assert some_a[0][0].length==2;
   
-    int x=10;
-    int y=20;
+    int x=3;
+    int y=5;
     int[][] int_array = new int[x][y];
     
     for(int i=0; i
+
 int main()
 {
   int N;
diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc
index 5b4797b9b00..555f7b0e61f 100644
--- a/regression/cbmc/Quantifiers-assertion/test.desc
+++ b/regression/cbmc/Quantifiers-assertion/test.desc
@@ -8,6 +8,5 @@ main.c
 ^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$
 ^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
 ^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
-
 ^\*\* 2 of 6 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
index cfc835ce948..289e8a47efc 100644
--- a/regression/cbmc/Quantifiers-assignment/test.desc
+++ b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -6,6 +6,5 @@ main.c
 ^\[main.assertion.2\] assertion y: FAILURE$
 ^\[main.assertion.3\] assertion z1: SUCCESS$
 ^\[main.assertion.4\] assertion z2: SUCCESS$
-
 ^\*\* 1 of 4 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-copy/test.desc b/regression/cbmc/Quantifiers-copy/test.desc
index 5682d588b9c..993061a5b3a 100644
--- a/regression/cbmc/Quantifiers-copy/test.desc
+++ b/regression/cbmc/Quantifiers-copy/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion b\[.*\] == 2: SUCCESS$
 ^\[main.assertion.4\] assertion b\[.*\] == 3: SUCCESS$
 ^\[main.assertion.5\] assertion b\[.*\] == 4: SUCCESS$
-
 ^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc
index e121e2e1955..be4945b25ef 100644
--- a/regression/cbmc/Quantifiers-if/test.desc
+++ b/regression/cbmc/Quantifiers-if/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] success 1: SUCCESS$
 ^\[main.assertion.4\] failure 3: FAILURE$
 ^\[main.assertion.5\] success 2: SUCCESS$
-
 ^\*\* 3 of 5 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-initialisation/test.desc b/regression/cbmc/Quantifiers-initialisation/test.desc
index b10b600c308..d0e4c279e1f 100644
--- a/regression/cbmc/Quantifiers-initialisation/test.desc
+++ b/regression/cbmc/Quantifiers-initialisation/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\] == 3: SUCCESS$
 ^\[main.assertion.4\] assertion a\[.*\] == 4: SUCCESS$
 ^\[main.assertion.5\] assertion a\[.*\] == 5: SUCCESS$
-
 ^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc
index ad5913e4d92..0f309d9332d 100644
--- a/regression/cbmc/Quantifiers-initialisation2/test.desc
+++ b/regression/cbmc/Quantifiers-initialisation2/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\] > a\[.*\]: FAILURE$
 ^\[main.assertion.4\] forall c\[\]: SUCCESS$
 ^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
-
 ^\*\* 1 of 5 failed \(2 iterations\)$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
index e38af4ddbdb..a3e1bce313f 100644
--- a/regression/cbmc/Quantifiers-invalid-var-range/test.desc
+++ b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
@@ -2,6 +2,5 @@ CORE
 main.c
 
 ^\*\* Results:$
-
 ^\*\* 0 of 1 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc
index 51feeae3b08..630e54eb224 100644
--- a/regression/cbmc/Quantifiers-not-exists/test.desc
+++ b/regression/cbmc/Quantifiers-not-exists/test.desc
@@ -8,6 +8,5 @@ main.c
 ^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$
 ^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$
 ^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$
-
 ^\*\* 0 of 6 failed \(1 iteration\)$
 ^\VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc
index b1b6a0d1d60..2e862045758 100644
--- a/regression/cbmc/Quantifiers-not/test.desc
+++ b/regression/cbmc/Quantifiers-not/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] failure 1: FAILURE$
 ^\[main.assertion.4\] success 3: SUCCESS$
 ^\[main.assertion.5\] failure 2: FAILURE$
-
 ^\*\* 2 of 5 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc
index 2874b9dc0eb..b8501be880e 100644
--- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc
+++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$
 ^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$
-
 ^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc
index 3bc8a8d2a5f..b0b25cc9903 100644
--- a/regression/cbmc/Quantifiers-type/test.desc
+++ b/regression/cbmc/Quantifiers-type/test.desc
@@ -4,6 +4,5 @@ main.c
 ^\*\* Results:$
 ^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
 ^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
-
 ^\*\* 1 of 2 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc
index 9e7f5b42724..bfd4cf4f3f4 100644
--- a/regression/cbmc/graphml_witness1/test.desc
+++ b/regression/cbmc/graphml_witness1/test.desc
@@ -46,29 +46,29 @@ main.c
   
     C
     
-    
+    
       true
     
     
       main.c
       21
     
-    
-    
+    
+    
       main.c
       29
       main
     
-    
-    
+    
+    
       main.c
       15
       remove_one
     
-    
+    
       true
     
-    
+    
       main.c
       31
     
diff --git a/regression/goto-analyzer/Makefile b/regression/goto-analyzer/Makefile
index 5701431a37e..2630bf17097 100644
--- a/regression/goto-analyzer/Makefile
+++ b/regression/goto-analyzer/Makefile
@@ -1,10 +1,16 @@
 default: tests.log
 
 test:
-	@../test.pl -c ../../../src/goto-analyzer/goto-analyzer
+	@if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 tests.log: ../test.pl
-	@../test.pl -c ../../../src/goto-analyzer/goto-analyzer
+	@if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 show:
 	@for dir in *; do \
diff --git a/regression/goto-instrument/slice01/test.desc b/regression/goto-instrument/slice01/test.desc
index 76cbcfa81bd..73b1ad786c4 100644
--- a/regression/goto-instrument/slice01/test.desc
+++ b/regression/goto-instrument/slice01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---unwind 2 --full-slice
+--unwind 2 --full-slice --add-library
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/goto-instrument/slice13/main.c b/regression/goto-instrument/slice13/main.c
index 3354961512a..a24498017a7 100644
--- a/regression/goto-instrument/slice13/main.c
+++ b/regression/goto-instrument/slice13/main.c
@@ -17,7 +17,9 @@ void test (int mode, double d, float result) {
 
 int main (void)
 {
+#ifdef __GNUC__
   // Nearer to 0x1.fffffep+127 than to 0x1.000000p+128
   test(FE_UPWARD, 0x1.fffffe0000001p+127, +INFINITY);
+#endif
   return 1;
 }
diff --git a/regression/goto-instrument/slice13/test.desc b/regression/goto-instrument/slice13/test.desc
index cc8dd41ed5f..50181efa86b 100644
--- a/regression/goto-instrument/slice13/test.desc
+++ b/regression/goto-instrument/slice13/test.desc
@@ -1,8 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---floatbv --full-slice
+--full-slice --add-library
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/goto-instrument/slice16/test.desc b/regression/goto-instrument/slice16/test.desc
index 846baaf2a8b..ab6fd2dd827 100644
--- a/regression/goto-instrument/slice16/test.desc
+++ b/regression/goto-instrument/slice16/test.desc
@@ -1,8 +1,6 @@
-KNOWNBUG
+CORE
 main.c
 --full-slice --unwind 2
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/goto-instrument/slice22/main.c b/regression/goto-instrument/slice22/main.c
new file mode 100644
index 00000000000..bac167b63d3
--- /dev/null
+++ b/regression/goto-instrument/slice22/main.c
@@ -0,0 +1,19 @@
+#include 
+#include 
+
+int main()
+{
+  int *ptr=malloc(sizeof(int));
+  *ptr=42;
+  ptr=realloc(ptr, 20);
+  assert(*ptr==42);
+
+  int *ptr2=malloc(2*sizeof(int));
+  *ptr2=42;
+  *(ptr2+1)=42;
+  ptr2=realloc(ptr2, 20);
+  assert(*ptr2==42);
+  assert(*(ptr2+1)==42);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice22/test.desc b/regression/goto-instrument/slice22/test.desc
new file mode 100644
index 00000000000..50181efa86b
--- /dev/null
+++ b/regression/goto-instrument/slice22/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/goto-instrument/slice23/main.c b/regression/goto-instrument/slice23/main.c
new file mode 100644
index 00000000000..d165e2c38b8
--- /dev/null
+++ b/regression/goto-instrument/slice23/main.c
@@ -0,0 +1,25 @@
+#include 
+#include 
+
+void foo(int argc)
+{
+  void* x=0;
+
+  if(argc>3)
+    x=malloc(4*sizeof(int));
+  else
+    x=malloc(3*sizeof(int));
+  *(int*)x=42;
+
+  x=realloc(x, sizeof(int));
+
+  assert(*(int*)x==42);
+}
+
+int main(int argc, char* argv[])
+{
+//__CPROVER_ASYNC_1:
+  foo(argc);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice23/test.desc b/regression/goto-instrument/slice23/test.desc
new file mode 100644
index 00000000000..50181efa86b
--- /dev/null
+++ b/regression/goto-instrument/slice23/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/test-script/excluded-line/program.c b/regression/test-script/excluded-line/program.c
deleted file mode 100755
index 882fedcc2fd..00000000000
--- a/regression/test-script/excluded-line/program.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include 
-
-int main(void) {
-  printf("Hello\n");
-  printf("World\n");
-  return 0;
-}
diff --git a/regression/test-script/excluded-line/test.desc b/regression/test-script/excluded-line/test.desc
index 2384efe0828..7fa478ad232 100644
--- a/regression/test-script/excluded-line/test.desc
+++ b/regression/test-script/excluded-line/test.desc
@@ -1,5 +1,5 @@
 CORE
-program.c
+test.txt
 
 ^Hello$
 --
diff --git a/regression/test-script/excluded-line/test.txt b/regression/test-script/excluded-line/test.txt
new file mode 100755
index 00000000000..0ac4c9a8b57
--- /dev/null
+++ b/regression/test-script/excluded-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/failing-excluded-line/program.c b/regression/test-script/failing-excluded-line/program.c
deleted file mode 100755
index 882fedcc2fd..00000000000
--- a/regression/test-script/failing-excluded-line/program.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include 
-
-int main(void) {
-  printf("Hello\n");
-  printf("World\n");
-  return 0;
-}
diff --git a/regression/test-script/failing-excluded-line/test.desc b/regression/test-script/failing-excluded-line/test.desc
index 36668db5a5f..3c8b8bc9f72 100644
--- a/regression/test-script/failing-excluded-line/test.desc
+++ b/regression/test-script/failing-excluded-line/test.desc
@@ -1,5 +1,5 @@
 KNOWNBUG
-program.c
+test.txt
 
 ^Hello$
 --
diff --git a/regression/test-script/failing-excluded-line/test.txt b/regression/test-script/failing-excluded-line/test.txt
new file mode 100755
index 00000000000..0ac4c9a8b57
--- /dev/null
+++ b/regression/test-script/failing-excluded-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/failing-multi-line/program.c b/regression/test-script/failing-multi-line/program.c
deleted file mode 100755
index 882fedcc2fd..00000000000
--- a/regression/test-script/failing-multi-line/program.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include 
-
-int main(void) {
-  printf("Hello\n");
-  printf("World\n");
-  return 0;
-}
diff --git a/regression/test-script/failing-multi-line/test.desc b/regression/test-script/failing-multi-line/test.desc
index cf4fcf3034b..b3b2f171842 100644
--- a/regression/test-script/failing-multi-line/test.desc
+++ b/regression/test-script/failing-multi-line/test.desc
@@ -1,5 +1,5 @@
 KNOWNBUG
-program.c
+test.txt
 
 activate-multi-line-match
 Hello\nAnother\nWorld
diff --git a/regression/test-script/failing-multi-line/test.txt b/regression/test-script/failing-multi-line/test.txt
new file mode 100755
index 00000000000..0ac4c9a8b57
--- /dev/null
+++ b/regression/test-script/failing-multi-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/failing-single-line/program.c b/regression/test-script/failing-single-line/program.c
deleted file mode 100755
index 882fedcc2fd..00000000000
--- a/regression/test-script/failing-single-line/program.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include 
-
-int main(void) {
-  printf("Hello\n");
-  printf("World\n");
-  return 0;
-}
diff --git a/regression/test-script/failing-single-line/test.desc b/regression/test-script/failing-single-line/test.desc
index 604682ecbdb..973b5aa464b 100644
--- a/regression/test-script/failing-single-line/test.desc
+++ b/regression/test-script/failing-single-line/test.desc
@@ -1,5 +1,5 @@
 KNOWNBUG
-program.c
+test.txt
 
 ^Goodbye$
 --
diff --git a/regression/test-script/failing-single-line/test.txt b/regression/test-script/failing-single-line/test.txt
new file mode 100755
index 00000000000..0ac4c9a8b57
--- /dev/null
+++ b/regression/test-script/failing-single-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/multi-line/program.c b/regression/test-script/multi-line/program.c
deleted file mode 100755
index 882fedcc2fd..00000000000
--- a/regression/test-script/multi-line/program.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include 
-
-int main(void) {
-  printf("Hello\n");
-  printf("World\n");
-  return 0;
-}
diff --git a/regression/test-script/multi-line/test.desc b/regression/test-script/multi-line/test.desc
index cf9bb072880..2ef644c2082 100644
--- a/regression/test-script/multi-line/test.desc
+++ b/regression/test-script/multi-line/test.desc
@@ -1,5 +1,5 @@
 CORE
-program.c
+test.txt
 
 activate-multi-line-match
 Hello\nWorld
diff --git a/regression/test-script/multi-line/test.txt b/regression/test-script/multi-line/test.txt
new file mode 100755
index 00000000000..0ac4c9a8b57
--- /dev/null
+++ b/regression/test-script/multi-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/program_runner.sh b/regression/test-script/program_runner.sh
index 8e09b75f0ab..851f1716b12 100755
--- a/regression/test-script/program_runner.sh
+++ b/regression/test-script/program_runner.sh
@@ -2,5 +2,4 @@
 
 set -e
 
-gcc $1 -o a.out
-./a.out
+cat $1
diff --git a/regression/test-script/single-line-windows-line-ends/test.desc b/regression/test-script/single-line-windows-line-ends/test.desc
new file mode 100644
index 00000000000..d7c83bd851e
--- /dev/null
+++ b/regression/test-script/single-line-windows-line-ends/test.desc
@@ -0,0 +1,5 @@
+CORE
+test.txt
+
+^Hello$
+--
diff --git a/regression/test-script/single-line-windows-line-ends/test.txt b/regression/test-script/single-line-windows-line-ends/test.txt
new file mode 100755
index 00000000000..7c9ae46963c
--- /dev/null
+++ b/regression/test-script/single-line-windows-line-ends/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/single-line/program.c b/regression/test-script/single-line/program.c
deleted file mode 100755
index 882fedcc2fd..00000000000
--- a/regression/test-script/single-line/program.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include 
-
-int main(void) {
-  printf("Hello\n");
-  printf("World\n");
-  return 0;
-}
diff --git a/regression/test-script/single-line/test.desc b/regression/test-script/single-line/test.desc
index 2507fd6a412..d7c83bd851e 100644
--- a/regression/test-script/single-line/test.desc
+++ b/regression/test-script/single-line/test.desc
@@ -1,5 +1,5 @@
 CORE
-program.c
+test.txt
 
 ^Hello$
 --
diff --git a/regression/test-script/single-line/test.txt b/regression/test-script/single-line/test.txt
new file mode 100755
index 00000000000..0ac4c9a8b57
--- /dev/null
+++ b/regression/test-script/single-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test.pl b/regression/test.pl
index a2ac088d0e0..d27c663b0aa 100755
--- a/regression/test.pl
+++ b/regression/test.pl
@@ -73,7 +73,7 @@ ($$$$$)
   $options =~ s/$ign//g if(defined($ign));
 
   my $output = $input;
-  $output =~ s/\.(c|i|gb|cpp|ii|xml|class|jar)$/.out/;
+  $output =~ s/\.[^.]*$/.out/;
 
   if($output eq $input) {
     print("Error in test file -- $test\n");
@@ -125,6 +125,7 @@ ($$$$$)
             local $/ = undef;
             binmode $fh;
             my $whole_file = <$fh>;
+            $whole_file =~ s/\r\n/\n/g;
             my $is_match = $whole_file =~ /$result/;
             $r = ($included ? !$is_match : $is_match);
           }
@@ -132,6 +133,7 @@ ($$$$$)
           {
             my $found_line = 0;
             while(my $line = <$fh>) {
+              $line =~ s/\r$//;
               if($line =~ /$result/) {
                 # We've found the line, therefore if it is included we set
                 # the result to 0 (OK) If it is excluded, we set the result
diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h
index 1a4d6090f47..930d0ae69b9 100644
--- a/src/analyses/cfg_dominators.h
+++ b/src/analyses/cfg_dominators.h
@@ -224,6 +224,13 @@ void dominators_pretty_print_node(const T &node, std::ostream &out)
   out << node;
 }
 
+inline void dominators_pretty_print_node(
+  const goto_programt::targett& target,
+  std::ostream& out)
+{
+  out << target->code.pretty();
+}
+
 /*******************************************************************\
 
 Function: cfg_dominators_templatet::output
@@ -241,7 +248,7 @@ void cfg_dominators_templatet::output(std::ostream &out) const
 {
   for(const auto &node : cfg.entry_map)
   {
-    T n=node.first;
+    auto n=node.first;
 
     dominators_pretty_print_node(n, out);
     if(post_dom)
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 1fe89a7b8f6..189048994b8 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -6,8 +6,6 @@ Author: Peter Schrammel
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 4494aa33e76..7bba83bd298 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -55,6 +55,7 @@ class goto_checkt
     retain_trivial=_options.get_bool_option("retain-trivial");
     enable_assert_to_assume=_options.get_bool_option("assert-to-assume");
     enable_assertions=_options.get_bool_option("assertions");
+    enable_built_in_assertions=_options.get_bool_option("built-in-assertions");
     enable_assumptions=_options.get_bool_option("assumptions");
     error_labels=_options.get_list_option("error-label");
   }
@@ -125,6 +126,7 @@ class goto_checkt
   bool retain_trivial;
   bool enable_assert_to_assume;
   bool enable_assertions;
+  bool enable_built_in_assertions;
   bool enable_assumptions;
 
   typedef optionst::value_listt error_labelst;
@@ -1730,9 +1732,10 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
     }
     else if(i.is_assert())
     {
-      if(i.source_location.get_bool("user-provided") &&
-         i.source_location.get_property_class()!="error label" &&
-         !enable_assertions)
+      bool is_user_provided=i.source_location.get_bool("user-provided");
+      if((is_user_provided && !enable_assertions &&
+          i.source_location.get_property_class()!="error label") ||
+         (!is_user_provided && !enable_built_in_assertions))
         i.type=SKIP;
     }
     else if(i.is_assume())
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index 43cb5c1d360..3fc0d10bb09 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -253,7 +253,9 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
   {
     if(rhs.operands().size()>=3)
     {
-      return get_rec(make_binary(rhs), loc_info_src);
+      assert(rhs.op0().type().id()==ID_pointer);
+      return get_rec(rhs.op0(), loc_info_src) |
+             flagst::mk_uses_offset();
     }
     else if(rhs.operands().size()==2)
     {
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index 53d089b9544..ffaefe73667 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include 
 #include 
 #include 
-#include 
 
 #include 
 #include 
@@ -309,7 +308,8 @@ void local_may_aliast::get_rec(
   {
     if(rhs.operands().size()>=3)
     {
-      get_rec(dest, make_binary(rhs), loc_info_src);
+      assert(rhs.op0().type().id()==ID_pointer);
+      get_rec(dest, rhs.op0(), loc_info_src);
     }
     else if(rhs.operands().size()==2)
     {
diff --git a/src/analyses/natural_loops.cpp b/src/analyses/natural_loops.cpp
index 16985daa5e9..593fc78006d 100644
--- a/src/analyses/natural_loops.cpp
+++ b/src/analyses/natural_loops.cpp
@@ -10,8 +10,6 @@ Author: Georg Weissenbacher, georg@weissenbacher.name
 
 #include "natural_loops.h"
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: show_natural_loops
diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h
index 327ebbdf112..ff56c687c93 100644
--- a/src/analyses/natural_loops.h
+++ b/src/analyses/natural_loops.h
@@ -81,8 +81,6 @@ Function: natural_loops_templatet::compute
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index 2ef4a549040..a48a271a9a6 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -160,7 +160,7 @@ class rd_range_domaint:public ai_domain_baset
   typedef std::map ranges_at_loct;
 
   const ranges_at_loct &get(const irep_idt &identifier) const;
-  const void clear_cache(const irep_idt &identifier) const
+  void clear_cache(const irep_idt &identifier) const
   {
     export_cache[identifier].clear();
   }
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 5b26d02ce64..356aeded154 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -3331,7 +3331,7 @@ std::string expr2ct::convert_code_return(
   std::string dest=indent_str(indent);
   dest+="return";
 
-  if(src.operands().size()==1)
+  if(to_code_return(src).has_return_value())
     dest+=" "+convert(src.op0());
 
   dest+=';';
diff --git a/src/big-int/bigint-test.cc b/src/big-int/bigint-test.cc
index 6c8b9c84b64..5d506a89013 100644
--- a/src/big-int/bigint-test.cc
+++ b/src/big-int/bigint-test.cc
@@ -298,7 +298,7 @@ run_floorPow2_tests ()
 
   for (unsigned i = 0; i < 512; ++i) {
     unsigned x = 512 - i;
-    N = pow(2,x);
+    N = pow(BigInt(2),x);
     M.setPower2(x);
 
     if (!(N == M)) {
@@ -327,7 +327,7 @@ run_floorPow2_tests ()
 
   }
 
-  N = pow(2,0);  // 1
+  N = pow(BigInt(2),0);  // 1
   M.setPower2(0);
 
   if (!(N == M)) {
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 2f39d97b1ce..f1e005a46a1 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -687,7 +687,7 @@ void bmct::setup_unwind()
 
   for(auto &val : unwindset_loops)
   {
-    unsigned thread_nr;
+    unsigned thread_nr=0;
     bool thread_nr_set=false;
 
     if(!val.empty() &&
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 865e34edfad..60c0f706c62 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -240,6 +240,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   else
     options.set_option("assertions", true);
 
+  // check built-in assertions
+  if(cmdline.isset("no-built-in-assertions"))
+    options.set_option("built-in-assertions", false);
+  else
+    options.set_option("built-in-assertions", true);
+
   // use assumptions
   if(cmdline.isset("no-assumptions"))
     options.set_option("assumptions", false);
@@ -543,19 +549,6 @@ int cbmc_parse_optionst::doit()
     return 0; // should contemplate EX_OK from sysexits.h
   }
 
-  // may replace --show-properties
-  if(cmdline.isset("show-reachable-properties"))
-  {
-    const namespacet ns(symbol_table);
-
-    // Entry point will have been set before and function pointers removed
-    status() << "Removing Unused Functions" << eom;
-    remove_unused_functions(goto_functions, ui_message_handler);
-
-    show_properties(ns, get_ui(), goto_functions);
-    return 0; // should contemplate EX_OK from sysexits.h
-  }
-
   if(set_properties(goto_functions))
     return 7; // should contemplate EX_USAGE from sysexits.h
 
@@ -882,8 +875,6 @@ bool cbmc_parse_optionst::process_goto_program(
     remove_asm(symbol_table, goto_functions);
 
     // add the library
-    status() << "Adding CPROVER library ("
-             << config.ansi_c.arch << ")" << eom;
     link_to_library(symbol_table, goto_functions, ui_message_handler);
 
     if(cmdline.isset("string-abstraction"))
@@ -955,8 +946,14 @@ bool cbmc_parse_optionst::process_goto_program(
     // add loop ids
     goto_functions.compute_loop_numbers();
 
-    // instrument cover goals
+    if(cmdline.isset("drop-unused-functions"))
+    {
+      // Entry point will have been set before and function pointers removed
+      status() << "Removing unused functions" << eom;
+      remove_unused_functions(goto_functions, ui_message_handler);
+    }
 
+    // instrument cover goals
     if(cmdline.isset("cover"))
     {
       std::list criteria_strings=
@@ -1147,10 +1144,12 @@ void cbmc_parse_optionst::help()
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
+    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
     " --no-assertions              ignore user assertions\n"
+    " --no-built-in-assertions     ignore assertions in built-in library\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"
     " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
@@ -1203,5 +1202,6 @@ void cbmc_parse_optionst::help()
     " --xml-ui                     use XML-formatted output\n"
     " --xml-interface              bi-directional XML interface\n"
     " --json-ui                    use JSON-formatted output\n"
+    " --verbosity #                verbosity level\n"
     "\n";
 }
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index a3fc5e7e7d3..db987d3c304 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -32,6 +32,7 @@ class optionst;
   "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
+  "(no-built-in-assertions)" \
   "(xml-ui)(xml-interface)(json-ui)" \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
   "(no-sat-preprocessor)" \
@@ -41,7 +42,8 @@ class optionst;
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-loops)" \
   "(show-symbol-table)(show-parse-tree)(show-vcc)" \
-  "(show-claims)(claim):(show-properties)(show-reachable-properties)" \
+  "(show-claims)(claim):(show-properties)" \
+  "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \
   "(nondet-static)" \
diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp
index 8f64f9900a8..69af02e9e9e 100644
--- a/src/cbmc/symex_coverage.cpp
+++ b/src/cbmc/symex_coverage.cpp
@@ -318,7 +318,7 @@ void symex_coveraget::compute_overall_coverage(
       it!=file_records.end();
       ++it)
   {
-    if(has_prefix(id2string(it->first), "first)))
       continue;
 
     const coverage_recordt &f_cov=it->second;
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index 4ac42666639..803ab9db5b1 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -368,7 +368,6 @@ bool clobber_parse_optionst::get_goto_program(
 
     // finally add the library
     #if 0
-    status() << "Adding CPROVER library" << eom;
     link_to_library(symbol_table, goto_functions, ui_message_handler);
     #endif
 
diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h
index 9c26ebbe16f..55955cd0334 100644
--- a/src/cpp/cpp_typecheck.h
+++ b/src/cpp/cpp_typecheck.h
@@ -136,13 +136,6 @@ class cpp_typecheckt:public c_typecheck_baset
     const template_typet &old_type,
     template_typet &new_type);
 
-  #if 0
-  void check_template_restrictions(
-    const irept &cpp_name,
-    const irep_idt &final_identifier,
-    const typet &final_type);
-  #endif
-
   void convert_template_declaration(cpp_declarationt &declaration);
 
   void convert_non_template_declaration(cpp_declarationt &declaration);
diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp
index 002cdb51f69..79c609a0a4b 100644
--- a/src/cpp/cpp_typecheck_template.cpp
+++ b/src/cpp/cpp_typecheck_template.cpp
@@ -48,41 +48,6 @@ void cpp_typecheckt::salvage_default_arguments(
   }
 }
 
-#if 0
-/*******************************************************************\
-
-Function: cpp_typecheckt::check_template_restrictions
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void cpp_typecheckt::check_template_restrictions(
-  const irept &cpp_name,
-  const irep_idt &final_identifier,
-  const typet &final_type)
-{
-  if(final_type.id()==ID_template)
-  {
-    // subtype must be class or function
-
-    if(final_type.subtype().id()!=ID_struct &&
-       final_type.subtype().id()!=ID_code)
-    {
-      error().source_location=cpp_name.location();
-      error() << "template only allowed with classes or functions,"
-              << " but got `" << to_string(final_type.subtype())
-              << "'" << eom;
-      throw 0;
-    }
-  }
-}
-#endif
-
 /*******************************************************************\
 
 Function: cpp_typecheckt::typecheck_class_template
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index 5a7d2095a58..b16340c3eef 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -21,8 +21,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "cpp_member_spec.h"
 #include "cpp_enum_type.h"
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 
@@ -642,7 +640,7 @@ bool Parser::rDefinition(cpp_itemt &item)
   #ifdef DEBUG
   indenter _i;
   std::cout << std::string(__indent, ' ') << "Parser::rDefinition 1 " << t
-            << "\n";
+            << '\n';
   #endif
 
   if(t==';')
@@ -1238,11 +1236,11 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl)
   {
   case tdk_decl:
     #ifdef DEBUG
-    std::cout << std::string(__indent, ' ') << "BODY: " << body << std::endl;
+    std::cout << std::string(__indent, ' ') << "BODY: "
+              << body.pretty() << '\n';
     std::cout << std::string(__indent, ' ') << "TEMPLATE_TYPE: "
-              << template_type << std::endl;
+              << template_type.pretty() << '\n';
     #endif
-
     body.add(ID_template_type).swap(template_type);
     body.set(ID_is_template, true);
     decl.swap(body);
@@ -1912,9 +1910,8 @@ bool Parser::rIntegralDeclaration(
       #ifdef DEBUG
       std::cout << std::string(__indent, ' ')
                 << "Parser::rIntegralDeclaration 8 "
-                << declaration << "\n";
+                << declaration.pretty() << '\n';
       #endif
-
       lex.get_token(tk);
       return true;
     }
@@ -5118,10 +5115,9 @@ bool Parser::rClassBody(exprt &body)
       // body=Ptree::List(ob, nil, new Leaf(tk));
       return true;        // error recovery
     }
-
     #ifdef DEBUG
-    std::cout << std::string(__indent, ' ') << "Parser::rClassBody " << member
-              << std::endl;
+    std::cout << std::string(__indent, ' ') << "Parser::rClassBody "
+              << member.pretty() << '\n';
     #endif
 
     members.move_to_operands(
@@ -7583,7 +7579,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
   #ifdef DEBUG
   indenter _i;
   std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 0 "
-            << lex.LookAhead(0) << " " << lex.current_token().text <<"\n";
+            << lex.LookAhead(0) << ' ' << lex.current_token().text << '\n';
   #endif
 
   switch(lex.LookAhead(0))
@@ -9245,8 +9241,8 @@ bool Parser::rExprStatement(codet &statement)
     if(rDeclarationStatement(statement))
     {
       #ifdef DEBUG
-      std::cout << std::string(__indent, ' ') << "rDe: " << statement
-                << std::endl;
+      std::cout << std::string(__indent, ' ') << "rDe "
+                << statement.pretty() << '\n';
       #endif
       return true;
     }
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 160501e5a12..305bb2f80dd 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -378,8 +378,6 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     remove_asm(goto_model);
 
     // add the library
-    status() << "Adding CPROVER library ("
-             << config.ansi_c.arch << ")" << eom;
     link_to_library(goto_model, ui_message_handler);
     #endif
 
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index a405178652f..1ba3d96a9d4 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -480,8 +480,6 @@ bool goto_diff_parse_optionst::process_goto_program(
     remove_asm(symbol_table, goto_functions);
 
     // add the library
-    status() << "Adding CPROVER library ("
-             << config.ansi_c.arch << ")" << eom;
     link_to_library(symbol_table, goto_functions, ui_message_handler);
 
     // remove function pointers
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
index 93d0ca0dfd7..bb86d5a4d75 100644
--- a/src/goto-instrument/accelerate/accelerate.cpp
+++ b/src/goto-instrument/accelerate/accelerate.cpp
@@ -27,8 +27,6 @@ Author: Matt Lewis
 #include "overflow_instrumenter.h"
 #include "util.h"
 
-#define DEBUG
-
 goto_programt::targett acceleratet::find_back_jump(
   goto_programt::targett loop_header)
 {
diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp
index d90357d2246..1d42ebf1945 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.cpp
+++ b/src/goto-instrument/accelerate/acceleration_utils.cpp
@@ -42,8 +42,6 @@ Author: Matt Lewis
 #include "cone_of_influence.h"
 #include "overflow_instrumenter.h"
 
-#define DEBUG
-
 void acceleration_utilst::gather_rvalues(
   const exprt &expr,
   expr_sett &rvalues)
diff --git a/src/goto-instrument/accelerate/all_paths_enumerator.cpp b/src/goto-instrument/accelerate/all_paths_enumerator.cpp
index cfc1c3ae2ed..8b1038d426d 100644
--- a/src/goto-instrument/accelerate/all_paths_enumerator.cpp
+++ b/src/goto-instrument/accelerate/all_paths_enumerator.cpp
@@ -10,8 +10,6 @@ Author: Matt Lewis
 
 #include "all_paths_enumerator.h"
 
-// #define DEBUG
-
 bool all_paths_enumeratort::next(patht &path)
 {
   if(last_path.empty())
diff --git a/src/goto-instrument/accelerate/cone_of_influence.cpp b/src/goto-instrument/accelerate/cone_of_influence.cpp
index a1914756698..0f0b969e342 100644
--- a/src/goto-instrument/accelerate/cone_of_influence.cpp
+++ b/src/goto-instrument/accelerate/cone_of_influence.cpp
@@ -12,8 +12,6 @@ Author: Matt Lewis
 
 #include "cone_of_influence.h"
 
-// #define DEBUG
-
 void cone_of_influencet::cone_of_influence(
   const expr_sett &targets,
   expr_sett &cone)
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index 6f91824a8e7..29d5ac0f81b 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -43,9 +43,6 @@ Author: Matt Lewis
 #include "cone_of_influence.h"
 #include "overflow_instrumenter.h"
 
-#define DEBUG
-
-
 bool disjunctive_polynomial_accelerationt::accelerate(
   path_acceleratort &accelerator)
 {
diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp b/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp
index 1590eb6c127..d47c0c6287a 100644
--- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp
+++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp
@@ -10,8 +10,6 @@ Author: Matt Lewis
 
 #include "enumerating_loop_acceleration.h"
 
-// #define DEBUG
-
 bool enumerating_loop_accelerationt::accelerate(
   path_acceleratort &accelerator)
 {
diff --git a/src/goto-instrument/accelerate/overflow_instrumenter.cpp b/src/goto-instrument/accelerate/overflow_instrumenter.cpp
index 2bad8d1283b..6e126aeb581 100644
--- a/src/goto-instrument/accelerate/overflow_instrumenter.cpp
+++ b/src/goto-instrument/accelerate/overflow_instrumenter.cpp
@@ -18,8 +18,6 @@ Author: Matt Lewis
 #include "overflow_instrumenter.h"
 #include "util.h"
 
-// #define DEBUG
-
 /*
  * This code is copied wholesale from analyses/goto_check.cpp.
  */
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index a9dbb2ff58f..ccf24d6e475 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -39,9 +39,6 @@ Author: Matt Lewis
 #include "cone_of_influence.h"
 #include "overflow_instrumenter.h"
 
-#define DEBUG
-
-
 bool polynomial_acceleratort::accelerate(
   patht &loop,
   path_acceleratort &accelerator)
diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
index 17bc94ecce0..d8067ec3640 100644
--- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp
+++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
@@ -42,8 +42,6 @@ Author: Matt Lewis
 #include "util.h"
 #include "overflow_instrumenter.h"
 
-#define DEBUG
-
 bool sat_path_enumeratort::next(patht &path)
 {
   scratch_programt program(symbol_table);
diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
index f42cad26e0d..8f7e1f40c2d 100644
--- a/src/goto-instrument/accelerate/scratch_program.cpp
+++ b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -15,8 +15,6 @@ Author: Matt Lewis
 
 #include "scratch_program.h"
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
@@ -31,8 +29,8 @@ bool scratch_programt::check_sat(bool do_slice)
   update();
 
 #ifdef DEBUG
-  std::cout << "Checking following program for satness:" << endl;
-  output(ns, "scratch", cout);
+  std::cout << "Checking following program for satness:\n";
+  output(ns, "scratch", std::cout);
 #endif
 
   symex.constant_propagation=constant_propagation;
@@ -49,7 +47,7 @@ bool scratch_programt::check_sat(bool do_slice)
   {
     // Symex sliced away all our assertions.
 #ifdef DEBUG
-    std::cout << "Trivially unsat" << std::endl;
+    std::cout << "Trivially unsat\n";
 #endif
     return false;
   }
@@ -57,7 +55,7 @@ bool scratch_programt::check_sat(bool do_slice)
   equation.convert(*checker);
 
 #ifdef DEBUG
-  cout << "Finished symex, invoking decision procedure." << endl;
+  std::cout << "Finished symex, invoking decision procedure.\n";
 #endif
 
   return (checker->dec_solve()==decision_proceduret::D_SATISFIABLE);
diff --git a/src/goto-instrument/accelerate/trace_automaton.cpp b/src/goto-instrument/accelerate/trace_automaton.cpp
index 228048552e8..10682862e7b 100644
--- a/src/goto-instrument/accelerate/trace_automaton.cpp
+++ b/src/goto-instrument/accelerate/trace_automaton.cpp
@@ -12,8 +12,6 @@ Author: Matt Lewis
 #include "trace_automaton.h"
 #include "path.h"
 
-// #define DEBUG
-
 void trace_automatont::build()
 {
 #ifdef DEBUG
@@ -76,8 +74,10 @@ void trace_automatont::add_path(patht &path)
   for(const auto &step : path)
   {
     goto_programt::targett l=step.loc;
+
 #ifdef DEBUG
-      std::cout << ", " << l->location_number << ":" << l->location;
+    std::cout << ", " << l->location_number << ':'
+              << l->source_location.as_string();
 #endif
 
     if(in_alphabet(l))
@@ -112,7 +112,7 @@ void trace_automatont::determinise()
   std::cout << "Determinising automaton with " << nta.num_states
             << " states and " << nta.accept_states.size()
             << " accept states and " << nta.count_transitions()
-            << " transitions" << endl;
+            << " transitions\n";
 #endif
 
   dstates.clear();
@@ -124,7 +124,7 @@ void trace_automatont::determinise()
   epsilon_closure(init_states);
 
 #ifdef DEBUG
-  std::cout << "There are " << init_states.size() << " init states" << endl;
+  std::cout << "There are " << init_states.size() << " init states\n";
 #endif
 
   dta.init_state=add_dstate(init_states);
@@ -387,7 +387,7 @@ void automatont::reverse(goto_programt::targett epsilon)
 
   std::cout << "Reversing automaton, old init=" << init_state
             << ", new init=" << new_init << ", old accept="
-            << *(accept_states.begin()) << "/" << accept_states.size()
+            << *(accept_states.begin()) << '/' << accept_states.size()
             << " new accept=" << init_state << std::endl;
 
   accept_states.clear();
@@ -471,7 +471,7 @@ void automatont::output(std::ostream &str)
   str << "Accept states: ";
 
   for(const auto &state : accept_states)
-    str << state << " ";
+    str << state << ' ';
 
   str << std::endl;
 
diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp
index 2988b8637d2..96b21195a82 100644
--- a/src/goto-instrument/count_eloc.cpp
+++ b/src/goto-instrument/count_eloc.cpp
@@ -44,7 +44,7 @@ static void collect_eloc(
       const irep_idt &file=it->source_location.get_file();
 
       if(!file.empty() &&
-         !has_prefix(id2string(file), "source_location.is_built_in())
         files[file].insert(it->source_location.get_line());
     }
   }
diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp
index fa92bc27cc7..ede599b6d8b 100644
--- a/src/goto-instrument/cover.cpp
+++ b/src/goto-instrument/cover.cpp
@@ -1082,9 +1082,7 @@ void instrument_cover_goals(
 
   // ignore if built-in library
   if(!goto_program.instructions.empty() &&
-     has_prefix(
-       id2string(goto_program.instructions.front().source_location.get_file()),
-       "code.get_statement();
+  if(statement==ID_array_copy)
+    return true;
+
   if(!target->is_assign())
     return false;
 
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index b5486355277..21000a78da6 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -744,6 +744,14 @@ int goto_instrument_parse_optionst::doit()
       return 0;
     }
 
+    if(cmdline.isset("drop-unused-functions"))
+    {
+      do_indirect_call_and_rtti_removal();
+
+      status() << "Removing unused functions" << eom;
+      remove_unused_functions(goto_functions, get_message_handler());
+    }
+
     // write new binary?
     if(cmdline.args.size()==2)
     {
@@ -983,7 +991,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
        cmdline.isset("custom-bitvector-analysis"))
       config.ansi_c.defines.push_back("__CPROVER_CUSTOM_BITVECTOR_ANALYSIS");
 
-    status() << "Adding CPROVER library" << eom;
+    // add the library
     link_to_library(symbol_table, goto_functions, ui_message_handler);
   }
 
@@ -1182,6 +1190,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   if(cmdline.isset("string-abstraction"))
   {
+    do_indirect_call_and_rtti_removal();
+    do_remove_returns();
+
     status() << "String Abstraction" << eom;
     string_abstraction(
       symbol_table,
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index d3efb975767..180eeb7a2f5 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -45,6 +45,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(stack-depth):(nondet-static)" \
   "(function-enter):(function-exit):(branch):" \
   OPT_SHOW_GOTO_FUNCTIONS \
+  "(drop-unused-functions)" \
   "(show-value-sets)" \
   "(show-global-may-alias)" \
   "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 615470b7f9e..8fdcd28ae07 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -851,13 +851,19 @@ void goto_convertt::do_java_new_array(
     goto_programt tmp;
 
     symbol_exprt tmp_i=
-      new_tmp_symbol(index_type(), "index", tmp, location).symbol_expr();
+      new_tmp_symbol(length.type(), "index", tmp, location).symbol_expr();
 
     code_fort for_loop;
 
     side_effect_exprt sub_java_new=rhs;
     sub_java_new.operands().erase(sub_java_new.operands().begin());
 
+    assert(rhs.type().id()==ID_pointer);
+    typet sub_type=
+      static_cast(rhs.type().subtype().find("#element_type"));
+    assert(sub_type.id()==ID_pointer);
+    sub_java_new.type()=sub_type;
+
     side_effect_exprt inc(ID_assign);
     inc.operands().resize(2);
     inc.op0()=tmp_i;
@@ -866,11 +872,21 @@ void goto_convertt::do_java_new_array(
     dereference_exprt deref_expr(
       plus_exprt(data, tmp_i), data.type().subtype());
 
+    code_blockt for_body;
+    symbol_exprt init_sym=
+      new_tmp_symbol(sub_type, "subarray_init", tmp, location).symbol_expr();
+
+    code_assignt init_subarray(init_sym, sub_java_new);
+    code_assignt assign_subarray(
+      deref_expr,
+      typecast_exprt(init_sym, deref_expr.type()));
+    for_body.move_to_operands(init_subarray);
+    for_body.move_to_operands(assign_subarray);
+
     for_loop.init()=code_assignt(tmp_i, from_integer(0, tmp_i.type()));
     for_loop.cond()=binary_relation_exprt(tmp_i, ID_lt, rhs.op0());
     for_loop.iter()=inc;
-    for_loop.body()=code_skipt();
-    for_loop.body()=code_assignt(deref_expr, sub_java_new);
+    for_loop.body()=for_body;
 
     convert(for_loop, tmp);
     dest.destructive_append(tmp);
@@ -1304,7 +1320,9 @@ void goto_convertt::do_function_call_symbol(
     goto_programt::targett t=dest.add_instruction(ASSERT);
     t->guard=arguments[0];
     t->source_location=function.source_location();
-    t->source_location.set("user-provided", true);
+    t->source_location.set(
+      "user-provided",
+      !function.source_location().is_built_in());
     t->source_location.set_property_class(ID_assertion);
     t->source_location.set_comment(description);
 
diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp
index ed423a35629..f7c8e4509af 100644
--- a/src/goto-programs/goto_inline_class.cpp
+++ b/src/goto-programs/goto_inline_class.cpp
@@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 8e95a03d853..8b0bd6dc46c 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -196,7 +196,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
        (it->is_goto() && it->pc->guard.is_true()) ||
        source_location.is_nil() ||
        source_location.get_file().empty() ||
-       source_location.get_file()=="" ||
+       source_location.is_built_in() ||
        source_location.get_line().empty())
     {
       step_to_node[it->step_nr]=sink;
@@ -392,7 +392,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
        (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
        (it->is_goto() && it->source.pc->guard.is_true()) ||
        source_location.is_nil() ||
-       source_location.get_file()=="" ||
+       source_location.is_built_in() ||
        source_location.get_line().empty())
     {
       step_to_node[step_nr]=sink;
diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp
index 46cd45c36da..c3ead7e6ecb 100644
--- a/src/goto-programs/link_to_library.cpp
+++ b/src/goto-programs/link_to_library.cpp
@@ -6,6 +6,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
+#include 
+
 #include 
 
 #include "link_to_library.h"
@@ -54,6 +56,11 @@ void link_to_library(
   // this needs a fixedpoint, as library functions
   // may depend on other library functions
 
+  messaget message(message_handler);
+
+  message.status() << "Adding CPROVER library ("
+                   << config.ansi_c.arch << ")" << messaget::eom;
+
   std::set added_functions;
 
   while(true)
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index c93b50a2500..fde2f5f8405 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -57,8 +57,11 @@ class remove_virtual_functionst
   typedef std::vector functionst;
   void get_functions(const exprt &, functionst &);
   void get_child_functions_rec(
-    const irep_idt &, const symbol_exprt &,
-    const irep_idt &, functionst &) const;
+    const irep_idt &,
+    const symbol_exprt &,
+    const irep_idt &,
+    functionst &,
+    std::set &visited) const;
   exprt get_method(
     const irep_idt &class_id,
     const irep_idt &component_name) const;
@@ -254,7 +257,8 @@ void remove_virtual_functionst::get_child_functions_rec(
   const irep_idt &this_id,
   const symbol_exprt &last_method_defn,
   const irep_idt &component_name,
-  functionst &functions) const
+  functionst &functions,
+  std::set &visited) const
 {
   auto findit=class_hierarchy.class_map.find(this_id);
   if(findit==class_hierarchy.class_map.end())
@@ -262,6 +266,8 @@ void remove_virtual_functionst::get_child_functions_rec(
 
   for(const auto &child : findit->second.children)
   {
+    if(!visited.insert(child).second)
+      continue;
     exprt method=get_method(child, component_name);
     functiont function(child);
     if(method.is_not_nil())
@@ -279,7 +285,8 @@ void remove_virtual_functionst::get_child_functions_rec(
       child,
       function.symbol_expr,
       component_name,
-      functions);
+      functions,
+      visited);
   }
 }
 
@@ -333,11 +340,13 @@ void remove_virtual_functionst::get_functions(
   }
 
   // iterate over all children, transitively
+  std::set visited;
   get_child_functions_rec(
     class_id,
     root_function.symbol_expr,
     component_name,
-    functions);
+    functions,
+    visited);
 
   if(root_function.symbol_expr!=symbol_exprt())
     functions.push_back(root_function);
diff --git a/src/goto-programs/show_goto_functions.h b/src/goto-programs/show_goto_functions.h
index 5bb7320963e..a496682961e 100644
--- a/src/goto-programs/show_goto_functions.h
+++ b/src/goto-programs/show_goto_functions.h
@@ -19,7 +19,7 @@ class goto_modelt;
   "(show-goto-functions)"
 
 #define HELP_SHOW_GOTO_FUNCTIONS \
-  " --show-goto-functions         show goto program\n"
+  " --show-goto-functions        show goto program\n"
 
 void show_goto_functions(
   const namespacet &ns,
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 0e0a6f07dad..909a437bd9c 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -158,11 +158,17 @@ void build_goto_trace(
 
   mp_integer current_time=0;
 
+  const goto_trace_stept *end_ptr=nullptr;
+  bool end_step_seen=false;
+
   for(symex_target_equationt::SSA_stepst::const_iterator
       it=target.SSA_steps.begin();
-      it!=end_step;
+      it!=target.SSA_steps.end();
       it++)
   {
+    if(it==end_step)
+      end_step_seen=true;
+
     const symex_target_equationt::SSA_stept &SSA_step=*it;
 
     if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
@@ -221,6 +227,8 @@ void build_goto_trace(
     goto_tracet::stepst &steps=time_map[current_time];
     steps.push_back(goto_trace_stept());
     goto_trace_stept &goto_trace_step=steps.back();
+    if(!end_step_seen)
+      end_ptr=&goto_trace_step;
 
     goto_trace_step.thread_nr=SSA_step.source.thread_nr;
     goto_trace_step.pc=SSA_step.source.pc;
@@ -286,6 +294,17 @@ void build_goto_trace(
   for(auto &t_it : time_map)
     goto_trace.steps.splice(goto_trace.steps.end(), t_it.second);
 
+  // cut off the trace at the desired end
+  for(goto_tracet::stepst::iterator
+      s_it1=goto_trace.steps.begin();
+      s_it1!=goto_trace.steps.end();
+      ++s_it1)
+    if(end_step_seen && end_ptr==&(*s_it1))
+    {
+      goto_trace.trim_after(s_it1);
+      break;
+    }
+
   // produce the step numbers
   unsigned step_nr=0;
 
@@ -321,7 +340,7 @@ void build_goto_trace(
       s_it1++)
     if(s_it1->is_assert() && !s_it1->cond_value)
     {
-      goto_trace.steps.erase(++s_it1, goto_trace.steps.end());
+      goto_trace.trim_after(s_it1);
       break;
     }
 }
diff --git a/src/java_bytecode/bytecode_info.cpp b/src/java_bytecode/bytecode_info.cpp
index 556e208129c..87b1942b54e 100644
--- a/src/java_bytecode/bytecode_info.cpp
+++ b/src/java_bytecode/bytecode_info.cpp
@@ -218,5 +218,5 @@ struct bytecode_infot const bytecode_info[]=
 { "impdep1",        0xfe, ' ', 0, 0, ' ' }, // ; reserved for implementation-dependent operations within debuggers; should not appear in any class file  NOLINT(*)
 { "impdep2",        0xff, ' ', 0, 0, ' ' }, // ; reserved for implementation-dependent operations within debuggers; should not appear in any class file  NOLINT(*)
 { "wide",           0xc4, ' ', 0, 0, ' ' }, // modifier for others  NOLINT(*)
-{ 0, 0 }
+{ nullptr,          0x00, '\0',0, 0, '\0'}, // zero-initialized NOLINT (*)
 };
diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp
index f21b0bb1ce2..0330794a8e7 100644
--- a/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -27,14 +27,12 @@ class java_bytecode_convert_classt:public messaget
   java_bytecode_convert_classt(
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
-    bool _disable_runtime_checks,
     size_t _max_array_length,
     lazy_methodst& _lazy_methods,
     lazy_methods_modet _lazy_methods_mode,
     bool _string_refinement_enabled):
     messaget(_message_handler),
     symbol_table(_symbol_table),
-    disable_runtime_checks(_disable_runtime_checks),
     max_array_length(_max_array_length),
     lazy_methods(_lazy_methods),
     lazy_methods_mode(_lazy_methods_mode),
@@ -60,7 +58,6 @@ class java_bytecode_convert_classt:public messaget
 
 protected:
   symbol_tablet &symbol_table;
-  const bool disable_runtime_checks;
   const size_t max_array_length;
   lazy_methodst &lazy_methods;
   lazy_methods_modet lazy_methods_mode;
@@ -169,7 +166,6 @@ void java_bytecode_convert_classt::convert(const classt &c)
         method,
         symbol_table,
         get_message_handler(),
-        disable_runtime_checks,
         max_array_length);
     }
     else
@@ -364,7 +360,6 @@ bool java_bytecode_convert_class(
   const java_bytecode_parse_treet &parse_tree,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length,
   lazy_methodst &lazy_methods,
   lazy_methods_modet lazy_methods_mode,
@@ -373,7 +368,6 @@ bool java_bytecode_convert_class(
   java_bytecode_convert_classt java_bytecode_convert_class(
     symbol_table,
     message_handler,
-    disable_runtime_checks,
     max_array_length,
     lazy_methods,
     lazy_methods_mode,
diff --git a/src/java_bytecode/java_bytecode_convert_class.h b/src/java_bytecode/java_bytecode_convert_class.h
index 0d2be3d8202..9ce5cc8c7cc 100644
--- a/src/java_bytecode/java_bytecode_convert_class.h
+++ b/src/java_bytecode/java_bytecode_convert_class.h
@@ -19,7 +19,6 @@ bool java_bytecode_convert_class(
   const java_bytecode_parse_treet &parse_tree,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length,
   lazy_methodst &,
   lazy_methods_modet,
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 0912ec8b22a..695048ec421 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1084,20 +1084,17 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       assert(op.size()==1 && results.size()==1);
       code_blockt block;
-      if(!disable_runtime_checks)
-      {
-        // TODO throw NullPointerException instead
-        const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
-        const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
-        const exprt not_equal_null(
-          binary_relation_exprt(lhs, ID_notequal, rhs));
-        code_assertt check(not_equal_null);
-        check.add_source_location()
-          .set_comment("Throw null");
-        check.add_source_location()
-          .set_property_class("null-pointer-exception");
-        block.move_to_operands(check);
-      }
+      // TODO throw NullPointerException instead
+      const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
+      const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
+      const exprt not_equal_null(
+        binary_relation_exprt(lhs, ID_notequal, rhs));
+      code_assertt check(not_equal_null);
+      check.add_source_location()
+        .set_comment("Throw null");
+      check.add_source_location()
+        .set_property_class("null-pointer-exception");
+      block.move_to_operands(check);
 
       side_effect_expr_throwt throw_expr;
       throw_expr.add_source_location()=i_it->source_location;
@@ -1110,20 +1107,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="checkcast")
     {
-      if(!disable_runtime_checks)
-      {
-        // checkcast throws an exception in case a cast of object
-        // on stack to given type fails.
-        // The stack isn't modified.
-        // TODO: convert assertions to exceptions.
-        assert(op.size()==1 && results.size()==1);
-        binary_predicate_exprt check(op[0], ID_java_instanceof, arg0);
-        c=code_assertt(check);
-        c.add_source_location().set_comment("Dynamic cast check");
-        c.add_source_location().set_property_class("bad-dynamic-cast");
-      }
-      else
-        c=code_skipt();
+      // checkcast throws an exception in case a cast of object
+      // on stack to given type fails.
+      // The stack isn't modified.
+      // TODO: convert assertions to exceptions.
+      assert(op.size()==1 && results.size()==1);
+      binary_predicate_exprt check(op[0], ID_java_instanceof, arg0);
+      c=code_assertt(check);
+      c.add_source_location().set_comment("Dynamic cast check");
+      c.add_source_location().set_property_class("bad-dynamic-cast");
 
       results[0]=op[0];
     }
@@ -1308,13 +1300,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const dereference_exprt element(data_plus_offset, element_type);
 
       c=code_blockt();
-      if(!disable_runtime_checks)
-      {
-        codet bounds_check=
-          get_array_bounds_check(deref, op[1], i_it->source_location);
-        bounds_check.add_source_location()=i_it->source_location;
-        c.move_to_operands(bounds_check);
-      }
+      codet bounds_check=
+        get_array_bounds_check(deref, op[1], i_it->source_location);
+      bounds_check.add_source_location()=i_it->source_location;
+      c.move_to_operands(bounds_check);
       code_assignt array_put(element, op[2]);
       array_put.add_source_location()=i_it->source_location;
       c.move_to_operands(array_put);
@@ -1354,11 +1343,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
       typet element_type=data_ptr.type().subtype();
       dereference_exprt element(data_plus_offset, element_type);
 
-      if(!disable_runtime_checks)
-      {
-        c=get_array_bounds_check(deref, op[1], i_it->source_location);
-        c.add_source_location()=i_it->source_location;
-      }
+      c=get_array_bounds_check(deref, op[1], i_it->source_location);
+      c.add_source_location()=i_it->source_location;
       results[0]=java_bytecode_promotion(element);
     }
     else if(statement==patternt("?load"))
@@ -1899,17 +1885,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
         java_new_array.add_source_location()=i_it->source_location;
 
       c=code_blockt();
-      if(!disable_runtime_checks)
-      {
-        // TODO make this throw NegativeArrayIndexException instead.
-        constant_exprt intzero=from_integer(0, java_int_type());
-        binary_relation_exprt gezero(op[0], ID_ge, intzero);
-        code_assertt check(gezero);
-        check.add_source_location().set_comment("Array size < 0");
-        check.add_source_location()
-          .set_property_class("array-create-negative-size");
-        c.move_to_operands(check);
-      }
+      // TODO make this throw NegativeArrayIndexException instead.
+      constant_exprt intzero=from_integer(0, java_int_type());
+      binary_relation_exprt gezero(op[0], ID_ge, intzero);
+      code_assertt check(gezero);
+      check.add_source_location().set_comment("Array size < 0");
+      check.add_source_location()
+        .set_property_class("array-create-negative-size");
+      c.move_to_operands(check);
+
       if(max_array_length!=0)
       {
         constant_exprt size_limit=
@@ -1941,26 +1925,24 @@ codet java_bytecode_convert_methodt::convert_instructions(
         java_new_array.add_source_location()=i_it->source_location;
 
       code_blockt checkandcreate;
-      if(!disable_runtime_checks)
+      // TODO make this throw NegativeArrayIndexException instead.
+      constant_exprt intzero=from_integer(0, java_int_type());
+      binary_relation_exprt gezero(op[0], ID_ge, intzero);
+      code_assertt check(gezero);
+      check.add_source_location().set_comment("Array size < 0");
+      check.add_source_location()
+        .set_property_class("array-create-negative-size");
+      checkandcreate.move_to_operands(check);
+
+      if(max_array_length!=0)
       {
-        // TODO make this throw NegativeArrayIndexException instead.
-        constant_exprt intzero=from_integer(0, java_int_type());
-        binary_relation_exprt gezero(op[0], ID_ge, intzero);
-        code_assertt check(gezero);
-        check.add_source_location().set_comment("Array size < 0");
-        check.add_source_location()
-          .set_property_class("array-create-negative-size");
-        checkandcreate.move_to_operands(check);
-
-        if(max_array_length!=0)
-        {
-          constant_exprt size_limit=
-            from_integer(max_array_length, java_int_type());
-          binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
-          code_assumet assume_le_max_size(le_max_size);
-          checkandcreate.move_to_operands(assume_le_max_size);
-        }
+        constant_exprt size_limit=
+          from_integer(max_array_length, java_int_type());
+        binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
+        code_assumet assume_le_max_size(le_max_size);
+        checkandcreate.move_to_operands(assume_le_max_size);
       }
+
       const exprt tmp=tmp_variable("newarray", ref_type);
       c=code_assignt(tmp, java_new_array);
       results[0]=tmp;
@@ -2301,7 +2283,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
   // First create a simple flat list of basic blocks. We'll add lexical nesting
   // constructs as variable live-ranges require next.
   bool start_new_block=true;
-  int previous_address=-1;
+  bool has_seen_previous_address=false;
+  unsigned previous_address=0;
   for(const auto &address_pair : address_map)
   {
     const unsigned address=address_pair.first;
@@ -2316,7 +2299,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     if(!start_new_block)
       start_new_block=address_pair.second.predecessors.size()>1;
     // Start a new lexical block if we've just entered a try block
-    if(!start_new_block && previous_address!=-1)
+    if(!start_new_block && has_seen_previous_address)
     {
       for(const auto &exception_row : method.exception_table)
         if(exception_row.start_pc==previous_address)
@@ -2346,6 +2329,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     start_new_block=address_pair.second.successors.size()>1;
 
     previous_address=address;
+    has_seen_previous_address=true;
   }
 
   // Find out where temporaries are used:
@@ -2428,7 +2412,6 @@ void java_bytecode_convert_method(
   const java_bytecode_parse_treet::methodt &method,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length,
   safe_pointer > needed_methods,
   safe_pointer > needed_classes)
@@ -2436,7 +2419,6 @@ void java_bytecode_convert_method(
   java_bytecode_convert_methodt java_bytecode_convert_method(
     symbol_table,
     message_handler,
-    disable_runtime_checks,
     max_array_length,
     needed_methods,
     needed_classes);
diff --git a/src/java_bytecode/java_bytecode_convert_method.h b/src/java_bytecode/java_bytecode_convert_method.h
index e81881f44e1..bc25eccb0c7 100644
--- a/src/java_bytecode/java_bytecode_convert_method.h
+++ b/src/java_bytecode/java_bytecode_convert_method.h
@@ -22,7 +22,6 @@ void java_bytecode_convert_method(
   const java_bytecode_parse_treet::methodt &,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length,
   safe_pointer > needed_methods,
   safe_pointer > needed_classes);
@@ -33,7 +32,6 @@ inline void java_bytecode_convert_method(
   const java_bytecode_parse_treet::methodt &method,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length)
 {
   java_bytecode_convert_method(
@@ -41,7 +39,6 @@ inline void java_bytecode_convert_method(
     method,
     symbol_table,
     message_handler,
-    disable_runtime_checks,
     max_array_length,
     safe_pointer >::create_null(),
     safe_pointer >::create_null());
diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h
index 4fb24c47b84..60b69a60f34 100644
--- a/src/java_bytecode/java_bytecode_convert_method_class.h
+++ b/src/java_bytecode/java_bytecode_convert_method_class.h
@@ -30,13 +30,11 @@ class java_bytecode_convert_methodt:public messaget
   java_bytecode_convert_methodt(
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
-    bool _disable_runtime_checks,
     size_t _max_array_length,
     safe_pointer > _needed_methods,
     safe_pointer > _needed_classes):
     messaget(_message_handler),
     symbol_table(_symbol_table),
-    disable_runtime_checks(_disable_runtime_checks),
     max_array_length(_max_array_length),
     needed_methods(_needed_methods),
     needed_classes(_needed_classes)
@@ -56,7 +54,6 @@ class java_bytecode_convert_methodt:public messaget
 
 protected:
   symbol_tablet &symbol_table;
-  const bool disable_runtime_checks;
   const size_t max_array_length;
   safe_pointer > needed_methods;
   safe_pointer > needed_classes;
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 2ff38efef13..277b117c715 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -42,7 +42,6 @@ Function: java_bytecode_languaget::get_language_options
 
 void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
 {
-  disable_runtime_checks=cmd.isset("disable-runtime-check");
   assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
   string_refinement_enabled=cmd.isset("string-refine");
   if(cmd.isset("java-max-input-array-length"))
@@ -387,9 +386,16 @@ static void gather_needed_globals(
 {
   if(e.id()==ID_symbol)
   {
-    const auto &sym=symbol_table.lookup(to_symbol_expr(e).get_identifier());
-    if(sym.is_static_lifetime)
-      needed.add(sym);
+    // If the symbol isn't in the symbol table at all, then it is defined
+    // on an opaque type (i.e. we don't have the class definition at this point)
+    // and will be created during the typecheck phase.
+    // We don't mark it as 'needed' as it doesn't exist yet to keep.
+    auto findit=symbol_table.symbols.find(to_symbol_expr(e).get_identifier());
+    if(findit!=symbol_table.symbols.end() &&
+       findit->second.is_static_lifetime)
+    {
+      needed.add(findit->second);
+    }
   }
   else
     forall_operands(opit, e)
@@ -518,7 +524,6 @@ bool java_bytecode_languaget::typecheck(
          c_it->second,
          symbol_table,
          get_message_handler(),
-         disable_runtime_checks,
          max_user_array_length,
          lazy_methods,
          lazy_methods_mode,
@@ -639,7 +644,6 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
           *parsed_method.second,
           symbol_table,
           get_message_handler(),
-          disable_runtime_checks,
           max_user_array_length,
           safe_pointer >::create_non_null(
             &method_worklist2),
@@ -754,7 +758,6 @@ void java_bytecode_languaget::convert_lazy_method(
     *lazy_method_entry.second,
     symtab,
     get_message_handler(),
-    disable_runtime_checks,
     max_user_array_length);
 }
 
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index 9d7fd98f1d6..a9f917ee567 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -98,12 +98,6 @@ class java_bytecode_languaget:public languaget
   std::vector main_jar_classes;
   java_class_loadert java_class_loader;
   bool assume_inputs_non_null;      // assume inputs variables to be non-null
-
-  bool disable_runtime_checks;      // disable run-time checks for java, i.e.,
-                                    // ASSERTS for
-                                    //  - checkcast / instanceof
-                                    //  - array bounds check
-                                    //  - array size for newarray
   size_t max_nondet_array_length;   // maximal length for non-det array creation
   size_t max_user_array_length;     // max size for user code created arrays
   lazy_methodst lazy_methods;
diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp
index 33e8a39f5db..85e9766d5ab 100644
--- a/src/java_bytecode/java_local_variable_table.cpp
+++ b/src/java_bytecode/java_local_variable_table.cpp
@@ -352,7 +352,7 @@ static void populate_predecessor_map(
             // handling is presently vague (any subroutine is assumed to
             // be able to return to any callsite)
             msg.warning() << "Local variable table: ignoring flow from "
-                          << "out of range for " << it->var.name << " "
+                          << "out of range for " << it->var.name << ' '
                           << pred << " -> " << amapit->first
                           << messaget::eom;
             continue;
@@ -375,7 +375,7 @@ static void populate_predecessor_map(
             // assumed to be able to return to any callsite)
             msg.warning() << "Local variable table: ignoring flow from "
                           << "clashing variable for "
-                          << it->var.name << " " << pred << " -> "
+                          << it->var.name << ' ' << pred << " -> "
                           << amapit->first << messaget::eom;
             continue;
           }
@@ -549,9 +549,8 @@ static void merge_variable_table_entries(
 #ifdef DEBUG
   debug_out << "Merged " << merge_vars.size() << " variables named "
             << merge_into.var.name << "; new live range "
-            << merge_into.var.start_pc << "-"
-            << merge_into.var.start_pc + merge_into.var.length
-            << messaget::eom;
+            << merge_into.var.start_pc << '-'
+            << merge_into.var.start_pc + merge_into.var.length << '\n';
 #endif
 
   // Nuke the now-subsumed var-table entries:
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 088a25f7038..166be7827c9 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -25,18 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_types.h"
 #include "java_utils.h"
 
-/*******************************************************************\
-
-Function: gen_nondet_init
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
 class java_object_factoryt:public messaget
 {
   code_blockt &init_code;
@@ -75,25 +63,20 @@ class java_object_factoryt:public messaget
     bool is_sub,
     irep_idt class_identifier,
     const source_locationt &loc,
-    bool skip_classid,
     bool create_dynamic_objects,
     bool override=false,
     const typet &override_type=empty_typet());
 };
 
-
 /*******************************************************************\
 
-Function: gen_nondet_array_init
+Function: java_object_factoryt::allocate_object
 
-  Inputs: the target expression, desired object type, source location
-          and Boolean whether to create a dynamic object
+  Inputs:
 
- Outputs: the allocated object
+ Outputs:
 
- Purpose: Returns false if we can't figure out the size of allocate_type.
-          allocate_type may differ from target_expr, e.g. for target_expr
-          having type int* and allocate_type being an int[10].
+ Purpose:
 
 \*******************************************************************/
 
@@ -165,16 +148,33 @@ exprt java_object_factoryt::allocate_object(
   }
 }
 
-// Override type says to ignore the LHS' real type, and init it with the given
-// type regardless. Used at the moment for reference arrays, which are
-// implemented as void* arrays but should be init'd as their true type with
-// appropriate casts.
+/*******************************************************************\
+
+Function: java_object_factoryt::gen_nondet_init
+
+  Inputs:
+   expr -
+   is_sub -
+   class_identifier -
+   loc -
+   create_dynamic_objects -
+   override - Ignore the LHS' real type. Used at the moment for
+              reference arrays, which are implemented as void*
+              arrays but should be init'd as their true type with
+              appropriate casts.
+   override_type - Type to use if ignoring the LHS' real type
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 void java_object_factoryt::gen_nondet_init(
   const exprt &expr,
   bool is_sub,
   irep_idt class_identifier,
   const source_locationt &loc,
-  bool skip_classid,
   bool create_dynamic_objects,
   bool override,
   const typet &override_type)
@@ -250,20 +250,17 @@ void java_object_factoryt::gen_nondet_init(
     {
       exprt allocated=
         allocate_object(expr, subtype, loc, create_dynamic_objects);
-      {
-        exprt init_expr;
-        if(allocated.id()==ID_address_of)
-          init_expr=allocated.op0();
-        else
-          init_expr=dereference_exprt(allocated, allocated.type().subtype());
-        gen_nondet_init(
-          init_expr,
-          false,
-          "",
-          loc,
-          false,
-          create_dynamic_objects);
-      }
+      exprt init_expr;
+      if(allocated.id()==ID_address_of)
+        init_expr=allocated.op0();
+      else
+        init_expr=dereference_exprt(allocated, allocated.type().subtype());
+      gen_nondet_init(
+        init_expr,
+        false,
+        "",
+        loc,
+        create_dynamic_objects);
     }
 
     if(!assume_non_null)
@@ -297,9 +294,6 @@ void java_object_factoryt::gen_nondet_init(
 
       if(name=="@class_identifier")
       {
-        if(skip_classid)
-          continue;
-
         irep_idt qualified_clsid="java::"+as_string(class_identifier);
         constant_exprt ci(qualified_clsid, string_typet());
         code_assignt code(me, ci);
@@ -327,7 +321,6 @@ void java_object_factoryt::gen_nondet_init(
           _is_sub,
           class_identifier,
           loc,
-          false,
           create_dynamic_objects);
       }
     }
@@ -345,7 +338,7 @@ void java_object_factoryt::gen_nondet_init(
 
 /*******************************************************************\
 
-Function: gen_nondet_array_init
+Function: java_object_factoryt::gen_nondet_array_init
 
   Inputs:
 
@@ -379,7 +372,7 @@ void java_object_factoryt::gen_nondet_array_init(
   const auto &length_sym_expr=length_sym.symbol_expr();
 
   // Initialize array with some undetermined length:
-  gen_nondet_init(length_sym_expr, false, irep_idt(), loc, false, false);
+  gen_nondet_init(length_sym_expr, false, irep_idt(), loc, false);
 
   // Insert assumptions to bound its length:
   binary_relation_exprt
@@ -464,7 +457,6 @@ void java_object_factoryt::gen_nondet_array_init(
     false,
     irep_idt(),
     loc,
-    false,
     true,
     true,
     element_type);
@@ -479,44 +471,6 @@ void java_object_factoryt::gen_nondet_array_init(
 
 /*******************************************************************\
 
-Function: gen_nondet_init
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void gen_nondet_init(
-  const exprt &expr,
-  code_blockt &init_code,
-  symbol_tablet &symbol_table,
-  const source_locationt &loc,
-  bool skip_classid,
-  bool create_dyn_objs,
-  bool assume_non_null,
-  message_handlert &message_handler,
-  size_t max_nondet_array_length)
-{
-  java_object_factoryt state(
-    init_code,
-    assume_non_null,
-    max_nondet_array_length,
-    symbol_table,
-    message_handler);
-  state.gen_nondet_init(
-    expr,
-    false,
-    "",
-    loc,
-    skip_classid,
-    create_dyn_objs);
-}
-
-/*******************************************************************\
-
 Function: new_tmp_symbol
 
   Inputs:
@@ -592,17 +546,18 @@ exprt object_factory(
 
     exprt object=aux_symbol.symbol_expr();
 
-    const namespacet ns(symbol_table);
-    gen_nondet_init(
-      object,
+    java_object_factoryt state(
       init_code,
+      !allow_null,
+      max_nondet_array_length,
       symbol_table,
-      loc,
-      false,
+      message_handler);
+    state.gen_nondet_init(
+      object,
       false,
-      !allow_null,
-      message_handler,
-      max_nondet_array_length);
+      "",
+      loc,
+      false);
 
     return object;
   }
diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h
index 6122d3e2780..37ed40f0ec9 100644
--- a/src/java_bytecode/java_object_factory.h
+++ b/src/java_bytecode/java_object_factory.h
@@ -22,18 +22,6 @@ exprt object_factory(
   const source_locationt &,
   message_handlert &message_handler);
 
-void gen_nondet_init(
-  const exprt &expr,
-  code_blockt &init_code,
-  symbol_tablet &symbol_table,
-  const source_locationt &,
-  bool skip_classid,
-  bool create_dynamic_objects,
-  bool assume_non_null,
-  message_handlert &message_handler,
-  size_t max_nondet_array_length=5);
-
-
 exprt get_nondet_bool(const typet &);
 
 symbolt &new_tmp_symbol(
diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
index 38a1b94e6be..a644f1acf99 100644
--- a/src/jsil/jsil_typecheck.cpp
+++ b/src/jsil/jsil_typecheck.cpp
@@ -87,7 +87,10 @@ void jsil_typecheckt::update_expr_type(exprt &expr, const typet &type)
     const irep_idt &id=to_symbol_expr(expr).get_identifier();
 
     if(!symbol_table.has_symbol(id))
-      throw "unexpected symbol: "+id2string(id);
+    {
+      error() << "unexpected symbol: " << id << eom;
+      throw 0;
+    }
 
     symbolt &s=symbol_table.lookup(id);
     if(s.type.id().empty() || s.type.is_nil())
@@ -924,7 +927,10 @@ void jsil_typecheckt::typecheck_symbol_expr(symbol_exprt &symbol_expr)
       symbol_table.symbols.find(identifier);
 
     if(s_it==symbol_table.symbols.end())
-      throw "unexpected internal symbol: "+id2string(identifier);
+    {
+      error() << "unexpected internal symbol: " << identifier << eom;
+      throw 0;
+    }
     else
     {
       // symbol already exists
@@ -1006,7 +1012,12 @@ void jsil_typecheckt::typecheck_code(codet &code)
   else if(statement==ID_expression)
   {
     if(code.operands().size()!=1)
-      throw "expression statement expected to have one operand";
+    {
+      err_location(code);
+      error() << "expression statement expected to have one operand"
+              << eom;
+      throw 0;
+    }
 
     typecheck_expr(code.op0());
   }
@@ -1090,7 +1101,11 @@ void jsil_typecheckt::typecheck_try_catch(code_try_catcht &code)
 {
   // A special case of try catch with one catch clause
   if(code.operands().size()!=3)
-    throw "try_catch expected to have three operands";
+  {
+    err_location(code);
+    error() << "try_catch expected to have three operands" << eom;
+    throw 0;
+  }
 
   // function call
   typecheck_function_call(to_code_function_call(code.try_code()));
@@ -1116,7 +1131,11 @@ void jsil_typecheckt::typecheck_function_call(
   code_function_callt &call)
 {
   if(call.operands().size()!=3)
-    throw "function call expected to have three operands";
+  {
+    err_location(call);
+    error() << "function call expected to have three operands" << eom;
+    throw 0;
+  }
 
   exprt &lhs=call.lhs();
   typecheck_expr(lhs);
@@ -1194,7 +1213,12 @@ void jsil_typecheckt::typecheck_function_call(
       make_type_compatible(lhs, jsil_any_type(), true);
 
       if(symbol_table.add(new_symbol))
-        throw "failed to add expression symbol to symbol table";
+      {
+        error().source_location=new_symbol.location;
+        error() << "failed to add expression symbol to symbol table"
+                << eom;
+        throw 0;
+      }
     }
   }
   else
@@ -1287,8 +1311,12 @@ void jsil_typecheckt::typecheck_non_type_symbol(symbolt &symbol)
     // Do nothing
   }
   else
-    throw "non-type symbol value expected code, but got "+
-      symbol.value.pretty();
+  {
+    error().source_location=symbol.location;
+    error() << "non-type symbol value expected code, but got "
+            << symbol.value.pretty() << eom;
+    throw 0;
+  }
 }
 
 /*******************************************************************\
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index 55badd462f1..10816f055c5 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -31,10 +31,10 @@ Function: language_uit::language_uit
 \*******************************************************************/
 
 language_uit::language_uit(
-  const cmdlinet &__cmdline,
+  const cmdlinet &cmdline,
   ui_message_handlert &_ui_message_handler):
   ui_message_handler(_ui_message_handler),
-  _cmdline(__cmdline),
+  _cmdline(cmdline),
   generate_start_function(true)
 {
   set_message_handler(ui_message_handler);
@@ -159,9 +159,7 @@ bool language_uit::typecheck()
 
   if(language_files.typecheck(symbol_table))
   {
-    if(get_ui()==ui_message_handlert::PLAIN)
-      std::cerr << "CONVERSION ERROR" << std::endl;
-
+    error() << "CONVERSION ERROR" << eom;
     return true;
   }
 
@@ -186,9 +184,7 @@ bool language_uit::final()
 
   if(language_files.final(symbol_table, generate_start_function))
   {
-    if(get_ui()==ui_message_handlert::PLAIN)
-      std::cerr << "CONVERSION ERROR" << std::endl;
-
+    error() << "CONVERSION ERROR" << eom;
     return true;
   }
 
diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h
index 4258a03e6a3..c9cf36cec2b 100644
--- a/src/langapi/language_ui.h
+++ b/src/langapi/language_ui.h
@@ -23,7 +23,7 @@ class language_uit:public messaget
   symbol_tablet symbol_table;
 
   language_uit(
-    const cmdlinet &__cmdline,
+    const cmdlinet &cmdline,
     ui_message_handlert &ui_message_handler);
   virtual ~language_uit();
 
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index b66c0591b4b..173d5b2cf4c 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -936,11 +936,6 @@ bool linkingt::adjust_object_type_rec(
   else if(t1.id()!=t2.id())
   {
     // type classes do not match and can't be fixed
-    #ifdef DEBUG
-    str << "LINKING: cannot join " << t1.id() << " vs. " << t2.id();
-    debug_msg();
-    #endif
-
     return true;
   }
 
@@ -1041,11 +1036,6 @@ bool linkingt::adjust_object_type(
   const symbolt &new_symbol,
   bool &set_to_new)
 {
-  #ifdef DEBUG
-  str << "LINKING: trying to adjust types of " << old_symbol.name;
-  debug_msg();
-  #endif
-
   const typet &old_type=follow_tags_symbols(ns, old_symbol.type);
   const typet &new_type=follow_tags_symbols(ns, new_symbol.type);
 
@@ -1133,17 +1123,20 @@ void linkingt::duplicate_object_symbol(
       }
       else
       {
-        err_location(new_symbol.value);
-        error() << "error: conflicting initializers for variable \""
-                << old_symbol.name
-                << "\"" << '\n';
-        error() << "old value in module " << old_symbol.module
-                << " " << old_symbol.value.find_source_location() << '\n'
-                << expr_to_string(ns, old_symbol.name, tmp_old) << '\n';
-        error() << "new value in module " << new_symbol.module
-                << " " << new_symbol.value.find_source_location() << '\n'
-                << expr_to_string(ns, new_symbol.name, tmp_new) << eom;
-        throw 0;
+        warning().source_location=new_symbol.location;
+
+        warning() << "warning: conflicting initializers for"
+                  << " variable \"" << old_symbol.name << "\"\n";
+        warning() << "using old value in module "
+                  << old_symbol.module << " "
+                  << old_symbol.value.find_source_location() << '\n'
+                  << expr_to_string(ns, old_symbol.name, tmp_old)
+                  << '\n';
+        warning() << "ignoring new value in module "
+                  << new_symbol.module << " "
+                  << new_symbol.value.find_source_location() << '\n'
+                  << expr_to_string(ns, new_symbol.name, tmp_new)
+                  << eom;
       }
     }
   }
diff --git a/src/musketeer/fencer.cpp b/src/musketeer/fencer.cpp
index a787ce06393..4fc213908d4 100644
--- a/src/musketeer/fencer.cpp
+++ b/src/musketeer/fencer.cpp
@@ -87,9 +87,9 @@ void fence_weak_memory(
   {
     instrumenter.collect_cycles_by_SCCs(model);
     message.statistics() << "cycles collected: " << messaget::eom;
-    unsigned interesting_scc = 0;
-    unsigned total_cycles = 0;
-    for(unsigned i=0; i=4)
       {
         message.statistics() << "SCC #" << i << ": "
diff --git a/src/musketeer/musketeer_parse_options.cpp b/src/musketeer/musketeer_parse_options.cpp
index 707ec50bd0b..9114b8d7802 100644
--- a/src/musketeer/musketeer_parse_options.cpp
+++ b/src/musketeer/musketeer_parse_options.cpp
@@ -200,7 +200,6 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program(
 
   // we add the library, as some analyses benefit
 
-  status() << "Adding CPROVER library" << eom;
   link_to_library(symbol_table, goto_functions, ui_message_handler);
 
   namespacet ns(symbol_table);
diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp
index d8c5e0ea3de..eb58b330ab6 100644
--- a/src/path-symex/path_symex.cpp
+++ b/src/path-symex/path_symex.cpp
@@ -22,8 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "path_symex.h"
 #include "path_symex_class.h"
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp
index 2ce47fedc0f..3dfc319d6d6 100644
--- a/src/path-symex/path_symex_state.cpp
+++ b/src/path-symex/path_symex_state.cpp
@@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "path_symex_state.h"
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #include 
diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp
index df3621ee290..3aea2c24983 100644
--- a/src/path-symex/path_symex_state_read.cpp
+++ b/src/path-symex/path_symex_state_read.cpp
@@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "path_symex_state.h"
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #include 
diff --git a/src/path-symex/var_map.cpp b/src/path-symex/var_map.cpp
index 8f18b3f9726..d981cf1cca9 100644
--- a/src/path-symex/var_map.cpp
+++ b/src/path-symex/var_map.cpp
@@ -14,8 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "var_map.h"
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: var_mapt::var_infot::operator()
diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp
index b21313f85bf..8638dff9e67 100644
--- a/src/pointer-analysis/dereference.cpp
+++ b/src/pointer-analysis/dereference.cpp
@@ -6,15 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #include 
 #endif
 
 #include 
-#include 
 #include 
 #include 
 #include 
@@ -279,11 +276,18 @@ exprt dereferencet::dereference_plus(
   const exprt &offset,
   const typet &type)
 {
+  exprt pointer=expr.op0();
+  exprt integer=expr.op1();
+
+  // need not be binary
   if(expr.operands().size()>2)
-    return dereference_rec(make_binary(expr), offset, type);
+  {
+    assert(expr.op0().type().id()==ID_pointer);
 
-  // binary
-  exprt pointer=expr.op0(), integer=expr.op1();
+    exprt::operandst plus_ops(
+      ++expr.operands().begin(), expr.operands().end());
+    integer.operands().swap(plus_ops);
+  }
 
   if(ns.follow(integer.type()).id()==ID_pointer)
     std::swap(pointer, integer);
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index cb8fe315444..c3e4dee0cf1 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -809,8 +809,7 @@ void value_sett::get_value_set_rec(
         static_cast(expr.find("#type"));
 
       dynamic_object_exprt dynamic_object(dynamic_type);
-      dynamic_object.instance()=
-        from_integer(location_number, typet(ID_natural));
+      dynamic_object.set_instance(location_number);
       dynamic_object.valid()=true_exprt();
 
       insert(dest, dynamic_object, 0);
@@ -822,8 +821,7 @@ void value_sett::get_value_set_rec(
       assert(expr_type.id()==ID_pointer);
 
       dynamic_object_exprt dynamic_object(expr_type.subtype());
-      dynamic_object.instance()=
-        from_integer(location_number, typet(ID_natural));
+      dynamic_object.set_instance(location_number);
       dynamic_object.valid()=true_exprt();
 
       insert(dest, dynamic_object, 0);
@@ -907,7 +905,7 @@ void value_sett::get_value_set_rec(
 
     const std::string prefix=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     // first try with suffix
     const std::string full_name=prefix+suffix;
@@ -1455,7 +1453,7 @@ void value_sett::do_free(
   const object_map_dt &object_map=value_set.read();
 
   // find out which *instances* interest us
-  expr_sett to_mark;
+  dynamic_object_id_sett to_mark;
 
   for(object_map_dt::const_iterator
       it=object_map.begin();
@@ -1470,7 +1468,7 @@ void value_sett::do_free(
         to_dynamic_object_expr(object);
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.instance());
+        to_mark.insert(dynamic_object.get_instance());
     }
   }
 
@@ -1496,10 +1494,10 @@ void value_sett::do_free(
 
       if(object.id()==ID_dynamic_object)
       {
-        const exprt &instance=
-          to_dynamic_object_expr(object).instance();
+        const dynamic_object_exprt &dynamic_object=
+          to_dynamic_object_expr(object);
 
-        if(to_mark.count(instance)==0)
+        if(to_mark.count(dynamic_object.get_instance())==0)
           set(new_object_map, o_it);
         else
         {
@@ -1569,7 +1567,7 @@ void value_sett::assign_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     entryt &e=get_entry(entryt(name, suffix), lhs.type(), ns);
 
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index 94ed55febb7..e863a969744 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -126,6 +126,8 @@ class value_sett
 
   typedef std::set expr_sett;
 
+  typedef std::set dynamic_object_id_sett;
+
   #ifdef USE_DSTRING
   typedef std::map valuest;
   #else
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 98e6ab2cb2a..04598ac67fa 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 125a2cae58a..0fbcd7dec00 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -727,9 +727,8 @@ void value_set_fit::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(dynamic_type);
       // let's make up a `unique' number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert(dest, dynamic_object, 0);
@@ -742,9 +741,8 @@ void value_set_fit::get_value_set_rec(
       assert(expr.type().id()==ID_pointer);
 
       dynamic_object_exprt dynamic_object(expr.type().subtype());
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert(dest, dynamic_object, 0);
@@ -776,7 +774,7 @@ void value_set_fit::get_value_set_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value)+
+      std::to_string(dynamic_object.get_instance())+
       suffix;
 
     // look it up
@@ -1322,7 +1320,7 @@ void value_set_fit::do_free(
   const object_map_dt &object_map=value_set.read();
 
   // find out which *instances* interest us
-  expr_sett to_mark;
+  dynamic_object_id_sett to_mark;
 
   forall_objects(it, object_map)
   {
@@ -1334,7 +1332,7 @@ void value_set_fit::do_free(
         to_dynamic_object_expr(object);
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.instance());
+        to_mark.insert(dynamic_object.get_instance());
     }
   }
 
@@ -1357,10 +1355,10 @@ void value_set_fit::do_free(
 
       if(object.id()==ID_dynamic_object)
       {
-        const exprt &instance=
-          to_dynamic_object_expr(object).instance();
+        const dynamic_object_exprt &dynamic_object=
+          to_dynamic_object_expr(object);
 
-        if(to_mark.count(instance)==0)
+        if(to_mark.count(dynamic_object.get_instance())==0)
           set(new_object_map, o_it);
         else
         {
@@ -1452,7 +1450,7 @@ void value_set_fit::assign_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     if(make_union(get_entry(name, suffix).object_map, values_rhs))
       changed = true;
@@ -1729,6 +1727,9 @@ void value_set_fit::apply_code(
   else if(statement==ID_fence)
   {
   }
+  else if(statement==ID_array_copy)
+  {
+  }
   else if(statement==ID_input || statement==ID_output)
   {
     // doesn't do anything
diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h
index 5b76d0f48d9..13defa545ae 100644
--- a/src/pointer-analysis/value_set_fi.h
+++ b/src/pointer-analysis/value_set_fi.h
@@ -155,6 +155,8 @@ class value_set_fit
 
   typedef std::unordered_set expr_sett;
 
+  typedef std::unordered_set dynamic_object_id_sett;
+
   #ifdef USE_DSTRING
   typedef std::map valuest;
   typedef std::set flatten_seent;
diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp
index 582fe015dd3..e06d73b245b 100644
--- a/src/pointer-analysis/value_set_fivr.cpp
+++ b/src/pointer-analysis/value_set_fivr.cpp
@@ -857,9 +857,8 @@ void value_set_fivrt::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(dynamic_type);
       // let's make up a `unique' number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert_from(dest, dynamic_object, 0);
@@ -873,9 +872,8 @@ void value_set_fivrt::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(expr.type().subtype());
       // let's make up a unique number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert_from(dest, dynamic_object, 0);
@@ -902,7 +900,7 @@ void value_set_fivrt::get_value_set_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value)+
+      std::to_string(dynamic_object.get_instance())+
       suffix;
 
     // look it up
@@ -1446,7 +1444,7 @@ void value_set_fivrt::do_free(
   const object_map_dt &object_map=value_set.read();
 
   // find out which *instances* interest us
-  expr_sett to_mark;
+  dynamic_object_id_sett to_mark;
 
   forall_objects(it, object_map)
   {
@@ -1458,7 +1456,7 @@ void value_set_fivrt::do_free(
         to_dynamic_object_expr(object);
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.instance());
+        to_mark.insert(dynamic_object.get_instance());
     }
   }
 
@@ -1481,10 +1479,10 @@ void value_set_fivrt::do_free(
 
       if(object.id()==ID_dynamic_object)
       {
-        const exprt &instance=
-          to_dynamic_object_expr(object).instance();
+        const dynamic_object_exprt &dynamic_object=
+          to_dynamic_object_expr(object);
 
-        if(to_mark.count(instance)==0)
+        if(to_mark.count(dynamic_object.get_instance())==0)
           set(new_object_map, o_it);
         else
         {
@@ -1590,7 +1588,7 @@ void value_set_fivrt::assign_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     entryt &temp_entry=get_temporary_entry(name, suffix);
 
diff --git a/src/pointer-analysis/value_set_fivr.h b/src/pointer-analysis/value_set_fivr.h
index 5a96e537e77..e12563252ae 100644
--- a/src/pointer-analysis/value_set_fivr.h
+++ b/src/pointer-analysis/value_set_fivr.h
@@ -216,6 +216,8 @@ class value_set_fivrt
 
   typedef std::unordered_set expr_sett;
 
+  typedef std::unordered_set dynamic_object_id_sett;
+
   #ifdef USE_DSTRING
   typedef std::map valuest;
   typedef std::unordered_set flatten_seent;
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
index 41907d54cfb..4591bdd938d 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -631,9 +631,8 @@ void value_set_fivrnst::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(dynamic_type);
       // let's make up a `unique' number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert_from(dest, dynamic_object, 0);
@@ -647,9 +646,8 @@ void value_set_fivrnst::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(expr.type().subtype());
       // let's make up a unique number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert_from(dest, dynamic_object, 0);
@@ -676,7 +674,7 @@ void value_set_fivrnst::get_value_set_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value)+
+      std::to_string(dynamic_object.get_instance())+
       suffix;
 
     // look it up
@@ -1105,7 +1103,7 @@ void value_set_fivrnst::do_free(
   const object_map_dt &object_map=value_set.read();
 
   // find out which *instances* interest us
-  expr_sett to_mark;
+  dynamic_object_id_sett to_mark;
 
   forall_objects(it, object_map)
   {
@@ -1117,7 +1115,7 @@ void value_set_fivrnst::do_free(
         to_dynamic_object_expr(object);
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.instance());
+        to_mark.insert(dynamic_object.get_instance());
     }
   }
 
@@ -1140,10 +1138,10 @@ void value_set_fivrnst::do_free(
 
       if(object.id()==ID_dynamic_object)
       {
-        const exprt &instance=
-          to_dynamic_object_expr(object).instance();
+        const dynamic_object_exprt &dynamic_object=
+          to_dynamic_object_expr(object);
 
-        if(to_mark.count(instance)==0)
+        if(to_mark.count(dynamic_object.get_instance())==0)
           set(new_object_map, o_it);
         else
         {
@@ -1225,7 +1223,7 @@ void value_set_fivrnst::assign_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     entryt &temp_entry = get_temporary_entry(name, suffix);
 
diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h
index c1d826f2550..f3afc204ef2 100644
--- a/src/pointer-analysis/value_set_fivrns.h
+++ b/src/pointer-analysis/value_set_fivrns.h
@@ -216,6 +216,8 @@ class value_set_fivrnst
 
   typedef std::unordered_set expr_sett;
 
+  typedef std::unordered_set dynamic_object_id_sett;
+
   #ifdef USE_DSTRING
   typedef std::map valuest;
   #else
diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index 9c710fc3737..9f72a8e3475 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #include 
 #include 
 
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index f5e9aad9f8b..aaa63e69fd2 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -27,8 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "../floatbv/float_utils.h"
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: boolbvt::literal
@@ -144,9 +142,6 @@ const bvt &boolbvt::convert_bv(const exprt &expr)
     bv_cache.insert(std::make_pair(expr, bvt()));
   if(!cache_result.second)
   {
-    #ifdef DEBUG
-    std::cout << "Cache hit on " << expr << "\n";
-    #endif
     return cache_result.first->second;
   }
 
@@ -205,10 +200,6 @@ Function: boolbvt::convert_bitvector
 
 bvt boolbvt::convert_bitvector(const exprt &expr)
 {
-  #ifdef DEBUG
-  std::cout << "BV: " << expr.pretty() << std::endl;
-  #endif
-
   if(expr.type().id()==ID_bool)
   {
     bvt bv;
diff --git a/src/solvers/flattening/boolbv_floatbv_op.cpp b/src/solvers/flattening/boolbv_floatbv_op.cpp
index 087faa0485a..e4926dc617e 100644
--- a/src/solvers/flattening/boolbv_floatbv_op.cpp
+++ b/src/solvers/flattening/boolbv_floatbv_op.cpp
@@ -138,7 +138,7 @@ bvt boolbvt::convert_floatbv_op(const exprt &expr)
     else if(expr.id()==ID_floatbv_rem)
       return float_utils.rem(bv0, bv1);
     else
-      assert(false);
+      throw "unexpected operator "+expr.id_string();
   }
   else if(type.id()==ID_vector || type.id()==ID_complex)
   {
diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp
index 3e74ec872c1..943ef98b19c 100644
--- a/src/solvers/flattening/boolbv_get.cpp
+++ b/src/solvers/flattening/boolbv_get.cpp
@@ -17,8 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv.h"
 #include "boolbv_type.h"
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: boolbvt::get
diff --git a/src/solvers/flattening/boolbv_map.cpp b/src/solvers/flattening/boolbv_map.cpp
index dbbb097e7b2..6c6e647a31c 100644
--- a/src/solvers/flattening/boolbv_map.cpp
+++ b/src/solvers/flattening/boolbv_map.cpp
@@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv_map.h"
 #include "boolbv_width.h"
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
diff --git a/src/solvers/flattening/equality.cpp b/src/solvers/flattening/equality.cpp
index 208a4510a35..63ca7e2e147 100644
--- a/src/solvers/flattening/equality.cpp
+++ b/src/solvers/flattening/equality.cpp
@@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
@@ -110,11 +108,6 @@ literalt equalityt::equality2(const exprt &e1, const exprt &e2)
       l=result->second;
   }
 
-  #ifdef DEBUG
-  std::cout << "EQUALITY " << l << "<=>"
-            << e1 << "=" << e2 << std::endl;
-  #endif
-
   return l;
 }
 
diff --git a/src/solvers/flattening/functions.cpp b/src/solvers/flattening/functions.cpp
index 37380aa323b..6b23229c958 100644
--- a/src/solvers/flattening/functions.cpp
+++ b/src/solvers/flattening/functions.cpp
@@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #include 
 
 #include 
diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp
index c277e51e6b0..a772ae0b8a7 100644
--- a/src/solvers/floatbv/float_utils.cpp
+++ b/src/solvers/floatbv/float_utils.cpp
@@ -206,7 +206,7 @@ bvt float_utilst::to_integer(
     return result;
   }
   else
-    assert(0);
+    throw "unsupported rounding mode";
 }
 
 /*******************************************************************\
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
index 01ae3fcd841..33a572191c0 100644
--- a/src/solvers/prop/prop_conv.cpp
+++ b/src/solvers/prop/prop_conv.cpp
@@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "prop_conv.h"
 #include "literal_expr.h"
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: prop_convt::is_in_conflict
diff --git a/src/solvers/sat/satcheck_limmat.cpp b/src/solvers/sat/satcheck_limmat.cpp
index a1aadbbff39..a8393cf30e8 100644
--- a/src/solvers/sat/satcheck_limmat.cpp
+++ b/src/solvers/sat/satcheck_limmat.cpp
@@ -16,8 +16,6 @@ extern "C"
 #include "limmat.h"
 }
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: satcheck_limmatt::satcheck_limmatt
diff --git a/src/solvers/sat/satcheck_zchaff.cpp b/src/solvers/sat/satcheck_zchaff.cpp
index 5a94615e221..6697d6b3c6c 100644
--- a/src/solvers/sat/satcheck_zchaff.cpp
+++ b/src/solvers/sat/satcheck_zchaff.cpp
@@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include 
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: satcheck_zchaff_baset::satcheck_zchaff_baset
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 8342f000531..8001a5b8155 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -34,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include 
 #include 
 #include 
+#include 
 
 #include 
 #include 
@@ -354,7 +355,6 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
   try
   {
     // we add the library
-    status() << "Adding CPROVER library" << eom;
     link_to_library(goto_model, ui_message_handler);
 
     // do partial inlining
@@ -383,6 +383,13 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     // add loop ids
     goto_model.goto_functions.compute_loop_numbers();
 
+    if(cmdline.isset("drop-unused-functions"))
+    {
+      // Entry point will have been set before and function pointers removed
+      status() << "Removing unused functions" << eom;
+      remove_unused_functions(goto_model.goto_functions, ui_message_handler);
+    }
+
     if(cmdline.isset("cover"))
     {
       std::string criterion=cmdline.get_value("cover");
@@ -697,6 +704,7 @@ void symex_parse_optionst::help()
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
+    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     " --ppc-macos                  set MACOS/PPC architecture\n"
     " --mm model                   set memory model (default: sc)\n"
     " --arch                       set architecture (default: "
@@ -730,5 +738,6 @@ void symex_parse_optionst::help()
     "Other options:\n"
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
+    " --verbosity #                verbosity level\n"
     "\n";
 }
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index a67469d71e5..5e178eec14e 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -41,6 +41,7 @@ class optionst;
   "(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(show-locs)(show-vcc)(show-properties)" \
+  "(drop-unused-functions)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \
   "(no-simplify)(no-unwinding-assertions)(no-propagation)"
diff --git a/src/util/Makefile b/src/util/Makefile
index 049f70aee4c..870b524e609 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -12,7 +12,7 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \
       rational.cpp options.cpp dstring.cpp \
       find_symbols.cpp rational_tools.cpp ui_message.cpp simplify_utils.cpp \
       time_stopping.cpp symbol.cpp irep_hash_container.cpp cout_message.cpp \
-      type_eq.cpp guard.cpp array_name.cpp message_stream.cpp \
+      type_eq.cpp guard.cpp array_name.cpp \
       substitute.cpp decision_procedure.cpp union_find.cpp \
       xml.cpp xml_irep.cpp xml_expr.cpp std_types.cpp std_code.cpp \
       format_constant.cpp find_macros.cpp ref_expr_set.cpp std_expr.cpp \
diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp
index af315c696c5..393ec62432f 100644
--- a/src/util/cout_message.cpp
+++ b/src/util/cout_message.cpp
@@ -211,5 +211,6 @@ void gcc_message_handlert::print(
   const std::string &message)
 {
   // gcc appears to send everything to cerr
-  std::cerr << message << '\n' << std::flush;
+  if(verbosity>=level)
+    std::cerr << message << '\n' << std::flush;
 }
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index f3d792a9716..38252a3683f 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -55,13 +55,19 @@ exprt make_binary(const exprt &expr)
   if(operands.size()<=2)
     return expr;
 
+  // types must be identical for make_binary to be safe to use
+  const typet &type=expr.type();
+
   exprt previous=operands.front();
+  assert(previous.type()==type);
 
   for(exprt::operandst::const_iterator
       it=++operands.begin();
       it!=operands.end();
       ++it)
   {
+    assert(it->type()==type);
+
     exprt tmp=expr;
     tmp.operands().clear();
     tmp.operands().resize(2);
diff --git a/src/util/file_util.cpp b/src/util/file_util.cpp
index a5a44d4236f..180967b3338 100644
--- a/src/util/file_util.cpp
+++ b/src/util/file_util.cpp
@@ -136,8 +136,13 @@ void delete_directory(const std::string &path)
       // Needed for Alpine Linux
       if(strcmp(ent->d_name, ".")==0 || strcmp(ent->d_name, "..")==0)
         continue;
+
       std::string sub_path=path+"/"+ent->d_name;
-      if(ent->d_type==DT_DIR)
+
+      struct stat stbuf;
+      stat(sub_path.c_str(), &stbuf);
+
+      if(S_ISDIR(stbuf.st_mode))
         delete_directory(sub_path);
       else
         remove(sub_path.c_str());
diff --git a/src/util/irep.h b/src/util/irep.h
index 32567c82a94..7287eca93b6 100644
--- a/src/util/irep.h
+++ b/src/util/irep.h
@@ -288,11 +288,7 @@ class irept
 
     void clear()
     {
-      #ifdef USE_DSTRING
       data.clear();
-      #else
-      data="";
-      #endif
       sub.clear();
       named_sub.clear();
       comments.clear();
diff --git a/src/util/json_irep.cpp b/src/util/json_irep.cpp
index 403247c1d04..2740228d1db 100644
--- a/src/util/json_irep.cpp
+++ b/src/util/json_irep.cpp
@@ -164,8 +164,8 @@ void json_irept::convert_from_json(const jsont &in, irept &out) const
   }
 
   for(const auto &named_sub : in["namedSub"].object)
-    convert_from_json(named_sub.second, out.get_named_sub()[named_sub.first]);
+    convert_from_json(named_sub.second, out.add(named_sub.first));
 
   for(const auto &comment : in["comment"].object)
-    convert_from_json(comment.second, out.get_comments()[comment.first]);
+    convert_from_json(comment.second, out.add(comment.first));
 }
diff --git a/src/util/message_stream.cpp b/src/util/message_stream.cpp
deleted file mode 100644
index 347d87915d7..00000000000
--- a/src/util/message_stream.cpp
+++ /dev/null
@@ -1,182 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#include 
-
-#include "prefix.h"
-#include "message_stream.h"
-
-/*******************************************************************\
-
-Function: legacy_message_streamt::error_parse_line
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void legacy_message_streamt::error_parse_line(
-  unsigned level,
-  const std::string &line)
-{
-  std::string error_msg=line;
-
-  if(has_prefix(line, "file "))
-  {
-    const char *tptr=line.c_str();
-    int state=0;
-    std::string file, line_no, column, _error_msg, function;
-
-    tptr+=5;
-
-    char previous=0;
-
-    while(*tptr!=0)
-    {
-      if(strncmp(tptr, " line ", 6)==0 && state!=4)
-      {
-        state=1;
-        tptr+=6;
-        continue;
-      }
-      else if(strncmp(tptr, " column ", 8)==0 && state!=4)
-      {
-        state=2;
-        tptr+=8;
-        continue;
-      }
-      else if(strncmp(tptr, " function ", 10)==0 && state!=4)
-      {
-        state=3;
-        tptr+=10;
-        continue;
-      }
-      else if(*tptr==':' && state!=4)
-      {
-        if(tptr[1]==' ' && previous!=':')
-        {
-          state=4;
-          tptr++;
-          while(*tptr==' ') tptr++;
-          continue;
-        }
-      }
-
-      if(state==0) // file
-        file+=*tptr;
-      else if(state==1) // line number
-        line_no+=*tptr;
-      else if(state==2) // column
-        column+=*tptr;
-      else if(state==3) // function
-        function+=*tptr;
-      else if(state==4) // error message
-        _error_msg+=*tptr;
-
-      previous=*tptr;
-
-      tptr++;
-    }
-
-    if(state==4)
-    {
-      saved_error_location.id(irep_idt());
-      saved_error_location.set_line(line_no);
-      saved_error_location.set_file(file);
-      saved_error_location.set_column(column);
-      error_msg=_error_msg;
-      saved_error_location.set_function(function);
-    }
-  }
-  else if(has_prefix(line, "In file included from "))
-  {
-  }
-  else
-  {
-    const char *tptr=line.c_str();
-    int state=0;
-    std::string file, line_no;
-
-    while(*tptr!=0)
-    {
-      if(state==0)
-      {
-        if(*tptr==':')
-          state++;
-        else
-          file+=*tptr;
-      }
-      else if(state==1)
-      {
-        if(*tptr==':')
-          state++;
-        else if(isdigit(*tptr))
-          line_no+=*tptr;
-        else
-          state=3;
-      }
-
-      tptr++;
-    }
-
-    if(state==2)
-    {
-      saved_error_location.id(irep_idt());
-      saved_error_location.set_line(line_no);
-      saved_error_location.set_file(file);
-      saved_error_location.set_function("");
-      saved_error_location.set_column("");
-    }
-  }
-
-  if(message_handler!=NULL)
-    message_handler->print(
-      level, error_msg, sequence_number++, saved_error_location);
-}
-
-/*******************************************************************\
-
-Function: legacy_message_streamt::error_parse
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void legacy_message_streamt::error_parse(
-  unsigned level,
-  const std::string &error)
-{
-  const char *tptr=error.c_str();
-
-  std::string line;
-
-  while(true)
-  {
-    switch(*tptr)
-    {
-     case 0: return;
-     case '\n':
-      error_parse_line(level, line);
-      line.clear();
-      break;
-
-     case '\r': break;
-     default:
-      line+=*tptr;
-    }
-
-    tptr++;
-  }
-}
diff --git a/src/util/message_stream.h b/src/util/message_stream.h
deleted file mode 100644
index 4b3fc48bb7d..00000000000
--- a/src/util/message_stream.h
+++ /dev/null
@@ -1,165 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#ifndef CPROVER_UTIL_MESSAGE_STREAM_H
-#define CPROVER_UTIL_MESSAGE_STREAM_H
-
-#include 
-
-#include "message.h"
-#include "expr.h"
-
-// deprecated; use warning(), error(), etc. streams in messaget
-
-class legacy_message_streamt:public message_clientt
-{
-public:
-  explicit legacy_message_streamt(message_handlert &_message_handler):
-    message_clientt(_message_handler),
-    error_found(false),
-    saved_error_location(static_cast(get_nil_irep())),
-    sequence_number(1)
-  {
-  }
-
-  virtual ~legacy_message_streamt() { }
-
-  // overload to use language specific syntax
-  virtual std::string to_string(const exprt &expr) { return expr.pretty(); }
-  virtual std::string to_string(const typet &type) { return type.pretty(); }
-
-  void err_location(const exprt &expr)
-  { saved_error_location=expr.find_source_location(); }
-  void err_location(const typet &type)
-  { saved_error_location=type.source_location(); }
-  void err_location(const irept &irep)
-  {
-    saved_error_location=
-      static_cast(irep.find(ID_C_source_location));
-  }
-  void err_location(const source_locationt &_location)
-  { saved_error_location=_location; }
-
-  void error_msg(const std::string &message)
-  {
-    send_msg(1, message);
-  }
-
-  void warning_msg(const std::string &message)
-  {
-    send_msg(2, message);
-  }
-
-  void statistics_msg(const std::string &message)
-  {
-    send_msg(8, message);
-  }
-
-  void debug_msg(const std::string &message)
-  {
-    send_msg(9, message);
-  }
-
-  void error_msg()
-  {
-    send_msg(1, str.str());
-    clear_err();
-    sequence_number++;
-  }
-
-  void warning_msg()
-  {
-    send_msg(2, str.str());
-    clear_err();
-    sequence_number++;
-  }
-
-  void status_msg()
-  {
-    send_msg(6, str.str());
-    clear_err();
-    sequence_number++;
-  }
-
-  void statistics_msg()
-  {
-    send_msg(8, str.str());
-    clear_err();
-    sequence_number++;
-  }
-
-  void debug_msg()
-  {
-    send_msg(9, str.str());
-    clear_err();
-    sequence_number++;
-  }
-
-  std::ostringstream str;
-
-  std::ostream &error()
-  {
-    return str;
-  }
-
-  // API stub, intentional noop
-  static inline std::ostream &eom(std::ostream &m)
-  {
-    return m;
-  }
-
-
-  bool get_error_found() const
-  {
-    return error_found;
-  }
-
-  void error_parse(unsigned level)
-  {
-    error_parse(level, str.str());
-    clear_err();
-  }
-
-  void clear_err()
-  {
-    str.clear();
-    str.str("");
-  }
-
-protected:
-  bool error_found;
-  source_locationt saved_error_location;
-  unsigned sequence_number;
-
-  void send_msg(unsigned level, const std::string &message)
-  {
-    if(message=="")
-      return;
-    if(level<=1)
-      error_found=true;
-
-    if(message_handler!=NULL)
-      message_handler->print(
-        level,
-        message,
-        sequence_number,
-        saved_error_location);
-
-    saved_error_location.make_nil();
-  }
-
-  void error_parse_line(
-    unsigned level,
-    const std::string &line);
-
-  void error_parse(
-    unsigned level,
-    const std::string &error);
-};
-
-#endif // CPROVER_UTIL_MESSAGE_STREAM_H
diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp
index 55a9a7ff484..c6930a01d87 100644
--- a/src/util/rename_symbol.cpp
+++ b/src/util/rename_symbol.cpp
@@ -133,6 +133,9 @@ Function: rename_symbolt::have_to_rename
 
 bool rename_symbolt::have_to_rename(const exprt &dest) const
 {
+  if(expr_map.empty() && type_map.empty())
+    return false;
+
   // first look at type
 
   if(have_to_rename(dest.type()))
@@ -274,6 +277,9 @@ Function: rename_symbolt::have_to_rename
 
 bool rename_symbolt::have_to_rename(const typet &dest) const
 {
+  if(expr_map.empty() && type_map.empty())
+    return false;
+
   if(dest.has_subtype())
     if(have_to_rename(dest.subtype()))
       return true;
diff --git a/src/util/source_location.h b/src/util/source_location.h
index b24befcb8c4..b9cf434f3b0 100644
--- a/src/util/source_location.h
+++ b/src/util/source_location.h
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_UTIL_SOURCE_LOCATION_H
 
 #include "irep.h"
+#include "prefix.h"
 
 class source_locationt:public irept
 {
@@ -138,6 +139,18 @@ class source_locationt:public irept
     return get_bool(ID_hide);
   }
 
+  static bool is_built_in(const std::string &s)
+  {
+    std::string built_in1="";
+    std::string built_in2="";
+    return has_prefix(s, built_in1) || has_prefix(s, built_in2);
+  }
+
+  bool is_built_in() const
+  {
+    return is_built_in(id2string(get_file()));
+  }
+
   static const source_locationt &nil()
   {
     return static_cast(get_nil_irep());
diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
index 5efc4d6e70c..4cb9eeff9cc 100644
--- a/src/util/std_expr.cpp
+++ b/src/util/std_expr.cpp
@@ -61,6 +61,16 @@ exprt disjunction(const exprt::operandst &op)
   }
 }
 
+void dynamic_object_exprt::set_instance(unsigned int instance)
+{
+  op0()=from_integer(instance, typet(ID_natural));
+}
+
+unsigned int dynamic_object_exprt::get_instance() const
+{
+  return std::stoul(id2string(to_constant_expr(op0()).get_value()));
+}
+
 /*******************************************************************\
 
 Function: conjunction
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index f034978953c..a233a22569f 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -1541,15 +1541,9 @@ class dynamic_object_exprt:public exprt
       (recent ? ID_most_recent_allocation : ID_any_allocation));
   }
 
-  exprt &instance()
-  {
-    return op0();
-  }
+  void set_instance(unsigned int instance);
 
-  const exprt &instance() const
-  {
-    return op0();
-  }
+  unsigned int get_instance() const;
 
   exprt &valid()
   {
diff --git a/src/util/std_types.h b/src/util/std_types.h
index 9d691ecd8dc..d6b1d899a08 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -215,7 +215,7 @@ class struct_union_typet:public typet
       return set(ID_pretty_name, name);
     }
 
-    const bool get_anonymous() const
+    bool get_anonymous() const
     {
       return get_bool(ID_anonymous);
     }
@@ -225,7 +225,7 @@ class struct_union_typet:public typet
       return set(ID_anonymous, anonymous);
     }
 
-    const bool get_is_padding() const
+    bool get_is_padding() const
     {
       return get_bool(ID_C_is_padding);
     }
diff --git a/src/util/typecheck.cpp b/src/util/typecheck.cpp
index a305fa7ad4c..67b695e53fa 100644
--- a/src/util/typecheck.cpp
+++ b/src/util/typecheck.cpp
@@ -20,45 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-bool legacy_typecheckt::typecheck_main()
-{
-  try
-  {
-    typecheck();
-  }
-
-  catch(int)
-  {
-    error_msg();
-  }
-
-  catch(const char *e)
-  {
-    str << e;
-    error_msg();
-  }
-
-  catch(const std::string &e)
-  {
-    str << e;
-    error_msg();
-  }
-
-  return error_found;
-}
-
-/*******************************************************************\
-
-Function:
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
 bool typecheckt::typecheck_main()
 {
   try
diff --git a/src/util/typecheck.h b/src/util/typecheck.h
index 7de4557de64..ee80f6e42f0 100644
--- a/src/util/typecheck.h
+++ b/src/util/typecheck.h
@@ -9,23 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_TYPECHECK_H
 #define CPROVER_UTIL_TYPECHECK_H
 
-#include "message_stream.h"
-
-class legacy_typecheckt:public legacy_message_streamt
-{
-public:
-  explicit legacy_typecheckt(message_handlert &_message_handler):
-    legacy_message_streamt(_message_handler) { }
-  virtual ~legacy_typecheckt() { }
-
-protected:
-  // main function -- overload this one
-  virtual void typecheck()=0;
-
-public:
-  // call that one
-  virtual bool typecheck_main();
-};
+#include "expr.h"
+#include "message.h"
 
 class typecheckt:public messaget
 {
diff --git a/src/util/union_find.h b/src/util/union_find.h
index 5b2ff2504e4..2fee15e495b 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -157,7 +157,8 @@ class union_find:public numbering
   // are 'a' and 'b' in the same set?
   bool same_set(const T &a, const T &b) const
   {
-    typename subt::number_type na, nb;
+    typedef typename subt::number_type subt_number_typet;
+    subt_number_typet na=subt_number_typet(), nb=subt_number_typet();
     bool have_na=!subt::get_number(a, na),
          have_nb=!subt::get_number(b, nb);
 
diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h
index 7a1050bcb00..1ef5aaedae1 100644
--- a/src/xmllang/graphml.h
+++ b/src/xmllang/graphml.h
@@ -49,7 +49,7 @@ class graphmlt:public grapht
     return false;
   }
 
-  const node_indext add_node_if_not_exists(std::string node_name)
+  node_indext add_node_if_not_exists(std::string node_name)
   {
     for(node_indext i=0; i