diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 9578d6d7376..dcf84fcfdde 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -3572,6 +3572,26 @@ std::string expr2ct::convert_r_or_w_ok(const r_or_w_ok_exprt &src)
   return dest;
 }
 
+std::string
+expr2ct::convert_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &src)
+{
+  // we hide prophecy expressions in C-style output
+  std::string dest = src.id() == ID_prophecy_r_ok   ? "R_OK"
+                     : src.id() == ID_prophecy_w_ok ? "W_OK"
+                                                    : "RW_OK";
+
+  dest += '(';
+
+  unsigned p;
+  dest += convert_with_precedence(src.pointer(), p);
+  dest += ", ";
+  dest += convert_with_precedence(src.size(), p);
+
+  dest += ')';
+
+  return dest;
+}
+
 std::string expr2ct::convert_pointer_in_range(const pointer_in_range_exprt &src)
 {
   std::string dest = CPROVER_PREFIX "pointer_in_range";
@@ -3590,6 +3610,26 @@ std::string expr2ct::convert_pointer_in_range(const pointer_in_range_exprt &src)
   return dest;
 }
 
+std::string expr2ct::convert_prophecy_pointer_in_range(
+  const prophecy_pointer_in_range_exprt &src)
+{
+  // we hide prophecy expressions in C-style output
+  std::string dest = CPROVER_PREFIX "pointer_in_range";
+
+  dest += '(';
+
+  unsigned p;
+  dest += convert_with_precedence(src.lower_bound(), p);
+  dest += ", ";
+  dest += convert_with_precedence(src.pointer(), p);
+  dest += ", ";
+  dest += convert_with_precedence(src.upper_bound(), p);
+
+  dest += ')';
+
+  return dest;
+}
+
 std::string expr2ct::convert_with_precedence(
   const exprt &src,
   unsigned &precedence)
@@ -4002,9 +4042,22 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id() == ID_r_ok || src.id() == ID_w_ok || src.id() == ID_rw_ok)
     return convert_r_or_w_ok(to_r_or_w_ok_expr(src));
 
+  else if(
+    auto prophecy_r_or_w_ok =
+      expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(src))
+  {
+    return convert_prophecy_r_or_w_ok(*prophecy_r_or_w_ok);
+  }
+
   else if(src.id() == ID_pointer_in_range)
     return convert_pointer_in_range(to_pointer_in_range_expr(src));
 
+  else if(src.id() == ID_prophecy_pointer_in_range)
+  {
+    return convert_prophecy_pointer_in_range(
+      to_prophecy_pointer_in_range_expr(src));
+  }
+
   auto function_string_opt = convert_function(src);
   if(function_string_opt.has_value())
     return *function_string_opt;
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
index 2a09024a7de..07d73975a3f 100644
--- a/src/ansi-c/expr2c_class.h
+++ b/src/ansi-c/expr2c_class.h
@@ -28,6 +28,8 @@ class qualifierst;
 class namespacet;
 class r_or_w_ok_exprt;
 class pointer_in_range_exprt;
+class prophecy_r_or_w_ok_exprt;
+class prophecy_pointer_in_range_exprt;
 
 class expr2ct
 {
@@ -285,7 +287,10 @@ class expr2ct
   std::string convert_bitreverse(const bitreverse_exprt &src);
 
   std::string convert_r_or_w_ok(const r_or_w_ok_exprt &src);
+  std::string convert_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &src);
   std::string convert_pointer_in_range(const pointer_in_range_exprt &src);
+  std::string
+  convert_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &src);
 };
 
 #endif // CPROVER_ANSI_C_EXPR2C_CLASS_H
diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp
index b051a09f244..26e437195b9 100644
--- a/src/ansi-c/goto_check_c.cpp
+++ b/src/ansi-c/goto_check_c.cpp
@@ -228,7 +228,6 @@ class goto_check_ct
   void conversion_check(const exprt &, const guardt &);
   void float_overflow_check(const exprt &, const guardt &);
   void nan_check(const exprt &, const guardt &);
-  optionalt<exprt> expand_pointer_checks(exprt);
 
   std::string array_name(const exprt &);
 
@@ -1444,6 +1443,8 @@ void goto_check_ct::pointer_primitive_check(
   const exprt pointer =
     (expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
       ? to_r_or_w_ok_expr(expr).pointer()
+    : can_cast_expr<prophecy_r_or_w_ok_exprt>(expr)
+      ? to_prophecy_r_or_w_ok_expr(expr).pointer()
       : to_unary_expr(expr).op();
 
   CHECK_RETURN(pointer.type().id() == ID_pointer);
@@ -1484,6 +1485,7 @@ bool goto_check_ct::requires_pointer_primitive_check(const exprt &expr)
   // will equally be non-deterministic.
   return can_cast_expr<object_size_exprt>(expr) || expr.id() == ID_r_ok ||
          expr.id() == ID_w_ok || expr.id() == ID_rw_ok ||
+         can_cast_expr<prophecy_r_or_w_ok_exprt>(expr) ||
          expr.id() == ID_is_dynamic_object;
 }
 
@@ -1992,62 +1994,6 @@ void goto_check_ct::check(const exprt &expr)
   check_rec(expr, identity);
 }
 
-/// expand the r_ok, w_ok, rw_ok, pointer_in_range predicates
-optionalt<exprt> goto_check_ct::expand_pointer_checks(exprt expr)
-{
-  bool modified = false;
-
-  for(auto &op : expr.operands())
-  {
-    auto op_result = expand_pointer_checks(op);
-    if(op_result.has_value())
-    {
-      op = *op_result;
-      modified = true;
-    }
-  }
-
-  if(expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
-  {
-    // these get an address as first argument and a size as second
-    DATA_INVARIANT(
-      expr.operands().size() == 2, "r/w_ok must have two operands");
-
-    const auto conditions = get_pointer_dereferenceable_conditions(
-      to_r_or_w_ok_expr(expr).pointer(), to_r_or_w_ok_expr(expr).size());
-
-    exprt::operandst conjuncts;
-
-    for(const auto &c : conditions)
-      conjuncts.push_back(c.assertion);
-
-    exprt c = conjunction(conjuncts);
-    if(enable_simplify)
-      simplify(c, ns);
-    return c;
-  }
-  else if(expr.id() == ID_pointer_in_range)
-  {
-    const auto &pointer_in_range_expr = to_pointer_in_range_expr(expr);
-
-    auto expanded = pointer_in_range_expr.lower();
-
-    // rec. call
-    auto expanded_rec_opt = expand_pointer_checks(expanded);
-    if(expanded_rec_opt.has_value())
-      expanded = *expanded_rec_opt;
-
-    if(enable_simplify)
-      simplify(expanded, ns);
-
-    return expanded;
-  }
-  else if(modified)
-    return std::move(expr);
-  else
-    return {};
-}
-
 void goto_check_ct::memory_leak_check(const irep_idt &function_id)
 {
   const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak");
@@ -2267,8 +2213,6 @@ void goto_check_ct::goto_check(
       }
     }
 
-    i.transform([this](exprt expr) { return expand_pointer_checks(expr); });
-
     for(auto &instruction : new_code.instructions)
     {
       if(instruction.source_location().is_nil())
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 8867e612a83..882dbf4c13e 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -406,6 +406,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 
   // Options for process_goto_program
+  options.set_option("rewrite-rw-ok", true);
   options.set_option("rewrite-union", true);
 
   if(cmdline.isset("smt1"))
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 840621d0baf..b64119b6b9e 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -393,6 +393,7 @@ int goto_analyzer_parse_optionst::doit()
 
   // Preserve backwards compatibility in processing
   options.set_option("partial-inline", true);
+  options.set_option("rewrite-rw-ok", false);
   options.set_option("rewrite-union", false);
   options.set_option("remove-returns", true);
 
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 55a129324b9..b30a71df7d3 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -65,6 +65,7 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
   options.set_option("show-properties", cmdline.isset("show-properties"));
 
   // Options for process_goto_program
+  options.set_option("rewrite-rw-ok", false);
   options.set_option("rewrite-union", true);
 }
 
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 6d8bd441e7a..c58c6a7b3c4 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -45,6 +45,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_rw_ok.h>
 #include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
@@ -569,6 +570,7 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-reaching-definitions"))
     {
       do_indirect_call_and_rtti_removal();
+      rewrite_rw_ok(goto_model);
 
       const namespacet ns(goto_model.symbol_table);
       reaching_definitions_analysist rd_analysis(ns);
@@ -581,6 +583,7 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-dependence-graph"))
     {
       do_indirect_call_and_rtti_removal();
+      rewrite_rw_ok(goto_model);
 
       const namespacet ns(goto_model.symbol_table);
       dependence_grapht dependence_graph(ns);
@@ -1767,6 +1770,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   {
     do_indirect_call_and_rtti_removal();
     do_remove_returns();
+    rewrite_rw_ok(goto_model);
 
     log.warning() << "**** WARNING: Experimental option --full-slice, "
                   << "analysis results may be unsound. See "
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index 3d6a56f5416..f2557edc4c9 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -56,6 +56,7 @@ SRC = allocate_objects.cpp \
       remove_vector.cpp \
       remove_virtual_functions.cpp \
       restrict_function_pointers.cpp \
+      rewrite_rw_ok.cpp \
       rewrite_union.cpp \
       resolve_inherited_component.cpp \
       safety_checker.cpp \
diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp
index 57cbdd6115b..15341312159 100644
--- a/src/goto-programs/process_goto_program.cpp
+++ b/src/goto-programs/process_goto_program.cpp
@@ -23,6 +23,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_vector.h>
+#include <goto-programs/rewrite_rw_ok.h>
 #include <goto-programs/rewrite_union.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
@@ -70,6 +71,9 @@ bool process_goto_program(
   if(options.get_bool_option("rewrite-union"))
     rewrite_union(goto_model);
 
+  if(options.get_bool_option("rewrite-rw-ok"))
+    rewrite_rw_ok(goto_model);
+
   // add generic checks
   log.status() << "Generic Property Instrumentation" << messaget::eom;
   goto_check_c(options, goto_model, log.get_message_handler());
diff --git a/src/goto-programs/rewrite_rw_ok.cpp b/src/goto-programs/rewrite_rw_ok.cpp
new file mode 100644
index 00000000000..09433e5d8df
--- /dev/null
+++ b/src/goto-programs/rewrite_rw_ok.cpp
@@ -0,0 +1,83 @@
+/*******************************************************************\
+
+Module: Rewrite {r,w,rw}_ok expressions as required by symbolic execution
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "rewrite_rw_ok.h"
+
+#include <util/expr_iterator.h>
+#include <util/pointer_expr.h>
+
+#include <goto-programs/goto_model.h>
+
+static optionalt<exprt> rewrite_rw_ok(exprt expr, const namespacet &ns)
+{
+  bool unchanged = true;
+
+  for(auto it = expr.depth_begin(), itend = expr.depth_end();
+      it != itend;) // no ++it
+  {
+    if(auto r_or_w_ok = expr_try_dynamic_cast<r_or_w_ok_exprt>(*it))
+    {
+      const auto &id = it->id();
+      exprt replacement =
+        prophecy_r_or_w_ok_exprt{
+          id == ID_r_ok   ? ID_prophecy_r_ok
+          : id == ID_w_ok ? ID_prophecy_w_ok
+                          : ID_prophecy_rw_ok,
+          r_or_w_ok->pointer(),
+          r_or_w_ok->size(),
+          ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(),
+          ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()}
+          .with_source_location<exprt>(*it);
+
+      it.mutate() = std::move(replacement);
+      unchanged = false;
+      it.next_sibling_or_parent();
+    }
+    else if(
+      auto pointer_in_range =
+        expr_try_dynamic_cast<pointer_in_range_exprt>(*it))
+    {
+      exprt replacement =
+        prophecy_pointer_in_range_exprt{
+          pointer_in_range->lower_bound(),
+          pointer_in_range->pointer(),
+          pointer_in_range->upper_bound(),
+          ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(),
+          ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()}
+          .with_source_location<exprt>(*it);
+
+      it.mutate() = std::move(replacement);
+      unchanged = false;
+      it.next_sibling_or_parent();
+    }
+    else
+      ++it;
+  }
+
+  if(unchanged)
+    return {};
+  else
+    return std::move(expr);
+}
+
+static void rewrite_rw_ok(
+  goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns)
+{
+  for(auto &instruction : goto_function.body.instructions)
+    instruction.transform(
+      [&ns](exprt expr) { return rewrite_rw_ok(expr, ns); });
+}
+
+void rewrite_rw_ok(goto_modelt &goto_model)
+{
+  const namespacet ns(goto_model.symbol_table);
+
+  for(auto &gf_entry : goto_model.goto_functions.function_map)
+    rewrite_rw_ok(gf_entry.second, ns);
+}
diff --git a/src/goto-programs/rewrite_rw_ok.h b/src/goto-programs/rewrite_rw_ok.h
new file mode 100644
index 00000000000..269ce9365a2
--- /dev/null
+++ b/src/goto-programs/rewrite_rw_ok.h
@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Rewrite {r,w,rw}_ok expressions as required by symbolic execution
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+/// \file
+/// Rewrite r/w/rw_ok expressions to ones including prophecy variables recording
+/// the state.
+
+#ifndef CPROVER_GOTO_PROGRAMS_REWRITE_RW_OK_H
+#define CPROVER_GOTO_PROGRAMS_REWRITE_RW_OK_H
+
+class goto_modelt;
+
+/// Replace all occurrences of `r_ok_exprt`, `w_ok_exprt`, `rw_ok_exprt`,
+/// `pointer_in_range_exprt` by their prophecy variants
+/// `prophecy_r_or_w_ok_exprt` and `prophecy_pointer_in_range_exprt`,
+/// respectively.
+/// Each analysis may choose to natively support `r_ok_exprt` etc. (like
+/// `cprover_parse_optionst` does) or may instead require the expression to be
+/// lowered to other primitives (like `goto_symext`).
+void rewrite_rw_ok(goto_modelt &);
+
+#endif // CPROVER_GOTO_PROGRAMS_REWRITE_RW_OK_H
diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp
index 72c1050aceb..5729c9c29b6 100644
--- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp
+++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp
@@ -199,6 +199,7 @@ optionst goto_synthesizer_parse_optionst::get_options()
   options.set_option("depth", UINT32_MAX);
   options.set_option("exploration-strategy", "lifo");
   options.set_option("symex-cache-dereferences", false);
+  options.set_option("rewrite-rw-ok", true);
   options.set_option("rewrite-union", true);
   options.set_option("self-loops-to-assumptions", true);
 
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 09973306a93..be28f5eef2e 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
 
 /// Map bytes according to the configured endianness. The key difference to
 /// endianness_mapt is that bv_endianness_mapt is aware of the bit-level
@@ -204,6 +205,18 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
           bv_utilst::representationt::UNSIGNED));
     }
   }
+  else if(
+    auto prophecy_r_or_w_ok =
+      expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(expr))
+  {
+    return convert(simplify_expr(prophecy_r_or_w_ok->lower(ns), ns));
+  }
+  else if(
+    auto prophecy_pointer_in_range =
+      expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(expr))
+  {
+    return convert(simplify_expr(prophecy_pointer_in_range->lower(ns), ns));
+  }
 
   return SUB::convert_rest(expr);
 }
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 2cb65bcff1e..0f04d0ce6f3 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -4864,6 +4864,30 @@ exprt smt2_convt::prepare_for_convert_expr(const exprt &expr)
     !has_byte_operator(lowered_expr),
     "lower_byte_operators should remove all byte operators");
 
+  // Perform rewrites that may introduce new symbols
+  for(auto it = lowered_expr.depth_begin(), itend = lowered_expr.depth_end();
+      it != itend;) // no ++it
+  {
+    if(
+      auto prophecy_r_or_w_ok =
+        expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(*it))
+    {
+      exprt lowered = simplify_expr(prophecy_r_or_w_ok->lower(ns), ns);
+      it.mutate() = lowered;
+      it.next_sibling_or_parent();
+    }
+    else if(
+      auto prophecy_pointer_in_range =
+        expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(*it))
+    {
+      exprt lowered = simplify_expr(prophecy_pointer_in_range->lower(ns), ns);
+      it.mutate() = lowered;
+      it.next_sibling_or_parent();
+    }
+    else
+      ++it;
+  }
+
   // Now create symbols for all composite expressions present in lowered_expr:
   find_symbols(lowered_expr);
 
diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
index 5f0a97ad98e..45bd6fd79f3 100644
--- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -1463,6 +1463,24 @@ static smt_termt convert_expr_to_smt(
     count_trailing_zeros.pretty());
 }
 
+static smt_termt convert_expr_to_smt(
+  const prophecy_r_or_w_ok_exprt &prophecy_r_or_w_ok,
+  const sub_expression_mapt &converted)
+{
+  UNREACHABLE_BECAUSE(
+    "prophecy_r_or_w_ok expression should have been lowered by the decision "
+    "procedure before conversion to smt terms");
+}
+
+static smt_termt convert_expr_to_smt(
+  const prophecy_pointer_in_range_exprt &prophecy_pointer_in_range,
+  const sub_expression_mapt &converted)
+{
+  UNREACHABLE_BECAUSE(
+    "prophecy_pointer_in_range expression should have been lowered by the "
+    "decision procedure before conversion to smt terms");
+}
+
 static smt_termt dispatch_expr_to_smt_conversion(
   const exprt &expr,
   const sub_expression_mapt &converted,
@@ -1798,6 +1816,18 @@ static smt_termt dispatch_expr_to_smt_conversion(
   {
     return convert_expr_to_smt(*count_trailing_zeros, converted);
   }
+  if(
+    const auto prophecy_r_or_w_ok =
+      expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(expr))
+  {
+    return convert_expr_to_smt(*prophecy_r_or_w_ok, converted);
+  }
+  if(
+    const auto prophecy_pointer_in_range =
+      expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(expr))
+  {
+    return convert_expr_to_smt(*prophecy_pointer_in_range, converted);
+  }
 
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for unknown kind of expression: " +
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 16b26ce3a3f..29a873e60d0 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -7,6 +7,7 @@
 #include <util/namespace.h>
 #include <util/nodiscard.h>
 #include <util/range.h>
+#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/string_constant.h>
 #include <util/symbol.h>
@@ -273,6 +274,25 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
   solver_process->send(is_dynamic_object_function.declaration);
 }
 
+static exprt lower_rw_ok_pointer_in_range(exprt expr, const namespacet &ns)
+{
+  expr.visit_pre([&ns](exprt &expr) {
+    if(
+      auto prophecy_r_or_w_ok =
+        expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(expr))
+    {
+      expr = simplify_expr(prophecy_r_or_w_ok->lower(ns), ns);
+    }
+    else if(
+      auto prophecy_pointer_in_range =
+        expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(expr))
+    {
+      expr = simplify_expr(prophecy_pointer_in_range->lower(ns), ns);
+    }
+  });
+  return expr;
+}
+
 void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
   const exprt &in_expr)
 {
@@ -623,8 +643,9 @@ void smt2_incremental_decision_proceduret::define_object_properties()
 
 exprt smt2_incremental_decision_proceduret::lower(exprt expression) const
 {
-  const exprt lowered = struct_encoding.encode(
-    lower_enum(lower_byte_operators(expression, ns), ns));
+  const exprt lowered = struct_encoding.encode(lower_enum(
+    lower_byte_operators(lower_rw_ok_pointer_in_range(expression, ns), ns),
+    ns));
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
     if(lowered != expression)
       debug << "lowered to -\n  " << lowered.pretty(2, 0) << messaget::eom;
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index e66f620b755..3fc64bc77e3 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -904,6 +904,10 @@ IREP_ID_TWO(overflow_result_unary_minus, overflow_result-unary-)
 IREP_ID_ONE(field_sensitive_ssa)
 IREP_ID_ONE(checked_assigns)
 IREP_ID_ONE(enum_is_in_range)
+IREP_ID_ONE(prophecy_rw_ok)
+IREP_ID_ONE(prophecy_r_ok)
+IREP_ID_ONE(prophecy_w_ok)
+IREP_ID_ONE(prophecy_pointer_in_range)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree
diff --git a/src/util/pointer_expr.cpp b/src/util/pointer_expr.cpp
index 38a3af19039..939cd04b6cb 100644
--- a/src/util/pointer_expr.cpp
+++ b/src/util/pointer_expr.cpp
@@ -238,3 +238,30 @@ exprt pointer_in_range_exprt::lower() const
      binary_relation_exprt(
        pointer_offset(op1()), ID_le, pointer_offset(op2()))});
 }
+
+exprt prophecy_r_or_w_ok_exprt::lower(const namespacet &ns) const
+{
+  return and_exprt{
+    {not_exprt{null_object(pointer())},
+     not_exprt{is_invalid_pointer_exprt{pointer()}},
+     not_exprt{same_object(pointer(), deallocated_ptr())},
+     not_exprt{same_object(pointer(), dead_ptr())},
+     not_exprt{object_lower_bound(pointer(), nil_exprt())},
+     not_exprt{object_upper_bound(pointer(), size())}}};
+}
+
+exprt prophecy_pointer_in_range_exprt::lower(const namespacet &ns) const
+{
+  return and_exprt{
+    {same_object(op0(), op1()),
+     same_object(op1(), op2()),
+     prophecy_r_ok_exprt(
+       op0(),
+       minus_exprt(pointer_offset(op2()), pointer_offset(op0())),
+       deallocated_ptr(),
+       dead_ptr())
+       .lower(ns),
+     binary_relation_exprt(pointer_offset(op0()), ID_le, pointer_offset(op1())),
+     binary_relation_exprt(
+       pointer_offset(op1()), ID_le, pointer_offset(op2()))}};
+}
diff --git a/src/util/pointer_expr.h b/src/util/pointer_expr.h
index baface3794d..d3130b3110c 100644
--- a/src/util/pointer_expr.h
+++ b/src/util/pointer_expr.h
@@ -447,6 +447,94 @@ inline pointer_in_range_exprt &to_pointer_in_range_expr(exprt &expr)
   return static_cast<pointer_in_range_exprt &>(expr);
 }
 
+/// pointer_in_range (see \ref pointer_in_range_exprt) with prophecy expressions
+/// to encode whether a pointer refers to a deallocated or out-of-scope object.
+class prophecy_pointer_in_range_exprt : public expr_protectedt
+{
+public:
+  prophecy_pointer_in_range_exprt(
+    exprt a,
+    exprt b,
+    exprt c,
+    exprt is_deallocated,
+    exprt is_dead)
+    : expr_protectedt(
+        ID_prophecy_pointer_in_range,
+        bool_typet{},
+        {std::move(a),
+         std::move(b),
+         std::move(c),
+         std::move(is_deallocated),
+         std::move(is_dead)})
+  {
+    PRECONDITION(op0().type().id() == ID_pointer);
+    PRECONDITION(op1().type().id() == ID_pointer);
+    PRECONDITION(op2().type().id() == ID_pointer);
+  }
+
+  const exprt &lower_bound() const
+  {
+    return op0();
+  }
+
+  const exprt &pointer() const
+  {
+    return op1();
+  }
+
+  const exprt &upper_bound() const
+  {
+    return op2();
+  }
+
+  const exprt &deallocated_ptr() const
+  {
+    return op3();
+  }
+
+  const exprt &dead_ptr() const
+  {
+    return operands()[4];
+  }
+
+  // translate into equivalent conjunction
+  exprt lower(const namespacet &ns) const;
+};
+
+template <>
+inline bool can_cast_expr<prophecy_pointer_in_range_exprt>(const exprt &base)
+{
+  return base.id() == ID_prophecy_pointer_in_range;
+}
+
+inline void validate_expr(const prophecy_pointer_in_range_exprt &value)
+{
+  validate_operands(
+    value, 5, "prophecy_pointer_in_range must have five operands");
+}
+
+inline const prophecy_pointer_in_range_exprt &
+to_prophecy_pointer_in_range_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_prophecy_pointer_in_range);
+  DATA_INVARIANT(
+    expr.operands().size() == 5,
+    "prophecy_pointer_in_range must have five operands");
+  return static_cast<const prophecy_pointer_in_range_exprt &>(expr);
+}
+
+/// \copydoc to_prophecy_pointer_in_range_expr(const exprt &)
+/// \ingroup gr_std_expr
+inline prophecy_pointer_in_range_exprt &
+to_prophecy_pointer_in_range_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_prophecy_pointer_in_range);
+  DATA_INVARIANT(
+    expr.operands().size() == 5,
+    "prophecy_pointer_in_range must have five operands");
+  return static_cast<prophecy_pointer_in_range_exprt &>(expr);
+}
+
 /// \brief Operator to return the address of an object
 class address_of_exprt : public unary_exprt
 {
@@ -925,6 +1013,191 @@ inline const w_ok_exprt &to_w_ok_expr(const exprt &expr)
   return ret;
 }
 
+/// \brief A base class for a predicate that indicates that an
+/// address range is ok to read or write or both
+class prophecy_r_or_w_ok_exprt : public expr_protectedt
+{
+public:
+  prophecy_r_or_w_ok_exprt(
+    irep_idt id,
+    exprt pointer,
+    exprt size,
+    exprt is_deallocated,
+    exprt is_dead)
+    : expr_protectedt(
+        id,
+        bool_typet{},
+        {std::move(pointer),
+         std::move(size),
+         std::move(is_deallocated),
+         std::move(is_dead)})
+  {
+  }
+
+  prophecy_r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
+    : prophecy_r_or_w_ok_exprt(
+        id,
+        std::move(pointer),
+        std::move(size),
+        nil_exprt{},
+        nil_exprt{})
+  {
+  }
+
+  const exprt &pointer() const
+  {
+    return op0();
+  }
+
+  const exprt &size() const
+  {
+    return op1();
+  }
+
+  const exprt &deallocated_ptr() const
+  {
+    return op2();
+  }
+
+  exprt &deallocated_ptr()
+  {
+    return op2();
+  }
+
+  const exprt &dead_ptr() const
+  {
+    return op3();
+  }
+
+  exprt &dead_ptr()
+  {
+    return op3();
+  }
+
+  /// Lower an r_or_w_ok_exprt to arithmetic and logic expressions.
+  /// \return Semantically equivalent expression
+  exprt lower(const namespacet &ns) const;
+};
+
+template <>
+inline bool can_cast_expr<prophecy_r_or_w_ok_exprt>(const exprt &base)
+{
+  return base.id() == ID_prophecy_r_ok || base.id() == ID_prophecy_w_ok ||
+         base.id() == ID_prophecy_rw_ok;
+}
+
+inline void validate_expr(const prophecy_r_or_w_ok_exprt &value)
+{
+  validate_operands(value, 4, "r_or_w_ok must have four operands");
+}
+
+inline const prophecy_r_or_w_ok_exprt &
+to_prophecy_r_or_w_ok_expr(const exprt &expr)
+{
+  PRECONDITION(
+    expr.id() == ID_prophecy_r_ok || expr.id() == ID_prophecy_w_ok ||
+    expr.id() == ID_prophecy_rw_ok);
+  auto &ret = static_cast<const prophecy_r_or_w_ok_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \brief A predicate that indicates that an address range is ok to read
+class prophecy_r_ok_exprt : public prophecy_r_or_w_ok_exprt
+{
+public:
+  prophecy_r_ok_exprt(
+    exprt pointer,
+    exprt size,
+    exprt is_deallocated,
+    exprt is_dead)
+    : prophecy_r_or_w_ok_exprt(
+        ID_prophecy_r_ok,
+        std::move(pointer),
+        std::move(size),
+        std::move(is_deallocated),
+        std::move(is_dead))
+  {
+  }
+
+  prophecy_r_ok_exprt(exprt pointer, exprt size)
+    : prophecy_r_ok_exprt(
+        std::move(pointer),
+        std::move(size),
+        nil_exprt{},
+        nil_exprt{})
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<prophecy_r_ok_exprt>(const exprt &base)
+{
+  return base.id() == ID_prophecy_r_ok;
+}
+
+inline void validate_expr(const prophecy_r_ok_exprt &value)
+{
+  validate_operands(value, 4, "r_ok must have four operands");
+}
+
+inline const prophecy_r_ok_exprt &to_prophecy_r_ok_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_prophecy_r_ok);
+  const prophecy_r_ok_exprt &ret =
+    static_cast<const prophecy_r_ok_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \brief A predicate that indicates that an address range is ok to write
+class prophecy_w_ok_exprt : public prophecy_r_or_w_ok_exprt
+{
+public:
+  prophecy_w_ok_exprt(
+    exprt pointer,
+    exprt size,
+    exprt is_deallocated,
+    exprt is_dead)
+    : prophecy_r_or_w_ok_exprt(
+        ID_prophecy_w_ok,
+        std::move(pointer),
+        std::move(size),
+        std::move(is_deallocated),
+        std::move(is_dead))
+  {
+  }
+
+  prophecy_w_ok_exprt(exprt pointer, exprt size)
+    : prophecy_w_ok_exprt(
+        std::move(pointer),
+        std::move(size),
+        nil_exprt{},
+        nil_exprt{})
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<prophecy_w_ok_exprt>(const exprt &base)
+{
+  return base.id() == ID_prophecy_w_ok;
+}
+
+inline void validate_expr(const prophecy_w_ok_exprt &value)
+{
+  validate_operands(value, 4, "w_ok must have four operands");
+}
+
+inline const prophecy_w_ok_exprt &to_prophecy_w_ok_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_prophecy_w_ok);
+  const prophecy_w_ok_exprt &ret =
+    static_cast<const prophecy_w_ok_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 /// \brief Pointer-typed bitvector constant annotated with the pointer
 /// expression that the bitvector is the numeric representation of.
 /// This variation of a constant expression is only used in the context of a
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 5c62282d74b..428bda505dc 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -2993,6 +2993,18 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
   {
     r = simplify_bitreverse(to_bitreverse_expr(expr));
   }
+  else if(
+    const auto prophecy_r_or_w_ok =
+      expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(expr))
+  {
+    r = simplify_prophecy_r_or_w_ok(*prophecy_r_or_w_ok);
+  }
+  else if(
+    const auto prophecy_pointer_in_range =
+      expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(expr))
+  {
+    r = simplify_prophecy_pointer_in_range(*prophecy_pointer_in_range);
+  }
 
   if(!no_change_join_operands)
     r = changed(r);
diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h
index f1ecb47e4a4..5e834c35421 100644
--- a/src/util/simplify_expr_class.h
+++ b/src/util/simplify_expr_class.h
@@ -65,6 +65,8 @@ class plus_exprt;
 class pointer_object_exprt;
 class pointer_offset_exprt;
 class popcount_exprt;
+class prophecy_pointer_in_range_exprt;
+class prophecy_r_or_w_ok_exprt;
 class refined_string_exprt;
 class shift_exprt;
 class sign_exprt;
@@ -228,6 +230,14 @@ class simplify_exprt
   /// Try to simplify find-first-set to a constant expression.
   NODISCARD resultt<> simplify_ffs(const find_first_set_exprt &);
 
+  /// Try to simplify prophecy_{r,w,rw}_ok to a constant expression.
+  NODISCARD resultt<>
+  simplify_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &);
+
+  /// Try to simplify prophecy_pointer_in_range to a constant expression.
+  NODISCARD resultt<>
+  simplify_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &);
+
   // auxiliary
   bool simplify_if_implies(
     exprt &expr, const exprt &cond, bool truth, bool &new_truth);
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index c774d5c3bbe..1334d4e645f 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -692,3 +692,23 @@ simplify_exprt::simplify_object_size(const object_size_exprt &expr)
   else
     return std::move(new_expr);
 }
+
+simplify_exprt::resultt<> simplify_exprt::simplify_prophecy_r_or_w_ok(
+  const prophecy_r_or_w_ok_exprt &expr)
+{
+  exprt new_expr = simplify_rec(expr.lower(ns));
+  if(!new_expr.is_constant())
+    return unchanged(expr);
+  else
+    return std::move(new_expr);
+}
+
+simplify_exprt::resultt<> simplify_exprt::simplify_prophecy_pointer_in_range(
+  const prophecy_pointer_in_range_exprt &expr)
+{
+  exprt new_expr = simplify_rec(expr.lower(ns));
+  if(!new_expr.is_constant())
+    return unchanged(expr);
+  else
+    return std::move(new_expr);
+}