diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
index 181aa87e0..624e48aeb 100644
--- a/src/hoaparse/hoaparse.yy
+++ b/src/hoaparse/hoaparse.yy
@@ -203,8 +203,11 @@
 %%
 aut: aut-1     { res.h->loc = @$; YYACCEPT; }
    | ENDOFFILE { YYABORT; }
+   | error ENDOFFILE { YYABORT; }
+
+aut-1: hoa
+     | never
 
-aut-1: hoa | never
 
 /**********************************************************************/
 /*                          Rules for HOA                             */
@@ -212,7 +215,6 @@ aut-1: hoa | never
 
 hoa: header "--BODY--" body "--END--"
 hoa: error "--END--"
-hoa: error ENDOFFILE
 
 string_opt: | STRING
 BOOLEAN: 't' | 'f'
diff --git a/src/hoaparse/hoascan.ll b/src/hoaparse/hoascan.ll
index 20cbefd6b..58a7b0a0b 100644
--- a/src/hoaparse/hoascan.ll
+++ b/src/hoaparse/hoascan.ll
@@ -149,9 +149,11 @@ identifier  [[:alpha:]_][[:alnum:]_-]*
   [^*/\n]*		continue;
   "/"[^*\n]*		continue;
   "*"+[^*/\n]*		continue;
-  "\n"+			yylloc->end.column = 1;	yylloc->lines(yyleng);
+  {eol}			yylloc->lines(yyleng); yylloc->end.column = 1;
+  {eol2}		yylloc->lines(yyleng / 2); yylloc->end.column = 1;
   "*"+"/"		if (--comment_level == 0) BEGIN(orig_cond);
   <<EOF>>		{
+                           BEGIN(orig_cond);
                            error_list.push_back(
 			     spot::hoa_parse_error(*yylloc,
 			       "unclosed comment"));
@@ -165,26 +167,36 @@ identifier  [[:alpha:]_][[:alnum:]_-]*
 			   yylval->str = new std::string(s);
 			   return token::STRING;
  			}
+  {eol}			{
+  			  s.append(yytext, yyleng);
+                          yylloc->lines(yyleng); yylloc->end.column = 1;
+			}
+  {eol2}		{
+  			  s.append(yytext, yyleng);
+                          yylloc->lines(yyleng / 2); yylloc->end.column = 1;
+			}
   \\.			s += yytext[1];
-  [^\\\"]+		s.append(yytext, yyleng);
+  [^\\\"\n\r]+		s.append(yytext, yyleng);
   <<EOF>>		{
                            error_list.push_back(
 			     spot::hoa_parse_error(*yylloc,
 			       "unclosed string"));
-			   return 0;
+                           BEGIN(orig_cond);
+			   yylval->str = new std::string(s);
+			   return token::STRING;
                         }
 }
 
 <in_NEVER_PAR>{
-	 "("		{
+  "("		        {
 			  ++parent_level;
 			  yylval->str->append(yytext, yyleng);
 			}
-         /* if we match ")&&(" or ")||(", stay in <in_NEVER_PAR> mode */
-         ")"[ \t]*("&&"|"||")[ \t!]*"(" {
+  /* if we match ")&&(" or ")||(", stay in <in_NEVER_PAR> mode */
+  ")"[ \t]*("&&"|"||")[ \t!]*"(" {
 	                  yylval->str->append(yytext, yyleng);
 			}
-	 ")"		{
+  ")"                   {
 	                  yylval->str->append(yytext, yyleng);
 			  if (!--parent_level)
 			    {
@@ -193,14 +205,23 @@ identifier  [[:alpha:]_][[:alnum:]_-]*
 			      return token::FORMULA;
 			    }
 			}
-         [^()]+		yylval->str->append(yytext, yyleng);
-	 <<EOF>>	{
-			  unput(')');
-			  if (!missing_parent)
-                             error_list.push_back(
-			       spot::hoa_parse_error(*yylloc,
- 				"missing closing parenthese"));
-				  missing_parent = true;
+  {eol}			{
+                          yylval->str->append(yytext, yyleng);
+			  yylloc->lines(yyleng); yylloc->end.column = 1;
+			}
+  {eol2}		{
+			  yylval->str->append(yytext, yyleng);
+  			  yylloc->lines(yyleng / 2); yylloc->end.column = 1;
+			}
+  [^()\n\r]+		yylval->str->append(yytext, yyleng);
+  <<EOF>>		{
+                          error_list.push_back(
+			    spot::hoa_parse_error(*yylloc,
+ 			      "missing closing parenthese"));
+                          yylval->str->append(parent_level, ')');
+                          BEGIN(in_NEVER);
+			  spot::trim(*yylval->str);
+			  return token::FORMULA;
 			}
 }
 
diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test
index 0632fd0b0..f25e26d1b 100755
--- a/src/tgbatest/hoaparse.test
+++ b/src/tgbatest/hoaparse.test
@@ -603,7 +603,9 @@ cat >input <<EOF
 HOA: v1
 States: 3
 Start: 0
-AP: 2 "a" "b"
+AP: 2 "a" "b"/* multi
+line
+comment */
 Acceptance: 1 Inf(0)
 --BODY--
 State: [1] 0 {0}
@@ -620,18 +622,21 @@ State: 2
 EOF
 
 expecterr input <<EOF
-input:8.1-4: cannot label this edge because...
-input:7.8-10: ... the state is already labeled.
-input:12.6: missing label for this edge (previous edge is labeled)
-input:15.1-3: ignoring this label, because previous edge has no label
+input:10.1-4: cannot label this edge because...
+input:9.8-10: ... the state is already labeled.
+input:14.6: missing label for this edge (previous edge is labeled)
+input:17.1-3: ignoring this label, because previous edge has no label
 EOF
 
 
 cat >input <<EOF
 HOA: v1
-States: 2
+States: /* multi-line
+comment
+*/2
 Start: 0
-Important: 4 very important "!"
+Important: 4 very important "with multi-line
+string!"
 AP: 0
 Acceptance: 1 Inf(0)
 --BODY--
@@ -641,7 +646,7 @@ State: 1 0
 EOF
 
 expecterr input <<EOF
-input:4.1-31: ignoring unsupported header "Important:"
+input:6.1-7.8: ignoring unsupported header "Important:"
 	(but the capital indicates information that should not be ignored)
 EOF
 
@@ -663,6 +668,13 @@ EOF
 
 diff expected input.out
 
+# DOS-style new lines should have the same output.
+sed 's/$/\r/g' input > input.dos
+mv input.dos input
+../../bin/autfilt --hoa input 2>stderr && exit 1
+cat stderr
+diff stderr input.exp
+diff expected input.out
 
 # Error recovery
 
@@ -719,6 +731,7 @@ input:25.1: $se \$undefined, expecting end of file or HOA: or never
 input:25.1-12: ignoring leading garbage
 input:32.1-5: $se header name, expecting --END-- or State:
 input:37.1: $se 't', expecting end of file or HOA: or never
+autfilt: failed to read automaton from input
 EOF
 
 # A comment can contain --BODY-- or --END--, so we do not want to be
@@ -786,8 +799,8 @@ State: 1
 EOF
 
 expecterr input <<EOF
-input:4.7-242: unclosed string
-input:4.7-242: syntax error, unexpected end of file, expecting string
+input:4.7-26.1: unclosed string
+input:26.1: syntax error, unexpected end of file
 autfilt: failed to read automaton from input
 EOF
 
diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test
index 61115fa0b..408bb28ef 100755
--- a/src/tgbatest/neverclaimread.test
+++ b/src/tgbatest/neverclaimread.test
@@ -312,10 +312,17 @@ T0_init:
 accept_all:
   skip
 }
+never { /* a U b */
+T0_init:
+  if
+  :: ((b)) -> goto accept_all
+  :: ((b) -> goto T0_init
+  fi;
+accept_all:
+  skip
+}
 EOF
-run 2 ../../bin/autfilt --dot <input >stdout 2>stderr
-grep '5.6-8: unexpected empty block' stderr
-
+../../bin/autfilt --dot <input >stdout 2>stderr && exit 1
 cat >expected <<EOF
 digraph G {
   0 [label="", style=invis, height=0]
@@ -328,6 +335,15 @@ digraph G {
 }
 EOF
 diff stdout expected
+# FIXME: the "ignoring trailing garbage" is unwanted
+cat >expected.err <<EOF
+5.6-8: unexpected empty block
+5.6-8: ignoring trailing garbage
+14.6-19.1: missing closing parenthese
+19.1: syntax error, unexpected end of file, expecting fi or ':'
+autfilt: failed to read automaton from -
+EOF
+diff stderr expected.err
 
 
 cat >formulae<<EOF