T parseNumber(const std::string& flag,

    if (!std::numeric_limits<T>::is_signed

        && (optionarg.find('-') != std::string::npos))

    size_t pos = 0;

      res = conv(optionarg, &pos);

    if (pos < optionarg.size())

    return res;

  std::string handleOption<std::string>(const std::string& flag,

    return optionarg;

  bool handleOption<bool>(const std::string& flag, const std::string& optionarg)

    if (optionarg == "true")

      return true;

    if (optionarg == "false")

      return false;

  int64_t handleOption<int64_t>(const std::string& flag,

    return parseNumber<int64_t>(

        [](const auto& s, auto p) { return std::stoll(s, p); },

        "int64_t");

  uint64_t handleOption<uint64_t>(const std::string& flag,

    return parseNumber<uint64_t>(

        [](const auto& s, auto p) { return std::stoull(s, p); },

        "uint64_t");

  ManagedIn handleOption<ManagedIn>(const std::string& flag,

    ManagedIn res;

    res.open(optionarg);

    return res;

  ManagedErr handleOption<ManagedErr>(const std::string& flag,

    ManagedErr res;

    res.open(optionarg);

    return res;

  ManagedOut handleOption<ManagedOut>(const std::string& flag,

    ManagedOut res;

    res.open(optionarg);

    return res;

  std::vector<std::string> getNames()

    };

  std::string get(const Options& options, const std::string& name)

    Trace("options") << "Options::getOption(" << name << ")" << std::endl;

  if (name == "abstract-values") return options.smt.abstractValues ? "true" : "false";

  if (name == "ackermann") return options.smt.ackermann ? "true" : "false";

  if (name == "ag-miniscope-quant") return options.quantifiers.aggressiveMiniscopeQuant ? "true" : "false";

  if (name == "approx-branch-depth") return std::to_string(options.arith.maxApproxDepth);

  if (name == "arith-brab") return options.arith.brabTest ? "true" : "false";

  if (name == "arith-cong-man") return options.arith.arithCongMan ? "true" : "false";

  if (name == "arith-eq-solver") return options.arith.arithEqSolver ? "true" : "false";

  if (name == "arith-no-partial-fun") return options.arith.arithNoPartialFun ? "true" : "false";

  if (name == "arith-prop") { std::stringstream s; s << options.arith.arithPropagationMode; return s.str(); }

  if (name == "arith-prop-clauses") return std::to_string(options.arith.arithPropAsLemmaLength);

  if (name == "arith-rewrite-equalities") return options.arith.arithRewriteEq ? "true" : "false";

  if (name == "arrays-eager-index") return options.arrays.arraysEagerIndexSplitting ? "true" : "false";

  if (name == "arrays-eager-lemmas") return options.arrays.arraysEagerLemmas ? "true" : "false";

  if (name == "arrays-exp") return options.arrays.arraysExp ? "true" : "false";

  if (name == "arrays-optimize-linear") return options.arrays.arraysOptimizeLinear ? "true" : "false";

  if (name == "arrays-prop") return std::to_string(options.arrays.arraysPropagate);

  if (name == "arrays-reduce-sharing") return options.arrays.arraysReduceSharing ? "true" : "false";

  if (name == "arrays-weak-equiv") return options.arrays.arraysWeakEquivalence ? "true" : "false";

  if (name == "assign-function-values") return options.theory.assignFunctionValues ? "true" : "false";

  if (name == "bitblast") { std::stringstream s; s << options.bv.bitblastMode; return s.str(); }

  if (name == "bitwise-eq") return options.bv.bitwiseEq ? "true" : "false";

  if (name == "block-models") { std::stringstream s; s << options.smt.blockModelsMode; return s.str(); }

  if (name == "bool-to-bv") { std::stringstream s; s << options.bv.boolToBitvector; return s.str(); }

  if (name == "bv-assert-input") return options.bv.bvAssertInput ? "true" : "false";

  if (name == "bv-extract-arith") return options.bv.bvExtractArithRewrite ? "true" : "false";

  if (name == "bv-gauss-elim") return options.bv.bvGaussElim ? "true" : "false";

  if (name == "bv-intro-pow2") return options.bv.bvIntroducePow2 ? "true" : "false";

  if (name == "bv-print-consts-as-indexed-symbols") return options.bv.bvPrintConstsAsIndexedSymbols ? "true" : "false";

  if (name == "bv-propagate") return options.bv.bitvectorPropagate ? "true" : "false";

  if (name == "bv-rw-extend-eq") return options.bv.rwExtendEq ? "true" : "false";

  if (name == "bv-sat-solver") { std::stringstream s; s << options.bv.bvSatSolver; return s.str(); }

  if (name == "bv-solver") { std::stringstream s; s << options.bv.bvSolver; return s.str(); }

  if (name == "bv-to-bool") return options.bv.bitvectorToBool ? "true" : "false";

  if (name == "bvand-integer-granularity") return std::to_string(options.smt.BVAndIntegerGranularity);

  if (name == "cdt-bisimilar") return options.datatypes.cdtBisimilar ? "true" : "false";

  if (name == "cegis-sample") { std::stringstream s; s << options.quantifiers.cegisSample; return s.str(); }

  if (name == "cegqi") return options.quantifiers.cegqi ? "true" : "false";

  if (name == "cegqi-all") return options.quantifiers.cegqiAll ? "true" : "false";

  if (name == "cegqi-bv") return options.quantifiers.cegqiBv ? "true" : "false";

  if (name == "cegqi-bv-concat-inv") return options.quantifiers.cegqiBvConcInv ? "true" : "false";

  if (name == "cegqi-bv-ineq") { std::stringstream s; s << options.quantifiers.cegqiBvIneqMode; return s.str(); }

  if (name == "cegqi-bv-interleave-value") return options.quantifiers.cegqiBvInterleaveValue ? "true" : "false";

  if (name == "cegqi-bv-linear") return options.quantifiers.cegqiBvLinearize ? "true" : "false";

  if (name == "cegqi-bv-rm-extract") return options.quantifiers.cegqiBvRmExtract ? "true" : "false";

  if (name == "cegqi-bv-solve-nl") return options.quantifiers.cegqiBvSolveNl ? "true" : "false";

  if (name == "cegqi-full") return options.quantifiers.cegqiFullEffort ? "true" : "false";

  if (name == "cegqi-innermost") return options.quantifiers.cegqiInnermost ? "true" : "false";

  if (name == "cegqi-midpoint") return options.quantifiers.cegqiMidpoint ? "true" : "false";

  if (name == "cegqi-min-bounds") return options.quantifiers.cegqiMinBounds ? "true" : "false";

  if (name == "cegqi-model") return options.quantifiers.cegqiModel ? "true" : "false";

  if (name == "cegqi-multi-inst") return options.quantifiers.cegqiMultiInst ? "true" : "false";

  if (name == "cegqi-nested-qe") return options.quantifiers.cegqiNestedQE ? "true" : "false";

  if (name == "cegqi-nopt") return options.quantifiers.cegqiNopt ? "true" : "false";

  if (name == "cegqi-repeat-lit") return options.quantifiers.cegqiRepeatLit ? "true" : "false";

  if (name == "cegqi-round-up-lia") return options.quantifiers.cegqiRoundUpLowerLia ? "true" : "false";

  if (name == "cegqi-sat") return options.quantifiers.cegqiSat ? "true" : "false";

  if (name == "cegqi-use-inf-int") return options.quantifiers.cegqiUseInfInt ? "true" : "false";

  if (name == "cegqi-use-inf-real") return options.quantifiers.cegqiUseInfReal ? "true" : "false";

  if (name == "check-abducts") return options.smt.checkAbducts ? "true" : "false";

  if (name == "check-interpols") return options.smt.checkInterpols ? "true" : "false";

  if (name == "check-models") return options.smt.checkModels ? "true" : "false";

  if (name == "check-proofs") return options.smt.checkProofs ? "true" : "false";

  if (name == "check-synth-sol") return options.smt.checkSynthSol ? "true" : "false";

  if (name == "check-unsat-cores") return options.smt.checkUnsatCores ? "true" : "false";

  if (name == "collect-pivot-stats") return options.arith.collectPivots ? "true" : "false";

  if (name == "cond-var-split-agg-quant") return options.quantifiers.condVarSplitQuantAgg ? "true" : "false";

  if (name == "cond-var-split-quant") return options.quantifiers.condVarSplitQuant ? "true" : "false";

  if (name == "condense-function-values") return options.theory.condenseFunctionValues ? "true" : "false";

  if (name == "conjecture-filter-active-terms") return options.quantifiers.conjectureFilterActiveTerms ? "true" : "false";

  if (name == "conjecture-filter-canonical") return options.quantifiers.conjectureFilterCanonical ? "true" : "false";

  if (name == "conjecture-filter-model") return options.quantifiers.conjectureFilterModel ? "true" : "false";

  if (name == "conjecture-gen") return options.quantifiers.conjectureGen ? "true" : "false";

  if (name == "conjecture-gen-gt-enum") return std::to_string(options.quantifiers.conjectureGenGtEnum);

  if (name == "conjecture-gen-max-depth") return std::to_string(options.quantifiers.conjectureGenMaxDepth);

  if (name == "conjecture-gen-per-round") return std::to_string(options.quantifiers.conjectureGenPerRound);

  if (name == "conjecture-gen-uee-intro") return options.quantifiers.conjectureUeeIntro ? "true" : "false";

  if (name == "conjecture-no-filter") return options.quantifiers.conjectureNoFilter ? "true" : "false";

  if (name == "cut-all-bounded") return options.arith.doCutAllBounded ? "true" : "false";

  if (name == "dag-thresh") return std::to_string(options.expr.defaultDagThresh);

  if (name == "debug-check-models") return options.smt.debugCheckModels ? "true" : "false";

  if (name == "decision-mode" || name == "decision") { std::stringstream s; s << options.decision.decisionMode; return s.str(); }

  if (name == "decision-random-weight") return std::to_string(options.decision.decisionRandomWeight);

  if (name == "decision-threshold") { std::stringstream s; s << options.decision.decisionThreshold; return s.str(); }

  if (name == "decision-use-weight") return options.decision.decisionUseWeight ? "true" : "false";

  if (name == "decision-weight-internal") { std::stringstream s; s << options.decision.decisionWeightInternal; return s.str(); }

  if (name == "difficulty-mode") { std::stringstream s; s << options.smt.difficultyMode; return s.str(); }

  if (name == "dio-decomps") return options.arith.exportDioDecompositions ? "true" : "false";

  if (name == "dio-solver") return options.arith.arithDioSolver ? "true" : "false";

  if (name == "dio-turns") return std::to_string(options.arith.dioSolverTurns);

  if (name == "dt-binary-split") return options.datatypes.dtBinarySplit ? "true" : "false";

  if (name == "dt-blast-splits") return options.datatypes.dtBlastSplits ? "true" : "false";

  if (name == "dt-cyclic") return options.datatypes.dtCyclic ? "true" : "false";

  if (name == "dt-force-assignment") return options.datatypes.dtForceAssignment ? "true" : "false";

  if (name == "dt-infer-as-lemmas") return options.datatypes.dtInferAsLemmas ? "true" : "false";

  if (name == "dt-nested-rec") return options.datatypes.dtNestedRec ? "true" : "false";

  if (name == "dt-polite-optimize") return options.datatypes.dtPoliteOptimize ? "true" : "false";

  if (name == "dt-rewrite-error-sel") return options.datatypes.dtRewriteErrorSel ? "true" : "false";

  if (name == "dt-share-sel") return options.datatypes.dtSharedSelectors ? "true" : "false";

  if (name == "dt-stc-ind") return options.quantifiers.dtStcInduction ? "true" : "false";

  if (name == "dt-var-exp-quant") return options.quantifiers.dtVarExpandQuant ? "true" : "false";

  if (name == "dump-difficulty") return options.driver.dumpDifficulty ? "true" : "false";

  if (name == "dump-instantiations") return options.driver.dumpInstantiations ? "true" : "false";

  if (name == "dump-instantiations-debug") return options.driver.dumpInstantiationsDebug ? "true" : "false";

  if (name == "dump-models") return options.driver.dumpModels ? "true" : "false";

  if (name == "dump-proofs") return options.driver.dumpProofs ? "true" : "false";

  if (name == "dump-unsat-cores") return options.driver.dumpUnsatCores ? "true" : "false";

  if (name == "e-matching") return options.quantifiers.eMatching ? "true" : "false";

  if (name == "early-exit") return options.driver.earlyExit ? "true" : "false";

  if (name == "early-ite-removal") return options.smt.earlyIteRemoval ? "true" : "false";

  if (name == "ee-mode") { std::stringstream s; s << options.theory.eeMode; return s.str(); }

  if (name == "elim-taut-quant") return options.quantifiers.elimTautQuant ? "true" : "false";

  if (name == "err" || name == "diagnostic-output-channel") { std::stringstream s; s << options.base.err; return s.str(); }

  if (name == "error-selection-rule") { std::stringstream s; s << options.arith.arithErrorSelectionRule; return s.str(); }

  if (name == "expand-definitions") return options.smt.expandDefinitions ? "true" : "false";

  if (name == "expr-depth") return std::to_string(options.expr.defaultExprDepth);

  if (name == "ext-rew-prep") return options.smt.extRewPrep ? "true" : "false";

  if (name == "ext-rew-prep-agg") return options.smt.extRewPrepAgg ? "true" : "false";

  if (name == "ext-rewrite-quant") return options.quantifiers.extRewriteQuant ? "true" : "false";

  if (name == "fc-penalties") return options.arith.havePenalties ? "true" : "false";

  if (name == "filename") return options.driver.filename;

  if (name == "filesystem-access") return options.parser.filesystemAccess ? "true" : "false";

  if (name == "finite-model-find") return options.quantifiers.finiteModelFind ? "true" : "false";

  if (name == "flatten-ho-chains") return options.printer.flattenHOChains ? "true" : "false";

  if (name == "fmf-bound") return options.quantifiers.fmfBound ? "true" : "false";

  if (name == "fmf-bound-int") return options.quantifiers.fmfBoundInt ? "true" : "false";

  if (name == "fmf-bound-lazy") return options.quantifiers.fmfBoundLazy ? "true" : "false";

  if (name == "fmf-fmc-simple") return options.quantifiers.fmfFmcSimple ? "true" : "false";

  if (name == "fmf-fresh-dc") return options.quantifiers.fmfFreshDistConst ? "true" : "false";

  if (name == "fmf-fun") return options.quantifiers.fmfFunWellDefined ? "true" : "false";

  if (name == "fmf-fun-rlv") return options.quantifiers.fmfFunWellDefinedRelevant ? "true" : "false";

  if (name == "fmf-inst-engine") return options.quantifiers.fmfInstEngine ? "true" : "false";

  if (name == "fmf-type-completion-thresh") return std::to_string(options.quantifiers.fmfTypeCompletionThresh);

  if (name == "force-logic") return options.parser.forceLogicString;

  if (name == "force-no-limit-cpu-while-dump") return options.driver.forceNoLimitCpuWhileDump ? "true" : "false";

  if (name == "foreign-theory-rewrite") return options.smt.foreignTheoryRewrite ? "true" : "false";

  if (name == "fp-exp") return options.fp.fpExp ? "true" : "false";

  if (name == "fp-lazy-wb") return options.fp.fpLazyWb ? "true" : "false";

  if (name == "fs-interleave") return options.quantifiers.fullSaturateInterleave ? "true" : "false";

  if (name == "fs-stratify") return options.quantifiers.fullSaturateStratify ? "true" : "false";

  if (name == "fs-sum") return options.quantifiers.fullSaturateSum ? "true" : "false";

  if (name == "full-saturate-quant") return options.quantifiers.fullSaturateQuant ? "true" : "false";

  if (name == "full-saturate-quant-limit") return std::to_string(options.quantifiers.fullSaturateLimit);

  if (name == "full-saturate-quant-rd") return options.quantifiers.fullSaturateQuantRd ? "true" : "false";

  if (name == "global-declarations") return options.parser.globalDeclarations ? "true" : "false";

  if (name == "global-negate") return options.quantifiers.globalNegate ? "true" : "false";

  if (name == "help") return options.driver.help ? "true" : "false";

  if (name == "heuristic-pivots") return std::to_string(options.arith.arithHeuristicPivots);

  if (name == "ho-elim") return options.quantifiers.hoElim ? "true" : "false";

  if (name == "ho-elim-store-ax") return options.quantifiers.hoElimStoreAx ? "true" : "false";

  if (name == "ho-matching") return options.quantifiers.hoMatching ? "true" : "false";

  if (name == "ho-matching-var-priority") return options.quantifiers.hoMatchingVarArgPriority ? "true" : "false";

  if (name == "ho-merge-term-db") return options.quantifiers.hoMergeTermDb ? "true" : "false";

  if (name == "iand-mode") { std::stringstream s; s << options.smt.iandMode; return s.str(); }

  if (name == "in") { std::stringstream s; s << options.base.in; return s.str(); }

  if (name == "increment-triggers") return options.quantifiers.incrementTriggers ? "true" : "false";

  if (name == "incremental") return options.base.incrementalSolving ? "true" : "false";

  if (name == "inst-level-input-only") return options.quantifiers.instLevelInputOnly ? "true" : "false";

  if (name == "inst-max-level") return std::to_string(options.quantifiers.instMaxLevel);

  if (name == "inst-max-rounds") return std::to_string(options.quantifiers.instMaxRounds);

  if (name == "inst-no-entail") return options.quantifiers.instNoEntail ? "true" : "false";

  if (name == "inst-when") { std::stringstream s; s << options.quantifiers.instWhenMode; return s.str(); }

  if (name == "inst-when-phase") return std::to_string(options.quantifiers.instWhenPhase);

  if (name == "inst-when-strict-interleave") return options.quantifiers.instWhenStrictInterleave ? "true" : "false";

  if (name == "inst-when-tc-first") return options.quantifiers.instWhenTcFirst ? "true" : "false";

  if (name == "int-wf-ind") return options.quantifiers.intWfInduction ? "true" : "false";

  if (name == "interactive") return options.driver.interactive ? "true" : "false";

  if (name == "ite-dtt-split-quant") return options.quantifiers.iteDtTesterSplitQuant ? "true" : "false";

  if (name == "ite-lift-quant") { std::stringstream s; s << options.quantifiers.iteLiftQuant; return s.str(); }

  if (name == "ite-simp") return options.smt.doITESimp ? "true" : "false";

  if (name == "jh-rlv-order") return options.decision.jhRlvOrder ? "true" : "false";

  if (name == "jh-skolem") { std::stringstream s; s << options.decision.jhSkolemMode; return s.str(); }

  if (name == "jh-skolem-rlv") { std::stringstream s; s << options.decision.jhSkolemRlvMode; return s.str(); }

  if (name == "input-language" || name == "lang") { std::stringstream s; s << options.base.inputLanguage; return s.str(); }

  if (name == "learned-rewrite") return options.smt.learnedRewrite ? "true" : "false";

  if (name == "lemmas-on-replay-failure") return options.arith.replayFailureLemma ? "true" : "false";

  if (name == "literal-matching") { std::stringstream s; s << options.quantifiers.literalMatchMode; return s.str(); }

  if (name == "macros-quant") return options.quantifiers.macrosQuant ? "true" : "false";

  if (name == "macros-quant-mode") { std::stringstream s; s << options.quantifiers.macrosQuantMode; return s.str(); }

  if (name == "maxCutsInContext") return std::to_string(options.arith.maxCutsInContext);

  if (name == "mbqi") { std::stringstream s; s << options.quantifiers.mbqiMode; return s.str(); }

  if (name == "mbqi-interleave") return options.quantifiers.mbqiInterleave ? "true" : "false";

  if (name == "mbqi-one-inst-per-round") return options.quantifiers.fmfOneInstPerRound ? "true" : "false";

  if (name == "minimal-unsat-cores") return options.smt.minimalUnsatCores ? "true" : "false";

  if (name == "minisat-dump-dimacs") return options.prop.minisatDumpDimacs ? "true" : "false";

  if (name == "minisat-elimination") return options.prop.minisatUseElim ? "true" : "false";

  if (name == "miniscope-quant") return options.quantifiers.miniscopeQuant ? "true" : "false";

  if (name == "miniscope-quant-fv") return options.quantifiers.miniscopeQuantFreeVar ? "true" : "false";

  if (name == "miplib-trick") return options.arith.arithMLTrick ? "true" : "false";

  if (name == "miplib-trick-subs") return std::to_string(options.arith.arithMLTrickSubstitutions);

  if (name == "mmap") return options.parser.memoryMap ? "true" : "false";

  if (name == "model-cores") { std::stringstream s; s << options.smt.modelCoresMode; return s.str(); }

  if (name == "model-u-print" || name == "model-uninterp-print") { std::stringstream s; s << options.smt.modelUninterpPrint; return s.str(); }

  if (name == "model-witness-value") return options.smt.modelWitnessValue ? "true" : "false";

  if (name == "multi-trigger-cache") return options.quantifiers.multiTriggerCache ? "true" : "false";

  if (name == "multi-trigger-linear") return options.quantifiers.multiTriggerLinear ? "true" : "false";

  if (name == "multi-trigger-priority") return options.quantifiers.multiTriggerPriority ? "true" : "false";

  if (name == "multi-trigger-when-single") return options.quantifiers.multiTriggerWhenSingle ? "true" : "false";

  if (name == "new-prop") return options.arith.newProp ? "true" : "false";

  if (name == "nl-cad") return options.arith.nlCad ? "true" : "false";

  if (name == "nl-cad-initial") return options.arith.nlCadUseInitial ? "true" : "false";

  if (name == "nl-cad-lift") { std::stringstream s; s << options.arith.nlCadLifting; return s.str(); }

  if (name == "nl-cad-proj") { std::stringstream s; s << options.arith.nlCadProjection; return s.str(); }

  if (name == "nl-ext") { std::stringstream s; s << options.arith.nlExt; return s.str(); }

  if (name == "nl-ext-ent-conf") return options.arith.nlExtEntailConflicts ? "true" : "false";

  if (name == "nl-ext-factor") return options.arith.nlExtFactor ? "true" : "false";

  if (name == "nl-ext-inc-prec") return options.arith.nlExtIncPrecision ? "true" : "false";

  if (name == "nl-ext-purify") return options.arith.nlExtPurify ? "true" : "false";

  if (name == "nl-ext-rbound") return options.arith.nlExtResBound ? "true" : "false";

  if (name == "nl-ext-rewrite") return options.arith.nlExtRewrites ? "true" : "false";

  if (name == "nl-ext-split-zero") return options.arith.nlExtSplitZero ? "true" : "false";

  if (name == "nl-ext-tf-taylor-deg") return std::to_string(options.arith.nlExtTfTaylorDegree);

  if (name == "nl-ext-tf-tplanes") return options.arith.nlExtTfTangentPlanes ? "true" : "false";

  if (name == "nl-ext-tplanes") return options.arith.nlExtTangentPlanes ? "true" : "false";

  if (name == "nl-ext-tplanes-interleave") return options.arith.nlExtTangentPlanesInterleave ? "true" : "false";

  if (name == "nl-icp") return options.arith.nlICP ? "true" : "false";

  if (name == "nl-rlv") { std::stringstream s; s << options.arith.nlRlvMode; return s.str(); }

  if (name == "nl-rlv-assert-bounds") return options.arith.nlRlvAssertBounds ? "true" : "false";

  if (name == "on-repeat-ite-simp") return options.smt.doITESimpOnRepeat ? "true" : "false";

  if (name == "out" || name == "regular-output-channel") { std::stringstream s; s << options.base.out; return s.str(); }

  if (name == "output") { std::stringstream s; s << options.base.outputTag; return s.str(); }

  if (name == "output-language" || name == "output-lang") { std::stringstream s; s << options.base.outputLanguage; return s.str(); }

  if (name == "parse-only") return options.base.parseOnly ? "true" : "false";

  if (name == "partial-triggers") return options.quantifiers.partialTriggers ? "true" : "false";

  if (name == "pb-rewrites") return options.arith.pbRewrites ? "true" : "false";

  if (name == "pivot-threshold") return std::to_string(options.arith.arithPivotThreshold);

  if (name == "pool-inst") return options.quantifiers.poolInst ? "true" : "false";

  if (name == "pp-assert-max-sub-size") return std::to_string(options.arith.ppAssertMaxSubSize);

  if (name == "pre-skolem-quant") return options.quantifiers.preSkolemQuant ? "true" : "false";

  if (name == "pre-skolem-quant-agg") return options.quantifiers.preSkolemQuantAgg ? "true" : "false";

  if (name == "pre-skolem-quant-nested") return options.quantifiers.preSkolemQuantNested ? "true" : "false";

  if (name == "prenex-quant") { std::stringstream s; s << options.quantifiers.prenexQuant; return s.str(); }

  if (name == "prenex-quant-user") return options.quantifiers.prenexQuantUser ? "true" : "false";

  if (name == "preprocess-only") return options.base.preprocessOnly ? "true" : "false";

  if (name == "print-inst") { std::stringstream s; s << options.printer.printInstMode; return s.str(); }

  if (name == "print-inst-full") return options.printer.printInstFull ? "true" : "false";

  if (name == "print-success") return options.base.printSuccess ? "true" : "false";

  if (name == "print-unsat-cores-full") return options.driver.printUnsatCoresFull ? "true" : "false";

  if (name == "produce-abducts") return options.smt.produceAbducts ? "true" : "false";

  if (name == "interactive-mode" || name == "produce-assertions") return options.smt.produceAssertions ? "true" : "false";

  if (name == "produce-assignments") return options.smt.produceAssignments ? "true" : "false";

  if (name == "produce-difficulty") return options.smt.produceDifficulty ? "true" : "false";

  if (name == "produce-interpols") { std::stringstream s; s << options.smt.produceInterpols; return s.str(); }

  if (name == "produce-models") return options.smt.produceModels ? "true" : "false";

  if (name == "produce-proofs") return options.smt.produceProofs ? "true" : "false";

  if (name == "produce-unsat-assumptions") return options.smt.unsatAssumptions ? "true" : "false";

  if (name == "produce-unsat-cores") return options.smt.unsatCores ? "true" : "false";

  if (name == "proof-check") { std::stringstream s; s << options.proof.proofCheck; return s.str(); }

  if (name == "proof-format-mode") { std::stringstream s; s << options.proof.proofFormatMode; return s.str(); }

  if (name == "proof-granularity") { std::stringstream s; s << options.proof.proofGranularityMode; return s.str(); }

  if (name == "proof-pedantic") return std::to_string(options.proof.proofPedantic);

  if (name == "proof-pp-merge") return options.proof.proofPpMerge ? "true" : "false";

  if (name == "proof-print-conclusion") return options.proof.proofPrintConclusion ? "true" : "false";

  if (name == "prop-row-length") return std::to_string(options.arith.arithPropagateMaxLength);

  if (name == "purify-triggers") return options.quantifiers.purifyTriggers ? "true" : "false";

  if (name == "qcf-all-conflict") return options.quantifiers.qcfAllConflict ? "true" : "false";

  if (name == "qcf-eager-check-rd") return options.quantifiers.qcfEagerCheckRd ? "true" : "false";

  if (name == "qcf-eager-test") return options.quantifiers.qcfEagerTest ? "true" : "false";

  if (name == "qcf-nested-conflict") return options.quantifiers.qcfNestedConflict ? "true" : "false";

  if (name == "qcf-skip-rd") return options.quantifiers.qcfSkipRd ? "true" : "false";

  if (name == "qcf-tconstraint") return options.quantifiers.qcfTConstraint ? "true" : "false";

  if (name == "qcf-vo-exp") return options.quantifiers.qcfVoExp ? "true" : "false";

  if (name == "quant-alpha-equiv") return options.quantifiers.quantAlphaEquiv ? "true" : "false";

  if (name == "quant-cf") return options.quantifiers.quantConflictFind ? "true" : "false";

  if (name == "quant-cf-mode") { std::stringstream s; s << options.quantifiers.qcfMode; return s.str(); }

  if (name == "quant-cf-when") { std::stringstream s; s << options.quantifiers.qcfWhenMode; return s.str(); }

  if (name == "quant-dsplit-mode") { std::stringstream s; s << options.quantifiers.quantDynamicSplit; return s.str(); }

  if (name == "quant-fun-wd") return options.quantifiers.quantFunWellDefined ? "true" : "false";

  if (name == "quant-ind") return options.quantifiers.quantInduction ? "true" : "false";

  if (name == "quant-rep-mode") { std::stringstream s; s << options.quantifiers.quantRepMode; return s.str(); }

  if (name == "quant-split") return options.quantifiers.quantSplit ? "true" : "false";

  if (name == "random-frequency" || name == "random-freq") return std::to_string(options.prop.satRandomFreq);

  if (name == "random-seed") return std::to_string(options.prop.satRandomSeed);

  if (name == "re-elim") return options.strings.regExpElim ? "true" : "false";

  if (name == "re-elim-agg") return options.strings.regExpElimAgg ? "true" : "false";

  if (name == "re-inter-mode") { std::stringstream s; s << options.strings.stringRegExpInterMode; return s.str(); }

  if (name == "refine-conflicts") return options.prop.sat_refine_conflicts ? "true" : "false";

  if (name == "register-quant-body-terms") return options.quantifiers.registerQuantBodyTerms ? "true" : "false";

  if (name == "relational-triggers") return options.quantifiers.relationalTriggers ? "true" : "false";

  if (name == "relevance-filter") return options.theory.relevanceFilter ? "true" : "false";

  if (name == "relevant-triggers") return options.quantifiers.relevantTriggers ? "true" : "false";

  if (name == "repeat-simp") return options.smt.repeatSimp ? "true" : "false";

  if (name == "replay-early-close-depth") return std::to_string(options.arith.replayEarlyCloseDepths);

  if (name == "replay-lemma-reject-cut") return std::to_string(options.arith.lemmaRejectCutSize);

  if (name == "replay-num-err-penalty") return std::to_string(options.arith.replayNumericFailurePenalty);

  if (name == "replay-reject-cut") return std::to_string(options.arith.replayRejectCutSize);

  if (name == "restart-int-base") return std::to_string(options.prop.satRestartFirst);

  if (name == "restart-int-inc") return std::to_string(options.prop.satRestartInc);

  if (name == "restrict-pivots") return options.arith.restrictedPivots ? "true" : "false";

  if (name == "revert-arith-models-on-unsat") return options.arith.revertArithModels ? "true" : "false";

  if (name == "rlimit") return std::to_string(options.base.cumulativeResourceLimit);

  if (name == "rlimit-per" || name == "reproducible-resource-limit") return std::to_string(options.base.perCallResourceLimit);

  if (name == "rr-turns") return std::to_string(options.arith.rrTurns);

  if (name == "se-solve-int") return options.arith.trySolveIntStandardEffort ? "true" : "false";

  if (name == "seed") return std::to_string(options.driver.seed);

  if (name == "segv-spin") return options.driver.segvSpin ? "true" : "false";

  if (name == "semantic-checks") return options.parser.semanticChecks ? "true" : "false";

  if (name == "sep-check-neg") return options.sep.sepCheckNeg ? "true" : "false";

  if (name == "sep-child-refine") return options.sep.sepChildRefine ? "true" : "false";

  if (name == "sep-deq-c") return options.sep.sepDisequalC ? "true" : "false";

  if (name == "sep-min-refine") return options.sep.sepMinimalRefine ? "true" : "false";

  if (name == "sep-pre-skolem-emp") return options.sep.sepPreSkolemEmp ? "true" : "false";

  if (name == "sets-ext") return options.sets.setsExt ? "true" : "false";

  if (name == "sets-infer-as-lemmas") return options.sets.setsInferAsLemmas ? "true" : "false";

  if (name == "sets-proxy-lemmas") return options.sets.setsProxyLemmas ? "true" : "false";

  if (name == "simp-ite-compress") return options.smt.compressItes ? "true" : "false";

  if (name == "simp-ite-hunt-zombies") return std::to_string(options.smt.zombieHuntThreshold);

  if (name == "simp-with-care") return options.smt.simplifyWithCareEnabled ? "true" : "false";

  if (name == "simplex-check-period") return std::to_string(options.arith.arithSimplexCheckPeriod);

  if (name == "simplification-mode" || name == "simplification") { std::stringstream s; s << options.smt.simplificationMode; return s.str(); }

  if (name == "soi-qe") return options.arith.soiQuickExplain ? "true" : "false";

  if (name == "solve-bv-as-int") { std::stringstream s; s << options.smt.solveBVAsInt; return s.str(); }

  if (name == "solve-int-as-bv") return std::to_string(options.smt.solveIntAsBV);

  if (name == "solve-real-as-int") return options.smt.solveRealAsInt ? "true" : "false";

  if (name == "sort-inference") return options.smt.sortInference ? "true" : "false";

  if (name == "standard-effort-variable-order-pivots") return std::to_string(options.arith.arithStandardCheckVarOrderPivots);

  if (name == "static-learning") return options.smt.doStaticLearning ? "true" : "false";

  if (name == "stats") return options.base.statistics ? "true" : "false";

  if (name == "stats-all") return options.base.statisticsAll ? "true" : "false";

  if (name == "stats-every-query") return options.base.statisticsEveryQuery ? "true" : "false";

  if (name == "stats-expert") return options.base.statisticsExpert ? "true" : "false";

  if (name == "strict-parsing") return options.parser.strictParsing ? "true" : "false";

  if (name == "strings-alpha-card") return std::to_string(options.strings.stringsAlphaCard);

  if (name == "strings-check-entail-len") return options.strings.stringCheckEntailLen ? "true" : "false";

  if (name == "strings-deq-ext") return options.strings.stringsDeqExt ? "true" : "false";

  if (name == "strings-eager") return options.strings.stringEager ? "true" : "false";

  if (name == "strings-eager-eval") return options.strings.stringEagerEval ? "true" : "false";

  if (name == "strings-eager-len") return options.strings.stringEagerLen ? "true" : "false";

  if (name == "strings-exp") return options.strings.stringExp ? "true" : "false";

  if (name == "strings-ff") return options.strings.stringFlatForms ? "true" : "false";

  if (name == "strings-fmf") return options.strings.stringFMF ? "true" : "false";

  if (name == "strings-guess-model") return options.strings.stringGuessModel ? "true" : "false";

  if (name == "strings-infer-as-lemmas") return options.strings.stringInferAsLemmas ? "true" : "false";

  if (name == "strings-infer-sym") return options.strings.stringInferSym ? "true" : "false";

  if (name == "strings-lazy-pp") return options.strings.stringLazyPreproc ? "true" : "false";

  if (name == "strings-len-norm") return options.strings.stringLenNorm ? "true" : "false";

  if (name == "strings-min-prefix-explain") return options.strings.stringMinPrefixExplain ? "true" : "false";

  if (name == "strings-process-loop-mode") { std::stringstream s; s << options.strings.stringProcessLoopMode; return s.str(); }

  if (name == "strings-rexplain-lemmas") return options.strings.stringRExplainLemmas ? "true" : "false";

  if (name == "strings-unified-vspt") return options.strings.stringUnifiedVSpt ? "true" : "false";

  if (name == "sygus") return options.quantifiers.sygus ? "true" : "false";

  if (name == "sygus-abort-size") return std::to_string(options.datatypes.sygusAbortSize);

  if (name == "sygus-active-gen") { std::stringstream s; s << options.quantifiers.sygusActiveGenMode; return s.str(); }

  if (name == "sygus-active-gen-cfactor") return std::to_string(options.quantifiers.sygusActiveGenEnumConsts);

  if (name == "sygus-add-const-grammar") return options.quantifiers.sygusAddConstGrammar ? "true" : "false";

  if (name == "sygus-arg-relevant") return options.quantifiers.sygusArgRelevant ? "true" : "false";

  if (name == "sygus-auto-unfold") return options.quantifiers.sygusInvAutoUnfold ? "true" : "false";

  if (name == "sygus-bool-ite-return-const") return options.quantifiers.sygusBoolIteReturnConst ? "true" : "false";

  if (name == "sygus-core-connective") return options.quantifiers.sygusCoreConnective ? "true" : "false";

  if (name == "sygus-crepair-abort") return options.quantifiers.sygusConstRepairAbort ? "true" : "false";

  if (name == "sygus-eval-opt") return options.quantifiers.sygusEvalOpt ? "true" : "false";

  if (name == "sygus-eval-unfold") return options.quantifiers.sygusEvalUnfold ? "true" : "false";

  if (name == "sygus-eval-unfold-bool") return options.quantifiers.sygusEvalUnfoldBool ? "true" : "false";

  if (name == "sygus-expr-miner-check-timeout") return std::to_string(options.quantifiers.sygusExprMinerCheckTimeout);

  if (name == "sygus-ext-rew") return options.quantifiers.sygusExtRew ? "true" : "false";

  if (name == "sygus-fair") { std::stringstream s; s << options.datatypes.sygusFair; return s.str(); }

  if (name == "sygus-fair-max") return options.datatypes.sygusFairMax ? "true" : "false";

  if (name == "sygus-filter-sol") { std::stringstream s; s << options.quantifiers.sygusFilterSolMode; return s.str(); }

  if (name == "sygus-filter-sol-rev") return options.quantifiers.sygusFilterSolRevSubsume ? "true" : "false";

  if (name == "sygus-grammar-cons") { std::stringstream s; s << options.quantifiers.sygusGrammarConsMode; return s.str(); }

  if (name == "sygus-grammar-norm") return options.quantifiers.sygusGrammarNorm ? "true" : "false";

  if (name == "sygus-inference") return options.quantifiers.sygusInference ? "true" : "false";

  if (name == "sygus-inst") return options.quantifiers.sygusInst ? "true" : "false";

  if (name == "sygus-inst-mode") { std::stringstream s; s << options.quantifiers.sygusInstMode; return s.str(); }

  if (name == "sygus-inst-scope") { std::stringstream s; s << options.quantifiers.sygusInstScope; return s.str(); }

  if (name == "sygus-inst-term-sel") { std::stringstream s; s << options.quantifiers.sygusInstTermSel; return s.str(); }

  if (name == "sygus-inv-templ") { std::stringstream s; s << options.quantifiers.sygusInvTemplMode; return s.str(); }

  if (name == "sygus-inv-templ-when-sg") return options.quantifiers.sygusInvTemplWhenSyntax ? "true" : "false";

  if (name == "sygus-min-grammar") return options.quantifiers.sygusMinGrammar ? "true" : "false";

  if (name == "sygus-out") { std::stringstream s; s << options.smt.sygusOut; return s.str(); }

  if (name == "sygus-pbe") return options.quantifiers.sygusUnifPbe ? "true" : "false";

  if (name == "sygus-pbe-multi-fair") return options.quantifiers.sygusPbeMultiFair ? "true" : "false";

  if (name == "sygus-pbe-multi-fair-diff") return std::to_string(options.quantifiers.sygusPbeMultiFairDiff);

  if (name == "sygus-qe-preproc") return options.quantifiers.sygusQePreproc ? "true" : "false";

  if (name == "sygus-query-gen") { std::stringstream s; s << options.quantifiers.sygusQueryGen; return s.str(); }

  if (name == "sygus-query-gen-check") return options.quantifiers.sygusQueryGenCheck ? "true" : "false";

  if (name == "sygus-query-gen-dump-files") { std::stringstream s; s << options.quantifiers.sygusQueryGenDumpFiles; return s.str(); }

  if (name == "sygus-query-gen-thresh") return std::to_string(options.quantifiers.sygusQueryGenThresh);

  if (name == "sygus-rec-fun") return options.quantifiers.sygusRecFun ? "true" : "false";

  if (name == "sygus-rec-fun-eval-limit") return std::to_string(options.quantifiers.sygusRecFunEvalLimit);

  if (name == "sygus-repair-const") return options.quantifiers.sygusRepairConst ? "true" : "false";

  if (name == "sygus-repair-const-timeout") return std::to_string(options.quantifiers.sygusRepairConstTimeout);

  if (name == "sygus-rr") return options.quantifiers.sygusRew ? "true" : "false";

  if (name == "sygus-rr-synth") return options.quantifiers.sygusRewSynth ? "true" : "false";

  if (name == "sygus-rr-synth-accel") return options.quantifiers.sygusRewSynthAccel ? "true" : "false";

  if (name == "sygus-rr-synth-check") return options.quantifiers.sygusRewSynthCheck ? "true" : "false";

  if (name == "sygus-rr-synth-filter-cong") return options.quantifiers.sygusRewSynthFilterCong ? "true" : "false";

  if (name == "sygus-rr-synth-filter-match") return options.quantifiers.sygusRewSynthFilterMatch ? "true" : "false";

  if (name == "sygus-rr-synth-filter-nl") return options.quantifiers.sygusRewSynthFilterNonLinear ? "true" : "false";

  if (name == "sygus-rr-synth-filter-order") return options.quantifiers.sygusRewSynthFilterOrder ? "true" : "false";

  if (name == "sygus-rr-synth-input") return options.quantifiers.sygusRewSynthInput ? "true" : "false";

  if (name == "sygus-rr-synth-input-nvars") return std::to_string(options.quantifiers.sygusRewSynthInputNVars);

  if (name == "sygus-rr-synth-input-use-bool") return options.quantifiers.sygusRewSynthInputUseBool ? "true" : "false";

  if (name == "sygus-rr-synth-rec") return options.quantifiers.sygusRewSynthRec ? "true" : "false";

  if (name == "sygus-rr-verify") return options.quantifiers.sygusRewVerify ? "true" : "false";

  if (name == "sygus-rr-verify-abort") return options.quantifiers.sygusRewVerifyAbort ? "true" : "false";

  if (name == "sygus-sample-fp-uniform") return options.quantifiers.sygusSampleFpUniform ? "true" : "false";

  if (name == "sygus-sample-grammar") return options.quantifiers.sygusSampleGrammar ? "true" : "false";

  if (name == "sygus-samples") return std::to_string(options.quantifiers.sygusSamples);

  if (name == "sygus-si") { std::stringstream s; s << options.quantifiers.cegqiSingleInvMode; return s.str(); }

  if (name == "sygus-si-abort") return options.quantifiers.cegqiSingleInvAbort ? "true" : "false";

  if (name == "sygus-si-rcons") { std::stringstream s; s << options.quantifiers.cegqiSingleInvReconstruct; return s.str(); }

  if (name == "sygus-si-rcons-limit") return std::to_string(options.quantifiers.cegqiSingleInvReconstructLimit);

  if (name == "sygus-stream") return options.quantifiers.sygusStream ? "true" : "false";

  if (name == "sygus-sym-break") return options.datatypes.sygusSymBreak ? "true" : "false";

  if (name == "sygus-sym-break-agg") return options.datatypes.sygusSymBreakAgg ? "true" : "false";

  if (name == "sygus-sym-break-dynamic") return options.datatypes.sygusSymBreakDynamic ? "true" : "false";

  if (name == "sygus-sym-break-lazy") return options.datatypes.sygusSymBreakLazy ? "true" : "false";

  if (name == "sygus-sym-break-pbe") return options.datatypes.sygusSymBreakPbe ? "true" : "false";

  if (name == "sygus-sym-break-rlv") return options.datatypes.sygusSymBreakRlv ? "true" : "false";

  if (name == "sygus-templ-embed-grammar") return options.quantifiers.sygusTemplEmbedGrammar ? "true" : "false";

  if (name == "sygus-unif-cond-independent-no-repeat-sol") return options.quantifiers.sygusUnifCondIndNoRepeatSol ? "true" : "false";

  if (name == "sygus-unif-pi") { std::stringstream s; s << options.quantifiers.sygusUnifPi; return s.str(); }

  if (name == "sygus-unif-shuffle-cond") return options.quantifiers.sygusUnifShuffleCond ? "true" : "false";

  if (name == "sygus-verify-inst-max-rounds") return std::to_string(options.quantifiers.sygusVerifyInstMaxRounds);

  if (name == "symmetry-breaker" || name == "uf-symmetry-breaker") return options.uf.ufSymmetryBreaker ? "true" : "false";

  if (name == "tc-mode") { std::stringstream s; s << options.theory.tcMode; return s.str(); }

  if (name == "term-db-cd") return options.quantifiers.termDbCd ? "true" : "false";

  if (name == "term-db-mode") { std::stringstream s; s << options.quantifiers.termDbMode; return s.str(); }

  if (name == "theoryof-mode") { std::stringstream s; s << options.theory.theoryOfMode; return s.str(); }

  if (name == "tlimit") return std::to_string(options.base.cumulativeMillisecondLimit);

  if (name == "tlimit-per") return std::to_string(options.base.perCallMillisecondLimit);

  if (name == "trigger-active-sel") { std::stringstream s; s << options.quantifiers.triggerActiveSelMode; return s.str(); }

  if (name == "trigger-sel") { std::stringstream s; s << options.quantifiers.triggerSelMode; return s.str(); }

  if (name == "type-checking") return options.expr.typeChecking ? "true" : "false";

  if (name == "uf-ho-ext") return options.uf.ufHoExt ? "true" : "false";

  if (name == "uf-ss") { std::stringstream s; s << options.uf.ufssMode; return s.str(); }

  if (name == "uf-ss-abort-card") return std::to_string(options.uf.ufssAbortCardinality);

  if (name == "uf-ss-fair") return options.uf.ufssFairness ? "true" : "false";

  if (name == "uf-ss-fair-monotone") return options.uf.ufssFairnessMonotone ? "true" : "false";

  if (name == "unate-lemmas") { std::stringstream s; s << options.arith.arithUnateLemmaMode; return s.str(); }

  if (name == "unconstrained-simp") return options.smt.unconstrainedSimp ? "true" : "false";

  if (name == "unsat-cores-mode") { std::stringstream s; s << options.smt.unsatCoresMode; return s.str(); }

  if (name == "use-approx") return options.arith.useApprox ? "true" : "false";

  if (name == "use-fcsimplex") return options.arith.useFC ? "true" : "false";

  if (name == "use-soi") return options.arith.useSOI ? "true" : "false";

  if (name == "user-pat") { std::stringstream s; s << options.quantifiers.userPatternsQuant; return s.str(); }

  if (name == "var-elim-quant") return options.quantifiers.varElimQuant ? "true" : "false";

  if (name == "var-ineq-elim-quant") return options.quantifiers.varIneqElimQuant ? "true" : "false";

  if (name == "verbosity") return std::to_string(options.base.verbosity);

    throw OptionException("Unrecognized option key or setting: " + name);

  void set(

    Trace("options") << "set option " << name << " = " << optionarg

                     << std::endl;

  if (name == "abstract-values") {

    opts.smt.abstractValues = handlers::handleOption<bool>(name, optionarg);

    opts.smt.abstractValuesWasSetByUser = true;

  } else if (name == "ackermann") {

    opts.smt.ackermann = handlers::handleOption<bool>(name, optionarg);

    opts.smt.ackermannWasSetByUser = true;

  } else if (name == "ag-miniscope-quant") {

    opts.quantifiers.aggressiveMiniscopeQuant = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.aggressiveMiniscopeQuantWasSetByUser = true;

  } else if (name == "approx-branch-depth") {

  } else if (name == "arith-brab") {

    opts.arith.brabTest = handlers::handleOption<bool>(name, optionarg);

    opts.arith.brabTestWasSetByUser = true;

  } else if (name == "arith-cong-man") {

  } else if (name == "arith-eq-solver") {

    opts.arith.arithEqSolver = handlers::handleOption<bool>(name, optionarg);

    opts.arith.arithEqSolverWasSetByUser = true;

  } else if (name == "arith-no-partial-fun") {

    opts.arith.arithNoPartialFun = handlers::handleOption<bool>(name, optionarg);

    opts.arith.arithNoPartialFunWasSetByUser = true;

  } else if (name == "arith-prop") {

  } else if (name == "arith-prop-clauses") {

  } else if (name == "arith-rewrite-equalities") {

    opts.arith.arithRewriteEq = handlers::handleOption<bool>(name, optionarg);

    opts.arith.arithRewriteEqWasSetByUser = true;

  } else if (name == "arrays-eager-index") {

  } else if (name == "arrays-eager-lemmas") {

  } else if (name == "arrays-exp") {

    opts.arrays.arraysExp = handlers::handleOption<bool>(name, optionarg);

    opts.arrays.arraysExpWasSetByUser = true;

  } else if (name == "arrays-optimize-linear") {

  } else if (name == "arrays-prop") {

  } else if (name == "arrays-reduce-sharing") {

  } else if (name == "arrays-weak-equiv") {

  } else if (name == "assign-function-values") {

    opts.theory.assignFunctionValues = handlers::handleOption<bool>(name, optionarg);

    opts.theory.assignFunctionValuesWasSetByUser = true;

  } else if (name == "bitblast") {

    opts.bv.bitblastMode = stringToBitblastMode(optionarg);

    opts.bv.bitblastModeWasSetByUser = true;

  } else if (name == "bitwise-eq") {

  } else if (name == "block-models") {

    opts.smt.blockModelsMode = stringToBlockModelsMode(optionarg);

    opts.smt.blockModelsModeWasSetByUser = true;

  } else if (name == "bool-to-bv") {

    opts.bv.boolToBitvector = stringToBoolToBVMode(optionarg);

    opts.bv.boolToBitvectorWasSetByUser = true;

  } else if (name == "bv-assert-input") {

    opts.bv.bvAssertInput = handlers::handleOption<bool>(name, optionarg);

    opts.bv.bvAssertInputWasSetByUser = true;

  } else if (name == "bv-extract-arith") {

  } else if (name == "bv-gauss-elim") {

  } else if (name == "bv-intro-pow2") {

    opts.bv.bvIntroducePow2 = handlers::handleOption<bool>(name, optionarg);

    opts.bv.bvIntroducePow2WasSetByUser = true;

  } else if (name == "bv-print-consts-as-indexed-symbols") {

    opts.bv.bvPrintConstsAsIndexedSymbols = handlers::handleOption<bool>(name, optionarg);

    opts.bv.bvPrintConstsAsIndexedSymbolsWasSetByUser = true;

  } else if (name == "bv-propagate") {

  } else if (name == "bv-rw-extend-eq") {

  } else if (name == "bv-sat-solver") {

    auto value = stringToSatSolverMode(optionarg);

    opts.handler().checkBvSatSolver(name, value);

    opts.bv.bvSatSolver = value;

    opts.bv.bvSatSolverWasSetByUser = true;

  } else if (name == "bv-solver") {

    opts.bv.bvSolver = stringToBVSolver(optionarg);

    opts.bv.bvSolverWasSetByUser = true;

  } else if (name == "bv-to-bool") {

    opts.bv.bitvectorToBool = handlers::handleOption<bool>(name, optionarg);

    opts.bv.bitvectorToBoolWasSetByUser = true;

  } else if (name == "bvand-integer-granularity") {

    opts.smt.BVAndIntegerGranularity = handlers::handleOption<uint64_t>(name, optionarg);

    opts.smt.BVAndIntegerGranularityWasSetByUser = true;

  } else if (name == "cdt-bisimilar") {

  } else if (name == "cegis-sample") {

    opts.quantifiers.cegisSample = stringToCegisSampleMode(optionarg);

    opts.quantifiers.cegisSampleWasSetByUser = true;

  } else if (name == "cegqi") {

    opts.quantifiers.cegqi = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.cegqiWasSetByUser = true;

  } else if (name == "cegqi-all") {

    opts.quantifiers.cegqiAll = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.cegqiAllWasSetByUser = true;

  } else if (name == "cegqi-bv") {

    opts.quantifiers.cegqiBv = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.cegqiBvWasSetByUser = true;

  } else if (name == "cegqi-bv-concat-inv") {

  } else if (name == "cegqi-bv-ineq") {

    opts.quantifiers.cegqiBvIneqMode = stringToCegqiBvIneqMode(optionarg);

    opts.quantifiers.cegqiBvIneqModeWasSetByUser = true;

  } else if (name == "cegqi-bv-interleave-value") {

  } else if (name == "cegqi-bv-linear") {

  } else if (name == "cegqi-bv-rm-extract") {

    opts.quantifiers.cegqiBvRmExtract = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.cegqiBvRmExtractWasSetByUser = true;

  } else if (name == "cegqi-bv-solve-nl") {

  } else if (name == "cegqi-full") {

    opts.quantifiers.cegqiFullEffort = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.cegqiFullEffortWasSetByUser = true;

  } else if (name == "cegqi-innermost") {

  } else if (name == "cegqi-midpoint") {

  } else if (name == "cegqi-min-bounds") {

  } else if (name == "cegqi-model") {

  } else if (name == "cegqi-multi-inst") {

    opts.quantifiers.cegqiMultiInst = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.cegqiMultiInstWasSetByUser = true;

  } else if (name == "cegqi-nested-qe") {

    opts.quantifiers.cegqiNestedQE = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.cegqiNestedQEWasSetByUser = true;

  } else if (name == "cegqi-nopt") {

  } else if (name == "cegqi-repeat-lit") {

  } else if (name == "cegqi-round-up-lia") {

  } else if (name == "cegqi-sat") {

  } else if (name == "cegqi-use-inf-int") {

    opts.quantifiers.cegqiUseInfInt = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.cegqiUseInfIntWasSetByUser = true;

  } else if (name == "cegqi-use-inf-real") {

    opts.quantifiers.cegqiUseInfReal = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.cegqiUseInfRealWasSetByUser = true;

  } else if (name == "check-abducts") {

    opts.smt.checkAbducts = handlers::handleOption<bool>(name, optionarg);

    opts.smt.checkAbductsWasSetByUser = true;

  } else if (name == "check-interpols") {

    opts.smt.checkInterpols = handlers::handleOption<bool>(name, optionarg);

    opts.smt.checkInterpolsWasSetByUser = true;

  } else if (name == "check-models") {

    opts.smt.checkModels = handlers::handleOption<bool>(name, optionarg);

    opts.smt.checkModelsWasSetByUser = true;

  } else if (name == "check-proofs") {

    opts.smt.checkProofs = handlers::handleOption<bool>(name, optionarg);

    opts.smt.checkProofsWasSetByUser = true;

  } else if (name == "check-synth-sol") {

    opts.smt.checkSynthSol = handlers::handleOption<bool>(name, optionarg);

    opts.smt.checkSynthSolWasSetByUser = true;

  } else if (name == "check-unsat-cores") {

    opts.smt.checkUnsatCores = handlers::handleOption<bool>(name, optionarg);

    opts.smt.checkUnsatCoresWasSetByUser = true;

  } else if (name == "collect-pivot-stats") {

  } else if (name == "cond-var-split-agg-quant") {

  } else if (name == "cond-var-split-quant") {

  } else if (name == "condense-function-values") {

  } else if (name == "conjecture-filter-active-terms") {

  } else if (name == "conjecture-filter-canonical") {

  } else if (name == "conjecture-filter-model") {

    opts.quantifiers.conjectureFilterModel = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.conjectureFilterModelWasSetByUser = true;

  } else if (name == "conjecture-gen") {

    opts.quantifiers.conjectureGen = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.conjectureGenWasSetByUser = true;

  } else if (name == "conjecture-gen-gt-enum") {

  } else if (name == "conjecture-gen-max-depth") {

  } else if (name == "conjecture-gen-per-round") {

  } else if (name == "conjecture-gen-uee-intro") {

  } else if (name == "conjecture-no-filter") {

    opts.quantifiers.conjectureNoFilter = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.conjectureNoFilterWasSetByUser = true;

  } else if (name == "copyright") {

  } else if (name == "cut-all-bounded") {

  } else if (name == "dag-thresh") {

    auto value = handlers::handleOption<int64_t>(name, optionarg);

    opts.handler().checkMinimum(name, value, static_cast<int64_t>(0));

    opts.handler().setDefaultDagThresh(name, value);

    opts.expr.defaultDagThresh = value;

    opts.expr.defaultDagThreshWasSetByUser = true;

  } else if (name == "debug") {

  } else if (name == "debug-check-models") {

    opts.smt.debugCheckModels = handlers::handleOption<bool>(name, optionarg);

    opts.smt.debugCheckModelsWasSetByUser = true;

  } else if (name == "decision-mode" || name == "decision") {

    opts.decision.decisionMode = stringToDecisionMode(optionarg);

    opts.decision.decisionModeWasSetByUser = true;

  } else if (name == "decision-random-weight") {

  } else if (name == "decision-threshold") {

  } else if (name == "decision-use-weight") {

  } else if (name == "decision-weight-internal") {

  } else if (name == "difficulty-mode") {

  } else if (name == "dio-decomps") {

  } else if (name == "dio-solver") {

  } else if (name == "dio-turns") {

  } else if (name == "dt-binary-split") {

  } else if (name == "dt-blast-splits") {

  } else if (name == "dt-cyclic") {

  } else if (name == "dt-force-assignment") {

  } else if (name == "dt-infer-as-lemmas") {

  } else if (name == "dt-nested-rec") {

    opts.datatypes.dtNestedRec = handlers::handleOption<bool>(name, optionarg);

    opts.datatypes.dtNestedRecWasSetByUser = true;

  } else if (name == "dt-polite-optimize") {

  } else if (name == "dt-rewrite-error-sel") {

    opts.datatypes.dtRewriteErrorSel = handlers::handleOption<bool>(name, optionarg);

    opts.datatypes.dtRewriteErrorSelWasSetByUser = true;

  } else if (name == "dt-share-sel") {

    opts.datatypes.dtSharedSelectors = handlers::handleOption<bool>(name, optionarg);

    opts.datatypes.dtSharedSelectorsWasSetByUser = true;

  } else if (name == "dt-stc-ind") {

  } else if (name == "dt-var-exp-quant") {

  } else if (name == "dump-difficulty") {

  } else if (name == "dump-instantiations") {

    opts.driver.dumpInstantiations = handlers::handleOption<bool>(name, optionarg);

    opts.driver.dumpInstantiationsWasSetByUser = true;

  } else if (name == "dump-instantiations-debug") {

  } else if (name == "dump-models") {

    opts.driver.dumpModels = handlers::handleOption<bool>(name, optionarg);

    opts.driver.dumpModelsWasSetByUser = true;

  } else if (name == "dump-proofs") {

    opts.driver.dumpProofs = handlers::handleOption<bool>(name, optionarg);

    opts.driver.dumpProofsWasSetByUser = true;

  } else if (name == "dump-unsat-cores") {

    opts.driver.dumpUnsatCores = handlers::handleOption<bool>(name, optionarg);

    opts.driver.dumpUnsatCoresWasSetByUser = true;

  } else if (name == "e-matching") {

    opts.quantifiers.eMatching = handlers::handleOption<bool>(name, optionarg);

    opts.quantifiers.eMatchingWasSetByUser = true;

  } else if (name == "early-exit") {