Method appendIf

smt/solver.cpp:233–239

  template <typename T1, typename T2>
  void appendIf(const char *probe, T1 &&then, T2 &&els) {
    IfTactic t(probe, make_unique<T1>(std::move(then)),
               make_unique<T2>(std::move(els)));
    append(t.t);
    if (tactic_verbose)
      tactics.emplace_back(make_unique<IfTactic>(std::move(t)));
  }

  TacticResult exec(const Goal &goal0) const override {
    Goal goal(goal0);