Index: test/small1/case_then_default_in_switch.c
===================================================================
--- test/small1/case_then_default_in_switch.c	(revision 0)
+++ test/small1/case_then_default_in_switch.c	(revision 0)
@@ -0,0 +1,13 @@
+// Running this file with --domakeCFG yields an incorrect result in CIL 1.3.7 (revision 12099).
+#include "testharness.h"
+
+int main() {
+	switch (1) {
+	case 0:
+	default:
+		break;
+	case 1: ;
+		SUCCESS;
+	}
+	E(0);
+}
Index: src/cil.ml
===================================================================
--- src/cil.ml	(revision 12099)
+++ src/cil.ml	(working copy)
@@ -6556,10 +6556,13 @@
       result, we sort the order in which we handle the labels (but not the
       order in which we print out the statements, so fall-through still
       works as expected). *)
-      let compare_choices s1 s2 = match s1.labels, s2.labels with
-      | (Default(_) :: _), _ -> 1
-      | _, (Default(_) :: _) -> -1
-      | _, _ -> 0
+      let compare_choices s1 s2 =
+          let contains_default labels =
+              List.exists (function Default _ -> true | _ -> false) labels
+          in
+          if contains_default s1.labels then 1
+          else if contains_default s2.labels then -1
+          else 0
       in
 
       let rec handle_choices sl = match sl with