// The sourcecode below is just a fragment of a larger program.
// variable bdd is declared and assigned previously

if (!pf.errors.empty()) {
        sout << "ERROR, syntax error while parsing formula.\n";
    }
    else {
        //check if ap's are in the automaton.
        spot::bdd_dict_ptr fbdd = spot::make_bdd_dict();
        // program crashes on next line where variable f is:
        // G((p0) & (((p15) <-> ((G((p5) & (((p14) xor (G(p2))) <-> (G(X(p1)))))) U ((G(p8)) M (p7)))) -> ((p12) M (p6))))
        // with:
        // terminate called after throwing an instance of 'std::bad_alloc'
        //  what():  std::bad_alloc
        spot::twa_graph_ptr aftemp = spot::translator(fbdd).run(f);
        std::vector<spot::formula> v = aut->ap();
        bool apmismatch = false;
        for (spot::formula ap: aftemp->ap())
            if (std::find(v.begin(), v.end(), ap) != v.end()) {} //exists?
            else {
                apmismatch = true;
                break;
            }
        if (apmismatch) {
            sout << "ERROR, atomic propositions in formula are not in automaton.\n";
        }

        else {
            spot::formula nf = spot::formula::Not(f);
            // program crashes on next line where variable f is:
            // (((G((F(p5)) <-> (G(p7)))) & ((p8) <-> (F(p9)))) xor ((!(p0)) U (p1))) M ((X(p5)) & (F(p4)))
            // with:
            // terminate called after throwing an instance of 'std::bad_alloc'
            //  what():  std::bad_alloc
            spot::twa_graph_ptr af = spot::translator(bdd).run(nf);
            spot::twa_run_ptr run;
            run = aut->intersecting_run(af);
            if (run) {
                sout << "FAIL, with counterexample:  \n" << *run; //needs emptiness.hh
            } else {
                af = spot::translator(bdd).run(f);
                run = aut->intersecting_run(af);
                sout << "PASS, with witness: \n" << *run;
            }
        }
    }