Purpose of z3::tactic and z3::goal

Viewed 263

I see that I can create goals, add them to a tactic, and create a solver from the tactic.

What is the advantage of this approach over simply creating a z3::solver instance and adding my expressions to it?

1 Answers
Related