Query with GROUP BY returns an extra row

The following test case produces a wrong result in MariaDB 5.2:

CREATE TABLE t1 (vc varchar(1), INDEX vc_idx (vc)) ;
INSERT INTO t1 VALUES (NULL), ('o'), (NULL), ('p'), ('c');
FLUSH TABLE t1;
SELECT vc FROM t1 GROUP BY vc;

MariaDB [test]> SELECT vc FROM t1 GROUP BY vc;
+------+
| vc |
+------+
| NULL |
| NULL |
| c |
| o |
| p |
+------+
5 rows in set (0.01 sec)

(See also bug #12837714 in mysql-trunk)