diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp
index f64071ec617..043ac0fb05c 100644
--- a/src/path-symex/path_symex.cpp
+++ b/src/path-symex/path_symex.cpp
@@ -422,6 +422,14 @@ void path_symext::assign_rec(
       var_state.value=propagate(ssa_rhs)?ssa_rhs:nil_exprt();
     }
   }
+  else if(ssa_lhs.id()==ID_typecast)
+  {
+    // dereferencing might yield a typecast
+    const exprt &new_lhs=to_typecast_expr(ssa_lhs).op();
+    typecast_exprt new_rhs(ssa_rhs, new_lhs.type());
+
+    assign_rec(state, guard, new_lhs, new_rhs);
+  }
   else if(ssa_lhs.id()==ID_member)
   {
     #ifdef DEBUG
@@ -541,14 +549,30 @@ void path_symext::assign_rec(
 
     assert(operands.size()==components.size());
 
-    for(std::size_t i=0; i<components.size(); i++)
+    if(ssa_rhs.id()==ID_struct &&
+       ssa_rhs.operands().size()==components.size())
     {
-      exprt new_rhs=
-        ssa_rhs.is_nil()?ssa_rhs:
-        simplify_expr(
-          member_exprt(ssa_rhs, components[i].get_name(), components[i].type()),
-          state.var_map.ns);
-      assign_rec(state, guard, operands[i], new_rhs);
+      exprt::operandst::const_iterator lhs_it=operands.begin();
+      forall_operands(it, ssa_rhs)
+      {
+        assign_rec(state, guard, *lhs_it, *it);
+        ++lhs_it;
+      }
+    }
+    else
+    {
+      for(std::size_t i=0; i<components.size(); i++)
+      {
+        exprt new_rhs=
+          ssa_rhs.is_nil()?ssa_rhs:
+          simplify_expr(
+            member_exprt(
+              ssa_rhs,
+              components[i].get_name(),
+              components[i].type()),
+            state.var_map.ns);
+        assign_rec(state, guard, operands[i], new_rhs);
+      }
     }
   }
   else if(ssa_lhs.id()==ID_array)
@@ -564,36 +588,30 @@ void path_symext::assign_rec(
     const exprt::operandst &operands=ssa_lhs.operands();
 
     // split up into elements
-    for(std::size_t i=0; i<operands.size(); i++)
+    if(ssa_rhs.id()==ID_array &&
+       ssa_rhs.operands().size()==operands.size())
     {
-      exprt new_rhs=
-        ssa_rhs.is_nil()?ssa_rhs:
-        simplify_expr(
-          index_exprt(
-            ssa_rhs,
-            from_integer(i, index_type()), array_type.subtype()),
-          state.var_map.ns);
-      assign_rec(state, guard, operands[i], new_rhs);
+      exprt::operandst::const_iterator lhs_it=operands.begin();
+      forall_operands(it, ssa_rhs)
+      {
+        assign_rec(state, guard, *lhs_it, *it);
+        ++lhs_it;
+      }
     }
-  }
-  else if(ssa_lhs.id()==ID_vector)
-  {
-    const vector_typet &vector_type=
-      to_vector_type(state.var_map.ns.follow(ssa_lhs.type()));
-
-    const exprt::operandst &operands=ssa_lhs.operands();
-
-    // split up into elements
-    for(std::size_t i=0; i<operands.size(); i++)
+    else
     {
-      exprt new_rhs=
-        ssa_rhs.is_nil()?ssa_rhs:
-        simplify_expr(
-          index_exprt(
-            ssa_rhs,
-            from_integer(i, index_type()), vector_type.subtype()),
-          state.var_map.ns);
-      assign_rec(state, guard, operands[i], new_rhs);
+      for(std::size_t i=0; i<operands.size(); i++)
+      {
+        exprt new_rhs=
+          ssa_rhs.is_nil()?ssa_rhs:
+          simplify_expr(
+            index_exprt(
+              ssa_rhs,
+              from_integer(i, index_type()),
+              array_type.subtype()),
+            state.var_map.ns);
+        assign_rec(state, guard, operands[i], new_rhs);
+      }
     }
   }
   else if(ssa_lhs.id()==ID_string_constant ||
diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp
index 495f598202a..fe663da5b7c 100644
--- a/src/path-symex/path_symex_state.cpp
+++ b/src/path-symex/path_symex_state.cpp
@@ -41,12 +41,6 @@ path_symex_statet initial_state(
   return s;
 }
 
-loc_reft path_symex_statet::get_pc() const
-{
-  assert(current_thread<threads.size());
-  return threads[current_thread].pc;
-}
-
 void path_symex_statet::output(const threadt &thread, std::ostream &out) const
 {
   out << "  PC: " << thread.pc << '\n';
diff --git a/src/path-symex/path_symex_state.h b/src/path-symex/path_symex_state.h
index eb23e891f83..bb6fc91187a 100644
--- a/src/path-symex/path_symex_state.h
+++ b/src/path-symex/path_symex_state.h
@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H
 #define CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H
 
+#include <util/invariant.h>
+
 #include "locs.h"
 #include "var_map.h"
 #include "path_symex_history.h"
@@ -111,11 +113,9 @@ struct path_symex_statet
     current_thread=_thread;
   }
 
-  loc_reft get_pc() const;
-
   goto_programt::const_targett get_instruction() const
   {
-    return locs[get_pc()].target;
+    return locs[pc()].target;
   }
 
   bool is_executable() const
@@ -145,6 +145,7 @@ struct path_symex_statet
 
   loc_reft pc() const
   {
+    PRECONDITION(current_thread<threads.size());
     return threads[current_thread].pc;
   }
 
diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp
index 87dea21be4a..06a7f10f59d 100644
--- a/src/path-symex/path_symex_state_read.cpp
+++ b/src/path-symex/path_symex_state_read.cpp
@@ -247,7 +247,14 @@ exprt path_symex_statet::instantiate_rec(
     {
       irep_idt id="symex::nondet"+std::to_string(var_map.nondet_count);
       var_map.nondet_count++;
-      return symbol_exprt(id, src.type());
+
+      auxiliary_symbolt nondet_symbol;
+      nondet_symbol.name=id;
+      nondet_symbol.base_name=id;
+      nondet_symbol.type=src.type();
+      var_map.new_symbols.add(nondet_symbol);
+
+      return nondet_symbol.symbol_expr();
     }
     else
       throw "instantiate_rec: unexpected side effect "+id2string(statement);
diff --git a/src/path-symex/var_map.h b/src/path-symex/var_map.h
index 7b17169c441..09511174cab 100644
--- a/src/path-symex/var_map.h
+++ b/src/path-symex/var_map.h
@@ -18,12 +18,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/namespace.h>
 #include <util/type.h>
 #include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 class var_mapt
 {
 public:
   explicit var_mapt(const namespacet &_ns):
-    ns(_ns), shared_count(0), local_count(0), nondet_count(0), dynamic_count(0)
+    ns(_ns.get_symbol_table(), new_symbols),
+    shared_count(0),
+    local_count(0),
+    nondet_count(0),
+    dynamic_count(0)
   {
   }
 
@@ -93,7 +98,8 @@ class var_mapt
 
   void init(var_infot &var_info);
 
-  const namespacet &ns;
+  const namespacet ns;
+  symbol_tablet new_symbols;
 
   void output(std::ostream &) const;
 
diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp
index 6b03b163fa5..b6743063401 100644
--- a/src/symex/path_search.cpp
+++ b/src/symex/path_search.cpp
@@ -68,9 +68,9 @@ path_searcht::resultt path_searcht::operator()(
       statet &state=tmp_queue.front();
 
       // record we have seen it
-      loc_data[state.get_pc().loc_number].visited=true;
+      loc_data[state.pc().loc_number].visited=true;
 
-      debug() << "Loc: #" << state.get_pc().loc_number
+      debug() << "Loc: #" << state.pc().loc_number
               << ", queue: " << queue.size()
               << ", depth: " << state.get_depth();
       for(const auto &s : queue)
@@ -102,10 +102,13 @@ path_searcht::resultt path_searcht::operator()(
 
       if(number_of_steps%1000==0)
       {
+        time_periodt running_time=current_time()-start_time;
         status() << "Queue " << queue.size()
-                 << " thread " << state.get_current_thread()
+                 << " thread " << state.get_current_thread()+1
                  << '/' << state.threads.size()
-                 << " PC " << state.pc() << messaget::eom;
+                 << " PC " << state.pc()
+                 << " [" << number_of_steps << " steps, "
+                 << running_time << "s]" << messaget::eom;
       }
 
       // an error, possibly?
@@ -264,34 +267,90 @@ bool path_searcht::drop_state(const statet &state)
 {
   goto_programt::const_targett pc=state.get_instruction();
 
+  const source_locationt &source_location=pc->source_location;
+
+  if(!source_location.is_nil() &&
+     last_source_location!=source_location)
+  {
+    debug() << "SYMEX at file " << source_location.get_file()
+            << " line " << source_location.get_line()
+            << " function " << source_location.get_function()
+            << eom;
+
+    last_source_location=source_location;
+  }
+
   // depth limit
-  if(depth_limit_set && state.get_depth()>depth_limit)
+  if(depth_limit>=0 && state.get_depth()>depth_limit)
     return true;
 
   // context bound
-  if(context_bound_set && state.get_no_thread_interleavings()>context_bound)
+  if(context_bound>=0 && state.get_no_thread_interleavings()>context_bound)
     return true;
 
   // branch bound
-  if(branch_bound_set && state.get_no_branches()>branch_bound)
+  if(branch_bound>=0 && state.get_no_branches()>branch_bound)
     return true;
 
   // unwinding limit -- loops
-  if(unwind_limit_set && state.get_instruction()->is_backwards_goto())
+  if(unwind_limit>=0 && pc->is_backwards_goto())
   {
+    bool stop=false;
+
     for(const auto &loop_info : state.unwinding_map)
       if(loop_info.second>unwind_limit)
-        return true;
+      {
+        stop=true;
+        break;
+      }
+
+    const irep_idt id=goto_programt::loop_id(pc);
+    path_symex_statet::unwinding_mapt::const_iterator entry=
+      state.unwinding_map.find(state.pc());
+    debug() << (stop?"Not unwinding":"Unwinding")
+      << " loop " << id << " iteration "
+      << (entry==state.unwinding_map.end()?-1:entry->second)
+      << " (" << unwind_limit << " max)"
+      << " " << source_location
+      << " thread " << state.get_current_thread() << eom;
+
+    if(stop)
+      return true;
   }
 
   // unwinding limit -- recursion
-  if(unwind_limit_set && state.get_instruction()->is_function_call())
+  if(unwind_limit>=0 && pc->is_function_call())
   {
+    bool stop=false;
+
     for(const auto &rec_info : state.recursion_map)
       if(rec_info.second>unwind_limit)
-        return true;
+      {
+        stop=true;
+        break;
+      }
+
+    exprt function=to_code_function_call(pc->code).function();
+    const irep_idt id=function.get(ID_identifier); // could be nil
+    path_symex_statet::recursion_mapt::const_iterator entry=
+      state.recursion_map.find(id);
+    if(entry!=state.recursion_map.end())
+      debug() << (stop?"Not unwinding":"Unwinding")
+        << " recursion " << id << " iteration "
+        << entry->second
+        << " (" << unwind_limit << " max)"
+        << " " << source_location
+        << " thread " << state.get_current_thread() << eom;
+
+    if(stop)
+      return true;
   }
 
+  // search time limit (--max-search-time)
+  if(time_limit>=0 &&
+     current_time().get_t()>start_time.get_t()+time_limit*1000)
+    return true;
+
   if(pc->is_assume() &&
      simplify_expr(pc->guard, ns).is_false())
   {
diff --git a/src/symex/path_search.h b/src/symex/path_search.h
index ca570819cc8..4823998ef8a 100644
--- a/src/symex/path_search.h
+++ b/src/symex/path_search.h
@@ -26,10 +26,11 @@ class path_searcht:public safety_checkert
     safety_checkert(_ns),
     show_vcc(false),
     eager_infeasibility(false),
-    depth_limit_set(false), // no limit
-    context_bound_set(false),
-    unwind_limit_set(false),
-    branch_bound_set(false),
+    depth_limit(-1), // no limit
+    context_bound(-1),
+    branch_bound(-1),
+    unwind_limit(-1),
+    time_limit(-1),
     search_heuristic(search_heuristict::DFS)
   {
   }
@@ -37,42 +38,43 @@ class path_searcht:public safety_checkert
   virtual resultt operator()(
     const goto_functionst &goto_functions);
 
-  void set_depth_limit(unsigned limit)
+  void set_depth_limit(int limit)
   {
-    depth_limit_set=true;
     depth_limit=limit;
   }
 
-  void set_context_bound(unsigned limit)
+  void set_context_bound(int limit)
   {
-    context_bound_set=true;
     context_bound=limit;
   }
 
-  void set_branch_bound(unsigned limit)
+  void set_branch_bound(int limit)
   {
-    branch_bound_set=true;
     branch_bound=limit;
   }
 
-  void set_unwind_limit(unsigned limit)
+  void set_unwind_limit(int limit)
   {
-    unwind_limit_set=true;
     unwind_limit=limit;
   }
 
+  void set_time_limit(int limit)
+  {
+    time_limit=limit;
+  }
+
   bool show_vcc;
   bool eager_infeasibility;
 
   // statistics
-  unsigned number_of_dropped_states;
-  unsigned number_of_paths;
-  unsigned number_of_steps;
-  unsigned number_of_feasible_paths;
-  unsigned number_of_infeasible_paths;
-  unsigned number_of_VCCs;
-  unsigned number_of_VCCs_after_simplification;
-  unsigned number_of_failed_properties;
+  std::size_t number_of_dropped_states;
+  std::size_t number_of_paths;
+  std::size_t number_of_steps;
+  std::size_t number_of_feasible_paths;
+  std::size_t number_of_infeasible_paths;
+  std::size_t number_of_VCCs;
+  std::size_t number_of_VCCs_after_simplification;
+  std::size_t number_of_failed_properties;
   std::size_t number_of_locs;
   absolute_timet start_time;
   time_periodt sat_time;
@@ -130,13 +132,15 @@ class path_searcht:public safety_checkert
   void initialize_property_map(
     const goto_functionst &goto_functions);
 
-  unsigned depth_limit;
-  unsigned context_bound;
-  unsigned branch_bound;
-  unsigned unwind_limit;
-  bool depth_limit_set, context_bound_set, unwind_limit_set, branch_bound_set;
+  int depth_limit;
+  int context_bound;
+  int branch_bound;
+  int unwind_limit;
+  int time_limit;
 
   enum class search_heuristict { DFS, BFS, LOCS } search_heuristic;
+
+  source_locationt last_source_location;
 };
 
 #endif // CPROVER_SYMEX_PATH_SEARCH_H
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 5fc475ee154..c2e567cc643 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -36,6 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/xml_goto_trace.h>
 #include <goto-programs/remove_complex.h>
+#include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_exceptions.h>
@@ -186,6 +187,10 @@ int symex_parse_optionst::doit()
       path_search.set_unwind_limit(
         unsafe_string2unsigned(cmdline.get_value("unwind")));
 
+    if(cmdline.isset("max-search-time"))
+      path_search.set_time_limit(
+        safe_string2unsigned(cmdline.get_value("max-search-time")));
+
     if(cmdline.isset("dfs"))
       path_search.set_dfs();
 
@@ -300,6 +305,12 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     // remove stuff
     remove_complex(goto_model);
     remove_vector(goto_model);
+    // remove function pointers
+    status() << "Removal of function pointers and virtual functions" << eom;
+    remove_function_pointers(
+      get_message_handler(),
+      goto_model,
+      cmdline.isset("pointer-check"));
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
     // Java throw and catch -> explicit exceptional return variables:
@@ -607,6 +618,7 @@ void symex_parse_optionst::help()
     " --depth nr                   limit search depth\n"
     " --context-bound nr           limit number of context switches\n"
     " --branch-bound nr            limit number of branches taken\n"
+    " --max-search-time s          limit search to approximately s seconds\n"
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index b4fc6fe2e1c..a9f3d9e3e83 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -30,7 +30,7 @@ class optionst;
 #define SYMEX_OPTIONS \
   "(function):" \
   "D:I:" \
-  "(depth):(context-bound):(branch-bound):(unwind):" \
+  "(depth):(context-bound):(branch-bound):(unwind):(max-search-time):" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \