diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 60be0403b6e..24275c65cc7 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -89,6 +89,37 @@ static exprt build_full_lhs_rec(
     else
       return std::move(tmp2);
   }
+  else if(id == ID_cond)
+  {
+    const auto &original_cond_expr = to_cond_expr(src_original);
+    const auto &ssa_cond_expr = to_cond_expr(src_ssa);
+    cond_exprt result(
+      {}, src_original.type(), original_cond_expr.is_exclusive());
+    for(std::size_t i = 0; i < original_cond_expr.get_n_cases(); ++i)
+    {
+      exprt condition =
+        decision_procedure.get(to_cond_expr(src_ssa).condition(i));
+      if(condition.is_false())
+        continue;
+
+      exprt value = build_full_lhs_rec(
+        decision_procedure,
+        ns,
+        original_cond_expr.value(i),
+        ssa_cond_expr.value(i));
+
+      if(
+        condition.is_true() &&
+        (result.get_n_cases() == 0 || result.is_exclusive()))
+      {
+        return value;
+      }
+
+      result.add_case(condition, value);
+    }
+
+    return std::move(result);
+  }
   else if(id==ID_typecast)
   {
     typecast_exprt tmp=to_typecast_expr(src_original);
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index f0d337b1e64..6cf95e8069c 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -534,6 +534,13 @@ class goto_symext
     const exprt &rhs,
     exprt::operandst &,
     assignment_typet);
+  void symex_assign_cond(
+    statet &,
+    const cond_exprt &lhs,
+    const exprt &full_lhs,
+    const exprt &rhs,
+    exprt::operandst &,
+    assignment_typet);
   void symex_assign_byte_extract(
     statet &,
     const byte_extract_exprt &lhs,
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 3943cf34788..261b96087d3 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -579,6 +579,16 @@ void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
 
       if_expr.type()=if_expr.true_case().type();
     }
+    else if(expr.id() == ID_cond)
+    {
+      cond_exprt &cond_expr = to_cond_expr(expr);
+      for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      {
+        cond_expr.condition(i) =
+          rename<level>(std::move(cond_expr.condition(i)), ns).get();
+        rename_address<level>(cond_expr.value(i), ns);
+      }
+    }
     else if(expr.id()==ID_member)
     {
       member_exprt &member_expr=to_member_expr(expr);
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 50c325dd715..553c830c3f2 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -155,6 +155,9 @@ void goto_symext::symex_assign_rec(
   else if(lhs.id()==ID_if)
     symex_assign_if(
       state, to_if_expr(lhs), full_lhs, rhs, guard, assignment_type);
+  else if(lhs.id() == ID_cond)
+    symex_assign_cond(
+      state, to_cond_expr(lhs), full_lhs, rhs, guard, assignment_type);
   else if(lhs.id()==ID_typecast)
     symex_assign_typecast(
       state, to_typecast_expr(lhs), full_lhs, rhs, guard, assignment_type);
@@ -613,6 +616,44 @@ void goto_symext::symex_assign_if(
   }
 }
 
+void goto_symext::symex_assign_cond(
+  statet &state,
+  const cond_exprt &lhs,
+  const exprt &full_lhs,
+  const exprt &rhs,
+  exprt::operandst &guard,
+  assignment_typet assignment_type)
+{
+  std::size_t old_guard_size = guard.size();
+
+  for(std::size_t i = 0; i < lhs.get_n_cases(); ++i)
+  {
+    exprt renamed_guard = state.rename(lhs.condition(i), ns).get();
+    do_simplify(renamed_guard);
+    if(!renamed_guard.is_false())
+    {
+      guard.push_back(renamed_guard);
+      symex_assign_rec(
+        state, lhs.value(i), full_lhs, rhs, guard, assignment_type);
+      guard.pop_back();
+    }
+
+    // If this one is a certainty the remaining cases are irrelevant:
+    if(renamed_guard.is_true())
+      break;
+
+    // If the conditions are non-exclusive, further cases can only happen if
+    // this one did not. If they are exclusive then they can be tested
+    // independently.
+    if(!lhs.is_exclusive())
+      guard.push_back(not_exprt(renamed_guard));
+  }
+
+  // Restore the guard to its state before entering this function:
+  INVARIANT(guard.size() >= old_guard_size, "must not shrink the guard!");
+  guard.resize(old_guard_size);
+}
+
 void goto_symext::symex_assign_byte_extract(
   statet &state,
   const byte_extract_exprt &lhs,
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 328e227ce9a..8c76ecab8d5 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/expr_iterator.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 
@@ -49,6 +50,27 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
 
     if_expr.type()=if_expr.true_case().type();
   }
+  else if(expr.id() == ID_cond)
+  {
+    cond_exprt &cond_expr = to_cond_expr(expr);
+    typet result_type;
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+    {
+      process_array_expr(cond_expr.value(i), do_simplify, ns);
+      if(i == 0)
+        result_type = cond_expr.value(i).type();
+      else if(cond_expr.value(i).type() != result_type)
+      {
+        cond_expr.value(i) = byte_extract_exprt(
+          byte_extract_id(),
+          cond_expr.value(i),
+          from_integer(0, index_type()),
+          result_type);
+      }
+    }
+
+    cond_expr.type() = result_type;
+  }
   else if(expr.id()==ID_address_of)
   {
     // strip
@@ -169,6 +191,33 @@ replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
   }
 }
 
+static void lower_cond_expr(exprt &expr)
+{
+  for(auto it = expr.depth_begin(), itend = expr.depth_end(); it != itend; ++it)
+  {
+    if(it->id() == ID_cond)
+    {
+      exprt new_expr;
+      const auto &cond_expr = to_cond_expr(*it);
+      INVARIANT(cond_expr.get_n_cases() >= 1, "cond_expr should not be empty");
+      for(std::size_t i = cond_expr.get_n_cases() - 1;; --i)
+      {
+        if(i == cond_expr.get_n_cases() - 1)
+          new_expr = cond_expr.value(i);
+        else
+        {
+          new_expr =
+            if_exprt(cond_expr.condition(i), cond_expr.value(i), new_expr);
+        }
+        if(i == 0)
+          break;
+      }
+
+      it.mutate() = std::move(new_expr);
+    }
+  }
+}
+
 void goto_symext::clean_expr(
   exprt &expr,
   statet &state,
@@ -177,6 +226,12 @@ void goto_symext::clean_expr(
   replace_nondet(expr, path_storage.build_symex_nondet);
   dereference(expr, state, write);
 
+  // We know how to handle cond_exprt on the LHS (symex_assign_rec does this),
+  // but cond_exprt on the RHS is currently patchily handled, especially by the
+  // Java string solver. For now, lower such expressions to nested if_exprts.
+  if(!write)
+    lower_cond_expr(expr);
+
   // make sure all remaining byte extract operations use the root
   // object to avoid nesting of with/update and byte_update when on
   // lhs
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index e6879fd491e..78989c0ca5b 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -123,6 +123,18 @@ exprt goto_symext::address_arithmetic(
 
     result=if_expr;
   }
+  else if(expr.id() == ID_cond)
+  {
+    cond_exprt cond_expr = to_cond_expr(expr);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+    {
+      dereference_rec(cond_expr.condition(i), state, false);
+      cond_expr.value(i) =
+        address_arithmetic(cond_expr.value(i), state, keep_array);
+    }
+
+    result = std::move(cond_expr);
+  }
   else if(expr.id()==ID_symbol ||
           expr.id()==ID_string_constant ||
           expr.id()==ID_label ||
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 2614e0da4f2..50c53d751ff 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -55,6 +55,21 @@ void goto_symext::havoc_rec(
     guard_f.add(not_exprt(if_expr.cond()));
     havoc_rec(state, guard_f, if_expr.false_case());
   }
+  else if(dest.id() == ID_cond)
+  {
+    const auto &cond_expr = to_cond_expr(dest);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+    {
+      guardt guard = state.guard;
+      if(!cond_expr.is_exclusive())
+      {
+        for(std::size_t j = 0; j < i; ++j)
+          guard.add(not_exprt(cond_expr.condition(j)));
+      }
+      guard.add(cond_expr.condition(i));
+      havoc_rec(state, guard, cond_expr.value(i));
+    }
+  }
   else if(dest.id()==ID_typecast)
   {
     havoc_rec(state, guard, to_typecast_expr(dest).op());
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index ea002102d36..6d4c794f62a 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -521,6 +521,12 @@ void value_sett::get_value_set_rec(
     get_value_set_rec(expr.op1(), dest, suffix, original_type, ns);
     get_value_set_rec(expr.op2(), dest, suffix, original_type, ns);
   }
+  else if(expr.id() == ID_cond)
+  {
+    const auto &cond_expr = to_cond_expr(expr);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      get_value_set_rec(cond_expr.value(i), dest, suffix, original_type, ns);
+  }
   else if(expr.id()==ID_address_of)
   {
     if(expr.operands().size()!=1)
@@ -1169,6 +1175,12 @@ void value_sett::get_reference_set_rec(
     get_reference_set_rec(expr.op2(), dest, ns);
     return;
   }
+  else if(expr.id() == ID_cond)
+  {
+    const auto &cond_expr = to_cond_expr(expr);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      get_reference_set_rec(cond_expr.value(i), dest, ns);
+  }
 
   insert(dest, exprt(ID_unknown, expr.type()));
 }
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 932b4a1237a..9f4f6634e42 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -36,7 +36,7 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
     throw "dereference expected pointer type, but got "+
           pointer.type().pretty();
 
-  // we may get ifs due to recursive calls
+  // we may get ifs or conds due to recursive calls
   if(pointer.id()==ID_if)
   {
     const if_exprt &if_expr=to_if_expr(pointer);
@@ -44,6 +44,13 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
     exprt false_case = dereference(if_expr.false_case());
     return if_exprt(if_expr.cond(), true_case, false_case);
   }
+  else if(pointer.id() == ID_cond)
+  {
+    cond_exprt result = to_cond_expr(pointer);
+    for(std::size_t i = 0; i < result.get_n_cases(); ++i)
+      result.value(i) = dereference(result.value(i));
+    return std::move(result);
+  }
 
   // type of the object
   const typet &type=pointer.type().subtype();
@@ -107,12 +114,12 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
         may_fail=true;
   }
 
+  exprt failure_value;
+
   if(may_fail)
   {
     // first see if we have a "failed object" for this pointer
 
-    exprt failure_value;
-
     if(
       const symbolt *failed_symbol =
         dereference_callback.get_or_create_failed_symbol(pointer))
@@ -138,36 +145,61 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
       failure_value=symbol.symbol_expr();
       failure_value.set(ID_C_invalid_object, true);
     }
-
-    valuet value;
-    value.value=failure_value;
-    value.pointer_guard=true_exprt();
-    values.push_front(value);
   }
 
   // now build big case split, but we only do "good" objects
 
-  exprt value=nil_exprt();
-
-  for(std::list<valuet>::const_iterator
-      it=values.begin();
-      it!=values.end();
-      it++)
+  optionalt<exprt> value_without_condition;
+  cond_exprt cond({}, type, true);
+  for(const auto &alias_value : values)
   {
-    if(it->value.is_not_nil())
+    if(alias_value.value.is_not_nil())
     {
-      if(value.is_nil()) // first?
-        value=it->value;
+      if(alias_value.pointer_guard.is_false())
+      {
+        INVARIANT(
+          !value_without_condition.has_value(),
+          "can't discriminate between two different catch-all aliases");
+        value_without_condition = alias_value.value;
+      }
       else
-        value=if_exprt(it->pointer_guard, it->value, value);
+      {
+        cond.add_case(alias_value.pointer_guard, alias_value.value);
+        INVARIANT(
+          alias_value.value.type() == type,
+          "deref value types should match the pointer being derefd");
+      }
     }
   }
 
-  #if 0
-  std::cout << "R: " << format(value) << "\n\n";
-  #endif
+  // I'd like to put an invariant here that values without a pointer guard, such
+  // as integer_address, cannot co-occur with failed objects, but this isn't the
+  // case. There's no way to write a GOTO condition to discriminate between the
+  // two however, so purely by historical accident, the failed object takes
+  // precedence:
+
+  if(may_fail || value_without_condition.has_value())
+  {
+    // The cases must be disjoint, so add
+    // "!(p == &o1 || p == &o2 || p == &o3 || ...) => failure-value"
+    exprt::operandst other_case_conditions;
+    for(std::size_t i = 0; i < cond.get_n_cases(); ++i)
+      other_case_conditions.push_back(cond.condition(i));
+    cond.add_case(
+      not_exprt(disjunction(other_case_conditions)),
+      may_fail ? failure_value : *value_without_condition);
+  }
 
-  return value;
+#if 0
+  std::cout << "R: " << format(cond) << "\n\n";
+#endif
+
+  if(cond.get_n_cases() == 0)
+    return nil_exprt();
+  else if(cond.get_n_cases() == 1)
+    return cond.value(0);
+  else
+    return std::move(cond);
 }
 
 /// Check if the two types have matching number of ID_pointer levels, with
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index d32ee5924dd..2301db4f323 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -270,6 +270,10 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   {
     return SUB::convert_if(to_if_expr(expr));
   }
+  else if(expr.id() == ID_cond)
+  {
+    return SUB::convert_cond(to_cond_expr(expr));
+  }
   else if(expr.id()==ID_index)
   {
     return SUB::convert_index(to_index_expr(expr));
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index acb9dc99dbf..822b7dd75d4 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -216,6 +216,24 @@ if_exprt lift_if(const exprt &src, std::size_t operand_number)
   return result;
 }
 
+cond_exprt lift_cond(const exprt &src, std::size_t operand_number)
+{
+  PRECONDITION(operand_number < src.operands().size());
+  PRECONDITION(src.operands()[operand_number].id() == ID_cond);
+
+  const cond_exprt cond_expr = to_cond_expr(src.operands()[operand_number]);
+  cond_exprt result({}, src.type(), cond_expr.is_exclusive());
+
+  for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+  {
+    exprt new_value = src;
+    new_value.operands()[operand_number] = cond_expr.value(i);
+    result.add_case(cond_expr.condition(i), new_value);
+  }
+
+  return result;
+}
+
 const exprt &skip_typecast(const exprt &expr)
 {
   if(expr.id()!=ID_typecast)
diff --git a/src/util/expr_util.h b/src/util/expr_util.h
index bc0b5099071..c37e440c94d 100644
--- a/src/util/expr_util.h
+++ b/src/util/expr_util.h
@@ -26,6 +26,7 @@ class symbol_exprt;
 class update_exprt;
 class with_exprt;
 class if_exprt;
+class cond_exprt;
 class symbolt;
 class typet;
 class namespacet;
@@ -74,6 +75,9 @@ bool has_subtype(const typet &, const irep_idt &id, const namespacet &);
 /// lift up an if_exprt one level
 if_exprt lift_if(const exprt &, std::size_t operand_number);
 
+/// lift up an cond_exprt one level
+cond_exprt lift_cond(const exprt &, std::size_t operand_number);
+
 /// find the expression nested inside typecasts, if any
 const exprt &skip_typecast(const exprt &expr);
 
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 0082f423b66..76791b81151 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -723,6 +723,7 @@ IREP_ID_ONE(to_member)
 IREP_ID_ONE(pointer_to_member)
 IREP_ID_ONE(tuple)
 IREP_ID_ONE(function_body)
+IREP_ID_ONE(exclusive)
 
 // 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/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 80520b58e74..08d656fd627 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1237,6 +1237,50 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr)
   return result;
 }
 
+bool simplify_exprt::simplify_cond_preorder(cond_exprt &expr)
+{
+  cond_exprt new_expr({}, expr.type(), expr.is_exclusive());
+  bool result = true;
+
+#ifdef USE_LOCAL_REPLACE_MAP
+#  error "TODO: implement simplify_cond_preorder use of replacement maps"
+#endif
+
+  for(std::size_t i = 0; i < expr.get_n_cases(); ++i)
+  {
+    exprt condition = as_const(expr).condition(i);
+    if(!simplify_rec(condition))
+      result = false;
+
+    if(condition.is_true() && (i == 0 || expr.is_exclusive()))
+    {
+      expr.swap(expr.value(i));
+      simplify_rec(expr);
+      return false;
+    }
+
+    if(!condition.is_false())
+    {
+      exprt value = as_const(expr).value(i);
+      if(!simplify_rec(value))
+        result = false;
+      new_expr.add_case(condition, value);
+    }
+    else
+    {
+      result = false;
+    }
+
+    if(condition.is_true())
+      break;
+  }
+
+  if(!result)
+    expr = std::move(new_expr);
+
+  return result;
+}
+
 bool simplify_exprt::simplify_if(if_exprt &expr)
 {
   exprt &cond=expr.cond();
@@ -1343,6 +1387,27 @@ bool simplify_exprt::simplify_if(if_exprt &expr)
   return result;
 }
 
+bool simplify_exprt::simplify_cond(cond_exprt &expr)
+{
+  optionalt<exprt> unique_value;
+  for(std::size_t i = 0; i < expr.get_n_cases(); ++i)
+  {
+    const exprt &value = as_const(expr).value(i);
+    if(!unique_value.has_value())
+      unique_value = value;
+    else if(value != *unique_value)
+      return true;
+  }
+
+  if(unique_value.has_value())
+  {
+    expr.swap(*unique_value);
+    return false;
+  }
+
+  return true;
+}
+
 bool simplify_exprt::get_values(
   const exprt &expr,
   value_listt &value_list)
@@ -1365,6 +1430,14 @@ bool simplify_exprt::get_values(
     return get_values(expr.op1(), value_list) ||
            get_values(expr.operands().back(), value_list);
   }
+  else if(expr.id() == ID_cond)
+  {
+    bool ret = false;
+    const auto &cond = to_cond_expr(expr);
+    for(std::size_t i = 0; i < cond.get_n_cases(); ++i)
+      ret |= get_values(cond.value(i), value_list);
+    return ret;
+  }
 
   return true;
 }
@@ -1877,6 +1950,15 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
     expr.swap(if_expr);
     return false;
   }
+  else if(expr.op().id() == ID_cond)
+  {
+    cond_exprt cond_expr = lift_cond(expr, 0);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      simplify_byte_extract(to_byte_extract_expr(cond_expr.value(i)));
+    simplify_cond(cond_expr);
+    expr.swap(cond_expr);
+    return false;
+  }
 
   const auto el_size = pointer_offset_bits(expr.type(), ns);
 
@@ -2387,6 +2469,8 @@ bool simplify_exprt::simplify_node_preorder(exprt &expr)
   }
   else if(expr.id()==ID_if)
     result=simplify_if_preorder(to_if_expr(expr));
+  else if(expr.id() == ID_cond)
+    result = simplify_cond_preorder(to_cond_expr(expr));
   else
   {
     if(expr.has_operands())
@@ -2423,6 +2507,8 @@ bool simplify_exprt::simplify_node(exprt &expr)
     result=simplify_inequality(expr) && result;
   else if(expr.id()==ID_if)
     result=simplify_if(to_if_expr(expr)) && result;
+  else if(expr.id() == ID_cond)
+    result = simplify_cond(to_cond_expr(expr)) && result;
   else if(expr.id()==ID_lambda)
     result=simplify_lambda(expr) && result;
   else if(expr.id()==ID_with)
diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp
index 4ef9a540706..6929fa5cb93 100644
--- a/src/util/simplify_expr_array.cpp
+++ b/src/util/simplify_expr_array.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "simplify_expr_class.h"
 
 #include "arith_tools.h"
+#include "expr_util.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
 #include "replace_expr.h"
@@ -213,15 +214,14 @@ bool simplify_exprt::simplify_index(exprt &expr)
   }
   else if(array.id()==ID_if)
   {
-    const if_exprt &if_expr=to_if_expr(array);
-    exprt cond=if_expr.cond();
-
-    index_exprt idx_false=to_index_expr(expr);
-    idx_false.array()=if_expr.false_case();
-
-    to_index_expr(expr).array()=if_expr.true_case();
+    expr = lift_if(expr, 0);
+    simplify_rec(expr);
 
-    expr=if_exprt(cond, expr, idx_false, expr.type());
+    return false;
+  }
+  else if(array.id() == ID_cond)
+  {
+    expr = lift_cond(expr, 0);
     simplify_rec(expr);
 
     return false;
diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h
index 83a73929d63..9d9f0395d2d 100644
--- a/src/util/simplify_expr_class.h
+++ b/src/util/simplify_expr_class.h
@@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 class bswap_exprt;
 class byte_extract_exprt;
 class byte_update_exprt;
+class cond_exprt;
 class exprt;
 class extractbits_exprt;
 class if_exprt;
@@ -81,6 +82,8 @@ class simplify_exprt
   bool simplify_bitwise(exprt &expr);
   bool simplify_if_preorder(if_exprt &expr);
   bool simplify_if(if_exprt &expr);
+  bool simplify_cond_preorder(cond_exprt &expr);
+  bool simplify_cond(cond_exprt &expr);
   bool simplify_bitnot(exprt &expr);
   bool simplify_not(exprt &expr);
   bool simplify_boolean(exprt &expr);
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index e35b1280099..353c403b242 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -1319,6 +1319,15 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
     return simplify_inequality(expr);
   }
 
+  // if rhs is ID_cond (and lhs is not), swap operands for == and !=
+  if(
+    (expr.id() == ID_equal || expr.id() == ID_notequal) &&
+    tmp0.id() != ID_cond && tmp1.id() == ID_cond)
+  {
+    expr.op0().swap(expr.op1());
+    return simplify_inequality(expr);
+  }
+
   if(tmp0.id()==ID_if && tmp0.operands().size()==3)
   {
     if_exprt if_expr=lift_if(expr, 0);
@@ -1330,6 +1339,17 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
     return false;
   }
 
+  if(tmp0.id() == ID_cond)
+  {
+    cond_exprt cond_expr = lift_cond(expr, 0);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      simplify_inequality(cond_expr.value(i));
+    simplify_cond(cond_expr);
+    expr.swap(cond_expr);
+
+    return false;
+  }
+
   // see if we are comparing pointers that are address_of
   if((tmp0.id()==ID_address_of ||
         (tmp0.id()==ID_typecast && tmp0.op0().id()==ID_address_of)) &&
@@ -1687,6 +1707,17 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
     return false;
   }
 
+  if(expr.op0().id() == ID_cond)
+  {
+    cond_exprt cond_expr = lift_cond(expr, 0);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      simplify_inequality_constant(cond_expr.value(i));
+    simplify_cond(cond_expr);
+    expr.swap(cond_expr);
+
+    return false;
+  }
+
   // do we deal with pointers?
   if(expr.op1().type().id()==ID_pointer)
   {
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index e1e41941896..c0bad20e49d 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -171,6 +171,49 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr)
       return result;
     }
   }
+  else if(expr.id() == ID_cond)
+  {
+    bool result = true;
+    const auto &cond_expr = to_cond_expr(expr);
+    cond_exprt new_cond_expr({}, cond_expr.type(), cond_expr.is_exclusive());
+
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+    {
+      exprt condition = cond_expr.condition(i);
+      exprt value = cond_expr.value(i);
+
+      if(!simplify_rec(condition))
+        result = false;
+
+      if(condition.is_false())
+        continue;
+
+      if(!simplify_address_of_arg(value))
+        result = false;
+
+      if(condition.is_true() && (cond_expr.is_exclusive() || i == 0))
+      {
+        expr.swap(value);
+        return false;
+      }
+
+      new_cond_expr.add_case(condition, value);
+
+      if(condition.is_true())
+        break;
+    }
+
+    if(new_cond_expr.get_n_cases() == 1)
+    {
+      expr = new_cond_expr.value(0);
+      return false;
+    }
+
+    if(!result)
+      expr = std::move(new_cond_expr);
+
+    return result;
+  }
 
   return true;
 }
@@ -230,6 +273,16 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
 
     return false;
   }
+  else if(ptr.id() == ID_cond)
+  {
+    cond_exprt cond_expr = lift_cond(expr, 0);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      simplify_pointer_offset(cond_expr.value(i));
+    simplify_cond(cond_expr);
+    expr.swap(cond_expr);
+
+    return false;
+  }
 
   if(ptr.type().id()!=ID_pointer)
     return true;
@@ -498,16 +551,21 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr)
 
   if(op.id()==ID_if)
   {
-    const if_exprt &if_expr=to_if_expr(op);
-    exprt cond=if_expr.cond();
-
-    exprt p_o_false=expr;
-    p_o_false.op0()=if_expr.false_case();
-
-    expr.op0()=if_expr.true_case();
+    if_exprt if_expr = lift_if(expr, 0);
+    simplify_pointer_object(if_expr.true_case());
+    simplify_pointer_object(if_expr.false_case());
+    simplify_if(if_expr);
+    expr.swap(if_expr);
 
-    expr=if_exprt(cond, expr, p_o_false, expr.type());
-    simplify_rec(expr);
+    return false;
+  }
+  else if(op.id() == ID_cond)
+  {
+    cond_exprt cond_expr = lift_cond(expr, 0);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      simplify_pointer_object(cond_expr.value(i));
+    simplify_cond(cond_expr);
+    expr.swap(cond_expr);
 
     return false;
   }
@@ -532,6 +590,16 @@ bool simplify_exprt::simplify_is_dynamic_object(exprt &expr)
 
     return false;
   }
+  else if(op.id() == ID_cond)
+  {
+    cond_exprt cond_expr = lift_cond(expr, 0);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      simplify_is_dynamic_object(cond_expr.value(i));
+    simplify_cond(cond_expr);
+    expr.swap(cond_expr);
+
+    return false;
+  }
 
   bool result=true;
 
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 76452119cff..268adbc53c8 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "arith_tools.h"
 #include "byte_operators.h"
+#include "expr_util.h"
 #include "invariant.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
@@ -276,15 +277,14 @@ bool simplify_exprt::simplify_member(exprt &expr)
   }
   else if(op.id()==ID_if)
   {
-    const if_exprt &if_expr=to_if_expr(op);
-    exprt cond=if_expr.cond();
-
-    member_exprt member_false=to_member_expr(expr);
-    member_false.compound()=if_expr.false_case();
-
-    to_member_expr(expr).compound()=if_expr.true_case();
+    expr = lift_if(expr, 0);
+    simplify_rec(expr);
 
-    expr=if_exprt(cond, expr, member_false, expr.type());
+    return false;
+  }
+  else if(op.id() == ID_cond)
+  {
+    expr = lift_cond(expr, 0);
     simplify_rec(expr);
 
     return false;
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index e9a4aff64ef..a6b1c6d0db0 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -4394,6 +4394,8 @@ inline popcount_exprt &to_popcount_expr(exprt &expr)
 /// this is a parametric version of an if-expression: it returns
 /// the value of the first case (using the ordering of the operands)
 /// whose condition evaluates to true.
+/// It can be exclusive, in which case the creator asserts that the conditions
+/// are mutually exclusive (i.e. they may be processed in any order).
 class cond_exprt : public multi_ary_exprt
 {
 public:
@@ -4402,9 +4404,11 @@ class cond_exprt : public multi_ary_exprt
   {
   }
 
-  cond_exprt(operandst _operands, typet _type)
+  cond_exprt(operandst _operands, typet _type, bool exclusive = false)
     : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
   {
+    if(exclusive)
+      set(ID_exclusive, true);
   }
 
   /// adds a case to a cond expression
@@ -4417,6 +4421,36 @@ class cond_exprt : public multi_ary_exprt
     operands().push_back(condition);
     operands().push_back(value);
   }
+
+  std::size_t get_n_cases() const
+  {
+    return operands().size() / 2;
+  }
+
+  const exprt &condition(std::size_t case_index) const
+  {
+    return operands().at(case_index * 2);
+  }
+
+  const exprt &value(std::size_t case_index) const
+  {
+    return operands().at((case_index * 2) + 1);
+  }
+
+  exprt &condition(std::size_t case_index)
+  {
+    return operands().at(case_index * 2);
+  }
+
+  exprt &value(std::size_t case_index)
+  {
+    return operands().at((case_index * 2) + 1);
+  }
+
+  bool is_exclusive() const
+  {
+    return get_bool(ID_exclusive);
+  }
 };
 
 template <>