diff --git a/src/neverparse/neverclaimscan.ll b/src/neverparse/neverclaimscan.ll index 79609034e..998c379c4 100644 --- a/src/neverparse/neverclaimscan.ll +++ b/src/neverparse/neverclaimscan.ll @@ -75,7 +75,7 @@ eol \n|\r|\n\r|\r\n yylval->str->append(yytext, yyleng); } /* if we match ")&&(" or ")||(", stay in mode */ - ")"[ \t]*("&&"|"||")[ \t]*"(" { + ")"[ \t]*("&&"|"||")[ \t!]*"(" { yylval->str->append(yytext, yyleng); } ")" { diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index 3d3b033d6..3e75a715e 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -117,7 +117,8 @@ cat >input < goto accept_all + :: (p1) && (p0) -> goto accept_all + :: (p1) && !(p0) -> goto accept_all fi; accept_all: skip @@ -130,20 +131,16 @@ digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label="accept_init", peripheries=2] - 1 -> 2 [label="p1 | p0\n{Acc[1]}"] + 1 -> 2 [label="p1\n{Acc[1]}"] 2 [label="accept_all", peripheries=2] 2 -> 2 [label="1\n{Acc[1]}"] } EOF -# Sort out some possible inversions in the output. -# (The order is not guaranteed by SPOT.) -sed -e 's/p0 | p1/p1 | p0/g' stdout > tmp_ && mv tmp_ stdout diff stdout expected rm input stdout expected - # Test broken guards in input cat >input <