diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index f9ede133877..9b8e2e4500c 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -45,6 +45,17 @@ void bmct::do_unwind_module()
   // this is a hook for hw-cbmc
 }
 
+/// Hook used by CEGIS to selectively freeze variables
+/// in the SAT solver after the SSA formula is added to the solver.
+/// Freezing variables is necessary to make use of incremental
+/// solving with MiniSat SimpSolver.
+/// Potentially a useful hook for other applications using
+/// incremental solving.
+void bmct::freeze_program_variables()
+{
+  // this is a hook for cegis
+}
+
 void bmct::error_trace()
 {
   status() << "Building error trace" << eom;
@@ -131,6 +142,8 @@ void bmct::do_conversion()
     forall_expr_list(it, bmc_constraints)
       prop_conv.set_to_true(*it);
   }
+  // hook for cegis to freeze synthesis program vars
+  freeze_program_variables();
 }
 
 decision_proceduret::resultt
@@ -305,11 +318,10 @@ void bmct::show_program()
   }
 }
 
-safety_checkert::resultt bmct::run(
-  const goto_functionst &goto_functions)
+
+void bmct::get_memory_model()
 {
   const std::string mm=options.get_option("mm");
-  std::unique_ptr<memory_model_baset> memory_model;
 
   if(mm.empty() || mm=="sc")
     memory_model=util_make_unique<memory_model_sct>(ns);
@@ -321,9 +333,13 @@ safety_checkert::resultt bmct::run(
   {
     error() << "Invalid memory model " << mm
             << " -- use one of sc, tso, pso" << eom;
-    return safety_checkert::resultt::ERROR;
+    throw "invalid memory model";
   }
+}
 
+void bmct::setup()
+{
+  get_memory_model();
   symex.set_message_handler(get_message_handler());
   symex.options=options;
 
@@ -337,11 +353,13 @@ safety_checkert::resultt bmct::run(
 
   symex.last_source_location.make_nil();
 
-  try
-  {
-    // get unwinding info
     setup_unwind();
+}
 
+safety_checkert::resultt bmct::execute(const goto_functionst &goto_functions)
+{
+  try
+  {
     // perform symbolic execution
     symex(goto_functions);
 
@@ -351,77 +369,12 @@ safety_checkert::resultt bmct::run(
       memory_model->set_message_handler(get_message_handler());
       (*memory_model)(equation);
     }
-  }
-
-  catch(const std::string &error_str)
-  {
-    messaget message(get_message_handler());
-    message.error().source_location=symex.last_source_location;
-    message.error() << error_str << messaget::eom;
-
-    return safety_checkert::resultt::ERROR;
-  }
-
-  catch(const char *error_str)
-  {
-    messaget message(get_message_handler());
-    message.error().source_location=symex.last_source_location;
-    message.error() << error_str << messaget::eom;
-
-    return safety_checkert::resultt::ERROR;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    return safety_checkert::resultt::ERROR;
-  }
 
   statistics() << "size of program expression: "
                << equation.SSA_steps.size()
                << " steps" << eom;
 
-  try
-  {
-    if(options.get_option("slice-by-trace")!="")
-    {
-      symex_slice_by_tracet symex_slice_by_trace(ns);
-
-      symex_slice_by_trace.slice_by_trace
-        (options.get_option("slice-by-trace"), equation);
-    }
-
-    if(equation.has_threads())
-    {
-      // we should build a thread-aware SSA slicer
-      statistics() << "no slicing due to threads" << eom;
-    }
-    else
-    {
-      if(options.get_bool_option("slice-formula"))
-      {
-        slice(equation);
-        statistics() << "slicing removed "
-                     << equation.count_ignored_SSA_steps()
-                     << " assignments" << eom;
-      }
-      else
-      {
-        if(options.get_list_option("cover").empty())
-        {
-          simple_slice(equation);
-          statistics() << "simple slicing removed "
-                       << equation.count_ignored_SSA_steps()
-                       << " assignments" << eom;
-        }
-      }
-    }
-
-    {
-      statistics() << "Generated " << symex.total_vccs
-                   << " VCC(s), " << symex.remaining_vccs
-                   << " remaining after simplification" << eom;
-    }
+    slice();
 
     // coverage report
     std::string cov_out=options.get_option("symex-coverage-report");
@@ -473,13 +426,19 @@ safety_checkert::resultt bmct::run(
 
   catch(const std::string &error_str)
   {
-    error() << error_str << eom;
+    messaget message(get_message_handler());
+    message.error().source_location=symex.last_source_location;
+    message.error() << error_str << messaget::eom;
+
     return safety_checkert::resultt::ERROR;
   }
 
   catch(const char *error_str)
   {
-    error() << error_str << eom;
+    messaget message(get_message_handler());
+    message.error().source_location=symex.last_source_location;
+    message.error() << error_str << messaget::eom;
+
     return safety_checkert::resultt::ERROR;
   }
 
@@ -490,6 +449,56 @@ safety_checkert::resultt bmct::run(
   }
 }
 
+void bmct::slice()
+{
+  if(options.get_option("slice-by-trace")!="")
+  {
+    symex_slice_by_tracet symex_slice_by_trace(ns);
+
+    symex_slice_by_trace.slice_by_trace
+    (options.get_option("slice-by-trace"),
+        equation);
+  }
+  // any properties to check at all?
+  if(equation.has_threads())
+  {
+    // we should build a thread-aware SSA slicer
+    statistics() << "no slicing due to threads" << eom;
+  }
+  else
+  {
+    if(options.get_bool_option("slice-formula"))
+    {
+      ::slice(equation);
+      statistics() << "slicing removed "
+                   << equation.count_ignored_SSA_steps()
+                   << " assignments"<<eom;
+    }
+    else
+    {
+      if(options.get_list_option("cover").empty())
+      {
+        simple_slice(equation);
+        statistics() << "simple slicing removed "
+                     << equation.count_ignored_SSA_steps()
+                     << " assignments"<<eom;
+      }
+    }
+  }
+  statistics() << "Generated "
+               << symex.total_vccs<<" VCC(s), "
+               << symex.remaining_vccs
+               << " remaining after simplification" << eom;
+}
+
+safety_checkert::resultt bmct::run(
+  const goto_functionst &goto_functions)
+{
+  setup();
+
+  return execute(goto_functions);
+}
+
 safety_checkert::resultt bmct::decide(
   const goto_functionst &goto_functions,
   prop_convt &prop_conv)
@@ -502,6 +511,19 @@ safety_checkert::resultt bmct::decide(
     return all_properties(goto_functions, prop_conv);
 }
 
+void bmct::show(const goto_functionst &goto_functions)
+{
+  if(options.get_bool_option("show-vcc"))
+  {
+    show_vcc();
+  }
+
+  if(options.get_bool_option("program-only"))
+  {
+    show_program();
+  }
+}
+
 safety_checkert::resultt bmct::stop_on_fail(
   const goto_functionst &goto_functions,
   prop_convt &prop_conv)
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index c1896935460..c81ee66e74b 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-symex/symex_target_equation.h>
 #include <goto-programs/safety_checker.h>
+#include <goto-symex/memory_model.h>
 
 #include "symex_bmc.h"
 
@@ -52,6 +53,8 @@ class bmct:public safety_checkert
   }
 
   virtual resultt run(const goto_functionst &goto_functions);
+  void setup();
+  safety_checkert::resultt execute(const goto_functionst &);
   virtual ~bmct() { }
 
   // additional stuff
@@ -73,7 +76,7 @@ class bmct:public safety_checkert
   symex_target_equationt equation;
   symex_bmct symex;
   prop_convt &prop_conv;
-
+  std::unique_ptr<memory_model_baset> memory_model;
   // use gui format
   ui_message_handlert::uit ui;
 
@@ -89,6 +92,8 @@ class bmct:public safety_checkert
   virtual void do_unwind_module();
   void do_conversion();
 
+  virtual void freeze_program_variables();
+
   virtual void show_vcc();
   virtual void show_vcc_plain(std::ostream &out);
   virtual void show_vcc_json(std::ostream &out);
@@ -108,6 +113,10 @@ class bmct:public safety_checkert
     resultt result,
     const goto_functionst &goto_functions);
 
+  void get_memory_model();
+  void slice();
+  void show(const goto_functionst &);
+
   bool cover(
     const goto_functionst &goto_functions,
     const optionst::value_listt &criteria);
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 096c4766377..5535791e0aa 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -80,6 +80,40 @@ class goto_symext
     const goto_functionst &goto_functions,
     const goto_programt &goto_program);
 
+  /// Symexes from the first instruction and the given state, terminating as
+  /// soon as the last instruction is reached.  This is useful to explicitly
+  /// symex certain ranges of a program, e.g. in an incremental decision
+  /// procedure.
+  /// \param state Symex state to start with.
+  /// \param goto_functions GOTO model to symex.
+  /// \param first Entry point in form of a first instruction.
+  /// \param limit Final instruction, which itself will not be symexed.
+  virtual void operator()(
+    statet &state,
+    const goto_functionst &goto_functions,
+    goto_programt::const_targett first,
+    goto_programt::const_targett limit);
+
+  /// Initialise the symbolic execution and the given state with <code>pc</code>
+  /// as entry point.
+  /// \param state Symex state to initialise.
+  /// \param goto_functions GOTO model to symex.
+  /// \param pc first instruction to symex
+  /// \param limit final instruction, which itself will not
+  /// be symexed.
+  void symex_entry_point(
+    statet &state,
+    const goto_functionst &goto_functions,
+    goto_programt::const_targett pc,
+    goto_programt::const_targett limit);
+
+  /// Invokes symex_step and verifies whether additional threads can be
+  /// executed.
+  /// \param state Current GOTO symex step.
+  /// \param goto_functions GOTO model to symex.
+  void symex_threaded_step(
+    statet &state, const goto_functionst &goto_functions);
+
   /** execute just one step */
   virtual void symex_step(
     const goto_functionst &goto_functions,
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 3deef4ae22c..787775c23a0 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -114,8 +114,8 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
   {
     // forall X. P -> P
     // we keep the quantified variable unique by means of L2 renaming
-    assert(expr.operands().size()==2);
-    assert(expr.op0().id()==ID_symbol);
+    PRECONDITION(expr.operands().size()==2);
+    PRECONDITION(expr.op0().id()==ID_symbol);
     symbol_exprt tmp0=
       to_symbol_expr(to_ssa_expr(expr.op0()).get_original_expr());
     symex_decl(state, tmp0);
@@ -124,44 +124,72 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
   }
 }
 
-/// symex from given state
-void goto_symext::operator()(
+void goto_symext::symex_entry_point(
   statet &state,
   const goto_functionst &goto_functions,
-  const goto_programt &goto_program)
+  const goto_programt::const_targett pc,
+  const goto_programt::const_targett limit)
 {
-  assert(!goto_program.instructions.empty());
-
-  state.source=symex_targett::sourcet(goto_program);
-  assert(!state.threads.empty());
-  assert(!state.call_stack().empty());
-  state.top().end_of_function=--goto_program.instructions.end();
+  PRECONDITION(!state.threads.empty());
+  PRECONDITION(!state.call_stack().empty());
+  state.source=symex_targett::sourcet(pc);
+  state.top().end_of_function=limit;
   state.top().calling_location.pc=state.top().end_of_function;
   state.symex_target=&target;
   state.dirty=util_make_unique<dirtyt>(goto_functions);
 
   symex_transition(state, state.source.pc);
+}
 
-  assert(state.top().end_of_function->is_end_function());
+void goto_symext::symex_threaded_step(
+  statet &state, const goto_functionst &goto_functions)
+{
+  symex_step(goto_functions, state);
 
-  while(!state.call_stack().empty())
+  // is there another thread to execute?
+  if(state.call_stack().empty() &&
+     state.source.thread_nr+1<state.threads.size())
   {
-    symex_step(goto_functions, state);
-
-    // is there another thread to execute?
-    if(state.call_stack().empty() &&
-       state.source.thread_nr+1<state.threads.size())
-    {
-      unsigned t=state.source.thread_nr+1;
-      // std::cout << "********* Now executing thread " << t << '\n';
-      state.switch_to_thread(t);
-      symex_transition(state, state.source.pc);
-    }
+    unsigned t=state.source.thread_nr+1;
+#if 0
+    std::cout << "********* Now executing thread " << t << '\n';
+#endif
+    state.switch_to_thread(t);
+    symex_transition(state, state.source.pc);
   }
+}
+
+/// symex from given state
+void goto_symext::operator()(
+  statet &state,
+  const goto_functionst &goto_functions,
+  const goto_programt &goto_program)
+{
+  PRECONDITION(!goto_program.instructions.empty());
+  symex_entry_point(
+    state,
+    goto_functions,
+    goto_program.instructions.begin(),
+    prev(goto_program.instructions.end()));
+  PRECONDITION(state.top().end_of_function->is_end_function());
+
+  while(!state.call_stack().empty())
+    symex_threaded_step(state, goto_functions);
 
   state.dirty=nullptr;
 }
 
+void goto_symext::operator()(
+  statet &state,
+  const goto_functionst &goto_functions,
+  const goto_programt::const_targett first,
+  const goto_programt::const_targett limit)
+{
+  symex_entry_point(state, goto_functions, first, limit);
+  while(state.source.pc->function!=limit->function || state.source.pc!=limit)
+    symex_threaded_step(state, goto_functions);
+}
+
 /// symex starting from given program
 void goto_symext::operator()(
   const goto_functionst &goto_functions,
@@ -197,8 +225,8 @@ void goto_symext::symex_step(
   std::cout << "Code: " << from_expr(ns, "", state.source.pc->code) << '\n';
   #endif
 
-  assert(!state.threads.empty());
-  assert(!state.call_stack().empty());
+  PRECONDITION(!state.threads.empty());
+  PRECONDITION(!state.call_stack().empty());
 
   const goto_programt::instructiont &instruction=*state.source.pc;