[Spot] LTLf to NBAs: inconsistent results from code and command line

Dear Spot developers, I am Yong Li, a Phd student from Chinese Academy of Sciences. I am writing to you to ask an implementation question about the translation from LTLf to NBAs  in Spot. currently if I use following command line: ltlfilt --from-ltlf -f "((G((P83) -> (X((P145)) | X(X((P145))) |  X(X(X((P145)))) )))   -> ( G((P21) -> (X( (P118) |  (P83)) |   X(X(  (P118) |  (P83))) |  X(X(X((P118) | (P83)))) )) &  G( (P118)  -> X(!(P118))) &  G( (P83) -> X(!(P118) U (P145)))))" | ltl2tgba | autfilt --remove-ap=alive --small -B I was able to get a weak DBA with only 8 states. However, if I use following c++ code to do the same job:     auto pf1 = spot::parse_infix_psl(argv[1]);     if (pf1.format_errors(std::cerr))     {       std::cerr << "error: " << argv[1] << std::endl;       return -1;     }     // formula     auto f1 = pf1.f;     std::cout << f1 << std::endl;     // translate to ltlf     //auto ltlf = spot::from_ltlf(f1, "alive");     spot::translator trans;     trans.set_type(spot::postprocessor::BA);     trans.set_pref(spot::postprocessor::Small);     trans.set_level(spot::postprocessor::High);     spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf1.f));     spot::remove_ap rem;     rem.add_ap("alive");     aut = rem.strip(aut);     spot::postprocessor post;     post.set_type(spot::postprocessor::BA);     post.set_pref(spot::postprocessor::Small); // or ::Deterministic     post.set_pref(spot::postprocessor::High); // or ::Deterministic     aut = post.run(aut); I would get a DBA with 16  states, which has much more states than the one from the command line. The full source code is attached to this email. Could you tell me how I can change the code above so to get the same DBA from the command line? Thank you very much. BTW: I would like to appreciate the Spot tool which  is a tool I would install on my every Ubuntu system. Yong