Hi, I am checking emptiness of a product of an automaton A with the complement of another automaton B, as usual. I would like to project a run of the product to a run on A. I am trying to do this as follows. spot::emptiness_check * ec = new spot::couvreur99_check(aut); spot::emptiness_check_result * res = ec->check(); spot::tgba_run* run = res->accepting_run(); spot::tgba_run * projrun = spot::project_tgba_run(aut, proj, run); Where aut is the product and proj is automaton A. I have also written (what I think are reasonable) project_state methods for A and B. This method is never called on B (perhaps because the complementation algorithm intercepts that?). However, if I try to use replay_run of the projected run, I get the message below, when setting debug=true. With debug=false, I get a segfault. state 1 in prefix: transition with label=p_0 & !p_1 & !p_2 and acc= state 2 in cycle: S1 t_1,t_2 ERROR: no transition with label=p_0 & p_1 & !p_2 and acc={Acc["1$1"]} leaving state 2 for state S3 t_1,t_2 The following transitions leave state 2: * S2 label=p_1 & !p_0 & !p_2 and acc= going to S2 t_2 * S3 label=p_0 & p_1 & !p_2 and acc= going to S3 t_1,t_2 Am I doing something obviously wrong here? Thanks! Nikos PS this is with the patch to the safra complementation algorithm.