diff --git a/regression/ansi-c/duplicate_label1/main.c b/regression/ansi-c/duplicate_label1/main.c
new file mode 100644
index 00000000000..1d3ff77dcce
--- /dev/null
+++ b/regression/ansi-c/duplicate_label1/main.c
@@ -0,0 +1,9 @@
+int main()
+{
+  int x;
+label:
+  x = 1;
+  goto label;
+label:
+  x = 2;
+}
diff --git a/regression/ansi-c/duplicate_label1/test.desc b/regression/ansi-c/duplicate_label1/test.desc
new file mode 100644
index 00000000000..696ed70b1f5
--- /dev/null
+++ b/regression/ansi-c/duplicate_label1/test.desc
@@ -0,0 +1,9 @@
+CORE test-c++-front-end
+main.c
+
+^EXIT=(1|64)$
+^SIGNAL=0$
+error: duplicate label 'label'
+^CONVERSION ERROR$
+--
+^warning: ignoring
diff --git a/regression/cbmc-concurrency/atomic_section_sc3/main.c b/regression/cbmc-concurrency/atomic_section_sc3/main.c
index 6886188da41..f20c5c903d5 100644
--- a/regression/cbmc-concurrency/atomic_section_sc3/main.c
+++ b/regression/cbmc-concurrency/atomic_section_sc3/main.c
@@ -85,8 +85,10 @@ unsigned dec() {
 
 int main(){
 __CPROVER_ASYNC_1: inc();
-__CPROVER_ASYNC_1: dec();
-__CPROVER_ASYNC_1: dec();
+__CPROVER_ASYNC_2:
+  dec();
+__CPROVER_ASYNC_3:
+  dec();
 
   return 0;
 }
diff --git a/regression/cbmc-concurrency/conditional_spawn2/main.c b/regression/cbmc-concurrency/conditional_spawn2/main.c
index 1d1b5338958..2586b0185d7 100644
--- a/regression/cbmc-concurrency/conditional_spawn2/main.c
+++ b/regression/cbmc-concurrency/conditional_spawn2/main.c
@@ -16,8 +16,10 @@ int main()
 __CPROVER_ASYNC_1: thread();
   }
 
-__CPROVER_ASYNC_1: thread();
-__CPROVER_ASYNC_1: thread();
+__CPROVER_ASYNC_2:
+  thread();
+__CPROVER_ASYNC_3:
+  thread();
 
   __CPROVER_assert(n<4, "3 threads spawned");
 
diff --git a/regression/cbmc-concurrency/generic_hw_sw_benchmark1/main.c b/regression/cbmc-concurrency/generic_hw_sw_benchmark1/main.c
index 51df07d68f2..a53a82fdb5d 100644
--- a/regression/cbmc-concurrency/generic_hw_sw_benchmark1/main.c
+++ b/regression/cbmc-concurrency/generic_hw_sw_benchmark1/main.c
@@ -8,9 +8,9 @@
 
 #ifdef _ENABLE_CBMC_
 
-#define ASYNC(c) __CPROVER_ASYNC_1: (c)
-#define ATOMIC_BEGIN  __CPROVER_atomic_begin()
-#define ATOMIC_END  __CPROVER_atomic_end()
+#  define ASYNC(n, c) __CPROVER_ASYNC_##n : (c)
+#  define ATOMIC_BEGIN __CPROVER_atomic_begin()
+#  define ATOMIC_END __CPROVER_atomic_end()
 
 char symbolic_char(char);
 
@@ -233,7 +233,7 @@ void* write_data_register(struct Hardware *hw, RegisterId reg_id, Register value
     pthread_create(&interrupt_thread, NULL, hw->interrupt_handler, (void *) hw->fw);
   }
 #else
-    ASYNC(hw->interrupt_handler((void *) hw->fw));
+    ASYNC(1, hw->interrupt_handler((void *)hw->fw));
 #endif
 
 SKIP:
@@ -346,7 +346,7 @@ int main(void)
   pthread_t firmware_thread;
   pthread_create(&firmware_thread, NULL, poll, (void *) fw);
 #else
-  ASYNC(poll((void *) fw));
+  ASYNC(1, poll((void *)fw));
 #endif
 
 #ifdef _EXPOSE_BUG_
@@ -358,7 +358,7 @@ int main(void)
   pthread_t stimulus_thread;
   pthread_create(&stimulus_thread, NULL, stimulus, (void *) hw);
 #else
-  ASYNC(stimulus((void *) hw));
+  ASYNC(2, stimulus((void *)hw));
 #endif
 
 #ifdef _EXPOSE_BUG_
diff --git a/regression/cbmc-concurrency/invalid_object1/main.c b/regression/cbmc-concurrency/invalid_object1/main.c
index 52ad9c51715..5f308c581f0 100644
--- a/regression/cbmc-concurrency/invalid_object1/main.c
+++ b/regression/cbmc-concurrency/invalid_object1/main.c
@@ -283,7 +283,7 @@ static signed int ethoc_reset(struct ethoc *dev)
 __CPROVER_ASYNC_1:
   open_eth_reg_write(dev->open_eth, (unsigned int)0, mode);
 
-__CPROVER_ASYNC_1:
+__CPROVER_ASYNC_2:
   open_eth_reg_write(dev->open_eth, (unsigned int)0, mode);
   return 0;
 }
diff --git a/regression/cbmc-concurrency/recursion1/main.c b/regression/cbmc-concurrency/recursion1/main.c
index dab775d4f60..3ca0a35e630 100644
--- a/regression/cbmc-concurrency/recursion1/main.c
+++ b/regression/cbmc-concurrency/recursion1/main.c
@@ -13,7 +13,7 @@ int main()
 
 start2:
   (void)0;
-__CPROVER_ASYNC_1:
+__CPROVER_ASYNC_2:
   goto start2;
 
   rec_spawn();
diff --git a/regression/cbmc-concurrency/svcomp13_qrcu_safe/main.c b/regression/cbmc-concurrency/svcomp13_qrcu_safe/main.c
index 0f277272d38..25d332953c7 100644
--- a/regression/cbmc-concurrency/svcomp13_qrcu_safe/main.c
+++ b/regression/cbmc-concurrency/svcomp13_qrcu_safe/main.c
@@ -118,7 +118,9 @@ void* qrcu_updater() {
 
 int main() {
 __CPROVER_ASYNC_1: qrcu_reader1();
-__CPROVER_ASYNC_1: qrcu_reader2();
-__CPROVER_ASYNC_1: qrcu_updater();
+__CPROVER_ASYNC_2:
+  qrcu_reader2();
+__CPROVER_ASYNC_3:
+  qrcu_updater();
   return 0;
 }
diff --git a/regression/cbmc-concurrency/svcomp13_qrcu_unsafe/main.c b/regression/cbmc-concurrency/svcomp13_qrcu_unsafe/main.c
index 4b8230404c6..d82bb0b799b 100644
--- a/regression/cbmc-concurrency/svcomp13_qrcu_unsafe/main.c
+++ b/regression/cbmc-concurrency/svcomp13_qrcu_unsafe/main.c
@@ -118,7 +118,9 @@ void* qrcu_updater() {
 
 int main() {
 __CPROVER_ASYNC_1: qrcu_reader1();
-__CPROVER_ASYNC_1: qrcu_reader2();
-__CPROVER_ASYNC_1: qrcu_updater();
+__CPROVER_ASYNC_2:
+  qrcu_reader2();
+__CPROVER_ASYNC_3:
+  qrcu_updater();
   return 0;
 }
diff --git a/regression/cbmc-concurrency/svcomp13_read_write_lock_safe/main.c b/regression/cbmc-concurrency/svcomp13_read_write_lock_safe/main.c
index 116c0cf351b..8895aff07a0 100644
--- a/regression/cbmc-concurrency/svcomp13_read_write_lock_safe/main.c
+++ b/regression/cbmc-concurrency/svcomp13_read_write_lock_safe/main.c
@@ -39,8 +39,11 @@ void *reader() { //reader
 
 int main() {
 __CPROVER_ASYNC_1: writer();
-__CPROVER_ASYNC_1: reader();
-__CPROVER_ASYNC_1: writer();
-__CPROVER_ASYNC_1: reader();
+__CPROVER_ASYNC_2:
+  reader();
+__CPROVER_ASYNC_3:
+  writer();
+__CPROVER_ASYNC_4:
+  reader();
   return 0;
 }
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 233cf3a1afc..2d3837c74ce 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -505,7 +505,12 @@ void c_typecheck_baset::typecheck_for(codet &code)
 void c_typecheck_baset::typecheck_label(code_labelt &code)
 {
   // record the label
-  labels_defined[code.get_label()]=code.source_location();
+  if(!labels_defined.emplace(code.get_label(), code.source_location()).second)
+  {
+    error().source_location = code.source_location();
+    error() << "duplicate label '" << code.get_label() << "'" << eom;
+    throw 0;
+  }
 
   typecheck_code(code.code());
 }