diff --git a/regression/contracts/do_while_syntax_fail/main.c b/regression/contracts/do_while_syntax_fail/main.c
new file mode 100644
index 00000000000..873efb04249
--- /dev/null
+++ b/regression/contracts/do_while_syntax_fail/main.c
@@ -0,0 +1,14 @@
+int main()
+{
+  int i = 0;
+  do
+  {
+    i++;
+  } while(i < 10)
+    // clang-format off
+   __CPROVER_assigns(i)
+   __CPROVER_loop_invariant(0 <= i && i <= 10)
+   __CPROVER_decreases(20 - i)
+    // clang-format on
+    ;
+}
diff --git a/regression/contracts/do_while_syntax_fail/test.desc b/regression/contracts/do_while_syntax_fail/test.desc
new file mode 100644
index 00000000000..7a77ac02a8f
--- /dev/null
+++ b/regression/contracts/do_while_syntax_fail/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^PARSING ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that loop contracts for do-while loops cannot be attached after
+the `while` keyword.
diff --git a/regression/contracts/do_while_syntax_pass/main.c b/regression/contracts/do_while_syntax_pass/main.c
new file mode 100644
index 00000000000..0501e6cf7d3
--- /dev/null
+++ b/regression/contracts/do_while_syntax_pass/main.c
@@ -0,0 +1,14 @@
+int main()
+{
+  int i = 0;
+  do
+    // clang-format off
+   __CPROVER_assigns(i)
+   __CPROVER_loop_invariant(0 <= i && i <= 10)
+   __CPROVER_decreases(20 - i)
+    // clang-format on
+    {
+      i++;
+    }
+  while(i < 10);
+}
diff --git a/regression/contracts/do_while_syntax_pass/test.desc b/regression/contracts/do_while_syntax_pass/test.desc
new file mode 100644
index 00000000000..021b4a9018e
--- /dev/null
+++ b/regression/contracts/do_while_syntax_pass/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Checks that loop contracts for do-while loops can be attached after the `do`
+keyword.
diff --git a/regression/contracts/loop_contracts_do_while/main.c b/regression/contracts/loop_contracts_do_while/main.c
index 88477df7fc2..3cd23019913 100644
--- a/regression/contracts/loop_contracts_do_while/main.c
+++ b/regression/contracts/loop_contracts_do_while/main.c
@@ -5,9 +5,15 @@ int main()
   int x = 0;
 
   do
-  {
-    x++;
-  } while(x < 10) __CPROVER_loop_invariant(0 <= x && x <= 10);
+    // clang-format off
+   __CPROVER_assigns(x)
+   __CPROVER_loop_invariant(0 <= x && x <= 10)
+   __CPROVER_decreases(20 - x)
+    // clang-format on
+    {
+      x++;
+    }
+  while(x < 10);
 
   assert(x == 10);
 }
diff --git a/regression/contracts/loop_contracts_do_while/test.desc b/regression/contracts/loop_contracts_do_while/test.desc
index 488a91f377f..b48cda7c0d9 100644
--- a/regression/contracts/loop_contracts_do_while/test.desc
+++ b/regression/contracts/loop_contracts_do_while/test.desc
@@ -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/parser.y b/src/ansi-c/parser.y
index 6d3889308a5..b5ca8bae4f3 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -2493,23 +2493,25 @@ iteration_statement:
           if(!parser_stack($7).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($7).operands());
         }
-        | TOK_DO statement TOK_WHILE '(' comma_expression ')'
+        | TOK_DO
           cprover_contract_assigns_opt
-          cprover_contract_loop_invariant_list_opt 
-          cprover_contract_decreases_opt ';'
+          cprover_contract_loop_invariant_list_opt
+          cprover_contract_decreases_opt
+          statement
+          TOK_WHILE '(' comma_expression ')' ';'
         {
           $$=$1;
           statement($$, ID_dowhile);
-          parser_stack($$).add_to_operands(std::move(parser_stack($5)), std::move(parser_stack($2)));
+          parser_stack($$).add_to_operands(std::move(parser_stack($8)), std::move(parser_stack($5)));
 
-          if(!parser_stack($7).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($7).operands());
+          if(!parser_stack($2).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($2).operands());
 
-          if(!parser_stack($8).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands());
+          if(!parser_stack($3).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($3).operands());
 
-          if(!parser_stack($9).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($9).operands());
+          if(!parser_stack($4).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($4).operands());
         }
         | TOK_FOR
           {