diff --git a/src/analyses/Makefile b/src/analyses/Makefile
index 690b119e83c..9be0609687f 100644
--- a/src/analyses/Makefile
+++ b/src/analyses/Makefile
@@ -22,7 +22,6 @@ SRC = ai.cpp \
       locals.cpp \
       natural_loops.cpp \
       reaching_definitions.cpp \
-      replace_symbol_ext.cpp \
       static_analysis.cpp \
       uninitialized_domain.cpp \
       # Empty last line
diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index 1eca272c19d..dfde5bd401f 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -37,7 +37,7 @@ xmlt ai_domain_baset::output_xml(
 {
   std::ostringstream out;
   output(out, ai, ns);
-  xmlt xml("domain");
+  xmlt xml("abstract_state");
   xml.data=out.str();
   return xml;
 }
@@ -166,7 +166,7 @@ jsont ai_baset::output_json(
       json_numbert(std::to_string(i_it->location_number));
     location["sourceLocation"]=
       json_stringt(i_it->source_location.as_string());
-    location["domain"]=find_state(i_it).output_json(*this, ns);
+    location["abstractState"]=find_state(i_it).output_json(*this, ns);
 
     // Ideally we need output_instruction_json
     std::ostringstream out;
@@ -427,7 +427,12 @@ bool ai_baset::do_function_call(
     assert(l_end->is_end_function());
 
     // do edge from end of function to instruction after call
-    std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_end)));
+    const statet &end_state=get_state(l_end);
+
+    if(end_state.is_bottom())
+      return false; // function exit point not reachable
+
+    std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
     tmp_state->transform(l_end, l_return, *this, ns);
 
     // Propagate those
diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index 3c078d2a9bb..eca4feb1d80 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -78,6 +78,10 @@ class ai_domain_baset
   // a reasonable entry-point state
   virtual void make_entry()=0;
 
+  virtual bool is_bottom() const=0;
+
+  virtual bool is_top() const=0;
+
   // also add
   //
   //   bool merge(const T &b, locationt from, locationt to);
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 15cda33e864..e1e22baaee8 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -1,6 +1,6 @@
 /*******************************************************************\
 
-Module: Constant Propagation
+Module: Constant propagation
 
 Author: Peter Schrammel
 
@@ -16,109 +16,29 @@ Author: Peter Schrammel
 #include <util/find_symbols.h>
 #include <util/arith_tools.h>
 #include <util/simplify_expr.h>
+#include <util/cprover_prefix.h>
 
 #include "constant_propagator.h"
 
-exprt concatenate_array_id(
-		const exprt &array, const exprt &index,
-		const typet &type)
-{
-  std::string a, idx, identifier;
-  a = array.get_string(ID_identifier);
-
-  if (index.id()==ID_typecast)
-    idx = index.op0().get_string(ID_value);
-  else
-    idx = index.get_string(ID_value);
-
-  mp_integer i=string2integer(idx);
-  identifier=a+"["+integer2string(i)+"]";
-  symbol_exprt new_expr(identifier, type);
-
-  return new_expr;
-}
-
-exprt concatenate_array_id(
-		const exprt &array, const mp_integer &index,
-		const typet &type)
-{
-  std::string a, identifier;
-  a = array.get_string(ID_identifier);
-  identifier=a+"["+integer2string(index)+"]";
-  symbol_exprt new_expr(identifier, type);
-
-  return new_expr;
-}
-
 void constant_propagator_domaint::assign_rec(
   valuest &values,
-  const exprt &lhs, const exprt &rhs,
+  const exprt &lhs,
+  const exprt &rhs,
   const namespacet &ns)
 {
-  const typet & lhs_type = ns.follow(lhs.type());
-  const typet & rhs_type = ns.follow(rhs.type());
+  if(lhs.id()!=ID_symbol)
+    return;
 
-#ifdef DEBUG
-  std::cout << "assign: " << from_expr(ns, "", lhs)
-            << " := " << from_type(ns, "", rhs_type) << '\n';
-#endif
+  const symbol_exprt &s=to_symbol_expr(lhs);
 
-  if(lhs.id()==ID_symbol && rhs.id()==ID_if)
-  {
-	exprt cond=rhs.op0();
-	assert(cond.operands().size()==2);
-	if(values.is_constant(cond.op0())
-			&& values.is_constant(cond.op1()))
-	{
-      if(cond.op0().id()==ID_index)
-      {
-    	exprt index=cond.op0();
-        exprt new_expr=concatenate_array_id(index.op0(), index.op1(), index.type());
-        values.replace_const(new_expr);
-        cond.op0()=new_expr;
-        cond = simplify_expr(cond,ns);
-      }
-      else
-        assert(0);
+  exprt tmp=rhs;
+  values.replace_const(tmp);
+  simplify(tmp, ns);
 
-      assign(values, to_symbol_expr(lhs), cond, ns);
-	}
-  }
-  else if(lhs.id()==ID_symbol && rhs_type.id()!=ID_array
-                         && rhs_type.id()!=ID_struct
-                         && rhs_type.id()!=ID_union)
-  {
-    if(values.is_constant(rhs))
-      assign(values, to_symbol_expr(lhs), rhs, ns);
-    else
-      values.set_to_top(to_symbol_expr(lhs));
-  }
-  else if(lhs.id()==ID_symbol && lhs_type.id()==ID_array
-		                       && rhs_type.id()==ID_array)
-  {
-	exprt new_expr;
-	mp_integer idx=0;
-    forall_operands(it, rhs)
-	{
-  	  new_expr=concatenate_array_id(lhs, idx, it->type());
-  	  assign(values, to_symbol_expr(new_expr), *it, ns);
-  	  idx = idx +1;
-	}
-  }
-  else if (lhs.id()==ID_index)
-  {
-	if (values.is_constant(lhs.op1())
-	 && values.is_constant(rhs))
-	{
-	  exprt new_expr=concatenate_array_id(lhs.op0(), lhs.op1(), rhs.type());
-      assign(values, to_symbol_expr(new_expr), rhs, ns);
-	}
-  }
-#if 0
-  else // TODO: could make field or array element-sensitive
-  {
-  }
-#endif
+  if(tmp.is_constant())
+    values.set_to(s, tmp);
+  else
+    values.set_to_top(s);
 }
 
 void constant_propagator_domaint::transform(
@@ -127,16 +47,29 @@ void constant_propagator_domaint::transform(
   ai_baset &ai,
   const namespacet &ns)
 {
-  #ifdef DEBUG
+#ifdef DEBUG
+  std::cout << "Transform from/to:\n";
   std::cout << from->location_number << " --> "
             << to->location_number << '\n';
-  #endif
+#endif
 
 #ifdef DEBUG
-  std::cout << "before:\n";
+  std::cout << "Before:\n";
   output(std::cout, ai, ns);
 #endif
 
+  // When the domain is used with constant_propagator_ait,
+  // information about dirty variables and config flags are
+  // available. Otherwise, the below will be null and we use default
+  // values
+  const constant_propagator_ait *cp=
+    dynamic_cast<constant_propagator_ait *>(&ai);
+  bool have_dirty=(cp!=nullptr);
+
+  // assert(!values.is_bottom);
+  if(values.is_bottom)
+    return;
+
   if(from->is_decl())
   {
     const code_declt &code_decl=to_code_decl(from->code);
@@ -146,8 +79,8 @@ void constant_propagator_domaint::transform(
   else if(from->is_assign())
   {
     const code_assignt &assignment=to_code_assign(from->code);
-    const exprt &lhs = assignment.lhs();
-    const exprt &rhs = assignment.rhs();
+    const exprt &lhs=assignment.lhs();
+    const exprt &rhs=assignment.rhs();
     assign_rec(values, lhs, rhs, ns);
   }
   else if(from->is_assume())
@@ -159,19 +92,17 @@ void constant_propagator_domaint::transform(
     exprt g;
 
     if(from->get_target()==to)
-      g = simplify_expr(from->guard, ns);
+      g=simplify_expr(from->guard, ns);
     else
-      g = simplify_expr(not_exprt(from->guard), ns);
+      g=simplify_expr(not_exprt(from->guard), ns);
 
-    if (g.is_false())
+    if(g.is_false())
      values.set_to_bottom();
     else
     {
-      //TODO: we need to support widening!
-      if (g.is_constant())
-        values.set_to_top();
-      else
-        two_way_propagate_rec(g, ns);
+      two_way_propagate_rec(g, ns);
+      assert(!values.is_bottom); // for now
+      // While two-way propagation is disabled this should be impossible.
     }
   }
   else if(from->is_dead())
@@ -181,30 +112,92 @@ void constant_propagator_domaint::transform(
   }
   else if(from->is_function_call())
   {
-    const exprt &function=to_code_function_call(from->code).function();
+    const code_function_callt &function_call=to_code_function_call(from->code);
+    const exprt &function=function_call.function();
+
+    locationt next=from;
+    next++;
 
     if(function.id()==ID_symbol)
     {
-      const irep_idt &identifier=to_symbol_expr(function).get_identifier();
-
-      if(identifier=="__CPROVER_set_must" ||
-         identifier=="__CPROVER_get_must" ||
-         identifier=="__CPROVER_set_may" ||
-         identifier=="__CPROVER_get_may" ||
-         identifier=="__CPROVER_cleanup" ||
-         identifier=="__CPROVER_clear_may" ||
-         identifier=="__CPROVER_clear_must")
+      // called function identifier
+      const symbol_exprt &symbol_expr=to_symbol_expr(function);
+      const irep_idt id=symbol_expr.get_identifier();
+
+      if(to==next)
       {
+        if(id==CPROVER_PREFIX "set_must" ||
+           id==CPROVER_PREFIX "get_must" ||
+           id==CPROVER_PREFIX "set_may" ||
+           id==CPROVER_PREFIX "get_may" ||
+           id==CPROVER_PREFIX "cleanup" ||
+           id==CPROVER_PREFIX "clear_may" ||
+           id==CPROVER_PREFIX "clear_must")
+        {
+          // no effect on constants
+        }
+        else
+        {
+          if(have_dirty)
+            values.set_dirty_to_top(cp->dirty, ns);
+          else
+            values.set_to_top();
+        }
       }
       else
-        values.set_to_top();
+      {
+        // we have an actual call
+
+        // parameters of called function
+        const symbolt &symbol=ns.lookup(id);
+        const code_typet &code_type=to_code_type(symbol.type);
+        const code_typet::parameterst &parameters=code_type.parameters();
+
+        const code_function_callt::argumentst &arguments=
+          function_call.arguments();
+
+        code_typet::parameterst::const_iterator p_it=parameters.begin();
+        for(const auto &arg : arguments)
+        {
+          if(p_it==parameters.end())
+            break;
+
+          const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
+          assign_rec(values, parameter_expr, arg, ns);
+
+          ++p_it;
+        }
+      }
     }
     else
-      values.set_to_top();
+    {
+      // unresolved call
+
+      assert(to==next);
+
+      if(have_dirty)
+        values.set_dirty_to_top(cp->dirty, ns);
+      else
+        values.set_to_top();
+    }
   }
+  else if(from->is_end_function())
+  {
+    // erase parameters
+
+    const irep_idt id=from->function;
+    const symbolt &symbol=ns.lookup(id);
+
+    const code_typet &type=to_code_type(symbol.type);
+
+    for(const auto &param : type.parameters())
+      values.set_to_top(param.get_identifier());
+  }
+
+  assert(from->is_goto() || !values.is_bottom);
 
 #ifdef DEBUG
-  std::cout << "after:\n";
+  std::cout << "After:\n";
   output(std::cout, ai, ns);
 #endif
 }
@@ -218,8 +211,11 @@ bool constant_propagator_domaint::two_way_propagate_rec(
 #ifdef DEBUG
   std::cout << "two_way_propagate_rec: " << from_expr(ns, "", expr) << '\n';
 #endif
-  bool change = false;
 
+  bool change=false;
+
+  // this seems to be buggy at present
+#if 0
   if(expr.id()==ID_and)
   {
     // need a fixed point here to get the most out of it
@@ -229,38 +225,29 @@ bool constant_propagator_domaint::two_way_propagate_rec(
 
       forall_operands(it, expr)
         if(two_way_propagate_rec(*it, ns))
-          change = true;
+          change=true;
     }
     while(change);
   }
   else if(expr.id()==ID_equal)
   {
-    const exprt &lhs = expr.op0();
-    const exprt &rhs = expr.op1();
+    const exprt &lhs=expr.op0();
+    const exprt &rhs=expr.op1();
 
     // two-way propagation
-    valuest copy_values = values;
+    valuest copy_values=values;
     assign_rec(copy_values, lhs, rhs, ns);
     if(!values.is_constant(rhs) || values.is_constant(lhs))
-      assign_rec(values, rhs, lhs, ns);
-    change = values.meet(copy_values);
+       assign_rec(values, rhs, lhs, ns);
+    change=values.meet(copy_values);
   }
+#endif
 
 #ifdef DEBUG
   std::cout << "two_way_propagate_rec: " << change << '\n';
 #endif
-  return change;
-}
 
-void constant_propagator_domaint::assign(
-  valuest &dest,
-  const symbol_exprt &lhs,
-  exprt rhs,
-  const namespacet &ns) const
-{
-  values.replace_const(rhs);
-  rhs = simplify_expr(rhs, ns);
-  dest.set_to(lhs, rhs);
+  return change;
 }
 
 /// Simplify the condition given context-sensitive knowledge from the abstract
@@ -277,17 +264,6 @@ bool constant_propagator_domaint::ai_simplify(
   return b;
 }
 
-bool constant_propagator_domaint::valuest::is_array_constant(const exprt &expr) const
-{
-  exprt new_expr = concatenate_array_id(expr.op0(),
-		  expr.op1(), expr.type());
-
-  if (replace_const.expr_map.find(to_symbol_expr(new_expr).get_identifier()) ==
-         replace_const.expr_map.end())
-    return false;
-
-  return true;
-}
 
 bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
 {
@@ -300,12 +276,12 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
     return false;
 
   if(expr.id()==ID_symbol)
-    if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier()) ==
+    if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier())==
        replace_const.expr_map.end())
       return false;
 
-  if (expr.id()==ID_index)
-	return is_array_constant(expr);
+  if(expr.id()==ID_index)
+    return false;
 
   if(expr.id()==ID_address_of)
     return is_constant_address_of(to_address_of_expr(expr).object());
@@ -339,19 +315,46 @@ bool constant_propagator_domaint::valuest::is_constant_address_of(
 /// Do not call this when iterating over replace_const.expr_map!
 bool constant_propagator_domaint::valuest::set_to_top(const irep_idt &id)
 {
-  bool result = false;
+  replace_symbolt::expr_mapt::size_type n_erased=
+    replace_const.expr_map.erase(id);
 
-  replace_symbolt::expr_mapt::iterator r_it =
-    replace_const.expr_map.find(id);
+  assert(n_erased==0 || !is_bottom);
+
+  return n_erased>0;
+}
+
+/*******************************************************************\
 
-  if(r_it != replace_const.expr_map.end())
+Function: constant_propagator_domaint::valuest::set_dirty_to_top
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void constant_propagator_domaint::valuest::set_dirty_to_top(
+  const dirtyt &dirty,
+  const namespacet &ns)
+{
+  typedef replace_symbolt::expr_mapt expr_mapt;
+  expr_mapt &expr_map=replace_const.expr_map;
+
+  for(expr_mapt::iterator it=expr_map.begin();
+      it!=expr_map.end();)
   {
-    assert(!is_bottom);
-    replace_const.expr_map.erase(r_it);
-    result = true;
-  }
+    const irep_idt id=it->first;
 
-  return result;
+    const symbolt &symbol=ns.lookup(id);
+
+    if((!symbol.is_procedure_local() || dirty(id)) &&
+       !symbol.type.get_bool(ID_C_constant))
+      it=expr_map.erase(it);
+    else
+      it++;
+  }
 }
 
 void constant_propagator_domaint::valuest::output(
@@ -361,11 +364,23 @@ void constant_propagator_domaint::valuest::output(
   out << "const map:\n";
 
   if(is_bottom)
+  {
     out << "  bottom\n";
+    assert(replace_const.expr_map.empty());
+    return;
+  }
+
+  assert(!is_bottom);
+  if(replace_const.expr_map.empty())
+  {
+    out << "top\n";
+    return;
+  }
 
-  for(const auto &replace_pair : replace_const.expr_map)
-    out << ' ' << replace_pair.first << "="
-        << from_expr(ns, "", replace_pair.second) << '\n';
+  for(const auto &p : replace_const.expr_map)
+  {
+    out << ' ' << p.first << "=" << from_expr(ns, "", p.second) << '\n';
+  }
 }
 
 void constant_propagator_domaint::output(
@@ -387,38 +402,62 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src)
   // just copy
   if(is_bottom)
   {
-    replace_const = src.replace_const;
-    is_bottom = src.is_bottom;
+    assert(!src.is_bottom);
+    replace_const=src.replace_const; // copy
+    is_bottom=false;
     return true;
   }
 
-  bool changed = false;
+  assert(!is_bottom && !src.is_bottom);
+
+  bool changed=false;
+
+  replace_symbolt::expr_mapt &expr_map=replace_const.expr_map;
+  const replace_symbolt::expr_mapt &src_expr_map=src.replace_const.expr_map;
 
-  // set everything to top that is not in src
-  for(replace_symbolt::expr_mapt::const_iterator
-        it=replace_const.expr_map.begin();
-      it!=replace_const.expr_map.end();
-      ) // no it++
+  // handle top
+  if(src_expr_map.empty())
   {
-    const replace_symbolt::expr_mapt::const_iterator
-      b_it=src.replace_const.expr_map.find(it->first);
+    // change if it was not top
+    changed=!expr_map.empty();
 
-    if(b_it==src.replace_const.expr_map.end())
+    set_to_top();
+
+    return changed;
+  }
+
+  // remove those that are
+  // - different in src
+  // - do not exist in src
+  for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
+      it!=expr_map.end();)
+  {
+    const irep_idt id=it->first;
+    const exprt &expr=it->second;
+
+    replace_symbolt::expr_mapt::const_iterator s_it;
+    s_it=src_expr_map.find(id);
+
+    if(s_it!=src_expr_map.end())
     {
-      //cannot use set_to_top here
-      replace_const.expr_map.erase(it);
-      changed = true;
-      break;
+      // check value
+      const exprt &src_expr=s_it->second;
+
+      if(expr!=src_expr)
+      {
+        it=expr_map.erase(it);
+        changed=true;
+      }
+      else
+        it++;
     }
     else
     {
-      const exprt previous=it->second;
-      replace_const.expr_map[b_it->first]=b_it->second;
-      if (it->second != previous) changed = true;
-
-      it++;
+      it=expr_map.erase(it);
+      changed=true;
     }
   }
+
   return changed;
 }
 
@@ -429,16 +468,16 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src)
   if(src.is_bottom || is_bottom)
     return false;
 
-  bool changed = false;
+  bool changed=false;
 
-  for(const auto &src_replace_pair : src.replace_const.expr_map)
+  for(const auto &m : src.replace_const.expr_map)
   {
-    replace_symbolt::expr_mapt::iterator c_it=
-      replace_const.expr_map.find(src_replace_pair.first);
+    replace_symbolt::expr_mapt::iterator
+      c_it=replace_const.expr_map.find(m.first);
 
     if(c_it!=replace_const.expr_map.end())
     {
-      if(c_it->second!=src_replace_pair.second)
+      if(c_it->second!=m.second)
       {
         set_to_bottom();
         changed=true;
@@ -447,7 +486,7 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src)
     }
     else
     {
-      set_to(src_replace_pair.first, src_replace_pair.second);
+      set_to(m.first, m.second);
       changed=true;
     }
   }
@@ -472,21 +511,6 @@ void constant_propagator_ait::replace(
     replace(f_it->second, ns);
 }
 
-void constant_propagator_ait::replace_array_symbol(exprt &expr)
-{
-  if (expr.id()==ID_index)
-	expr = concatenate_array_id(expr.op0(),
-			  expr.op1(), expr.type());
-
-  Forall_operands(it, expr)
-  {
-	if (it->id()==ID_equal)
-	  replace_array_symbol(it->op0());
-	else if (it->id()==ID_index)
-	  replace_array_symbol(expr.op0());
-  }
-
-}
 
 void constant_propagator_ait::replace(
   goto_functionst::goto_functiont &goto_function,
@@ -494,9 +518,9 @@ void constant_propagator_ait::replace(
 {
   Forall_goto_program_instructions(it, goto_function.body)
   {
-    state_mapt::iterator s_it = state_map.find(it);
+    state_mapt::iterator s_it=state_map.find(it);
 
-    if(s_it == state_map.end())
+    if(s_it==state_map.end())
       continue;
 
     replace_types_rec(s_it->second.values.replace_const, it->code);
@@ -504,32 +528,32 @@ void constant_propagator_ait::replace(
 
     if(it->is_goto() || it->is_assume() || it->is_assert())
     {
-      replace_array_symbol(it->guard);
       s_it->second.values.replace_const(it->guard);
-      it->guard = simplify_expr(it->guard, ns);
+      simplify(it->guard, ns);
     }
     else if(it->is_assign())
     {
-      exprt &rhs = to_code_assign(it->code).rhs();
+      exprt &rhs=to_code_assign(it->code).rhs();
       s_it->second.values.replace_const(rhs);
-      rhs = simplify_expr(rhs, ns);
-      if (rhs.id()==ID_constant)
+      simplify(rhs, ns);
+      if(rhs.id()==ID_constant)
         rhs.add_source_location()=it->code.op0().source_location();
     }
     else if(it->is_function_call())
     {
       s_it->second.values.replace_const(
         to_code_function_call(it->code).function());
-      simplify_expr(to_code_function_call(it->code).function(), ns);
 
-      exprt::operandst &args =
+      simplify(to_code_function_call(it->code).function(), ns);
+
+      exprt::operandst &args=
         to_code_function_call(it->code).arguments();
 
-      for(exprt::operandst::iterator o_it = args.begin();
-          o_it != args.end(); ++o_it)
+      for(exprt::operandst::iterator o_it=args.begin();
+          o_it!=args.end(); ++o_it)
       {
         s_it->second.values.replace_const(*o_it);
-        *o_it = simplify_expr(*o_it, ns);
+        simplify(*o_it, ns);
       }
     }
     else if(it->is_other())
diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 0b54c79bdb8..1b98e6272fe 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -12,93 +12,137 @@ Author: Peter Schrammel
 #ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
 #define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
 
-#include "ai.h"
+#include <iosfwd>
+#include <util/replace_symbol.h>
 
-#include "replace_symbol_ext.h"
+#include "ai.h"
+#include "dirty.h"
 
 class constant_propagator_domaint:public ai_domain_baset
 {
 public:
-  void transform(
-    locationt,
-    locationt,
-    ai_baset &,
-    const namespacet &) final;
-  void output(
-    std::ostream &,
-    const ai_baset &,
-    const namespacet &) const final;
-  void make_top() final { values.set_to_top(); }
-  void make_bottom() final { values.set_to_bottom(); }
-  void make_entry() final { values.set_to_top(); }
-  bool merge(const constant_propagator_domaint &, locationt, locationt);
+  virtual void transform(
+    locationt from,
+    locationt to,
+    ai_baset &ai_base,
+    const namespacet &ns) final override;
+
+  virtual void output(
+    std::ostream &out,
+    const ai_baset &ai_base,
+    const namespacet &ns) const override;
+
+  bool merge(
+    const constant_propagator_domaint &other,
+    locationt from,
+    locationt to);
 
   virtual bool ai_simplify(
     exprt &condition,
-    const namespacet &ns) const override;
+    const namespacet &ns) const final override;
+
+  virtual void make_bottom() final override
+  {
+    values.set_to_bottom();
+  }
+
+  virtual void make_top() final override
+  {
+    values.set_to_top();
+  }
+
+  virtual void make_entry() final override
+  {
+    make_top();
+  }
+
+  virtual bool is_bottom() const final override
+  {
+    return values.is_bot();
+  }
+
+  virtual bool is_top() const final override
+  {
+    return values.is_top();
+  }
 
   struct valuest
   {
   public:
-    valuest():is_bottom(true) { }
+    valuest():is_bottom(true) {}
 
     // maps variables to constants
-    replace_symbol_extt replace_const;
+    replace_symbolt replace_const;
     bool is_bottom;
 
-    void output(std::ostream &, const namespacet &) const;
-
     bool merge(const valuest &src);
     bool meet(const valuest &src);
 
+    // set whole state
+
     void set_to_bottom()
     {
       replace_const.clear();
-      is_bottom = true;
+      is_bottom=true;
     }
 
-    void set_to(const irep_idt &lhs_id, const exprt &rhs_val)
+    void set_to_top()
     {
-      replace_const.expr_map[lhs_id] = rhs_val;
-      is_bottom = false;
+      replace_const.clear();
+      is_bottom=false;
     }
 
-    void set_to(const symbol_exprt &lhs, const exprt &rhs_val)
+    bool is_bot() const
     {
-      set_to(lhs.get_identifier(), rhs_val);
+      return is_bottom && replace_const.empty();
     }
 
-    bool is_constant(const exprt &expr) const;
-    bool is_array_constant(const exprt &expr) const;
-    bool is_constant_address_of(const exprt &expr) const;
-    bool set_to_top(const irep_idt &id);
+    bool is_top() const
+    {
+      return !is_bottom && replace_const.empty();
+    }
+
+    // set single identifier
+
+    void set_to(const irep_idt &lhs, const exprt &rhs)
+    {
+      replace_const.expr_map[lhs]=rhs;
+      is_bottom=false;
+    }
+
+    void set_to(const symbol_exprt &lhs, const exprt &rhs)
+    {
+      set_to(lhs.get_identifier(), rhs);
+    }
 
     bool set_to_top(const symbol_exprt &expr)
     {
       return set_to_top(expr.get_identifier());
     }
 
-    void set_to_top()
+    bool set_to_top(const irep_idt &id);
+
+    void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns);
+
+    bool is_constant(const exprt &expr) const;
+    bool is_array_constant(const exprt &expr) const;
+    bool is_constant_address_of(const exprt &expr) const;
+
+    bool is_empty() const
     {
-      replace_const.clear();
-      is_bottom = false;
+      assert(replace_const.type_map.empty());
+      return replace_const.expr_map.empty();
     }
 
+    void output(std::ostream &out, const namespacet &ns) const;
   };
 
   valuest values;
 
-private:
-  void assign(
-    valuest &dest,
-    const symbol_exprt &lhs,
-    exprt rhs,
-    const namespacet &ns) const;
-
+protected:
   void assign_rec(
     valuest &values,
-    const exprt &lhs,
-    const exprt &rhs,
+    const exprt &lhs, const exprt &rhs,
     const namespacet &ns);
 
   bool two_way_propagate_rec(
@@ -109,9 +153,14 @@ class constant_propagator_domaint:public ai_domain_baset
 class constant_propagator_ait:public ait<constant_propagator_domaint>
 {
 public:
+  explicit constant_propagator_ait(const goto_functionst &goto_functions):
+    dirty(goto_functions)
+  {
+  }
+
   constant_propagator_ait(
     goto_functionst &goto_functions,
-    const namespacet &ns)
+    const namespacet &ns):dirty(goto_functions)
   {
     operator()(goto_functions, ns);
     replace(goto_functions, ns);
@@ -119,18 +168,17 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
 
   constant_propagator_ait(
     goto_functionst::goto_functiont &goto_function,
-    const namespacet &ns)
+    const namespacet &ns):dirty(goto_function)
   {
     operator()(goto_function, ns);
     replace(goto_function, ns);
   }
 
+  dirtyt dirty;
+
 protected:
   friend class constant_propagator_domaint;
 
-  void replace_array_symbol(
-		  exprt &expr);
-
   void replace(
     goto_functionst::goto_functiont &,
     const namespacet &);
@@ -142,7 +190,6 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
   void replace_types_rec(
     const replace_symbolt &replace_const,
     exprt &expr);
-
 };
 
 #endif // CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h
index ff2884cc2ec..294dfb98989 100644
--- a/src/analyses/custom_bitvector_analysis.h
+++ b/src/analyses/custom_bitvector_analysis.h
@@ -27,32 +27,44 @@ class custom_bitvector_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     may_bits.clear();
     must_bits.clear();
     has_values=tvt(false);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     may_bits.clear();
     must_bits.clear();
     has_values=tvt(true);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_bottom() const final override
+  {
+    assert(!has_values.is_false() || (may_bits.empty() && must_bits.empty()));
+    return has_values.is_false();
+  }
+
+  bool is_top() const final override
+  {
+    assert(!has_values.is_true() || (may_bits.empty() && must_bits.empty()));
+    return has_values.is_true();
+  }
+
   bool merge(
     const custom_bitvector_domaint &b,
     locationt from,
diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h
index 4cd7be4c589..c130aa7737c 100644
--- a/src/analyses/dependence_graph.h
+++ b/src/analyses/dependence_graph.h
@@ -83,12 +83,12 @@ class dep_graph_domaint:public ai_domain_baset
     goto_programt::const_targett from,
     goto_programt::const_targett to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
   jsont output_json(
     const ai_baset &ai,
@@ -103,7 +103,7 @@ class dep_graph_domaint:public ai_domain_baset
     data_deps.clear();
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     assert(node_id!=std::numeric_limits<node_indext>::max());
 
@@ -112,11 +112,31 @@ class dep_graph_domaint:public ai_domain_baset
     data_deps.clear();
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_top() const final override
+  {
+    assert(node_id!=std::numeric_limits<node_indext>::max());
+
+    assert(!has_values.is_true() ||
+           (control_deps.empty() && data_deps.empty()));
+
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const final override
+  {
+    assert(node_id!=std::numeric_limits<node_indext>::max());
+
+    assert(!has_values.is_false() ||
+           (control_deps.empty() && data_deps.empty()));
+
+    return has_values.is_false();
+  }
+
   void set_node_id(node_indext id)
   {
     node_id=id;
diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h
index 00f865b45e4..54c2ba408ba 100644
--- a/src/analyses/escape_analysis.h
+++ b/src/analyses/escape_analysis.h
@@ -32,33 +32,45 @@ class escape_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
   bool merge(
     const escape_domaint &b,
     locationt from,
     locationt to);
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     cleanup_map.clear();
     aliases.clear();
     has_values=tvt(false);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     cleanup_map.clear();
     aliases.clear();
     has_values=tvt(true);
   }
 
-  void make_entry() final
+  bool is_bottom() const override final
+  {
+    assert(!has_values.is_false() || (cleanup_map.empty() && aliases.empty()));
+    return has_values.is_false();
+  }
+
+  bool is_top() const override final
+  {
+    assert(!has_values.is_true() || (cleanup_map.empty() && aliases.empty()));
+    return has_values.is_true();
+  }
+
+  void make_entry() override final
   {
     make_top();
   }
diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h
index d946b371c05..f16ced0c4bd 100644
--- a/src/analyses/global_may_alias.h
+++ b/src/analyses/global_may_alias.h
@@ -32,35 +32,47 @@ class global_may_alias_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
   bool merge(
     const global_may_alias_domaint &b,
     locationt from,
     locationt to);
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     aliases.clear();
     has_values=tvt(false);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     aliases.clear();
     has_values=tvt(true);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_bottom() const final override
+  {
+    assert(!has_values.is_false() || aliases.empty());
+    return has_values.is_false();
+  }
+
+  bool is_top() const final override
+  {
+    assert(!has_values.is_true() || aliases.empty());
+    return has_values.is_true();
+  }
+
   typedef union_find<irep_idt> aliasest;
   aliasest aliases;
 
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index 3076442a3ee..d4496fec4bb 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -36,12 +36,12 @@ class interval_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const override;
 
 protected:
   bool join(const interval_domaint &b);
@@ -56,7 +56,7 @@ class interval_domaint:public ai_domain_baset
   }
 
   // no states
-  void make_bottom() final
+  void make_bottom() final override
   {
     int_map.clear();
     float_map.clear();
@@ -64,18 +64,30 @@ class interval_domaint:public ai_domain_baset
   }
 
   // all states
-  void make_top() final
+  void make_top() final override
   {
     int_map.clear();
     float_map.clear();
     bottom=false;
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_bottom() const override final
+  {
+    // assert(!bottom || (int_map.empty() && float_map.empty()));
+
+    return bottom;
+  }
+
+  bool is_top() const override final
+  {
+    return !bottom && int_map.empty() && float_map.empty();
+  }
+
   exprt make_expression(const symbol_exprt &) const;
 
   void assume(const exprt &, const namespacet &);
@@ -90,11 +102,6 @@ class interval_domaint:public ai_domain_baset
     return src.id()==ID_floatbv;
   }
 
-  bool is_bottom() const
-  {
-    return bottom;
-  }
-
   virtual bool ai_simplify(
     exprt &condition,
     const namespacet &ns) const override;
diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h
index 4d38b6b2657..367e987c709 100644
--- a/src/analyses/invariant_set_domain.h
+++ b/src/analyses/invariant_set_domain.h
@@ -44,7 +44,7 @@ class invariant_set_domaint:public ai_domain_baset
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final
+    const namespacet &ns) const final override
   {
     if(has_values.is_known())
       out << has_values.to_string() << '\n';
@@ -56,25 +56,35 @@ class invariant_set_domaint:public ai_domain_baset
     locationt from_l,
     locationt to_l,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
-  void make_top() final
+  void make_top() final override
   {
     invariant_set.make_true();
     has_values=tvt(true);
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     invariant_set.make_false();
     has_values=tvt(false);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     invariant_set.make_true();
     has_values=tvt(true);
   }
+
+  bool is_top() const override final
+  {
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const override final
+  {
+    return has_values.is_false();
+  }
 };
 
 #endif // CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H
diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
index 64b1e48f959..d6276cbdb27 100644
--- a/src/analyses/is_threaded.cpp
+++ b/src/analyses/is_threaded.cpp
@@ -51,7 +51,7 @@ class is_threaded_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final
+    const namespacet &ns) final override
   {
     // assert(reachable);
 
@@ -62,23 +62,35 @@ class is_threaded_domaint:public ai_domain_baset
       is_threaded=true;
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     reachable=false;
     is_threaded=false;
   }
 
-  void make_top() final
+  void make_top() final override
   {
     reachable=true;
     is_threaded=true;
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     reachable=true;
     is_threaded=false;
   }
+
+  bool is_bottom() const override final
+  {
+    assert(reachable || !is_threaded);
+
+    return !reachable;
+  }
+
+  bool is_top() const override final
+  {
+    return reachable && is_threaded;
+  }
 };
 
 void is_threadedt::compute(const goto_functionst &goto_functions)
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index 2cc7d815fa3..a9a52a062b5 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -116,17 +116,17 @@ class rd_range_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final
+    const namespacet &ns) const final override
   {
     output(out);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     values.clear();
     if(bv_container)
@@ -134,7 +134,7 @@ class rd_range_domaint:public ai_domain_baset
     has_values=tvt(true);
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     values.clear();
     if(bv_container)
@@ -142,11 +142,23 @@ class rd_range_domaint:public ai_domain_baset
     has_values=tvt(false);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_top() const override final
+  {
+    assert(!has_values.is_true() || values.empty());
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const override final
+  {
+    assert(!has_values.is_false() || values.empty());
+    return has_values.is_false();
+  }
+
   // returns true iff there is s.th. new
   bool merge(
     const rd_range_domaint &other,
@@ -252,9 +264,9 @@ class reaching_definitions_analysist:
   virtual ~reaching_definitions_analysist();
 
   virtual void initialize(
-    const goto_functionst &goto_functions);
+    const goto_functionst &goto_functions) override;
 
-  virtual statet &get_state(goto_programt::const_targett l)
+  virtual statet &get_state(goto_programt::const_targett l) override
   {
     statet &s=concurrency_aware_ait<rd_range_domaint>::get_state(l);
 
diff --git a/src/analyses/replace_symbol_ext.cpp b/src/analyses/replace_symbol_ext.cpp
deleted file mode 100644
index 75c697030b7..00000000000
--- a/src/analyses/replace_symbol_ext.cpp
+++ /dev/null
@@ -1,76 +0,0 @@
-/*******************************************************************\
-
-Module: Modified expression replacement for constant propagator
-
-Author: Peter Schrammel
-
-\*******************************************************************/
-
-/// \file
-/// Modified expression replacement for constant propagator
-
-#include <util/std_types.h>
-#include <util/std_expr.h>
-
-#include "replace_symbol_ext.h"
-
-/// does not replace object in address_of expressions
-bool replace_symbol_extt::replace(exprt &dest) const
-{
-  bool result=true;
-
-  // first look at type
-
-  if(have_to_replace(dest.type()))
-    if(!replace_symbolt::replace(dest.type()))
-      result=false;
-
-  // now do expression itself
-
-  if(!have_to_replace(dest))
-    return result;
-
-  // do not replace object in address_of expressions
-  if(dest.id()==ID_address_of)
-  {
-    const exprt &object = to_address_of_expr(dest).object();
-    if(object.id()==ID_symbol)
-    {
-      expr_mapt::const_iterator it=
-        expr_map.find(object.get(ID_identifier));
-
-      if(it!=expr_map.end())
-        return false;
-    }
-  }
-  else if(dest.id()==ID_symbol)
-  {
-    expr_mapt::const_iterator it=
-      expr_map.find(dest.get(ID_identifier));
-
-    if(it!=expr_map.end())
-    {
-      dest=it->second;
-      return false;
-    }
-  }
-
-  Forall_operands(it, dest)
-    if(!replace(*it))
-      result=false;
-
-  const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
-
-  if(c_sizeof_type.is_not_nil() &&
-     !replace_symbolt::replace(
-       static_cast<typet&>(dest.add(ID_C_c_sizeof_type))))
-    result=false;
-
-  const irept &va_arg_type=dest.find(ID_C_va_arg_type);
-
-  if(va_arg_type.is_not_nil() &&
-     !replace_symbolt::replace(static_cast<typet&>(dest.add(ID_C_va_arg_type))))
-    result=false;
-
-  return result;
-}
diff --git a/src/analyses/replace_symbol_ext.h b/src/analyses/replace_symbol_ext.h
deleted file mode 100644
index 05d7226be40..00000000000
--- a/src/analyses/replace_symbol_ext.h
+++ /dev/null
@@ -1,23 +0,0 @@
-/*******************************************************************\
-
-Module: Modified expression replacement for constant propagator
-
-Author: Peter Schrammel
-
-\*******************************************************************/
-
-/// \file
-/// Modified expression replacement for constant propagator
-
-#ifndef CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H
-#define CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H
-
-#include <util/replace_symbol.h>
-
-class replace_symbol_extt:public replace_symbolt
-{
-public:
-  virtual bool replace(exprt &dest) const;
-};
-
-#endif // CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H
diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h
index a48f9954388..c95222e5027 100644
--- a/src/analyses/uninitialized_domain.h
+++ b/src/analyses/uninitialized_domain.h
@@ -33,30 +33,42 @@ class uninitialized_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
     const namespacet &ns) const final;
 
-  void make_top() final
+  void make_top() final override
   {
     uninitialized.clear();
     has_values=tvt(true);
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     uninitialized.clear();
     has_values=tvt(false);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_top() const override final
+  {
+    assert(!has_values.is_true() || uninitialized.empty());
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const override final
+  {
+    assert(!has_values.is_false() || uninitialized.empty());
+    return has_values.is_false();
+  }
+
   // returns true iff there is s.th. new
   bool merge(
     const uninitialized_domaint &other,
diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp
index 51d4a140493..06ffdd7ef7e 100644
--- a/src/util/replace_symbol.cpp
+++ b/src/util/replace_symbol.cpp
@@ -27,9 +27,11 @@ void replace_symbolt::insert(
     old_expr.get_identifier(), new_expr));
 }
 
-bool replace_symbolt::replace(exprt &dest) const
+bool replace_symbolt::replace(
+  exprt &dest,
+  const bool replace_with_const) const
 {
-  bool result=true;
+  bool result=true; // unchanged
 
   // first look at type
 
@@ -42,33 +44,75 @@ bool replace_symbolt::replace(exprt &dest) const
   if(!have_to_replace(dest))
     return result;
 
-  if(dest.id()==ID_symbol)
+  if(dest.id()==ID_member)
+  {
+    member_exprt &me=to_member_expr(dest);
+
+    if(!replace(me.struct_op(), replace_with_const)) // Could give non l-value.
+      result=false;
+  }
+  else if(dest.id()==ID_index)
+  {
+    index_exprt &ie=to_index_expr(dest);
+
+    if(!replace(ie.array(), replace_with_const)) // Could give non l-value.
+      result=false;
+
+    if(!replace(ie.index()))
+      result=false;
+  }
+  else if(dest.id()==ID_address_of)
+  {
+    address_of_exprt &aoe=to_address_of_expr(dest);
+
+    if(!replace(aoe.object(), false))
+      result=false;
+  }
+  else if(dest.id()==ID_symbol)
   {
+    const symbol_exprt &s=to_symbol_expr(dest);
+
     expr_mapt::const_iterator it=
-      expr_map.find(dest.get(ID_identifier));
+      expr_map.find(s.get_identifier());
 
     if(it!=expr_map.end())
     {
-      dest=it->second;
+      const exprt &e=it->second;
+
+      if(!replace_with_const && e.is_constant())  // Would give non l-value.
+        return true;
+
+      dest=e;
+
       return false;
     }
   }
-
-  Forall_operands(it, dest)
-    if(!replace(*it))
-      result=false;
+  else
+  {
+    Forall_operands(it, dest)
+      if(!replace(*it))
+        result=false;
+  }
 
   const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
 
-  if(c_sizeof_type.is_not_nil() &&
-     !replace(static_cast<typet&>(dest.add(ID_C_c_sizeof_type))))
-    result=false;
+  if(c_sizeof_type.is_not_nil())
+  {
+    typet &type=static_cast<typet &>(dest.add(ID_C_c_sizeof_type));
+
+    if(!replace(type))
+      result=false;
+  }
 
   const irept &va_arg_type=dest.find(ID_C_va_arg_type);
 
-  if(va_arg_type.is_not_nil() &&
-     !replace(static_cast<typet&>(dest.add(ID_C_va_arg_type))))
-    result=false;
+  if(va_arg_type.is_not_nil())
+  {
+    typet &type=static_cast<typet &>(dest.add(ID_C_va_arg_type));
+
+    if(!replace(type))
+      result=false;
+  }
 
   return result;
 }
diff --git a/src/util/replace_symbol.h b/src/util/replace_symbol.h
index ebc1102e921..ea9b4c14701 100644
--- a/src/util/replace_symbol.h
+++ b/src/util/replace_symbol.h
@@ -38,7 +38,21 @@ class replace_symbolt
     type_map.insert(std::pair<irep_idt, typet>(identifier, type));
   }
 
-  virtual bool replace(exprt &dest) const;
+  /* If you are replacing symbols with constants in an l-value, you can
+   * create something that is not an l-value.   For example if your
+   * l-value is "a[i]" then substituting i for a constant results in an
+   * l-value but substituting a for a constant (array) wouldn't.  This
+   * only applies to the "top level" of the expression, for example, it
+   * is OK to replace b with a constant array in a[b[0]].
+   *
+   * If replace_with_const == false then it disables the rewrites that
+   * could result in something that is not an l-value.
+   */
+
+  virtual bool replace(
+    exprt &dest,
+    const bool replace_with_const=true) const;
+
   virtual bool replace(typet &dest) const;
 
   void operator()(exprt &dest) const