diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 66295a7da..785b3f073 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -349,7 +349,7 @@ public void Emit(TokenTextWriter stream) {
       this.topLevelDeclarations.Emit(stream);
     }
 
-    public void ProcessDatatypeConstructors() {
+    public void ProcessDatatypeConstructors(Errors errors) {
       Dictionary<string, DatatypeConstructor> constructors = new Dictionary<string, DatatypeConstructor>();
       List<Declaration> prunedTopLevelDeclarations = new List<Declaration>();
       foreach (Declaration decl in TopLevelDeclarations) {
@@ -358,14 +358,22 @@ public void ProcessDatatypeConstructors() {
           prunedTopLevelDeclarations.Add(decl);
           continue;
         }
-        if (constructors.ContainsKey(func.Name)) continue;
+        if (constructors.ContainsKey(func.Name))
+        {
+          errors.SemErr(func.tok, string.Format("more than one declaration of datatype constructor name: {0}", func.Name));
+          continue;
+        }
         DatatypeConstructor constructor = new DatatypeConstructor(func);
         constructors.Add(func.Name, constructor);
         prunedTopLevelDeclarations.Add(constructor);
       }
+      if (errors.count > 0)
+      {
+        return;
+      }
+
       ClearTopLevelDeclarations();
       AddTopLevelDeclarations(prunedTopLevelDeclarations);
-    
       foreach (DatatypeConstructor f in constructors.Values) {
         for (int i = 0; i < f.InParams.Count; i++) {
           DatatypeSelector selector = new DatatypeSelector(f, i);
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 9571872df..179294a17 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -84,17 +84,18 @@ public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Prog
 
   Parser parser = new Parser(scanner, errors, false);
   parser.Parse();
-  if (parser.errors.count == 0)
+  if (errors.count == 0)
   {
-    program = parser.Pgm;
-    program.ProcessDatatypeConstructors();
-    return 0;
+    parser.Pgm.ProcessDatatypeConstructors(errors);
   }
-  else
+  if (errors.count == 0)
+  {
+    program = parser.Pgm;
+  } else
   {
     program = null;
-    return parser.errors.count;
   }
+  return errors.count;
 }
 
 public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation)
diff --git a/Test/datatypes/t3.bpl b/Test/datatypes/t3.bpl
new file mode 100644
index 000000000..2b66f50c7
--- /dev/null
+++ b/Test/datatypes/t3.bpl
@@ -0,0 +1,7 @@
+// RUN: %boogie -typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type {:datatype} Value;
+function {:constructor} Int(i: int): Value;
+
+type {:datatype} Path;
+function {:constructor} Int(i: int): Path;
diff --git a/Test/datatypes/t3.bpl.expect b/Test/datatypes/t3.bpl.expect
new file mode 100644
index 000000000..c8dfb7434
--- /dev/null
+++ b/Test/datatypes/t3.bpl.expect
@@ -0,0 +1,2 @@
+t3.bpl(7,25): error: more than one declaration of datatype constructor name: Int
+1 parse errors detected in t3.bpl