Hi, I don't know if it's something peculiar about my grammars, but it seems when using "-Wcounterexamples", Bison either finds counterexamples almost immediately or runs into the timeout. (Or maybe 6 seconds (see below) are just so eternally long to a modern CPU that there's not much between that and infinity. ;)
So waiting so long seems pointless, especially when there are a lot of conflicts (as there often arise at once when experimenting with a grammar). RTFS shows me that the timeout can be set with an environment variable "TIME_LIMIT" which is undocumented (and named a bit too generic to my taste), but more importantly can't be set via something like BISON_FLAGS in a Makefile. The limit is parsed as a double, but checked in whole second increments due to using difftime which seems a strange function to me, taking two integers (time_t) and returning their difference as a double, so that might not be easy to change. Also, there seems to be an off-by-epsilon error in "time_passed > time_limit", so the default time_limit = 5.0 actually results in a timeout of 6.0 seconds, and to get a timeout of 1 second (the minimum possible), one needs "TIME_LIMIT=0" (or some value < 1 such as 0.9, but apart from looking strange, strtod is locale-dependent, so one would actually need something like "LC_ALL= LC_NUMERIC=C TIME_LIMIT=0.9"). So I suggest to change this check to ">=", and to introduce a command line option that either takes an integer or (if you plan to actually support split seconds) a double parsed in a locale-independent way.