Function error

tools/transform.cpp:115–344

using print_var_val_ty = function<void(ostream&, const Model&)>;

static bool error(Errors &errs, State &src_state, State &tgt_state,
                  const Result &r, Solver &solver, const Value *var,
                  const char *msg, bool check_each_var,
                  print_var_val_ty print_var_val) {

  if (r.isInvalid()) {
    errs.add("Invalid expr", false);
    return true;
  }

  if (r.isTimeout()) {
    errs.add("Timeout", false);
    return false;
  }

  if (r.isError()) {
    errs.add("SMT Error: " + r.getReason(), false);
    return false;
  }

  if (r.isSkip()) {
    errs.add("Skip", false);
    return true;
  }

  stringstream s;
  string empty;
  auto &var_name = var ? var->getName() : empty;

  {
    // filter out approximations that don't contribute to the bug
    // i.e., they don't show up in the SMT model
    auto &m = r.getModel();
    set<string> approx;
    for (auto *v : { &src_state.getApproximations(),
                     &tgt_state.getApproximations() }) {
      for (auto &[msg, var] : *v) {
        if (!var || m.hasFnModel(*var) || var->isConst())
          approx.emplace(msg);
      }
    }

    if (!approx.empty()) {
      s << "Couldn't prove the correctness of the transformation\n"
          "Alive2 approximated the semantics of the programs and therefore we\n"
          "cannot conclude whether the bug found is valid or not.\n\n"
          "Approximations done:\n";
      for (auto &msg : approx) {
        s << " - " << msg << '\n';
      }
      errs.add(std::move(s).str(), false);
      return false;
    }
  }

  if (config::quiet) {
    s << msg << " in " << src_state.getFn().getName() << '\n';
    errs.add(std::move(s).str(), true);