Method solveTactical

examples/java/JavaGenericExample.java:193–204

(Context ctx, Tactic t, Goal g, Status sat)

    }

    void solveTactical(Context ctx, Tactic t, Goal g, Status sat)
            throws TestFailedException
    {
        Solver s = ctx.mkSolver(t);
        System.out.printf("%nTactical solver: %s%n", s);

        s.add(g.getFormulas());
        System.out.printf("Solver: %s%n", s);

        if (s.check() != sat)
            throw new TestFailedException();
    }

    ApplyResult applyTactic(Context ctx, Tactic t, Goal g)
    {