diff --git a/NEWS b/NEWS
index 474d2082e..13e9282eb 100644
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,27 @@
 New in spot 1.99.5a (not yet released)
 
+  Library:
+
+  * Properties of automata (like the "properties:" line of the HOA
+    format) are stored as bits whose interpretation is True=yes,
+    False=maybe.  Having getters like "aut->is_deterministic()" or
+    "aut->is_unambiguous()" was confusing, because there are separate
+    functions "is_deterministic(aut)" and "is_unambiguous(aut)" that
+    do actually check the automaton.  The getters have been renamed
+    to avoid confusion, and get the names more in line with HOA.
+
+    - twa::has_state_based_acc() -> twa::prop_state_acc()
+    - twa::prop_state_based_acc(bool) -> twa::prop_state_acc(bool)
+    - twa::is_inherently_weak() -> twa::prop_inherently_weak()
+    - twa::is_deterministic() -> twa::prop_deterministic()
+    - twa::is_unambiguous() -> twa::prop_unambiguous()
+    - twa::is_stutter_invariant() -> twa::prop_stutter_invariant()
+    - twa::is_stutter_sensitive() -> twa::prop_stutter_sensitive()
+
+    The setters have the same name as the getters, except they take a
+    Boolean argument.  This argument used to be optionnal (defaulting
+    to True), but it no longer is.
+
   Bug fixes:
   * automaton parser was ignoring the "unambiguous" property.
 
diff --git a/doc/org/hoa.org b/doc/org/hoa.org
index cd731790d..d234d84d1 100644
--- a/doc/org/hoa.org
+++ b/doc/org/hoa.org
@@ -536,7 +536,7 @@ bit is false, it only means that it is unknown whether the property is
 true.  For instance if in some algorithm you want to know whether an
 automaton is deterministic (the equivalent of calling =autfilt -q
 --is-deterministic aut.hoa= from the command-line), you not call the
-method =aut->is_deterministic()= because that only check the property
+method =aut->prop_deterministic()= because that only check the property
 bit, and it might be false even if the =aut= is deterministic.
 Instead, call the function =is_deterministic(aut)=.  This function
 will first test the property bit, and do the actual check if it has
diff --git a/doc/org/tut21.org b/doc/org/tut21.org
index c1e2f0996..0eb819102 100644
--- a/doc/org/tut21.org
+++ b/doc/org/tut21.org
@@ -104,12 +104,12 @@ corresponding BDD variable number, and then use for instance
     // automaton, so they can be queried in constant time, and they are
     // only set whenever they can be determined at a cheap cost.
     out << "Deterministic: "
-        << (aut->is_deterministic() ? "yes\n" : "maybe\n");
+        << (aut->prop_deterministic() ? "yes\n" : "maybe\n");
     out << "StateBasedAcc: "
-        << (aut->has_state_based_acc() ? "yes\n" : "maybe\n");
+        << (aut->prop_state_acc() ? "yes\n" : "maybe\n");
     out << "Stutter Invariant: "
-        << (aut->is_stutter_invariant() ? "yes\n" :
-            aut->is_stutter_sensitive() ? "no\n" : "maybe\n");
+        << (aut->prop_stutter_invariant() ? "yes\n" :
+            aut->prop_stutter_sensitive() ? "no\n" : "maybe\n");
 
     // States are numbered from 0 to n-1
     unsigned n = aut->num_states();
diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy
index 722c8bac3..885d4ac8b 100644
--- a/src/parseaut/parseaut.yy
+++ b/src/parseaut/parseaut.yy
@@ -1158,7 +1158,7 @@ dstar_header: dstar_sizes
 	res.h->aut->new_states(res.states);;
 	res.info_states.resize(res.states);
       }
-    res.h->aut->prop_state_based_acc(true);
+    res.h->aut->prop_state_acc(true);
     res.h->aut->prop_deterministic(true);
     // res.h->aut->prop_complete();
     fill_guards(res);
@@ -1303,7 +1303,7 @@ dstar_states:
 
 never: "never" { res.namer = res.h->aut->create_namer<std::string>();
 	         res.h->aut->set_buchi();
-		 res.h->aut->prop_state_based_acc(true);
+		 res.h->aut->prop_state_acc(true);
 		 res.acc_state = State_Acc;
 		 res.pos_acc_sets = res.h->aut->acc().all_sets();
 	       }
@@ -1560,7 +1560,7 @@ lbtt-header-states: LBTT
 lbtt-header: lbtt-header-states INT_S
            {
 	     res.acc_mapper = new spot::acc_mapper_int(res.h->aut, $2);
-	     res.h->aut->prop_state_based_acc(true);
+	     res.h->aut->prop_state_acc(true);
 	     res.acc_state = State_Acc;
 	   }
            | lbtt-header-states INT
@@ -1869,7 +1869,7 @@ static void fix_properties(result_& r)
   //r.h->aut->prop_complete(r.complete);
   if (r.acc_style == State_Acc ||
       (r.acc_style == Mixed_Acc && !r.trans_acc_seen))
-    r.h->aut->prop_state_based_acc(true);
+    r.h->aut->prop_state_acc(true);
 }
 
 static void check_version(const result_& r)
diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc
index 8b36dfcc7..3818b6832 100644
--- a/src/tests/ikwiad.cc
+++ b/src/tests/ikwiad.cc
@@ -1026,7 +1026,7 @@ checked_main(int argc, char** argv)
       if (scc_filter)
 	{
 	  tm.start("SCC-filter");
-	  if (a->has_state_based_acc() & !scc_filter_all)
+	  if (a->prop_state_acc() & !scc_filter_all)
 	    a = spot::scc_filter_states(ensure_digraph(a));
 	  else
 	    a = spot::scc_filter(ensure_digraph(a), scc_filter_all);
diff --git a/src/twa/twa.hh b/src/twa/twa.hh
index 885e602e9..30aa17431 100644
--- a/src/twa/twa.hh
+++ b/src/twa/twa.hh
@@ -706,7 +706,7 @@ namespace spot
       set_num_sets_(num);
       acc_.set_acceptance(c);
       if (num == 0)
-	prop_state_based_acc(true);
+	prop_state_acc(true);
     }
 
     /// \brief Copy the acceptance condition of another tgba.
@@ -715,7 +715,7 @@ namespace spot
       acc_ = a->acc();
       unsigned num = acc_.num_sets();
       if (num == 0)
-	prop_state_based_acc(true);
+	prop_state_acc(true);
     }
 
     void copy_ap_of(const const_twa_ptr& a)
@@ -730,7 +730,7 @@ namespace spot
       set_num_sets_(num);
       acc_.set_generalized_buchi();
       if (num == 0)
-	prop_state_based_acc(true);
+	prop_state_acc(true);
     }
 
     acc_cond::mark_t set_buchi()
@@ -805,22 +805,22 @@ namespace spot
       named_prop_.clear();
     }
 
-    bool has_state_based_acc() const
+    bool prop_state_acc() const
     {
       return is.state_based_acc;
     }
 
-    void prop_state_based_acc(bool val)
+    void prop_state_acc(bool val)
     {
       is.state_based_acc = val;
     }
 
     bool is_sba() const
     {
-      return has_state_based_acc() && acc().is_buchi();
+      return prop_state_acc() && acc().is_buchi();
     }
 
-    bool is_inherently_weak() const
+    bool prop_inherently_weak() const
     {
       return is.inherently_weak;
     }
@@ -830,7 +830,7 @@ namespace spot
       is.inherently_weak = val;
     }
 
-    bool is_deterministic() const
+    bool prop_deterministic() const
     {
       return is.deterministic;
     }
@@ -840,7 +840,7 @@ namespace spot
       is.deterministic = val;
     }
 
-    bool is_unambiguous() const
+    bool prop_unambiguous() const
     {
       return is.unambiguous;
     }
@@ -850,12 +850,12 @@ namespace spot
       is.unambiguous = val;
     }
 
-    bool is_stutter_invariant() const
+    bool prop_stutter_invariant() const
     {
       return is.stutter_invariant;
     }
 
-    bool is_stutter_sensitive() const
+    bool prop_stutter_sensitive() const
     {
       return is.stutter_sensitive;
     }
@@ -888,25 +888,25 @@ namespace spot
     void prop_copy(const const_twa_ptr& other, prop_set p)
     {
       if (p.state_based)
-	prop_state_based_acc(other->has_state_based_acc());
+	prop_state_acc(other->prop_state_acc());
       if (p.inherently_weak)
-	prop_inherently_weak(other->is_inherently_weak());
+	prop_inherently_weak(other->prop_inherently_weak());
       if (p.deterministic)
 	{
-	  prop_deterministic(other->is_deterministic());
-	  prop_unambiguous(other->is_unambiguous());
+	  prop_deterministic(other->prop_deterministic());
+	  prop_unambiguous(other->prop_unambiguous());
 	}
       if (p.stutter_inv)
 	{
-	  prop_stutter_invariant(other->is_stutter_invariant());
-	  prop_stutter_sensitive(other->is_stutter_sensitive());
+	  prop_stutter_invariant(other->prop_stutter_invariant());
+	  prop_stutter_sensitive(other->prop_stutter_sensitive());
 	}
     }
 
     void prop_keep(prop_set p)
     {
       if (!p.state_based)
-	prop_state_based_acc(false);
+	prop_state_acc(false);
       if (!p.inherently_weak)
 	prop_inherently_weak(false);
       if (!p.deterministic)
diff --git a/src/twa/twagraph.hh b/src/twa/twagraph.hh
index a4d36bf0b..2b216c582 100644
--- a/src/twa/twagraph.hh
+++ b/src/twa/twagraph.hh
@@ -433,7 +433,7 @@ namespace spot
 
     acc_cond::mark_t state_acc_sets(unsigned s) const
     {
-      assert(has_state_based_acc() || num_sets() == 0);
+      assert(prop_state_acc() || num_sets() == 0);
       for (auto& t: g_.out(s))
 	// Stop at the first edge, since the remaining should be
 	// labeled identically.
@@ -443,7 +443,7 @@ namespace spot
 
     bool state_is_accepting(unsigned s) const
     {
-      assert(has_state_based_acc() || num_sets() == 0);
+      assert(prop_state_acc() || num_sets() == 0);
       for (auto& t: g_.out(s))
 	// Stop at the first edge, since the remaining should be
 	// labeled identically.
diff --git a/src/twaalgos/are_isomorphic.cc b/src/twaalgos/are_isomorphic.cc
index 7a42bac5d..57991a440 100644
--- a/src/twaalgos/are_isomorphic.cc
+++ b/src/twaalgos/are_isomorphic.cc
@@ -113,7 +113,7 @@ namespace spot
   isomorphism_checker::isomorphism_checker(const const_twa_graph_ptr ref)
   {
     ref_ = make_twa_graph(ref, twa::prop_set::all());
-    ref_deterministic_ = ref_->is_deterministic();
+    ref_deterministic_ = ref_->prop_deterministic();
     if (!ref_deterministic_)
       {
         nondet_states_ = spot::count_nondet_states(ref_);
@@ -130,14 +130,14 @@ namespace spot
 
     if (ref_deterministic_)
       {
-        if (aut->is_deterministic() || spot::is_deterministic(aut))
+        if (aut->prop_deterministic() || spot::is_deterministic(aut))
           {
             return are_isomorphic_det(ref_, aut);
           }
       }
     else
       {
-        if (aut->is_deterministic() ||
+        if (aut->prop_deterministic() ||
             nondet_states_ != spot::count_nondet_states(aut))
           {
             return false;
diff --git a/src/twaalgos/complete.cc b/src/twaalgos/complete.cc
index 153b399df..37b71f193 100644
--- a/src/twaalgos/complete.cc
+++ b/src/twaalgos/complete.cc
@@ -114,7 +114,7 @@ namespace spot
 	      }
 	    // In case the automaton use state-based acceptance, propagate
 	    // the acceptance of the first edge to the one we add.
-	    if (!aut->has_state_based_acc())
+	    if (!aut->prop_state_acc())
 	      acc = 0U;
 	    aut->new_edge(i, sink, missingcond, acc);
 	  }
diff --git a/src/twaalgos/degen.cc b/src/twaalgos/degen.cc
index 712179639..c8f807b7f 100644
--- a/src/twaalgos/degen.cc
+++ b/src/twaalgos/degen.cc
@@ -207,7 +207,7 @@ namespace spot
       res->copy_ap_of(a);
       res->set_buchi();
       if (want_sba)
-	res->prop_state_based_acc(true);
+	res->prop_state_acc(true);
       // Preserve determinism, weakness, and stutter-invariance
       res->prop_copy(a, { false, true, true, true });
 
diff --git a/src/twaalgos/dot.cc b/src/twaalgos/dot.cc
index a9cd9ed91..63bc09b47 100644
--- a/src/twaalgos/dot.cc
+++ b/src/twaalgos/dot.cc
@@ -468,7 +468,7 @@ namespace spot
 	  sn_ = aut->get_named_prop<std::vector<std::string>>("state-names");
 	if (opt_name_)
 	  name_ = aut_->get_named_prop<std::string>("automaton-name");
-	mark_states_ = !opt_force_acc_trans_ && aut_->has_state_based_acc();
+	mark_states_ = !opt_force_acc_trans_ && aut_->prop_state_acc();
 	if (opt_shape_ == ShapeAuto)
 	  {
 	    if (sn_ || aut->num_states() > 100)
diff --git a/src/twaalgos/dtbasat.cc b/src/twaalgos/dtbasat.cc
index bc1ef9caa..478a19cb3 100644
--- a/src/twaalgos/dtbasat.cc
+++ b/src/twaalgos/dtbasat.cc
@@ -640,7 +640,7 @@ namespace spot
       a->copy_ap_of(aut);
       acc_cond::mark_t acc = a->set_buchi();
       if (state_based)
-	a->prop_state_based_acc(true);
+	a->prop_state_acc(true);
       a->prop_deterministic(true);
       a->new_states(satdict.cand_size);
 
diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtgbasat.cc
index d193e40ed..8439ba6e2 100644
--- a/src/twaalgos/dtgbasat.cc
+++ b/src/twaalgos/dtgbasat.cc
@@ -1026,7 +1026,7 @@ namespace spot
       auto a = make_twa_graph(autdict);
       a->copy_ap_of(aut);
       if (state_based)
-	a->prop_state_based_acc(true);
+	a->prop_state_acc(true);
       a->prop_deterministic(true);
       a->set_acceptance(satdict.cand_nacc, satdict.cand_acc);
       a->new_states(satdict.cand_size);
@@ -1303,7 +1303,7 @@ namespace spot
     if (int preproc = om.get("preproc", 3))
       {
 	postprocessor post;
-	auto sba = (state_based && a->has_state_based_acc()) ?
+	auto sba = (state_based && a->prop_state_acc()) ?
 	  postprocessor::SBAcc : postprocessor::Any;
 	post.set_pref(postprocessor::Deterministic
 		      | postprocessor::Complete
@@ -1332,7 +1332,7 @@ namespace spot
 	// mode.  If the desired output is a Büchi automaton, or not
 	// desired acceptance was specified, stop here.  There is not
 	// point in minimizing a minimal automaton.
-	if (a->is_inherently_weak() && a->is_deterministic()
+	if (a->prop_inherently_weak() && a->prop_deterministic()
 	    && (target_is_buchi || !user_supplied_acc))
 	  return a;
       }
diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc
index 64384f039..887ec9776 100644
--- a/src/twaalgos/hoa.cc
+++ b/src/twaalgos/hoa.cc
@@ -153,8 +153,8 @@ namespace spot
 	is_colored = colored && (!has_state_acc || nodeadend);
 	// If the automaton declares that it is deterministic or
 	// state-based, make sure that it really is.
-	assert(!aut->is_deterministic() || deterministic);
-	assert(!aut->has_state_based_acc() || state_acc);
+	assert(!aut->prop_deterministic() || deterministic);
+	assert(!aut->prop_state_acc() || state_acc);
       }
 
       void number_all_ap()
@@ -402,14 +402,14 @@ namespace spot
       prop(" complete");
     if (md.is_deterministic)
       prop(" deterministic");
-    if (aut->is_unambiguous())
+    if (aut->prop_unambiguous())
       prop(" unambiguous");
-    assert(!(aut->is_stutter_invariant() && aut->is_stutter_sensitive()));
-    if (aut->is_stutter_invariant())
+    assert(!(aut->prop_stutter_invariant() && aut->prop_stutter_sensitive()));
+    if (aut->prop_stutter_invariant())
       prop(" stutter-invariant");
-    if (aut->is_stutter_sensitive())
+    if (aut->prop_stutter_sensitive())
       prop(" stutter-sensitive");
-    if (aut->is_inherently_weak())
+    if (aut->prop_inherently_weak())
       prop(" inherently-weak");
     os << nl;
 
diff --git a/src/twaalgos/isdet.cc b/src/twaalgos/isdet.cc
index 89bfb3788..7f618fa5f 100644
--- a/src/twaalgos/isdet.cc
+++ b/src/twaalgos/isdet.cc
@@ -63,7 +63,7 @@ namespace spot
   bool
   is_deterministic(const const_twa_graph_ptr& aut)
   {
-    if (aut->is_deterministic())
+    if (aut->prop_deterministic())
       return true;
     return !count_nondet_states_aux<false>(aut);
   }
diff --git a/src/twaalgos/isunamb.cc b/src/twaalgos/isunamb.cc
index 85bab2405..5621f5fa3 100644
--- a/src/twaalgos/isunamb.cc
+++ b/src/twaalgos/isunamb.cc
@@ -27,7 +27,7 @@ namespace spot
 {
   bool is_unambiguous(const const_twa_graph_ptr& aut)
   {
-    if (aut->is_deterministic() || aut->is_unambiguous())
+    if (aut->prop_deterministic() || aut->prop_unambiguous())
       return true;
     auto clean_a = scc_filter_states(aut);
     if (clean_a->num_edges() == 0)
@@ -41,6 +41,6 @@ namespace spot
   bool check_unambiguous(const twa_graph_ptr& aut)
   {
     aut->prop_unambiguous(is_unambiguous(aut));
-    return aut->is_unambiguous();
+    return aut->prop_unambiguous();
   }
 }
diff --git a/src/twaalgos/lbtt.cc b/src/twaalgos/lbtt.cc
index 467c195b5..cb628a3f9 100644
--- a/src/twaalgos/lbtt.cc
+++ b/src/twaalgos/lbtt.cc
@@ -133,7 +133,7 @@ namespace spot
       throw std::runtime_error
 	("LBTT only supports generalized Büchi acceptance");
 
-    bool sba = g->has_state_based_acc();
+    bool sba = g->prop_state_acc();
     if (opt)
       switch (char c = *opt++)
 	{
diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc
index eb6127733..c82cdc121 100644
--- a/src/twaalgos/minimize.cc
+++ b/src/twaalgos/minimize.cc
@@ -122,7 +122,7 @@ namespace spot
       auto dict = a->get_dict();
       auto res = make_twa_graph(dict);
       res->copy_ap_of(a);
-      res->prop_state_based_acc(true);
+      res->prop_state_acc(true);
 
       // For each set, create a state in the resulting automaton.
       // For a state s, state_num[s] is the number of the state in the minimal
@@ -483,7 +483,7 @@ namespace spot
     res->prop_copy(a, { false, false, false, true });
     res->prop_deterministic(true);
     res->prop_inherently_weak(true);
-    res->prop_state_based_acc(true);
+    res->prop_state_acc(true);
     return res;
   }
 
@@ -605,7 +605,7 @@ namespace spot
 
     // If the input automaton was already weak and deterministic, the
     // output is necessary correct.
-    if (aut_f->is_inherently_weak() && aut_f->is_deterministic())
+    if (aut_f->prop_inherently_weak() && aut_f->prop_deterministic())
       return min_aut_f;
 
     // if f is a syntactic obligation formula, the WDBA minimization
@@ -654,7 +654,7 @@ namespace spot
     if (product(min_aut_f, aut_neg_f)->is_empty())
       {
 	// Complement the minimized WDBA.
-	assert(min_aut_f->is_inherently_weak());
+	assert(min_aut_f->prop_inherently_weak());
 	auto neg_min_aut_f = remove_fin(dtwa_complement(min_aut_f));
 	if (product(aut_f, neg_min_aut_f)->is_empty())
 	  // Finally, we are now sure that it was safe
diff --git a/src/twaalgos/postproc.cc b/src/twaalgos/postproc.cc
index 1db74326a..3ae4e344f 100644
--- a/src/twaalgos/postproc.cc
+++ b/src/twaalgos/postproc.cc
@@ -146,7 +146,7 @@ namespace spot
       return a;
     // If the automaton is weak, using transition-based acceptance
     // won't help, so let's preserve it.
-    if ((state_based_ || a->is_inherently_weak()) && a->has_state_based_acc())
+    if ((state_based_ || a->prop_inherently_weak()) && a->prop_state_acc())
       return scc_filter_states(a, arg);
     else
       return scc_filter(a, arg);
@@ -253,7 +253,7 @@ namespace spot
       {
 	bool reject_bigger = (PREF_ == Small) && (level_ == Medium);
 	dba = minimize_obligation(a, f, nullptr, reject_bigger);
-	if (dba && dba->is_inherently_weak() && dba->is_deterministic())
+	if (dba && dba->prop_inherently_weak() && dba->prop_deterministic())
 	  {
 	    // The WDBA is a BA, so no degeneralization is required.
 	    // We just need to add an acceptance set if there is none.
@@ -272,7 +272,7 @@ namespace spot
     // at hard levels if we want a small output.
     if (!dba || (level_ == High && PREF_ == Small))
       {
-	if (((SBACC_ && a->has_state_based_acc())
+	if (((SBACC_ && a->prop_state_acc())
 	     || (type_ == BA && a->is_sba()))
 	    && !tba_determinisation_)
 	  {
diff --git a/src/twaalgos/product.cc b/src/twaalgos/product.cc
index 9b6bb78c3..aa061b7cc 100644
--- a/src/twaalgos/product.cc
+++ b/src/twaalgos/product.cc
@@ -103,14 +103,14 @@ namespace spot
 	      }
 	}
 
-      res->prop_deterministic(left->is_deterministic()
-			      && right->is_deterministic());
-      res->prop_stutter_invariant(left->is_stutter_invariant()
-				  && right->is_stutter_invariant());
-      res->prop_stutter_sensitive(left->is_stutter_sensitive()
-				  && right->is_stutter_sensitive());
-      res->prop_state_based_acc(left->has_state_based_acc()
-				&& right->has_state_based_acc());
+      res->prop_deterministic(left->prop_deterministic()
+			      && right->prop_deterministic());
+      res->prop_stutter_invariant(left->prop_stutter_invariant()
+				  && right->prop_stutter_invariant());
+      res->prop_stutter_sensitive(left->prop_stutter_sensitive()
+				  && right->prop_stutter_sensitive());
+      res->prop_state_acc(left->prop_state_acc()
+				&& right->prop_state_acc());
       return res;
     }
   }
diff --git a/src/twaalgos/randomgraph.cc b/src/twaalgos/randomgraph.cc
index 644401746..11002f1b0 100644
--- a/src/twaalgos/randomgraph.cc
+++ b/src/twaalgos/randomgraph.cc
@@ -132,7 +132,7 @@ namespace spot
     if (deterministic)
       res->prop_deterministic(true);
     if (state_acc)
-      res->prop_state_based_acc(true);
+      res->prop_state_acc(true);
 
     int props_n = ap->size();
     int* props = new int[props_n];
diff --git a/src/twaalgos/remfin.cc b/src/twaalgos/remfin.cc
index 28a38b0f9..0423510a1 100644
--- a/src/twaalgos/remfin.cc
+++ b/src/twaalgos/remfin.cc
@@ -87,7 +87,7 @@ namespace spot
 	  // check result, however it prevent recurring into this
 	  // procedure, because empty() will call to_tgba() wich will
 	  // call remove_fin()...
-	  sccaut->prop_state_based_acc(false);
+	  sccaut->prop_state_acc(false);
 	  // If SCCAUT is empty, the SCC is BA-type (and none
 	  // of its states are final).  If SCCAUT is nonempty, the SCC
 	  // is not BA type.
@@ -153,7 +153,7 @@ namespace spot
 	     acc_cond::mark_t inf_alone,
 	     acc_cond::mark_t fin_alone)
     {
-      assert(aut->has_state_based_acc());
+      assert(aut->prop_state_acc());
 
       scc_info si(aut);
       // For state-based Rabin automata, we check each SCC for
@@ -227,7 +227,7 @@ namespace spot
       res->new_states(nst);
       res->set_buchi();
       res->set_init_state(aut->get_init_state_number());
-      bool deterministic = aut->is_deterministic();
+      bool deterministic = aut->prop_deterministic();
 
       std::vector<unsigned> state_map(aut->num_states());
       for (unsigned n = 0; n < scc_max; ++n)
@@ -307,7 +307,7 @@ namespace spot
     static twa_graph_ptr
     rabin_to_buchi_maybe(const const_twa_graph_ptr& aut)
     {
-      if (!aut->has_state_based_acc())
+      if (!aut->prop_state_acc())
 	return nullptr;
 
       auto code = aut->get_acceptance();
@@ -468,7 +468,7 @@ namespace spot
       // We will modify res in place, and the resulting
       // automaton will only have one acceptance set.
       acc_cond::mark_t all_acc = res->set_buchi();
-      res->prop_state_based_acc(true);
+      res->prop_state_acc(true);
       res->prop_deterministic(true);
 
       unsigned sink = res->num_states();
@@ -508,7 +508,7 @@ namespace spot
       return std::const_pointer_cast<twa_graph>(aut);
 
     // FIXME: we should check whether the automaton is weak.
-    if (aut->is_inherently_weak() && is_deterministic(aut))
+    if (aut->prop_inherently_weak() && is_deterministic(aut))
       return remove_fin_det_weak(aut);
 
     if (auto maybe = streett_to_generalized_buchi_maybe(aut))
@@ -668,7 +668,7 @@ namespace spot
     res->set_acceptance(aut->num_sets() + extra_sets, new_code);
     res->set_init_state(aut->get_init_state_number());
 
-    bool sbacc = aut->has_state_based_acc();
+    bool sbacc = aut->prop_state_acc();
     scc_info si(aut);
     unsigned nscc = si.scc_count();
     std::vector<unsigned> state_map(nst);
@@ -746,7 +746,7 @@ namespace spot
 
     // If the input had no Inf, the output is a state-based automaton.
     if (allinf == 0U)
-      res->prop_state_based_acc(true);
+      res->prop_state_acc(true);
 
     res->purge_dead_states();
     trace << "before cleanup: " << res->get_acceptance() << '\n';
diff --git a/src/twaalgos/sbacc.cc b/src/twaalgos/sbacc.cc
index bee851530..c01a0afad 100644
--- a/src/twaalgos/sbacc.cc
+++ b/src/twaalgos/sbacc.cc
@@ -26,14 +26,14 @@ namespace spot
 {
   twa_graph_ptr sbacc(twa_graph_ptr old)
   {
-    if (old->has_state_based_acc())
+    if (old->prop_state_acc())
       return old;
 
     auto res = make_twa_graph(old->get_dict());
     res->copy_ap_of(old);
     res->copy_acceptance_of(old);
     res->prop_copy(old, {false, true, true, true});
-    res->prop_state_based_acc(true);
+    res->prop_state_acc(true);
 
     typedef std::pair<unsigned, acc_cond::mark_t> pair_t;
     std::map<pair_t, unsigned> s2n;
diff --git a/src/twaalgos/simulation.cc b/src/twaalgos/simulation.cc
index 23d97d877..3f400babd 100644
--- a/src/twaalgos/simulation.cc
+++ b/src/twaalgos/simulation.cc
@@ -642,7 +642,7 @@ namespace spot
         if (nb_minato == nb_satoneset && !Cosimulation)
 	  res->prop_deterministic(true);
 	if (Sba)
-	  res->prop_state_based_acc(true);
+	  res->prop_state_acc(true);
 	return res;
       }
 
@@ -770,7 +770,7 @@ namespace spot
         prev = next;
         direct_simulation<false, Sba> simul(res ? res : t);
         res = simul.run();
-        if (res->is_deterministic())
+        if (res->prop_deterministic())
 	  break;
 
         direct_simulation<true, Sba> cosimul(res);
diff --git a/src/twaalgos/stutter.cc b/src/twaalgos/stutter.cc
index fa8a2d8fa..3d0f010dc 100644
--- a/src/twaalgos/stutter.cc
+++ b/src/twaalgos/stutter.cc
@@ -620,7 +620,7 @@ namespace spot
   bool
   check_stutter_invariance(const twa_graph_ptr& aut, formula f)
   {
-    bool is_stut = aut->is_stutter_invariant();
+    bool is_stut = aut->prop_stutter_invariant();
     if (is_stut)
       return is_stut;
 
@@ -634,7 +634,7 @@ namespace spot
 	// If the automaton is deterministic, we
 	// know how to complement it.
 	aut->prop_deterministic(is_deterministic(aut));
-	if (!aut->is_deterministic())
+	if (!aut->prop_deterministic())
 	  return false;
 	neg = remove_fin(dtwa_complement(aut));
       }
diff --git a/src/twaalgos/totgba.cc b/src/twaalgos/totgba.cc
index 6a4a4ee56..83405f6f7 100644
--- a/src/twaalgos/totgba.cc
+++ b/src/twaalgos/totgba.cc
@@ -164,7 +164,7 @@ namespace spot
     bs2num[s] = out->new_state();
     todo.push_back(s);
 
-    bool sbacc = in->has_state_based_acc();
+    bool sbacc = in->prop_state_acc();
 
     // States of the original automaton are marked with s.pend == -1U.
     const acc_cond::mark_t orig_copy(-1U);
@@ -334,7 +334,7 @@ namespace spot
 	assert(cnf.front().mark == 0U);
 	res = make_twa_graph(aut->get_dict());
 	res->set_init_state(res->new_state());
-	res->prop_state_based_acc(true);
+	res->prop_state_acc(true);
 	res->prop_inherently_weak(true);
 	res->prop_deterministic(true);
 	res->prop_stutter_invariant(true);