diff --git a/src/derivation.c b/src/derivation.c
index fe00d3df..451fabdd 100644
--- a/src/derivation.c
+++ b/src/derivation.c
@@ -126,11 +126,12 @@ derivation_size (const derivation *deriv)
   return size;
 }
 
-/* Print DERIV, colored according to COUNTER.  */
-static void
+/* Print DERIV, colored according to COUNTER.
+   Return false if nothing is printed.  */
+static bool
 derivation_print_impl (const derivation *deriv, FILE *f,
                        bool leaves_only,
-                       int *counter)
+                       int *counter, const char *prefix)
 {
   if (deriv->children)
     {
@@ -142,41 +143,54 @@ derivation_print_impl (const derivation *deriv, FILE *f,
 
       if (!leaves_only)
         {
+          fputs (prefix, f);
           begin_use_class ("cex-step", f);
           fprintf (f, "%s ::=[ ", sym->tag);
           end_use_class ("cex-step", f);
+          prefix = "";
         }
-      const char *sep = "";
+      bool res = false;
       derivation *child;
       for (gl_list_iterator_t it = gl_list_iterator (deriv->children);
            derivation_list_next (&it, &child);
            )
         {
-          fputs (sep, f);
-          sep = " ";
-          derivation_print_impl (child, f, leaves_only, counter);
+          if (derivation_print_impl (child, f, leaves_only, counter, prefix))
+            {
+              prefix = " ";
+              res = true;
+            }
+          else if (!leaves_only)
+            prefix = " ";
         }
       if (!leaves_only)
         {
           begin_use_class ("cex-step", f);
-          fputs (" ]", f);
+          if (res)
+            fputs (" ]", f);
+          else
+            fputs ("]", f);
           end_use_class ("cex-step", f);
         }
       end_use_class (style, f);
+      return res;
     }
   else if (deriv == &d_dot)
     {
+      fputs (prefix, f);
       begin_use_class ("cex-dot", f);
       print_dot (f);
       end_use_class ("cex-dot", f);
     }
   else // leaf.
     {
+      fputs (prefix, f);
       const symbol *sym = symbols[deriv->sym];
       begin_use_class ("cex-leaf", f);
       fprintf (f, "%s", sym->tag);
       end_use_class ("cex-leaf", f);
     }
+  return true;
 }
 
 void
@@ -184,7 +198,7 @@ derivation_print (const derivation *deriv, FILE *out, const char *prefix)
 {
   int counter = 0;
   fputs (prefix, out);
-  derivation_print_impl (deriv, out, false, &counter);
+  derivation_print_impl (deriv, out, false, &counter, "");
   fputc ('\n', out);
 }
 
@@ -194,6 +208,6 @@ derivation_print_leaves (const derivation *deriv, FILE *out, const char *prefix)
 {
   int counter = 0;
   fputs (prefix, out);
-  derivation_print_impl (deriv, out, true, &counter);
+  derivation_print_impl (deriv, out, true, &counter, "");
   fputc ('\n', out);
 }
diff --git a/src/parse-simulation.c b/src/parse-simulation.c
index 825f74e0..aeff0539 100644
--- a/src/parse-simulation.c
+++ b/src/parse-simulation.c
@@ -426,7 +426,7 @@ nullable_closure (parse_state *ps, state_item *si, parse_state_list state_list)
       state_item *nsi = state_items + sin;
       current_ps = copy_parse_state (false, current_ps);
       ps_si_append (current_ps, nsi);
-      ps_derivs_append (current_ps, derivation_new_leaf (sp));
+      ps_derivs_append (current_ps, derivation_new (sp, derivation_list_new ()));
       parse_state_list_append (state_list, current_ps);
     }
 }
diff --git a/tests/counterexample.at b/tests/counterexample.at
index fd77e96e..65dc03cc 100644
--- a/tests/counterexample.at
+++ b/tests/counterexample.at
@@ -107,8 +107,8 @@ xby: B | X xby Y;
 AT_BISON_CHECK_CEX([input.y], [], [],
 [[input.y: warning: 2 shift/reduce conflicts [-Wconflicts-sr]
 Shift/reduce conflict on token B:
-  Example              A . B y
-  First derivation     s ::=[ ax ::=[ A x ::=[ . ] ] by ::=[ B y ] ]
+  Example              A . B
+  First derivation     s ::=[ ax ::=[ A x ::=[ . ] ] by ::=[ B y ::=[ ] ] ]
   Example              A . B
   Second derivation    s ::=[ A xby ::=[ . B ] ]
 
@@ -362,16 +362,16 @@ C : A c A;
 AT_BISON_CHECK_CEX([input.y], [], [],
 [[input.y: warning: 4 reduce/reduce conflicts [-Wconflicts-rr]
 Reduce/reduce conflict on tokens b, c:
-  Example              B . b A A c A
-  First derivation     S ::=[ B ::=[ A ::=[ B . ] b A ] C ::=[ A c A ] ]
-  Example              B . b A c A
-  Second derivation    S ::=[ B C ::=[ A ::=[ B ::=[ A ::=[ . ] b A ] ] c A ] ]
+  Example              B . b c
+  First derivation     S ::=[ B ::=[ A ::=[ B . ] b A ::=[ ] ] C ::=[ A ::=[ ] c A ::=[ ] ] ]
+  Example              B . b c
+  Second derivation    S ::=[ B C ::=[ A ::=[ B ::=[ A ::=[ . ] b A ::=[ ] ] ] c A ::=[ ] ] ]
 
 Reduce/reduce conflict on tokens b, c:
-  Example              C . c A A b A
-  First derivation     S ::=[ C ::=[ A ::=[ C . ] c A ] B ::=[ A b A ] ]
-  Example              C . c A b A
-  Second derivation    S ::=[ C B ::=[ A ::=[ C ::=[ A ::=[ . ] c A ] ] b A ] ]
+  Example              C . c b
+  First derivation     S ::=[ C ::=[ A ::=[ C . ] c A ::=[ ] ] B ::=[ A ::=[ ] b A ::=[ ] ] ]
+  Example              C . c b
+  Second derivation    S ::=[ C B ::=[ A ::=[ C ::=[ A ::=[ . ] c A ::=[ ] ] ] b A ::=[ ] ] ]
 
 ]])