diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
index 9c43dd404d5..4169a43ed7d 100644
--- a/regression/CMakeLists.txt
+++ b/regression/CMakeLists.txt
@@ -61,6 +61,7 @@ add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)
 add_subdirectory(validate-trace-xml-schema)
 add_subdirectory(cbmc-primitives)
+add_subdirectory(goto-interpreter)
 add_subdirectory(cbmc-sequentialization)
 
 if(WITH_MEMORY_ANALYZER)
diff --git a/regression/Makefile b/regression/Makefile
index 5722b681c64..c1c82b5f055 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -35,6 +35,7 @@ DIRS = cbmc \
        goto-ld \
        validate-trace-xml-schema \
        cbmc-primitives \
+       goto-interpreter \
        # Empty last line
 
 ifeq ($(OS),Windows_NT)
diff --git a/regression/goto-interpreter/CMakeLists.txt b/regression/goto-interpreter/CMakeLists.txt
new file mode 100644
index 00000000000..8b1e4b6ca39
--- /dev/null
+++ b/regression/goto-interpreter/CMakeLists.txt
@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> ${is_windows}"
+)
diff --git a/regression/goto-interpreter/Makefile b/regression/goto-interpreter/Makefile
new file mode 100644
index 00000000000..07b5e3c2690
--- /dev/null
+++ b/regression/goto-interpreter/Makefile
@@ -0,0 +1,35 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
+
+tests.log:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done
diff --git a/regression/goto-interpreter/byte_extract/main.c b/regression/goto-interpreter/byte_extract/main.c
new file mode 100644
index 00000000000..bd1cf3ee71f
--- /dev/null
+++ b/regression/goto-interpreter/byte_extract/main.c
@@ -0,0 +1,20 @@
+union U {
+  int x;
+  char c[sizeof(int)];
+};
+
+int main()
+{
+  union U u;
+  // make the lowest and highest byte 1
+  u.x = 1 | (1 << (sizeof(int) * 8 - 8));
+  int i = u.x;
+  char c0 = u.c[0];
+  char c1 = u.c[1];
+  char c2 = u.c[2];
+  char c3 = u.c[3];
+
+  __CPROVER_assert(u.c[0] == 1, "");
+
+  return 0;
+}
diff --git a/regression/goto-interpreter/byte_extract/test.desc b/regression/goto-interpreter/byte_extract/test.desc
new file mode 100644
index 00000000000..0888b32a645
--- /dev/null
+++ b/regression/goto-interpreter/byte_extract/test.desc
@@ -0,0 +1,13 @@
+KNOWNBUG
+main.c
+se
+^Starting interpreter$
+^\d+- Program End\.$
+^EXIT=0$
+^SIGNAL=0$
+--
+^assertion failed at \d+$
+--
+The memory model of the interpreter does not record individual bytes. Therefore,
+an access to individual bytes still yields the full object, making the assertion
+in this test spuriously fail.
diff --git a/regression/goto-interpreter/byte_extract/union.desc b/regression/goto-interpreter/byte_extract/union.desc
new file mode 100644
index 00000000000..4f4f713a8bb
--- /dev/null
+++ b/regression/goto-interpreter/byte_extract/union.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+se
+^Starting interpreter$
+^\d+- Program End\.$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/goto-interpreter/chain.sh b/regression/goto-interpreter/chain.sh
new file mode 100755
index 00000000000..d740a505aa7
--- /dev/null
+++ b/regression/goto-interpreter/chain.sh
@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+
+set -e
+
+goto_cc=$1
+goto_instrument=$2
+is_windows=$3
+
+options=${*:4:$#-4}
+name=${*:$#}
+base_name=${name%.c}
+
+if [[ "${is_windows}" == "true" ]]; then
+  "${goto_cc}" "${name}"
+  mv "${base_name}.exe" "${base_name}.gb"
+else
+  "${goto_cc}" "${name}" -o "${base_name}.gb"
+fi
+
+echo ${options} | tr , '\n' | "${goto_instrument}" --interpreter "${base_name}.gb"
diff --git a/regression/goto-interpreter/help-output/main.c b/regression/goto-interpreter/help-output/main.c
new file mode 100644
index 00000000000..f8b643afbf2
--- /dev/null
+++ b/regression/goto-interpreter/help-output/main.c
@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}
diff --git a/regression/goto-interpreter/help-output/test.desc b/regression/goto-interpreter/help-output/test.desc
new file mode 100644
index 00000000000..1613663c2da
--- /dev/null
+++ b/regression/goto-interpreter/help-output/test.desc
@@ -0,0 +1,19 @@
+CORE
+main.c
+h,q
+^Starting interpreter$
+^Interpreter help$
+^h: display this menu$
+^j: output json trace$
+^m: output memory dump$
+^o: output goto trace$
+^q: quit$
+^r: run up to entry point$
+^s#: step a number of instructions$
+^sa: step across a function$
+^so: step out of a function$
+^se: step until end of program$
+^\d+- Program End\.$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/goto-interpreter/memory-dump/main.c b/regression/goto-interpreter/memory-dump/main.c
new file mode 100644
index 00000000000..f8b643afbf2
--- /dev/null
+++ b/regression/goto-interpreter/memory-dump/main.c
@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}
diff --git a/regression/goto-interpreter/memory-dump/test.desc b/regression/goto-interpreter/memory-dump/test.desc
new file mode 100644
index 00000000000..be4e35a13e6
--- /dev/null
+++ b/regression/goto-interpreter/memory-dump/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+m
+^Starting interpreter$
+^__CPROVER_rounding_mode\[0\]=0$
+^\d+- Program End\.$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/goto-interpreter/step/main.c b/regression/goto-interpreter/step/main.c
new file mode 100644
index 00000000000..7ab98c582c1
--- /dev/null
+++ b/regression/goto-interpreter/step/main.c
@@ -0,0 +1,11 @@
+int main()
+{
+  __CPROVER_rounding_mode = 1;
+  // test single stepping
+  int i = 1;
+  i = 2;
+  i = 3;
+  int x;
+  __CPROVER_assert(x == 42, "should fail");
+  return 0;
+}
diff --git a/regression/goto-interpreter/step/r.desc b/regression/goto-interpreter/step/r.desc
new file mode 100644
index 00000000000..3772a56d954
--- /dev/null
+++ b/regression/goto-interpreter/step/r.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+r,q
+^Starting interpreter$
+^\d+- Program End\.$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/goto-interpreter/step/test.desc b/regression/goto-interpreter/step/test.desc
new file mode 100644
index 00000000000..ae084735a12
--- /dev/null
+++ b/regression/goto-interpreter/step/test.desc
@@ -0,0 +1,20 @@
+CORE
+main.c
+r0,s,sa,m,s2,m,s2,m,so,m,se
+^Starting interpreter$
+^__CPROVER_rounding_mode\[0\]=0$
+^__CPROVER_rounding_mode\[0\]=1$
+^main::1::i\[0\]=1$
+^\d+- Program End\.$
+^EXIT=0$
+^SIGNAL=0$
+--
+^main::1::i\[0\]=2$
+--
+Use the various step instructions: restart execution without running
+initialization (r0), execute one step (s), step over __CPROVER_initialize (sa),
+generate the first memory dump (__CPROVER_rounding_mode set to 0), step into
+main and execute the first assignment (__CPROVER_rounding_mode set to 1),
+execute two steps (s2) to declare i and assign 1 to i, step to the end of the
+function (so) without dumping intermittent values, thus never dumping i==2. The
+execute to the end of the program (se).
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 7733e4f0750..2f312dd5c46 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -41,6 +41,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/restrict_function_pointers.h>
+#include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
@@ -599,6 +600,9 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("interpreter"))
     {
+      do_indirect_call_and_rtti_removal();
+      rewrite_union(goto_model);
+
       log.status() << "Starting interpreter" << messaget::eom;
       interpreter(goto_model, ui_message_handler);
       return CPROVER_EXIT_SUCCESS;
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index c6030a22833..3b37abc856d 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -64,6 +64,8 @@ void interpretert::operator()()
 void interpretert::initialize(bool init)
 {
   build_memory_map();
+  // reset the call stack
+  call_stack = call_stackt{};
 
   total_steps=0;
   const goto_functionst::function_mapt::const_iterator
@@ -83,15 +85,20 @@ void interpretert::initialize(bool init)
   done=false;
   if(init)
   {
-    stack_depth=call_stack.size()+1;
-    show_state();
-    step();
-    while(!done && (stack_depth<=call_stack.size()) && (stack_depth!=npos))
+    // execute instructions up to and including __CPROVER_initialize()
+    while(!done && call_stack.size() == 0)
     {
       show_state();
       step();
     }
-    while(!done && (call_stack.size()==0))
+    // initialization
+    while(!done && call_stack.size() > 0)
+    {
+      show_state();
+      step();
+    }
+    // invoke the user entry point
+    while(!done && call_stack.size() == 0)
     {
       show_state();
       step();
@@ -140,18 +147,18 @@ void interpretert::command()
     done=true;
   else if(ch=='h')
   {
-    status()
-      << "Interpreter help\n"
-      << "h: display this menu\n"
-      << "j: output json trace\n"
-      << "m: output memory dump\n"
-      << "o: output goto trace\n"
-      << "q: quit\n"
-      << "r: run until completion\n"
-      << "s#: step a number of instructions\n"
-      << "sa: step across a function\n"
-      << "so: step out of a function\n"
-      << eom;
+    status() << "Interpreter help\n"
+             << "h: display this menu\n"
+             << "j: output json trace\n"
+             << "m: output memory dump\n"
+             << "o: output goto trace\n"
+             << "q: quit\n"
+             << "r: run up to entry point\n"
+             << "s#: step a number of instructions\n"
+             << "sa: step across a function\n"
+             << "so: step out of a function\n"
+             << "se: step until end of program\n"
+             << eom;
   }
   else if(ch=='j')
   {
@@ -200,7 +207,7 @@ void interpretert::command()
   else if((ch=='s') || (ch==0))
   {
     num_steps=1;
-    stack_depth=npos;
+    std::size_t stack_depth = npos;
     ch=tolower(command[1]);
     if(ch=='e')
       num_steps=npos;
@@ -210,7 +217,7 @@ void interpretert::command()
       stack_depth=call_stack.size()+1;
     else
     {
-      num_steps=safe_string2size_t(command+1);
+      num_steps = unsafe_string2size_t(command + 1);
       if(num_steps==0)
         num_steps=1;
     }
@@ -742,9 +749,7 @@ void interpretert::execute_assert()
 {
   if(!evaluate_boolean(pc->get_condition()))
   {
-    if((target_assert==pc) || stop_on_assertion)
-      throw "program assertion reached";
-    else if(show)
+    if(show)
       error() << "assertion failed at " << pc->location_number
               << "\n" << eom;
   }
@@ -860,6 +865,7 @@ void interpretert::execute_function_call()
 void interpretert::build_memory_map()
 {
   // put in a dummy for NULL
+  memory.clear();
   memory.resize(1);
   inverse_memory_map[0] = {};
 
@@ -1071,12 +1077,11 @@ void interpretert::print_memory(bool input_flags)
     const memory_cellt &cell=cell_address.second;
     const auto identifier = address_to_symbol(i).get_identifier();
     const auto offset=address_to_offset(i);
-    debug() << identifier << "[" << offset << "]"
-            << "=" << cell.value << eom;
+    status() << identifier << "[" << offset << "]"
+             << "=" << cell.value << eom;
     if(input_flags)
-      debug() << "(" << static_cast<int>(cell.initialized) << ")"
-              << eom;
-    debug() << eom;
+      status() << "(" << static_cast<int>(cell.initialized) << ")" << eom;
+    status() << eom;
   }
 }
 
diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h
index 78b54a4fe9d..49cff3755dd 100644
--- a/src/goto-programs/interpreter_class.h
+++ b/src/goto-programs/interpreter_class.h
@@ -30,14 +30,13 @@ class interpretert:public messaget
   interpretert(
     const symbol_tablet &_symbol_table,
     const goto_functionst &_goto_functions,
-    message_handlert &_message_handler):
-    messaget(_message_handler),
-    symbol_table(_symbol_table),
-    ns(_symbol_table),
-    goto_functions(_goto_functions),
-    stack_pointer(0),
-    done(false),
-    stop_on_assertion(false)
+    message_handlert &_message_handler)
+    : messaget(_message_handler),
+      symbol_table(_symbol_table),
+      ns(_symbol_table),
+      goto_functions(_goto_functions),
+      stack_pointer(0),
+      done(false)
   {
     show=true;
   }
@@ -265,18 +264,16 @@ class interpretert:public messaget
   list_input_varst function_input_vars;
 
   goto_functionst::function_mapt::const_iterator function;
-  goto_programt::const_targett pc, next_pc, target_assert;
+  goto_programt::const_targett pc, next_pc;
   goto_tracet steps;
   bool done;
   bool show;
-  bool stop_on_assertion;
   static const size_t npos;
   size_t num_steps;
   size_t total_steps;
 
   dynamic_typest dynamic_types;
   int num_dynamic_objects;
-  mp_integer stack_depth;
   unsigned thread_id;
 
   bool evaluate_boolean(const exprt &expr)
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index f4c7cd784d8..c9c97084ad9 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -857,41 +857,11 @@ void interpretert::evaluate(
     }
     return;
   }
-  else if(expr.id()==ID_byte_extract_little_endian ||
-          expr.id()==ID_byte_extract_big_endian)
-  {
-    const auto &byte_extract_expr = to_byte_extract_expr(expr);
-
-    mp_vectort extract_offset;
-    evaluate(byte_extract_expr.op1(), extract_offset);
-    mp_vectort extract_from;
-    evaluate(byte_extract_expr.op0(), extract_from);
-
-    if(extract_offset.size()==1 && extract_from.size()!=0)
-    {
-      const typet &target_type=expr.type();
-      mp_integer memory_offset;
-      // If memory offset is found (which should normally be the case)
-      // extract the corresponding data from the appropriate memory location
-      if(!byte_offset_to_memory_offset(
-           byte_extract_expr.op0().type(), extract_offset[0], memory_offset))
-      {
-        mp_integer target_type_leaves;
-        if(!count_type_leaves(target_type, target_type_leaves) &&
-           target_type_leaves>0)
-        {
-          dest.insert(dest.end(),
-            extract_from.begin()+memory_offset.to_long(),
-            extract_from.begin()+(memory_offset+target_type_leaves).to_long());
-          return;
-        }
-      }
-    }
-  }
-  else if(expr.id()==ID_dereference ||
-          expr.id()==ID_index ||
-          expr.id()==ID_symbol ||
-          expr.id()==ID_member)
+  else if(
+    expr.id() == ID_dereference || expr.id() == ID_index ||
+    expr.id() == ID_symbol || expr.id() == ID_member ||
+    expr.id() == ID_byte_extract_little_endian ||
+    expr.id() == ID_byte_extract_big_endian)
   {
     mp_integer address=evaluate_address(
       expr,
@@ -932,16 +902,45 @@ void interpretert::evaluate(
     }
     else if(!address.is_zero())
     {
-      if(!unbounded_size(expr.type()))
+      if(
+        expr.id() == ID_byte_extract_little_endian ||
+        expr.id() == ID_byte_extract_big_endian)
+      {
+        const auto &byte_extract_expr = to_byte_extract_expr(expr);
+
+        mp_vectort extract_from;
+        evaluate(byte_extract_expr.op(), extract_from);
+        INVARIANT(
+          !extract_from.empty(),
+          "evaluate_address should have returned address == 0");
+        const mp_integer memory_offset =
+          address - evaluate_address(byte_extract_expr.op(), true);
+        const typet &target_type = expr.type();
+        mp_integer target_type_leaves;
+        if(
+          !count_type_leaves(target_type, target_type_leaves) &&
+          target_type_leaves > 0)
+        {
+          dest.insert(
+            dest.end(),
+            extract_from.begin() + numeric_cast_v<std::size_t>(memory_offset),
+            extract_from.begin() +
+              numeric_cast_v<std::size_t>(memory_offset + target_type_leaves));
+          return;
+        }
+        // we fail
+      }
+      else if(!unbounded_size(expr.type()))
       {
         dest.resize(numeric_cast_v<std::size_t>(get_size(expr.type())));
         read(address, dest);
+        return;
       }
       else
       {
         read_unbounded(address, dest);
+        return;
       }
-      return;
     }
   }
   else if(expr.id()==ID_typecast)
diff --git a/src/util/sparse_vector.h b/src/util/sparse_vector.h
index 0b8332400a7..df2f3de289c 100644
--- a/src/util/sparse_vector.h
+++ b/src/util/sparse_vector.h
@@ -51,6 +51,12 @@ template<class T> class sparse_vectort
     _size=new_size;
   }
 
+  void clear()
+  {
+    underlying.clear();
+    _size = 0;
+  }
+
   typedef typename underlyingt::iterator iteratort;
   typedef typename underlyingt::const_iterator const_iteratort;