diff --git a/regression/contracts-dfcc/loop_contracts_do_while/assigns.c b/regression/contracts-dfcc/loop_contracts_do_while/assigns.c
new file mode 100644
index 00000000000..982f5dd55f3
--- /dev/null
+++ b/regression/contracts-dfcc/loop_contracts_do_while/assigns.c
@@ -0,0 +1,19 @@
+int global;
+
+int main()
+{
+  global = 0;
+  int argc = 1;
+  if(argc > 1)
+  {
+    do
+      __CPROVER_assigns(global)
+      {
+        global = 1;
+      }
+    while(0);
+  }
+  __CPROVER_assert(global == 0, "should be zero");
+
+  return 0;
+}
diff --git a/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc b/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc
new file mode 100644
index 00000000000..4fe2cf25dde
--- /dev/null
+++ b/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc
@@ -0,0 +1,9 @@
+CORE dfcc-only
+assigns.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that loop contracts work correctly on do/while loops.
diff --git a/regression/contracts-dfcc/loop_contracts_do_while/main.c b/regression/contracts-dfcc/loop_contracts_do_while/main.c
index 8519d3953fb..6cdce8ce510 100644
--- a/regression/contracts-dfcc/loop_contracts_do_while/main.c
+++ b/regression/contracts-dfcc/loop_contracts_do_while/main.c
@@ -5,7 +5,7 @@ int main()
   int x = 0;
 
   do
-    __CPROVER_loop_invariant(0 <= x && x <= 10)
+    __CPROVER_loop_invariant(0 <= x && x < 10)
     {
       x++;
     }
diff --git a/regression/contracts-dfcc/loop_contracts_do_while/side_effect.c b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.c
new file mode 100644
index 00000000000..2413640f98c
--- /dev/null
+++ b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.c
@@ -0,0 +1,24 @@
+int global;
+
+int foo()
+{
+  return 0;
+}
+
+int main()
+{
+  global = 0;
+  int argc = 1;
+  if(argc > 1)
+  {
+    do
+      __CPROVER_assigns(global)
+      {
+        global = 1;
+      }
+    while(foo());
+  }
+  __CPROVER_assert(global == 0, "should be zero");
+
+  return 0;
+}
diff --git a/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc
new file mode 100644
index 00000000000..6306416f3bf
--- /dev/null
+++ b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc
@@ -0,0 +1,9 @@
+CORE dfcc-only
+side_effect.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that loop contracts work correctly on do/while loops.
diff --git a/regression/contracts-dfcc/loop_contracts_do_while/test.desc b/regression/contracts-dfcc/loop_contracts_do_while/test.desc
index dbe8bafe65d..a5c1706022a 100644
--- a/regression/contracts-dfcc/loop_contracts_do_while/test.desc
+++ b/regression/contracts-dfcc/loop_contracts_do_while/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE dfcc-only
 main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=0$
diff --git a/regression/contracts/loop_contracts_do_while/test.desc b/regression/contracts/loop_contracts_do_while/test.desc
index 9c52a782fea..b48cda7c0d9 100644
--- a/regression/contracts/loop_contracts_do_while/test.desc
+++ b/regression/contracts/loop_contracts_do_while/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --apply-loop-contracts
 ^EXIT=0$
@@ -7,3 +7,4 @@ main.c
 --
 --
 This test checks that loop contracts work correctly on do/while loops.
+Fails because contracts are not yet supported on do while loops.
diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp
index c2a2e86ca1d..793fba651c3 100644
--- a/src/ansi-c/goto-conversion/goto_convert.cpp
+++ b/src/ansi-c/goto-conversion/goto_convert.cpp
@@ -432,8 +432,25 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest)
     // cannot compare iterators, so compare target number instead
     if(it->get_target()->target_number == it_z->target_number)
     {
+      DATA_INVARIANT(
+        it->condition().find(ID_C_spec_assigns).is_nil() &&
+          it->condition().find(ID_C_spec_loop_invariant).is_nil() &&
+          it->condition().find(ID_C_spec_decreases).is_nil(),
+        "no loop invariant expected");
+      irept y_assigns = it_goto_y->condition().find(ID_C_spec_assigns);
+      irept y_loop_invariant =
+        it_goto_y->condition().find(ID_C_spec_loop_invariant);
+      irept y_decreases = it_goto_y->condition().find(ID_C_spec_decreases);
+
       it->set_target(it_goto_y->get_target());
-      it->condition_nonconst() = boolean_negate(it->condition());
+      exprt updated_condition = boolean_negate(it->condition());
+      if(y_assigns.is_not_nil())
+        updated_condition.add(ID_C_spec_assigns).swap(y_assigns);
+      if(y_loop_invariant.is_not_nil())
+        updated_condition.add(ID_C_spec_loop_invariant).swap(y_loop_invariant);
+      if(y_decreases.is_not_nil())
+        updated_condition.add(ID_C_spec_decreases).swap(y_decreases);
+      it->condition_nonconst() = updated_condition;
       it_goto_y->turn_into_skip();
     }
   }
@@ -1301,7 +1318,7 @@ void goto_convertt::convert_dowhile(
   W->complete_goto(w);
 
   // assigns_clause, loop invariant and decreases clause
-  convert_loop_contracts(code, y);
+  convert_loop_contracts(code, W);
 
   dest.destructive_append(tmp_w);
   dest.destructive_append(side_effects.side_effects);
diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp
index 803cf47eb6a..6dd6cf7e681 100644
--- a/src/goto-instrument/contracts/utils.cpp
+++ b/src/goto-instrument/contracts/utils.cpp
@@ -250,7 +250,7 @@ void insert_before_and_update_jumps(
   const auto new_target = destination.insert_before(target, i);
   for(auto it : target->incoming_edges)
   {
-    if(it->is_goto())
+    if(it->is_goto() && it->get_target() == target)
       it->set_target(new_target);
   }
 }