diff --git a/regression/contracts/assigns_enforce_address_of/test.desc b/regression/contracts/assigns_enforce_address_of/test.desc
index 9e9033a30f9..7ddb24bb269 100644
--- a/regression/contracts/assigns_enforce_address_of/test.desc
+++ b/regression/contracts/assigns_enforce_address_of/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: non-lvalue target in assigns clause$
+^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_conditional_function_call_condition/main.c b/regression/contracts/assigns_enforce_conditional_function_call_condition/main.c
new file mode 100644
index 00000000000..26bb269263e
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_function_call_condition/main.c
@@ -0,0 +1,33 @@
+#include <stdbool.h>
+
+bool cond()
+{
+  return true;
+}
+
+int foo(int a, int *x, int *y)
+  // clang-format off
+__CPROVER_assigns(a && cond() : *x)
+// clang-format on
+{
+  if(a)
+  {
+    if(cond())
+      *x = 0; // must pass
+  }
+  else
+  {
+    *x = 0; // must fail
+  }
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc b/regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc
new file mode 100644
index 00000000000..daca51d2cfd
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo
+^main.c function foo$
+^\[foo\.\d+\] line 16 Check that \*x is assignable: SUCCESS$
+^\[foo\.\d+\] line 20 Check that \*x is assignable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that function calls are allowed in conditions.
+Remark: we allow function calls without further checks for now because they
+are mandatory for some applications.
+The next step must be to check that the called functions have a contract
+with an empty assigns clause and that they indeed satisfy their contract
+using a CI check.
diff --git a/regression/contracts/assigns_enforce_conditional_lvalue/main.c b/regression/contracts/assigns_enforce_conditional_lvalue/main.c
new file mode 100644
index 00000000000..a40a3d2b837
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_lvalue/main.c
@@ -0,0 +1,29 @@
+#include <stdbool.h>
+
+int foo(bool a, int *x, int *y) __CPROVER_assigns(a : *x; !a : *y)
+{
+  if(a)
+  {
+    *x = 0; // must pass
+    *y = 0; // must fail
+  }
+  else
+  {
+    *x = 0; // must fail
+    *y = 0; // must pass
+  }
+
+  *x = 0; // must fail
+  *y = 0; // must fail
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_lvalue/test.desc b/regression/contracts/assigns_enforce_conditional_lvalue/test.desc
new file mode 100644
index 00000000000..68f9ac72d9b
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_lvalue/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo
+main.c function foo
+^\[foo\.\d+\] line 7 Check that \*x is assignable: SUCCESS$
+^\[foo\.\d+\] line 8 Check that \*y is assignable: FAILURE$
+^\[foo\.\d+\] line 12 Check that \*x is assignable: FAILURE$
+^\[foo\.\d+\] line 13 Check that \*y is assignable: SUCCESS$
+^\[foo\.\d+\] line 16 Check that \*x is assignable: FAILURE$
+^\[foo\.\d+\] line 17 Check that \*y is assignable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that lvalue conditional assigns clause targets
+match with control flow path conditions.
diff --git a/regression/contracts/assigns_enforce_conditional_lvalue_list/main.c b/regression/contracts/assigns_enforce_conditional_lvalue_list/main.c
new file mode 100644
index 00000000000..71cd9844974
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_lvalue_list/main.c
@@ -0,0 +1,29 @@
+#include <stdbool.h>
+
+int foo(bool a, int *x, int *y) __CPROVER_assigns(a : *x, *y)
+{
+  if(a)
+  {
+    *x = 0; // must pass
+    *y = 0; // must pass
+  }
+  else
+  {
+    *x = 0; // must fail
+    *y = 0; // must fail
+  }
+
+  *x = 0; // must fail
+  *y = 0; // must fail
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc b/regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc
new file mode 100644
index 00000000000..4e13aecc929
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo
+main.c function foo
+^\[foo\.\d+\] line 7 Check that \*x is assignable: SUCCESS$
+^\[foo\.\d+\] line 8 Check that \*y is assignable: SUCCESS$
+^\[foo\.\d+\] line 12 Check that \*x is assignable: FAILURE$
+^\[foo\.\d+\] line 13 Check that \*y is assignable: FAILURE$
+^\[foo\.\d+\] line 16 Check that \*x is assignable: FAILURE$
+^\[foo\.\d+\] line 17 Check that \*y is assignable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that conditional assigns clause  `c ? {lvalue, ..}`
+match with control flow path conditions.
diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/main.c b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/main.c
new file mode 100644
index 00000000000..ca2fb2d98a0
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/main.c
@@ -0,0 +1,21 @@
+#include <stdbool.h>
+
+int *identity(int *ptr)
+{
+  return ptr;
+}
+
+int foo(bool a, int *x, int offset) __CPROVER_assigns(a : !x)
+{
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc
new file mode 100644
index 00000000000..4f48ab39f7d
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
+^CONVERSION ERROR
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that non-lvalue targets are rejected from conditional targets.
diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/main.c b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/main.c
new file mode 100644
index 00000000000..3021057d429
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/main.c
@@ -0,0 +1,21 @@
+#include <stdbool.h>
+
+int *identity(int *ptr)
+{
+  return ptr;
+}
+
+int foo(bool a, int *x, int *y) __CPROVER_assigns(a : !x, *y)
+{
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc
new file mode 100644
index 00000000000..4f48ab39f7d
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
+^CONVERSION ERROR
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that non-lvalue targets are rejected from conditional targets.
diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object/main.c b/regression/contracts/assigns_enforce_conditional_pointer_object/main.c
new file mode 100644
index 00000000000..bbf00141986
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_pointer_object/main.c
@@ -0,0 +1,35 @@
+#include <stdbool.h>
+
+int foo(bool a, char *x, char *y)
+  // clang-format off
+ __CPROVER_assigns(
+    a: __CPROVER_POINTER_OBJECT(x);
+   !a: __CPROVER_POINTER_OBJECT(y);
+  )
+// clang-format on
+{
+  if(a)
+  {
+    x[0] = 0; // must pass
+    y[0] = 0; // must fail
+  }
+  else
+  {
+    x[0] = 0; // must fail
+    y[0] = 0; // must pass
+  }
+
+  x[0] = 0; // must fail
+  y[0] = 0; // must fail
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  char x[2];
+  char y[2];
+
+  foo(a, &x, &y);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc b/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc
new file mode 100644
index 00000000000..cb7a980d68f
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo
+main.c function foo
+^\[foo\.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo\.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo\.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that conditional assigns clause  `c ? __CPROVER_POINTER_OBJECT((p)`
+match with control flow path conditions.
diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object_list/main.c b/regression/contracts/assigns_enforce_conditional_pointer_object_list/main.c
new file mode 100644
index 00000000000..d8cd1db323e
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_pointer_object_list/main.c
@@ -0,0 +1,34 @@
+#include <stdbool.h>
+
+int foo(bool a, char *x, char *y)
+  // clang-format off
+__CPROVER_assigns(
+   a : __CPROVER_POINTER_OBJECT(x), __CPROVER_POINTER_OBJECT(y)
+)
+// clang-format on
+{
+  if(a)
+  {
+    x[0] = 0; // must pass
+    y[0] = 0; // must pass
+  }
+  else
+  {
+    x[0] = 0; // must fail
+    y[0] = 0; // must fail
+  }
+
+  x[0] = 0; // must fail
+  y[0] = 0; // must fail
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  char x[2];
+  char y[2];
+
+  foo(a, &x, &y);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc b/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc
new file mode 100644
index 00000000000..7bb88a83c08
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo
+main.c function foo
+^\[foo\.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo\.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo\.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 18 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 21 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 22 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that conditional assigns clause  `c ? {__CPROVER_POINTER_OBJECT((p), .. }`
+match with control flow path conditions.
diff --git a/regression/contracts/assigns_enforce_conditional_side_effect_condition/main.c b/regression/contracts/assigns_enforce_conditional_side_effect_condition/main.c
new file mode 100644
index 00000000000..3242a0914b8
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_side_effect_condition/main.c
@@ -0,0 +1,20 @@
+#include <stdbool.h>
+
+int foo(int a, int *x, int *y) __CPROVER_assigns(a++ : *x)
+{
+  if(a)
+  {
+    *x = 0;
+  }
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_side_effect_condition/test.desc b/regression/contracts/assigns_enforce_conditional_side_effect_condition/test.desc
new file mode 100644
index 00000000000..5969b0728d2
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_side_effect_condition/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^.* error: side-effects not allowed in assigns clause conditions$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that side-effect expressions in target conditions cause hard errors.
diff --git a/regression/contracts/assigns_enforce_conditional_side_effect_target/main.c b/regression/contracts/assigns_enforce_conditional_side_effect_target/main.c
new file mode 100644
index 00000000000..3fe8b0569c8
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_side_effect_target/main.c
@@ -0,0 +1,16 @@
+#include <stdbool.h>
+
+int foo(bool a, int *x, int *y) __CPROVER_assigns(a : *x++)
+{
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_side_effect_target/test.desc b/regression/contracts/assigns_enforce_conditional_side_effect_target/test.desc
new file mode 100644
index 00000000000..cb413830d56
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_side_effect_target/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^.* error: side-effects not allowed in assigns clause targets$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that side-effect expressions are rejected from conditional targets.
diff --git a/regression/contracts/assigns_enforce_conditional_side_effect_target_list/main.c b/regression/contracts/assigns_enforce_conditional_side_effect_target_list/main.c
new file mode 100644
index 00000000000..a83f23b4a10
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_side_effect_target_list/main.c
@@ -0,0 +1,16 @@
+#include <stdbool.h>
+
+int foo(bool a, int *x, int *y) __CPROVER_assigns(a : *x++, *y)
+{
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_side_effect_target_list/test.desc b/regression/contracts/assigns_enforce_conditional_side_effect_target_list/test.desc
new file mode 100644
index 00000000000..cb413830d56
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_side_effect_target_list/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^.* error: side-effects not allowed in assigns clause targets$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that side-effect expressions are rejected from conditional targets.
diff --git a/regression/contracts/assigns_enforce_conditional_ternary_target/main.c b/regression/contracts/assigns_enforce_conditional_ternary_target/main.c
new file mode 100644
index 00000000000..54a0fb18a54
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_ternary_target/main.c
@@ -0,0 +1,16 @@
+#include <stdbool.h>
+
+int foo(bool a, int *x, int *y) __CPROVER_assigns(a : (x ? *x : *y))
+{
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_ternary_target/test.desc b/regression/contracts/assigns_enforce_conditional_ternary_target/test.desc
new file mode 100644
index 00000000000..43a8515c6b3
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_ternary_target/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^.* error: ternary expressions not allowed in assigns clause targets$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that ternary expressions are rejected from conditional targets.
diff --git a/regression/contracts/assigns_enforce_conditional_ternary_target_list/main.c b/regression/contracts/assigns_enforce_conditional_ternary_target_list/main.c
new file mode 100644
index 00000000000..9ac5893434e
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_ternary_target_list/main.c
@@ -0,0 +1,16 @@
+#include <stdbool.h>
+
+int foo(bool a, int *x, int *y) __CPROVER_assigns(a : *x, (x ? *x : *y))
+{
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_ternary_target_list/test.desc b/regression/contracts/assigns_enforce_conditional_ternary_target_list/test.desc
new file mode 100644
index 00000000000..43a8515c6b3
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_ternary_target_list/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^.* error: ternary expressions not allowed in assigns clause targets$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that ternary expressions are rejected from conditional targets.
diff --git a/regression/contracts/assigns_enforce_conditional_unions/main.c b/regression/contracts/assigns_enforce_conditional_unions/main.c
new file mode 100644
index 00000000000..bbbf480132b
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_unions/main.c
@@ -0,0 +1,116 @@
+#include <stdbool.h>
+
+typedef struct CTX
+{
+  int data[16];
+} CTX;
+
+union low_level_t {
+  CTX md5;
+};
+
+typedef struct HIGH_LEVEL_MD
+{
+  unsigned long flags;
+} HIGH_LEVEL_MD;
+
+typedef struct HIGH_LEVEL_MD_CTX
+{
+  HIGH_LEVEL_MD *digest;
+  unsigned long flags;
+} HIGH_LEVEL_MD_CTX;
+
+struct high_level_digest_t
+{
+  HIGH_LEVEL_MD_CTX *ctx;
+};
+
+struct high_level_t
+{
+  struct high_level_digest_t first;
+  struct high_level_digest_t second;
+};
+
+typedef struct state_t
+{
+  union {
+    union low_level_t low_level;
+    struct high_level_t high_level;
+  } digest;
+} state_t;
+
+bool nondet_bool();
+
+bool is_high_level()
+{
+  static bool latch = false;
+  static bool once = false;
+  if(!once)
+  {
+    latch = nondet_bool();
+    once = true;
+  }
+  return latch;
+}
+
+int update(state_t *state, bool also_second)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(state, sizeof(*state)))
+__CPROVER_requires(
+  is_high_level() ==> 
+    __CPROVER_is_fresh(state->digest.high_level.first.ctx, 
+              sizeof(*(state->digest.high_level.first.ctx))) &&
+    __CPROVER_is_fresh(state->digest.high_level.first.ctx->digest, 
+              sizeof(*(state->digest.high_level.first.ctx->digest))))
+__CPROVER_requires(
+  is_high_level() && also_second ==>
+    __CPROVER_is_fresh(state->digest.high_level.second.ctx, 
+              sizeof(*(state->digest.high_level.second.ctx))) &&
+    __CPROVER_is_fresh(state->digest.high_level.second.ctx->digest, 
+              sizeof(*(state->digest.high_level.second.ctx->digest))))
+__CPROVER_assigns(
+  is_high_level():
+    __CPROVER_POINTER_OBJECT(state->digest.high_level.first.ctx->digest),
+    state->digest.high_level.first.ctx->flags;
+  is_high_level() && also_second:
+    __CPROVER_POINTER_OBJECT(state->digest.high_level.second.ctx->digest),  
+    state->digest.high_level.second.ctx->flags;
+)
+// clang-format on
+{
+  if(is_high_level())
+  {
+    // must pass
+    __CPROVER_havoc_object(state->digest.high_level.first.ctx->digest);
+    state->digest.high_level.first.ctx->flags = 0;
+
+    if(also_second)
+    {
+      // must pass
+      __CPROVER_havoc_object(state->digest.high_level.second.ctx->digest);
+      state->digest.high_level.second.ctx->flags = 0;
+    }
+
+    // must fail
+    __CPROVER_havoc_object(state->digest.high_level.second.ctx->digest);
+    state->digest.high_level.second.ctx->flags = 0;
+  }
+
+  // must fail
+  __CPROVER_havoc_object(state->digest.high_level.first.ctx->digest);
+  state->digest.high_level.first.ctx->flags = 0;
+
+  // must fail
+  __CPROVER_havoc_object(state->digest.high_level.second.ctx->digest);
+  state->digest.high_level.second.ctx->flags = 0;
+
+  return 0;
+}
+
+int main()
+{
+  state_t *state;
+  bool also_second;
+  update(state, also_second);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_unions/test.desc b/regression/contracts/assigns_enforce_conditional_unions/test.desc
new file mode 100644
index 00000000000..f9b7044d64e
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_unions/test.desc
@@ -0,0 +1,22 @@
+CORE
+main.c
+--enforce-contract update _ --pointer-check --pointer-overflow-check --signed-overflow-check --unsigned-overflow-check --conversion-check
+^\[is_high_level.\d+\] line 50 Check that latch is assignable: SUCCESS$
+^\[is_high_level.\d+\] line 51 Check that once is assignable: SUCCESS$
+^\[update.\d+\] line 84 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: SUCCESS$
+^\[update.\d+\] line 85 Check that state->digest.high_level.first.ctx->flags is assignable: SUCCESS$
+^\[update.\d+\] line 90 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: SUCCESS$
+^\[update.\d+\] line 91 Check that state->digest.high_level.second.ctx->flags is assignable: SUCCESS$
+^\[update.\d+\] line 95 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$
+^\[update.\d+\] line 96 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
+^\[update.\d+\] line 100 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: FAILURE$
+^\[update.\d+\] line 101 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$
+^\[update.\d+\] line 104 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$
+^\[update.\d+\] line 105 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Tests that conditional assignments to whole objects and lvalues are supported,
+when conditions determine how to interpret a union type.
diff --git a/regression/contracts/assigns_enforce_conditional_void_target/main.c b/regression/contracts/assigns_enforce_conditional_void_target/main.c
new file mode 100644
index 00000000000..5eb7ce636b4
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_void_target/main.c
@@ -0,0 +1,15 @@
+#include <stdbool.h>
+
+int foo(bool a, void *x) __CPROVER_assigns(a : *x)
+{
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+
+  foo(a, &x);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_void_target/test.desc b/regression/contracts/assigns_enforce_conditional_void_target/test.desc
new file mode 100644
index 00000000000..dd1dc9cb31f
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_void_target/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^.* error: void-typed expressions not allowed as assigns clause targets$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that void-typed expressions are rejected from conditional targets.
diff --git a/regression/contracts/assigns_enforce_conditional_void_target_list/main.c b/regression/contracts/assigns_enforce_conditional_void_target_list/main.c
new file mode 100644
index 00000000000..0d6c98acd68
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_void_target_list/main.c
@@ -0,0 +1,16 @@
+#include <stdbool.h>
+
+int foo(bool a, void *x, int *y) __CPROVER_assigns(a : *x, *y)
+{
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+
+  foo(a, &x, &x);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_conditional_void_target_list/test.desc b/regression/contracts/assigns_enforce_conditional_void_target_list/test.desc
new file mode 100644
index 00000000000..dd1dc9cb31f
--- /dev/null
+++ b/regression/contracts/assigns_enforce_conditional_void_target_list/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^.* error: void-typed expressions not allowed as assigns clause targets$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that void-typed expressions are rejected from conditional targets.
diff --git a/regression/contracts/assigns_enforce_elvis_1/main.c b/regression/contracts/assigns_enforce_elvis_1/main.c
deleted file mode 100644
index 31f92a5b20d..00000000000
--- a/regression/contracts/assigns_enforce_elvis_1/main.c
+++ /dev/null
@@ -1,23 +0,0 @@
-#include <assert.h>
-#include <stdbool.h>
-#include <stdlib.h>
-
-int foo(bool a, int *x, int *y, int *z) __CPROVER_assigns(*(a ? x : y))
-{
-  if(a)
-    *x = 0; // must pass
-  else
-    *y = 0; // must pass
-  return 0;
-}
-
-int main()
-{
-  bool a;
-  int x;
-  int y;
-  int z;
-
-  foo(a, &x, &y, &z);
-  return 0;
-}
diff --git a/regression/contracts/assigns_enforce_elvis_1/test.desc b/regression/contracts/assigns_enforce_elvis_1/test.desc
deleted file mode 100644
index c7dd3e0650e..00000000000
--- a/regression/contracts/assigns_enforce_elvis_1/test.desc
+++ /dev/null
@@ -1,12 +0,0 @@
-CORE
-main.c
---enforce-contract foo
-^EXIT=0$
-^SIGNAL=0$
-main.c function foo
-^\[foo.1] line \d+ Check that \*x is assignable: SUCCESS$
-^\[foo.2] line \d+ Check that \*y is assignable: SUCCESS$
-^VERIFICATION SUCCESSFUL$
---
---
-Check that Elvis operator expressions '*(cond ? if_true : if_false)' are accepted in assigns clauses and work as expected.
diff --git a/regression/contracts/assigns_enforce_elvis_2/main.c b/regression/contracts/assigns_enforce_elvis_2/main.c
deleted file mode 100644
index bd2a3d04bc3..00000000000
--- a/regression/contracts/assigns_enforce_elvis_2/main.c
+++ /dev/null
@@ -1,23 +0,0 @@
-#include <assert.h>
-#include <stdbool.h>
-#include <stdlib.h>
-
-int foo(bool a, int *x, int *y, int *z) __CPROVER_assigns(*(a ? x : y))
-{
-  if(a)
-    *x = 0; // must pass
-  else
-    *z = 0; // must fail
-  return 0;
-}
-
-int main()
-{
-  bool a;
-  int x;
-  int y;
-  int z;
-
-  foo(a, &x, &y, &z);
-  return 0;
-}
diff --git a/regression/contracts/assigns_enforce_elvis_2/test.desc b/regression/contracts/assigns_enforce_elvis_2/test.desc
deleted file mode 100644
index d62accd4897..00000000000
--- a/regression/contracts/assigns_enforce_elvis_2/test.desc
+++ /dev/null
@@ -1,12 +0,0 @@
-CORE
-main.c
---enforce-contract foo
-^EXIT=10$
-^SIGNAL=0$
-main.c function foo
-^\[foo.1] line \d+ Check that \*x is assignable: SUCCESS$
-^\[foo.2] line \d+ Check that \*z is assignable: FAILURE$
-^VERIFICATION FAILED$
---
---
-Check that Elvis operator expressions '*(cond ? if_true : if_false)' are accepted in assigns clauses and work as expected.
diff --git a/regression/contracts/assigns_enforce_elvis_3/main.c b/regression/contracts/assigns_enforce_elvis_3/main.c
deleted file mode 100644
index 48f8b893475..00000000000
--- a/regression/contracts/assigns_enforce_elvis_3/main.c
+++ /dev/null
@@ -1,29 +0,0 @@
-#include <assert.h>
-#include <stdbool.h>
-#include <stdlib.h>
-
-int foo(bool a, int *x, int *y, int *z) __CPROVER_assigns(*(a ? x : y))
-{
-  if(a)
-  {
-    *x = 0; // must pass
-  }
-  else
-  {
-    // must pass because in the context of main, this branch is dead
-    // so foo never attempts to write to *z.
-    *z = 0;
-  }
-  return 0;
-}
-
-int main()
-{
-  bool a;
-  int x;
-  int y;
-  int z;
-
-  foo(true, &x, &y, &z);
-  return 0;
-}
diff --git a/regression/contracts/assigns_enforce_elvis_3/test.desc b/regression/contracts/assigns_enforce_elvis_3/test.desc
deleted file mode 100644
index 7499de51d58..00000000000
--- a/regression/contracts/assigns_enforce_elvis_3/test.desc
+++ /dev/null
@@ -1,12 +0,0 @@
-CORE
-main.c
---enforce-contract foo
-^EXIT=0$
-^SIGNAL=0$
-main.c function foo
-^\[foo.1] line \d+ Check that \*x is assignable: SUCCESS$
-^\[foo.2] line \d+ Check that \*z is assignable: SUCCESS$
-^VERIFICATION SUCCESSFUL$
---
---
-Check that Elvis operator expressions '*(cond ? if_true : if_false)' are accepted in assigns clauses.
diff --git a/regression/contracts/assigns_enforce_elvis_4/main.c b/regression/contracts/assigns_enforce_elvis_4/main.c
deleted file mode 100644
index 7d946352b0b..00000000000
--- a/regression/contracts/assigns_enforce_elvis_4/main.c
+++ /dev/null
@@ -1,26 +0,0 @@
-#include <assert.h>
-#include <stdbool.h>
-#include <stdlib.h>
-
-int foo(bool a, int *x, long long *y) __CPROVER_assigns(*(a ? x : y))
-{
-  if(a)
-  {
-    *x = 0;
-  }
-  else
-  {
-    *y = 0;
-  }
-  return 0;
-}
-
-int main()
-{
-  bool a;
-  int x;
-  long y;
-
-  foo(true, &x, &y);
-  return 0;
-}
diff --git a/regression/contracts/assigns_enforce_elvis_4/test.desc b/regression/contracts/assigns_enforce_elvis_4/test.desc
deleted file mode 100644
index b2f68af4a92..00000000000
--- a/regression/contracts/assigns_enforce_elvis_4/test.desc
+++ /dev/null
@@ -1,9 +0,0 @@
-CORE
-main.c
---enforce-contract foo
-^EXIT=(1|64)$
-^SIGNAL=0$
-^.*error: void-typed targets not permitted in assigns clause$
---
---
-Check that Elvis operator expressions '*(cond ? if_true : if_false)' with different types in true and false branches are rejected.
diff --git a/regression/contracts/assigns_enforce_elvis_5/main.c b/regression/contracts/assigns_enforce_elvis_5/main.c
deleted file mode 100644
index ffe9b915f02..00000000000
--- a/regression/contracts/assigns_enforce_elvis_5/main.c
+++ /dev/null
@@ -1,26 +0,0 @@
-#include <assert.h>
-#include <stdbool.h>
-#include <stdlib.h>
-
-int foo(bool a, int *x, int *y) __CPROVER_assigns((a ? *x : *y))
-{
-  if(a)
-  {
-    *x = 0;
-  }
-  else
-  {
-    *y = 0;
-  }
-  return 0;
-}
-
-int main()
-{
-  bool a;
-  int x;
-  int y;
-
-  foo(true, &x, &y);
-  return 0;
-}
diff --git a/regression/contracts/assigns_enforce_elvis_5/test.desc b/regression/contracts/assigns_enforce_elvis_5/test.desc
deleted file mode 100644
index 10c0f7a376a..00000000000
--- a/regression/contracts/assigns_enforce_elvis_5/test.desc
+++ /dev/null
@@ -1,12 +0,0 @@
-KNOWNBUG
-main.c
---enforce-contract foo
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
---
-Check that Elvis operator expressions of form '(cond ? *if_true : *if_false)'
-are supported in assigns clauses.
-
-BUG: `is_lvalue` in goto is not consistent with `target.get_bool(ID_C_lvalue)`.
diff --git a/regression/contracts/assigns_enforce_function_calls/main.c b/regression/contracts/assigns_enforce_function_calls/main.c
index 14e8d530642..dffa10e0575 100644
--- a/regression/contracts/assigns_enforce_function_calls/main.c
+++ b/regression/contracts/assigns_enforce_function_calls/main.c
@@ -1,7 +1,3 @@
-#include <assert.h>
-#include <stdbool.h>
-#include <stdlib.h>
-
 int *bar(int *x)
 {
   return *x;
diff --git a/regression/contracts/assigns_enforce_function_calls/test.desc b/regression/contracts/assigns_enforce_function_calls/test.desc
index a18e73b93cf..dae80dd0935 100644
--- a/regression/contracts/assigns_enforce_function_calls/test.desc
+++ b/regression/contracts/assigns_enforce_function_calls/test.desc
@@ -3,7 +3,8 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: non-lvalue target in assigns clause$
+^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
+^.*error: side-effects not allowed in assigns clause targets$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_literal/test.desc b/regression/contracts/assigns_enforce_literal/test.desc
index e5fa1712864..96b830b76af 100644
--- a/regression/contracts/assigns_enforce_literal/test.desc
+++ b/regression/contracts/assigns_enforce_literal/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: non-lvalue target in assigns clause$
+^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_side_effects_1/test.desc b/regression/contracts/assigns_enforce_side_effects_1/test.desc
index 57965527d2a..693bd0f8f05 100644
--- a/regression/contracts/assigns_enforce_side_effects_1/test.desc
+++ b/regression/contracts/assigns_enforce_side_effects_1/test.desc
@@ -1,10 +1,13 @@
 CORE
 main.c
 --enforce-contract foo
+^.*error: void-typed expressions not allowed as assigns clause targets$
+^.*error: side-effects not allowed in assigns clause targets$
+^.*error: ternary expressions not allowed in assigns clause targets$
+^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: void-typed targets not permitted in assigns clause$
-^CONVERSION ERROR$
 --
 --
-Check that expressions with side effects are rejected from assigns clauses.
+Check that expressions with void type, side effects and/or ternay operators are 
+rejected from assigns clauses.
diff --git a/regression/contracts/assigns_enforce_side_effects_2/test.desc b/regression/contracts/assigns_enforce_side_effects_2/test.desc
index c0ee204ba71..6894b4933b5 100644
--- a/regression/contracts/assigns_enforce_side_effects_2/test.desc
+++ b/regression/contracts/assigns_enforce_side_effects_2/test.desc
@@ -3,7 +3,8 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: non-lvalue target in assigns clause$
+^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
+^.*error: side-effects not allowed in assigns clause targets$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_side_effects_3/test.desc b/regression/contracts/assigns_enforce_side_effects_3/test.desc
index c0ee204ba71..6894b4933b5 100644
--- a/regression/contracts/assigns_enforce_side_effects_3/test.desc
+++ b/regression/contracts/assigns_enforce_side_effects_3/test.desc
@@ -3,7 +3,8 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: non-lvalue target in assigns clause$
+^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
+^.*error: side-effects not allowed in assigns clause targets$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_replace_conditional_targets/main.c b/regression/contracts/assigns_replace_conditional_targets/main.c
new file mode 100644
index 00000000000..ec6a23306de
--- /dev/null
+++ b/regression/contracts/assigns_replace_conditional_targets/main.c
@@ -0,0 +1,74 @@
+#include <stdbool.h>
+
+bool nz(int x)
+{
+  return x == 0;
+}
+
+int foo(bool a, int *x, int *y, char *z)
+  // clang-format off
+__CPROVER_requires(x && y && z)
+__CPROVER_assigns(
+   a && nz(*x): *x;
+  !a && nz(*y): *y;
+  !nz(*x) && !nz(*y): __CPROVER_POINTER_OBJECT(z);
+)
+__CPROVER_ensures(true)
+// clang-format on
+{
+  if(!nz(*x) && !nz(*y))
+    __CPROVER_havoc_object(z);
+
+  if(a && x)
+  {
+    if(nz(*x))
+      *x = 0;
+  }
+
+  if(~!a && y)
+  {
+    if(nz(*y))
+      *y = 0;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  bool a, old_a;
+  old_a = a;
+
+  int x, old_x;
+  old_x = x;
+
+  int y, old_y;
+  old_y = y;
+
+  char *z = malloc(1);
+  *z = '0';
+
+  foo(a, &x, &y, z);
+
+  // check frame conditions
+  // clang-format off
+  __CPROVER_assert(old_a == a, "a unchanged, expecting SUCCESS");
+
+  __CPROVER_assert(
+    old_a && nz(old_x) ==> x == old_x, "x changed, expecting FAILURE");
+  __CPROVER_assert(
+    !(old_a && nz(old_x)) ==> x == old_x, "x unchanged, expecting SUCCESS");
+
+  __CPROVER_assert(
+    !old_a && nz(old_y) ==> y == old_y, "y changed, expecting FAILURE");
+  __CPROVER_assert(
+    !(!old_a && nz(old_y)) ==> y == old_y, "y unchanged, expecting SUCCESS");
+
+  __CPROVER_assert(
+    !(nz(old_x) || nz(old_y)) ==> *z == '0', "z changed, expecting FAILURE");
+  __CPROVER_assert(
+    nz(old_x) || nz(old_y) ==> *z == '0', "z unchanged, expecting SUCCESS");
+  // clang-format on
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_replace_conditional_targets/test.desc b/regression/contracts/assigns_replace_conditional_targets/test.desc
new file mode 100644
index 00000000000..bc973ad8152
--- /dev/null
+++ b/regression/contracts/assigns_replace_conditional_targets/test.desc
@@ -0,0 +1,19 @@
+CORE
+main.c
+--replace-call-with-contract foo
+^main.c function main$
+^\[main\.assertion\.\d+\] line 55 a unchanged, expecting SUCCESS: SUCCESS$
+^\[main\.assertion\.\d+\] line 57 x changed, expecting FAILURE: FAILURE$
+^\[main\.assertion\.\d+\] line 59 x unchanged, expecting SUCCESS: SUCCESS$
+^\[main\.assertion\.\d+\] line 62 y changed, expecting FAILURE: FAILURE$
+^\[main\.assertion\.\d+\] line 64 y unchanged, expecting SUCCESS: SUCCESS$
+^\[main\.assertion\.\d+\] line 67 z changed, expecting FAILURE: FAILURE$
+^\[main\.assertion\.\d+\] line 69 z unchanged, expecting SUCCESS: SUCCESS$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that havocking of conditional targets works as expected when 
+replacing a call by a contract. We manually express frame conditions as 
+assertions in the main function.
diff --git a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc
index c77f85d72c7..3d83d1cf5e7 100644
--- a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc
+++ b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
-error: non-lvalue target in assigns clause
+^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
 --
-Checks whether type checking reports illegal target in assigns clause.
+Checks whether type checking rejects literal constants in assigns clause.
diff --git a/src/ansi-c/c_expr.h b/src/ansi-c/c_expr.h
index 9ef4902010c..c58c4e41716 100644
--- a/src/ansi-c/c_expr.h
+++ b/src/ansi-c/c_expr.h
@@ -225,4 +225,99 @@ to_history_expr(const exprt &expr, const irep_idt &id)
   return ret;
 }
 
+/// \brief A class for an expression that represents a conditional target or
+/// a list of targets sharing a common condition
+/// in an assigns clause.
+class conditional_target_group_exprt : public exprt
+{
+public:
+  explicit conditional_target_group_exprt(exprt _condition, exprt _target_list)
+    : exprt(ID_conditional_target_group, empty_typet{})
+  {
+    add_to_operands(std::move(_condition));
+    add_to_operands(std::move(_target_list));
+  }
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      vm,
+      expr.operands().size() == 2,
+      "conditional target expression must have two operands");
+
+    DATA_CHECK(
+      vm,
+      expr.operands()[1].id() == ID_expression_list,
+      "conditional target second operand must be an ID_expression_list "
+      "expression, found " +
+        id2string(expr.operands()[1].id()));
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check(expr, vm);
+  }
+
+  const exprt &condition() const
+  {
+    return op0();
+  }
+
+  exprt &condition()
+  {
+    return op0();
+  }
+
+  const exprt::operandst &targets() const
+  {
+    return op1().operands();
+  }
+
+  exprt::operandst &targets()
+  {
+    return op1().operands();
+  }
+};
+
+inline void validate_expr(const conditional_target_group_exprt &value)
+{
+  conditional_target_group_exprt::check(value);
+}
+
+template <>
+inline bool can_cast_expr<conditional_target_group_exprt>(const exprt &base)
+{
+  return base.id() == ID_conditional_target_group;
+}
+
+/// \brief Cast an exprt to a \ref conditional_target_group_exprt
+///
+/// \a expr must be known to be \ref conditional_target_group_exprt
+///
+/// \param expr: Source expression
+/// \return Object of type \ref conditional_target_group_exprt
+inline const conditional_target_group_exprt &
+to_conditional_target_group_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_conditional_target_group);
+  auto &ret = static_cast<const conditional_target_group_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_conditional_target_group_expr(const exprt &expr)
+inline conditional_target_group_exprt &
+to_conditional_target_group_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_conditional_target_group);
+  auto &ret = static_cast<conditional_target_group_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_ANSI_C_C_EXPR_H
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index 1b92f0e633a..fe537c10de5 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -147,6 +147,8 @@ class c_typecheck_baset:
 
   // contracts
   virtual void typecheck_spec_assigns(exprt::operandst &targets);
+  virtual void typecheck_spec_assigns_condition(exprt &condition);
+  virtual void typecheck_spec_assigns_target(exprt &target);
   virtual void typecheck_spec_loop_invariant(codet &code);
   virtual void typecheck_spec_decreases(codet &code);
 
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 2d3837c74ce..5cefafcf7ae 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "c_typecheck_base.h"
 
+#include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_util.h>
@@ -18,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/string_constant.h>
 
 #include "ansi_c_declaration.h"
+#include "c_expr.h"
 
 void c_typecheck_baset::start_typecheck_code()
 {
@@ -842,35 +844,168 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
   }
 }
 
+void c_typecheck_baset::typecheck_spec_assigns_condition(exprt &condition)
+{
+  // compute type
+  typecheck_expr(condition);
+
+  // make it boolean if needed
+  implicit_typecast_bool(condition);
+
+  // non-fatal warnings
+  if(has_subexpr(condition, can_cast_expr<side_effect_expr_function_callt>))
+  {
+    // Remark: we allow function calls without further checks for now because
+    // they are mandatory for some applications.
+    // The next step must be to check that the called functions have a contract
+    // with an empty assigns clause and that they indeed satisfy their contract
+    // using a CI check.
+    warning().source_location = condition.source_location();
+    warning()
+      << "function with possible side-effect called in target's condition"
+      << eom;
+  }
+
+  // fatal errors
+  bool must_throw = false;
+
+  if(condition.type().id() == ID_empty)
+  {
+    must_throw = true;
+    error().source_location = condition.source_location();
+    error() << "void-typed expressions not allowed as assigns clause conditions"
+            << eom;
+  }
+
+  if(has_subexpr(condition, [&](const exprt &subexpr) {
+       return can_cast_expr<side_effect_exprt>(subexpr) &&
+              !can_cast_expr<side_effect_expr_function_callt>(subexpr);
+     }))
+  {
+    must_throw = true;
+    error().source_location = condition.source_location();
+    error() << "side-effects not allowed in assigns clause conditions" << eom;
+  }
+
+  if(has_subexpr(condition, ID_if))
+  {
+    must_throw = true;
+    error().source_location = condition.source_location();
+    error() << "ternary expressions not allowed in assigns "
+               "clause conditions"
+            << eom;
+  }
+
+  if(must_throw)
+    throw 0;
+}
+
+void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target)
+{
+  // compute type
+  typecheck_expr(target);
+
+  // fatal errors
+  bool must_throw = false;
+  if(target.type().id() == ID_empty)
+  {
+    must_throw = true;
+    error().source_location = target.source_location();
+    error() << "void-typed expressions not allowed as assigns clause targets"
+            << eom;
+  }
+
+  if(!target.get_bool(ID_C_lvalue) && target.id() != ID_pointer_object)
+  {
+    must_throw = true;
+    error().source_location = target.source_location();
+    error() << "assigns clause target must be an lvalue or " CPROVER_PREFIX
+               "POINTER_OBJECT expression"
+            << eom;
+  }
+
+  // Remark: an expression can be an lvalue and still contain side effects
+  // or ternary expressions. We detect them in a second step.
+  if(has_subexpr(target, ID_side_effect))
+  {
+    must_throw = true;
+    error().source_location = target.source_location();
+    error() << "side-effects not allowed in assigns clause targets" << eom;
+  }
+
+  if(has_subexpr(target, ID_if))
+  {
+    must_throw = true;
+    error().source_location = target.source_location();
+    error() << "ternary expressions not allowed in assigns "
+               "clause targets"
+            << eom;
+  }
+
+  if(must_throw)
+    throw 0;
+}
+
 void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
 {
+  exprt::operandst tmp;
+  bool must_throw = false;
+
   for(auto &target : targets)
   {
-    typecheck_expr(target);
-
-    if(target.type().id() == ID_empty)
+    if(!can_cast_expr<conditional_target_group_exprt>(target))
     {
+      must_throw = true;
       error().source_location = target.source_location();
-      error() << "void-typed targets not permitted in assigns clause" << eom;
-      throw 0;
-    }
-    else if(target.id() == ID_pointer_object)
-    {
-      // skip
+      error() << "expected ID_conditional_target_group expression in assigns "
+                 "clause, found "
+              << id2string(target.id()) << eom;
     }
-    else if(!target.get_bool(ID_C_lvalue))
+
+    auto &conditional_target_group = to_conditional_target_group_expr(target);
+    validate_expr(conditional_target_group);
+
+    // typecheck condition
+    auto &condition = conditional_target_group.condition();
+    typecheck_spec_assigns_condition(condition);
+
+    if(condition.is_true())
     {
-      error().source_location = target.source_location();
-      error() << "non-lvalue target in assigns clause" << eom;
-      throw 0;
+      // if the condition is trivially true,
+      // simplify expr and expose the bare expressions
+      for(auto &actual_target : conditional_target_group.targets())
+      {
+        typecheck_spec_assigns_target(actual_target);
+        tmp.push_back(actual_target);
+      }
     }
-    else if(has_subexpr(target, ID_side_effect))
+    else
     {
-      error().source_location = target.source_location();
-      error() << "assigns clause is not side-effect free" << eom;
-      throw 0;
+      // if the condition is not trivially true,
+      // place each single target in its own conditional target expr,
+      // distributing the condition
+      for(auto &actual_target : conditional_target_group.targets())
+      {
+        typecheck_spec_assigns_target(actual_target);
+        exprt ops{ID_expression_list};
+        ops.add_to_operands(actual_target);
+        conditional_target_group_exprt result{condition, ops};
+        result.add_source_location() =
+          conditional_target_group.source_location();
+        tmp.push_back(std::move(result));
+      }
     }
   }
+
+  // at least one target was not as expected
+  if(must_throw)
+    throw 0;
+
+  // now each target is either a simple side-effect-free lvalue expression
+  // or a conditional target expression with a single target
+
+  // update original vector in-place
+  std::swap(targets, tmp);
 }
 
 void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 92b66ee0e17..b4aff20aa69 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -3470,6 +3470,31 @@ std::string expr2ct::convert_sizeof(
   return dest;
 }
 
+std::string expr2ct::convert_conditional_target_group(const exprt &src)
+{
+  std::string dest;
+  unsigned p;
+  const auto &cond = src.operands().front();
+  if(!cond.is_true())
+  {
+    dest += convert_with_precedence(cond, p);
+    dest += ": ";
+  }
+
+  const auto &targets = src.operands()[1];
+  forall_operands(it, targets)
+  {
+    std::string op = convert_with_precedence(*it, p);
+
+    if(it != targets.operands().begin())
+      dest += ", ";
+
+    dest += op;
+  }
+
+  return dest;
+}
+
 std::string expr2ct::convert_with_precedence(
   const exprt &src,
   unsigned &precedence)
@@ -3873,6 +3898,11 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id() == ID_rol || src.id() == ID_ror)
     return convert_rox(to_shift_expr(src), precedence);
 
+  else if(src.id() == ID_conditional_target_group)
+  {
+    return convert_conditional_target_group(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 7671b8004b2..76191617e93 100644
--- a/src/ansi-c/expr2c_class.h
+++ b/src/ansi-c/expr2c_class.h
@@ -275,6 +275,8 @@ class expr2ct
     const exprt &src,
     unsigned &precedence,
     bool include_padding_components);
+
+  std::string convert_conditional_target_group(const exprt &src);
 };
 
 #endif // CPROVER_ANSI_C_EXPR2C_CLASS_H
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 17b2bf89be1..e2ac4d54dd5 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -3297,12 +3297,65 @@ cprover_function_contract:
         | cprover_contract_assigns
         ;
 
+unary_expression_list:
+          unary_expression
+        {
+          init($$, ID_expression_list);
+          parser_stack($$).add_source_location()=parser_stack($1).source_location();
+          mto($$, $1);
+        }
+        | unary_expression_list ',' unary_expression
+        {
+          $$=$1;
+          mto($$, $3);
+        }
+        ;
+
+conditional_target_group:
+          unary_expression_list
+        {
+          init($$, ID_conditional_target_group);
+          parser_stack($$).add_source_location()=parser_stack($1).source_location();
+          parser_stack($$).add_to_operands(true_exprt{});
+          mto($$, $1);
+        }
+        | logical_equivalence_expression ':' unary_expression_list
+        { 
+          $$=$2;
+          set($$, ID_conditional_target_group);
+          mto($$, $1);
+          mto($$, $3);
+        }
+        ;
+
+conditional_target_list:
+          conditional_target_group
+        {
+          init($$, ID_target_list);
+          mto($$, $1);
+        }
+        | conditional_target_list ';' conditional_target_group
+        {
+          $$=$1;
+          mto($$, $3);
+        }
+        ;
+
+conditional_target_list_opt_semicol:
+          conditional_target_list ';'
+        {
+          $$ = $1;
+        }
+        | conditional_target_list
+        {
+          $$ = $1;          
+        }
+
 cprover_contract_assigns:
-         TOK_CPROVER_ASSIGNS '(' argument_expression_list ')'
+         TOK_CPROVER_ASSIGNS '(' conditional_target_list_opt_semicol ')'
         {
           $$=$1;
           set($$, ID_C_spec_assigns);
-          parser_stack($3).id(ID_target_list);
           mto($$, $3);
         }
         | TOK_CPROVER_ASSIGNS '(' ')'
diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp
index 6e17935a63e..4305d99bf01 100644
--- a/src/goto-instrument/contracts/assigns.cpp
+++ b/src/goto-instrument/contracts/assigns.cpp
@@ -18,8 +18,11 @@ Date: July 2021
 
 #include <langapi/language_util.h>
 
+#include <ansi-c/c_expr.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/expr_util.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 
@@ -42,7 +45,7 @@ static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns)
 
     INVARIANT(
       size.has_value(),
-      "`sizeof` must always be computable on l-value assigns clause targets.");
+      "no definite size for lvalue target: \n" + expr.pretty());
 
     return {typecast_exprt::conditional_cast(
               address_of_exprt{expr}, pointer_type(char_type())),
@@ -52,6 +55,41 @@ static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns)
   UNREACHABLE;
 }
 
+/// Normalises a assigns target expression to a guarded slice struct.
+///
+/// ```
+/// case expr of
+///  | guard ? target ->
+///          {guard
+///           target,
+///           normalize_to_slice(target)}
+///  | target ->
+///          {true,
+///           target,
+///           normalize_to_slice(target)}
+/// ```
+static const guarded_slicet
+normalize_to_guarded_slice(const exprt &expr, const namespacet &ns)
+{
+  if(can_cast_expr<conditional_target_group_exprt>(expr))
+  {
+    const auto &conditional_target_group =
+      to_conditional_target_group_expr(expr);
+    INVARIANT(
+      conditional_target_group.targets().size() == 1,
+      "expecting only a single target");
+    const auto &target = conditional_target_group.targets().front();
+    const auto slice = normalize_to_slice(target, ns);
+    return {
+      conditional_target_group.condition(), target, slice.first, slice.second};
+  }
+  else
+  {
+    const auto slice = normalize_to_slice(expr, ns);
+    return {true_exprt{}, expr, slice.first, slice.second};
+  }
+}
+
 const symbolt assigns_clauset::conditional_address_ranget::generate_new_symbol(
   const std::string &prefix,
   const typet &type,
@@ -71,15 +109,19 @@ assigns_clauset::conditional_address_ranget::conditional_address_ranget(
   : source_expr(expr),
     location(expr.source_location()),
     parent(parent),
-    slice(normalize_to_slice(expr, parent.ns)),
+    guarded_slice(normalize_to_guarded_slice(expr, parent.ns)),
     validity_condition_var(
       generate_new_symbol("__car_valid", bool_typet(), location).symbol_expr()),
-    lower_bound_address_var(
-      generate_new_symbol("__car_lb", slice.first.type(), location)
-        .symbol_expr()),
-    upper_bound_address_var(
-      generate_new_symbol("__car_ub", slice.first.type(), location)
-        .symbol_expr())
+    lower_bound_address_var(generate_new_symbol(
+                              "__car_lb",
+                              guarded_slice.start_adress.type(),
+                              location)
+                              .symbol_expr()),
+    upper_bound_address_var(generate_new_symbol(
+                              "__car_ub",
+                              guarded_slice.start_adress.type(),
+                              location)
+                              .symbol_expr())
 {
 }
 
@@ -93,6 +135,19 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
   source_locationt location_no_checks = location;
   disable_pointer_checks(location_no_checks);
 
+  // clean up side effects from the guard expression if needed
+  cleanert cleaner(parent.symbol_table, parent.log.get_message_handler());
+  exprt clean_guard(guarded_slice.guard);
+
+  if(has_subexpr(clean_guard, ID_side_effect))
+    cleaner.clean(
+      clean_guard,
+      instructions,
+      parent.symbol_table.lookup_ref(parent.function_name).mode);
+
+  // we want checks on the guard because it is user code
+  clean_guard.add_source_location() = location;
+
   instructions.add(
     goto_programt::make_decl(validity_condition_var, location_no_checks));
   instructions.add(
@@ -102,11 +157,11 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
 
   instructions.add(goto_programt::make_assignment(
     lower_bound_address_var,
-    null_pointer_exprt{to_pointer_type(slice.first.type())},
+    null_pointer_exprt{to_pointer_type(guarded_slice.start_adress.type())},
     location_no_checks));
   instructions.add(goto_programt::make_assignment(
     upper_bound_address_var,
-    null_pointer_exprt{to_pointer_type(slice.first.type())},
+    null_pointer_exprt{to_pointer_type(guarded_slice.start_adress.type())},
     location_no_checks));
 
   goto_programt skip_program;
@@ -114,8 +169,10 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
     skip_program.add(goto_programt::make_skip(location_no_checks));
 
   const auto validity_check_expr =
-    and_exprt{all_dereferences_are_valid(source_expr, parent.ns),
-              w_ok_exprt{slice.first, slice.second}};
+    and_exprt{clean_guard,
+              all_dereferences_are_valid(guarded_slice.expr, parent.ns),
+              w_ok_exprt{guarded_slice.start_adress, guarded_slice.size}};
+
   instructions.add(goto_programt::make_assignment(
     validity_condition_var, validity_check_expr, location_no_checks));
 
@@ -123,7 +180,7 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
     skip_target, not_exprt{validity_condition_var}, location_no_checks));
 
   instructions.add(goto_programt::make_assignment(
-    lower_bound_address_var, slice.first, location_no_checks));
+    lower_bound_address_var, guarded_slice.start_adress, location_no_checks));
 
   // the computation of the CAR upper bound can overflow into the object ID bits
   // of the pointer with very large allocation sizes.
@@ -133,7 +190,7 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
 
   instructions.add(goto_programt::make_assignment(
     upper_bound_address_var,
-    plus_exprt{slice.first, slice.second},
+    plus_exprt{guarded_slice.start_adress, guarded_slice.size},
     location_overflow_check));
   instructions.destructive_append(skip_program);
 
@@ -170,7 +227,7 @@ bool assigns_clauset::conditional_address_ranget::maybe_alive(
 
 assigns_clauset::assigns_clauset(
   const exprt::operandst &assigns,
-  const messaget &log,
+  messaget &log,
   const namespacet &ns,
   const irep_idt &function_name,
   symbol_tablet &symbol_table)
diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h
index f43251347de..9e92136af1b 100644
--- a/src/goto-instrument/contracts/assigns.h
+++ b/src/goto-instrument/contracts/assigns.h
@@ -22,6 +22,27 @@ Date: July 2021
 
 typedef std::pair<const exprt, const exprt> slicet;
 
+/// A guarded slice of memory
+typedef struct guarded_slicet
+{
+  guarded_slicet(exprt _guard, exprt _expr, exprt _start_address, exprt _size)
+    : guard(_guard), expr(_expr), start_adress(_start_address), size(_size)
+  {
+  }
+
+  /// Guard expression (may contain side_effect_exprt expressions)
+  const exprt guard;
+
+  /// Target expression
+  const exprt expr;
+
+  /// Start address of the target
+  const exprt start_adress;
+
+  /// Size of the target
+  const exprt size;
+} guarded_slicet;
+
 /// \brief A class for representing assigns clauses in code contracts
 class assigns_clauset
 {
@@ -56,7 +77,7 @@ class assigns_clauset
     const source_locationt &location;
     const assigns_clauset &parent;
 
-    const slicet slice;
+    const guarded_slicet guarded_slice;
     const symbol_exprt validity_condition_var;
     const symbol_exprt lower_bound_address_var;
     const symbol_exprt upper_bound_address_var;
@@ -78,11 +99,11 @@ class assigns_clauset
       write_sett;
 
   assigns_clauset(
-    const exprt::operandst &,
-    const messaget &,
-    const namespacet &,
-    const irep_idt &,
-    symbol_tablet &);
+    const exprt::operandst &assigns,
+    messaget &log,
+    const namespacet &ns,
+    const irep_idt &function_name,
+    symbol_tablet &symbol_table);
 
   write_sett::const_iterator add_to_write_set(const exprt &);
   void remove_from_write_set(const exprt &);
@@ -111,7 +132,7 @@ class assigns_clauset
     const goto_functionst &functions,
     const irep_idt &root_function);
 
-  const messaget &log;
+  messaget &log;
   const namespacet &ns;
   const irep_idt &function_name;
 
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index f857962818e..b55aad00eda 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -801,7 +801,8 @@ bool code_contractst::apply_function_contract(
       location,
       mode,
       ns,
-      symbol_table);
+      symbol_table,
+      log.get_message_handler());
   }
 
   // ...for the return value
diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp
index 7b6d3c8820c..bca49d297ee 100644
--- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp
+++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp
@@ -15,9 +15,12 @@ Author: Remi Delmas, delmasrd@amazon.com
 
 #include <langapi/language_util.h>
 
+#include <ansi-c/c_expr.h>
+
 #include <util/c_types.h>
 #include <util/format_expr.h>
 #include <util/format_type.h>
+#include <util/message.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
@@ -71,6 +74,7 @@ static exprt build_address_of(
 
     return address_of_exprt{target};
   }
+
   UNREACHABLE;
 }
 
@@ -78,18 +82,20 @@ static exprt build_address_of(
 /// of `target_pointer` into `target_snapshot_var`.
 ///
 /// ```
-/// DECL target_valid_var : bool
-/// DECL target_snapshot_var : <target_pointer.type()>
-/// ASSIGN target_valid_var := <all_dereferences_valid(target_pointer)>
-/// ASSIGN target_snapshot_var := NULL
-/// IF !target_valid_var GOTO skip_target
+/// DECL target_valid_var : bool;
+/// DECL target_snapshot_var : <target_pointer.type()>;
+/// ASSIGN target_valid_var := <condition> &
+///                            <all_dereferences_valid(target_pointer)>;
+/// ASSIGN target_snapshot_var := NULL;
+/// IF !target_valid_var GOTO skip_target;
 /// ASSIGN target_snapshot_var := target_pointer;
-/// skip_target: SKIP
+/// skip_target: SKIP;
 /// ```
 ///
 static void snapshot_if_valid(
   const symbol_exprt &target_valid_var,
   const symbol_exprt &target_snapshot_var,
+  const exprt &condition,
   const exprt &target_pointer,
   goto_programt &dest,
   // context parameters
@@ -105,7 +111,7 @@ static void snapshot_if_valid(
 
   dest.add(goto_programt::make_assignment(
     target_valid_var,
-    all_dereferences_are_valid(target_pointer, ns),
+    and_exprt{condition, all_dereferences_are_valid(target_pointer, ns)},
     source_location_no_checks));
 
   dest.add(goto_programt::make_assignment(
@@ -196,6 +202,53 @@ static void havoc_if_valid(
     goto_programt::make_dead(target_snapshot_var, source_location_no_checks));
 }
 
+void havoc_single_target(
+  const exprt &condition,
+  const exprt &target,
+  const source_locationt &source_location,
+  const irep_idt &replaced_function_id,
+  goto_programt &snapshot_program,
+  goto_programt &havoc_program,
+  const namespacet &ns,
+  symbol_tablet &st,
+  irep_idt mode)
+{
+  const auto target_pointer = build_address_of(target, ns);
+  const auto target_snapshot_var = new_tmp_symbol(
+                                     target_pointer.type(),
+                                     source_location,
+                                     mode,
+                                     st,
+                                     "__target_snapshot_var",
+                                     true)
+                                     .symbol_expr();
+  const auto target_valid_var =
+    new_tmp_symbol(
+      bool_typet(), source_location, mode, st, "__target_valid_var", true)
+      .symbol_expr();
+
+  snapshot_if_valid(
+    target_valid_var,
+    target_snapshot_var,
+    condition,
+    target_pointer,
+    snapshot_program,
+    source_location,
+    ns);
+
+  const auto &tracking_comment =
+    make_tracking_comment(target, replaced_function_id, ns);
+
+  havoc_if_valid(
+    target_valid_var,
+    target_snapshot_var,
+    target,
+    tracking_comment,
+    havoc_program,
+    source_location,
+    ns);
+}
+
 void havoc_assigns_clause_targets(
   const irep_idt &replaced_function_id,
   const std::vector<exprt> &targets,
@@ -204,45 +257,52 @@ void havoc_assigns_clause_targets(
   const source_locationt &source_location,
   const irep_idt &mode,
   namespacet &ns,
-  symbol_tablet &st)
+  symbol_tablet &st,
+  message_handlert &message_handler)
 {
   goto_programt snapshot_program;
   goto_programt havoc_program;
 
   for(const auto &target : targets)
   {
-    const auto &tracking_comment =
-      make_tracking_comment(target, replaced_function_id, ns);
-
-    const auto target_pointer = build_address_of(target, ns);
-    const auto target_snapshot_var = new_tmp_symbol(
-                                       target_pointer.type(),
-                                       source_location,
-                                       mode,
-                                       st,
-                                       "__target_snapshot_var",
-                                       true)
-                                       .symbol_expr();
-    const auto target_valid_var =
-      new_tmp_symbol(
-        bool_typet(), source_location, mode, st, "__target_valid_var", true)
-        .symbol_expr();
-
-    snapshot_if_valid(
-      target_valid_var,
-      target_snapshot_var,
-      target_pointer,
-      snapshot_program,
-      source_location,
-      ns);
-    havoc_if_valid(
-      target_valid_var,
-      target_snapshot_var,
-      target,
-      tracking_comment,
-      havoc_program,
-      source_location,
-      ns);
+    if(can_cast_expr<conditional_target_group_exprt>(target))
+    {
+      const auto &cond_target = to_conditional_target_group_expr(target);
+
+      // clean the condition if needed
+      cleanert cleaner(st, message_handler);
+      exprt condition(cond_target.condition());
+      if(has_subexpr(condition, ID_side_effect))
+        cleaner.clean(condition, snapshot_program, mode);
+
+      for(const auto &actual_target : cond_target.targets())
+      {
+        havoc_single_target(
+          condition,
+          actual_target,
+          source_location,
+          replaced_function_id,
+          snapshot_program,
+          havoc_program,
+          ns,
+          st,
+          mode);
+      }
+    }
+    else
+    {
+      // nonconditional target
+      havoc_single_target(
+        true_exprt{},
+        target,
+        source_location,
+        replaced_function_id,
+        snapshot_program,
+        havoc_program,
+        ns,
+        st,
+        mode);
+    }
   }
 
   dest.destructive_append(snapshot_program);
diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.h b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h
index 2a3c6272bda..24fa1daa07f 100644
--- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.h
+++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h
@@ -17,6 +17,7 @@ Author: Remi Delmas, delmasrd@amazon.com
 class namespacet;
 class symbol_tablet;
 class goto_programt;
+class message_handlert;
 
 /// Generates havocking instructions for target expressions of a
 /// function contract's assign clause (replacement).
@@ -29,6 +30,7 @@ class goto_programt;
 /// \param mode Language mode to use for newly generated symbols
 /// \param ns Namespace of the model
 /// \param st Symbol table of the model (new symbols will be added)
+/// \param message_handler handler used to log translation warnings/errors
 ///
 /// Assigns clause targets can be interdependent as shown in this example:
 ///
@@ -55,7 +57,8 @@ void havoc_assigns_clause_targets(
   const source_locationt &source_location,
   const irep_idt &mode,
   namespacet &ns,
-  symbol_tablet &st);
+  symbol_tablet &st,
+  message_handlert &message_handler);
 
 bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment);
 
diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h
index 3ff656953a9..04a4d917426 100644
--- a/src/goto-instrument/contracts/utils.h
+++ b/src/goto-instrument/contracts/utils.h
@@ -18,6 +18,7 @@ Date: September 2021
 
 #include <goto-instrument/havoc_utils.h>
 
+#include <goto-programs/goto_convert_class.h>
 #include <goto-programs/goto_model.h>
 
 #include <util/expr_cast.h>
@@ -206,4 +207,21 @@ class cfg_infot
   const localst locals;
 };
 
+/// Allows to clean expressions of side effects.
+class cleanert : public goto_convertt
+{
+public:
+  cleanert(
+    symbol_table_baset &_symbol_table,
+    message_handlert &_message_handler)
+    : goto_convertt(_symbol_table, _message_handler)
+  {
+  }
+
+  void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
+  {
+    goto_convertt::clean_expr(guard, dest, mode, true);
+  }
+};
+
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 8a793b6651b..9032a991b70 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -578,6 +578,7 @@ IREP_ID_TWO(C_spec_requires, #spec_requires)
 IREP_ID_TWO(C_spec_ensures, #spec_ensures)
 IREP_ID_TWO(C_spec_assigns, #spec_assigns)
 IREP_ID_ONE(target_list)
+IREP_ID_ONE(conditional_target_group)
 IREP_ID_ONE(virtual_function)
 IREP_ID_TWO(element_type, element_type)
 IREP_ID_ONE(working_directory)