diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index ab01b15f5..f6f4dbcfa 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1632,10 +1632,10 @@ namespace spot break; case op::first_match: props = children[0]->props; - // If first_match(r) == r && !(r;[*]), then it should follow - // that if r is stutter-inv, then first_match(r) is - // stutter-inv, so we do not reset the syntactic_si bit. assert(is_.sere_formula); + // {(a[+];b*);c*}<>->d is stutter invariant + // {first_match(a[+];b*);c*}<>->d is NOT. + is_.syntactic_si = false; is_.boolean = false; is_.ltl_formula = false; is_.psl_formula = false; diff --git a/tests/core/kind.test b/tests/core/kind.test index e07fd02b9..db04fc6d2 100755 --- a/tests/core/kind.test +++ b/tests/core/kind.test @@ -136,6 +136,8 @@ Fa M b,&!xLPgopra (!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla {b[+][:*0..3]},&!fPsopra {a->c[*]},xfPsopra +{(a[+];b*);c*}<>->d,&!xfPgopra +{first_match(a[+];b*);c*}<>->d,&!fPgopra EOF run 0 ../kind input