Source file options.ml

type _ key =
  | Log_level : int key
  | Produce_models : bool key
  | Produce_unsat_assumptions : bool key
  | Produce_unsat_cores : bool key
  | Seed : int key
  | Verbosity : int key
  | Time_limit_per : int key
  | Memory_limit : int key
  | Nthreads : int key
  | Bv_solver : bv_solver key
  | Rewrite_level : int key
  | Sat_solver : sat_solver key
  | Write_aiger : string key
  | Write_cnf : string key
  | Prop_const_bits : bool key
  | Prop_ineq_bounds : bool key
  | Prop_nprops : int key
  | Prop_nupdates : int key
  | Prop_opt_lt_concat_sext : bool key
  | Prop_path_sel : prop_path_sel key
  | Prop_prob_pick_rand_input : int key
  | Prop_prob_pick_inv_value : int key
  | Prop_sext : bool key
  | Abstraction : bool key
  | Abstraction_bv_size : int key
  | Abstraction_eager_refine : bool key
  | Abstraction_value_limit : int key
  | Abstraction_value_only : bool key
  | Abstraction_assert : bool key
  | Abstraction_assert_refs : int key
  | Abstraction_initial_lemmas : bool key
  | Abstraction_inc_bitblast : bool key
  | Abstraction_bvadd : bool key
  | Abstraction_bvmul : bool key
  | Abstraction_bvudiv : bool key
  | Abstraction_bvurem : bool key
  | Abstraction_eq : bool key
  | Abstraction_ite : bool key
  | Preprocess : bool key
  | Pp_contr_ands : bool key
  | Pp_elim_extracts : bool key
  | Pp_elim_bvudiv : bool key
  | Pp_embedded : bool key
  | Pp_flatten_and : bool key
  | Pp_normalize : bool key
  | Pp_skeleton_preproc : bool key
  | Pp_variable_subst : bool key
  | Pp_variable_subst_norm_eq : bool key
  | Pp_variable_subst_norm_diseq : bool key
  | Pp_variable_subst_norm_bv_ineq : bool key
  | Dbg_rw_node_thresh : int key
  | Dbg_pp_node_thresh : int key
  | Check_model : bool key
  | Check_unsat_core : bool key
and bv_solver =
  | Bitblast
  | Preprop
  | Prop
and sat_solver =
  | Cadical
  | Cms
  | Kissat
and prop_path_sel =
  | Essential
  | Random
let description : type a. a key -> string = function
  | Log_level -> "log level"
  | Produce_models -> "model production"
  | Produce_unsat_assumptions -> "unsat assumptions production"
  | Produce_unsat_cores -> "unsat core production"
  | Seed -> "seed for the random number generator"
  | Verbosity -> "verbosity level"
  | Time_limit_per -> "time limit in milliseconds per satisfiability check"
  | Memory_limit -> "set maximum memory limit in MB per satisfiability check"
  | Nthreads -> "set number of threads to utilize in parallel (currently, this only configures parallel threads in the CryptoMiniSat back end)"
  | Bv_solver -> "bv solver engine"
  | Rewrite_level -> "rewrite level"
  | Sat_solver -> "backend SAT solver"
  | Write_aiger -> "write bv abstraction as AIGER to filename"
  | Write_cnf -> "write bv abstraction as CNF to filename"
  | Prop_const_bits -> "use constant bits propagation"
  | Prop_ineq_bounds -> "infer inequality bounds for invertibility conditions and inverse value computation"
  | Prop_nprops -> "number of propagation steps used as a limit for propagation-based local search engine"
  | Prop_nupdates -> "number of model value updates used as a limit for propagation-based local search engine"
  | Prop_opt_lt_concat_sext -> "optimization for inverse value computation of inequalities over concat and sign extension operands"
  | Prop_path_sel -> "propagation path selection mode for propagation-based local search engine"
  | Prop_prob_pick_rand_input -> "probability for selecting a random input instead of an essential input (interpreted as <n>/1000)"
  | Prop_prob_pick_inv_value -> "probability for producing inverse rather than consistent values (interpreted as <n>/1000)"
  | Prop_sext -> "use sign_extend nodes for concats that represent sign_extend nodes for propagation-based local search engine"
  | Abstraction -> "enable abstraction module"
  | Abstraction_bv_size -> "enable abstraction for bit-vector terms of given minimum size"
  | Abstraction_eager_refine -> "add all violated abstraction lemmas at once"
  | Abstraction_value_limit -> "value instantiation limit bv-size/<n> until adding original term as refinement"
  | Abstraction_value_only -> "only add value instantiations"
  | Abstraction_assert -> "assertion abstraction"
  | Abstraction_assert_refs -> "number of assertion refinements per check"
  | Abstraction_initial_lemmas -> "use initial lemma refinements only"
  | Abstraction_inc_bitblast -> "incrementally bit-blast bvmul and bvadd"
  | Abstraction_bvadd -> "term abstraction for bvadd"
  | Abstraction_bvmul -> "term abstraction for bvmul"
  | Abstraction_bvudiv -> "term abstraction for bvudiv"
  | Abstraction_bvurem -> "term abstraction for bvurem"
  | Abstraction_eq -> "term abstraction for ="
  | Abstraction_ite -> "term abstraction for ite"
  | Preprocess -> "enable preprocessing"
  | Pp_contr_ands -> "enable contradicting ands preprocessing pass"
  | Pp_elim_extracts -> "eliminate extract on BV constants"
  | Pp_elim_bvudiv -> "eliminate bvudiv and bvurem"
  | Pp_embedded -> "enable embedded constraint preprocessing pass"
  | Pp_flatten_and -> "enable AND flattening preprocessing pass"
  | Pp_normalize -> "enable normalization pass"
  | Pp_skeleton_preproc -> "enable skeleton preprocessing pass"
  | Pp_variable_subst -> "enable variable substitution preprocessing pass"
  | Pp_variable_subst_norm_eq -> "enable equality normalization via Gaussian elimination if variable substitution preprocessing pass is enabled"
  | Pp_variable_subst_norm_diseq -> "enable disequality normalization if variable substitution preprocessing pass is enabled"
  | Pp_variable_subst_norm_bv_ineq -> "enable bit-vector unsigned inequality normalization if variable substitution preprocessing pass is enabled"
  | Dbg_rw_node_thresh -> "warn threshold [#] for new nodes created through rewriting steps"
  | Dbg_pp_node_thresh -> "warn threshold [%] for new nodes created through preprocessing in total"
  | Check_model -> "check model for each satisfiable query"
  | Check_unsat_core -> "check unsat core for each unsatisfiable query"
let to_string : type a. a key -> string = function
  | Log_level -> "log-level"
  | Produce_models -> "produce-models"
  | Produce_unsat_assumptions -> "produce-unsat-assumptions"
  | Produce_unsat_cores -> "produce-unsat-cores"
  | Seed -> "seed"
  | Verbosity -> "verbosity"
  | Time_limit_per -> "time-limit-per"
  | Memory_limit -> "memory-limit"
  | Nthreads -> "nthreads"
  | Bv_solver -> "bv-solver"
  | Rewrite_level -> "rewrite-level"
  | Sat_solver -> "sat-solver"
  | Write_aiger -> "write-aiger"
  | Write_cnf -> "write-cnf"
  | Prop_const_bits -> "prop-const-bits"
  | Prop_ineq_bounds -> "prop-ineq-bounds"
  | Prop_nprops -> "prop-nprops"
  | Prop_nupdates -> "prop-nupdates"
  | Prop_opt_lt_concat_sext -> "prop-opt-lt-concat-sext"
  | Prop_path_sel -> "prop-path-sel"
  | Prop_prob_pick_rand_input -> "prop-prob-pick-rand-input"
  | Prop_prob_pick_inv_value -> "prop-prob-pick-inv-value"
  | Prop_sext -> "prop-sext"
  | Abstraction -> "abstraction"
  | Abstraction_bv_size -> "abstraction-bv-size"
  | Abstraction_eager_refine -> "abstraction-eager-refine"
  | Abstraction_value_limit -> "abstraction-value-limit"
  | Abstraction_value_only -> "abstraction-value-only"
  | Abstraction_assert -> "abstraction-assert"
  | Abstraction_assert_refs -> "abstraction-assert-refs"
  | Abstraction_initial_lemmas -> "abstraction-initial-lemmas"
  | Abstraction_inc_bitblast -> "abstraction-inc-bitblast"
  | Abstraction_bvadd -> "abstraction-bvadd"
  | Abstraction_bvmul -> "abstraction-bvmul"
  | Abstraction_bvudiv -> "abstraction-bvudiv"
  | Abstraction_bvurem -> "abstraction-bvurem"
  | Abstraction_eq -> "abstraction-eq"
  | Abstraction_ite -> "abstraction-ite"
  | Preprocess -> "preprocess"
  | Pp_contr_ands -> "pp-contr-ands"
  | Pp_elim_extracts -> "pp-elim-extracts"
  | Pp_elim_bvudiv -> "pp-elim-bvudiv"
  | Pp_embedded -> "pp-embedded"
  | Pp_flatten_and -> "pp-flatten-and"
  | Pp_normalize -> "pp-normalize"
  | Pp_skeleton_preproc -> "pp-skeleton-preproc"
  | Pp_variable_subst -> "pp-variable-subst"
  | Pp_variable_subst_norm_eq -> "pp-variable-subst-norm-eq"
  | Pp_variable_subst_norm_diseq -> "pp-variable-subst-norm-diseq"
  | Pp_variable_subst_norm_bv_ineq -> "pp-variable-subst-norm-bv-ineq"
  | Dbg_rw_node_thresh -> "dbg-rw-node-thresh"
  | Dbg_pp_node_thresh -> "dbg-pp-node-thresh"
  | Check_model -> "check-model"
  | Check_unsat_core -> "check-unsat-core"
let to_cxx : type a. a key -> int = function
  | Log_level -> 0
  | Produce_models -> 1
  | Produce_unsat_assumptions -> 2
  | Produce_unsat_cores -> 3
  | Seed -> 4
  | Verbosity -> 5
  | Time_limit_per -> 6
  | Memory_limit -> 7
  | Nthreads -> 8
  | Bv_solver -> 9
  | Rewrite_level -> 10
  | Sat_solver -> 11
  | Write_aiger -> 12
  | Write_cnf -> 13
  | Prop_const_bits -> 14
  | Prop_ineq_bounds -> 15
  | Prop_nprops -> 16
  | Prop_nupdates -> 17
  | Prop_opt_lt_concat_sext -> 18
  | Prop_path_sel -> 19
  | Prop_prob_pick_rand_input -> 20
  | Prop_prob_pick_inv_value -> 21
  | Prop_sext -> 22
  | Abstraction -> 23
  | Abstraction_bv_size -> 24
  | Abstraction_eager_refine -> 25
  | Abstraction_value_limit -> 26
  | Abstraction_value_only -> 27
  | Abstraction_assert -> 28
  | Abstraction_assert_refs -> 29
  | Abstraction_initial_lemmas -> 30
  | Abstraction_inc_bitblast -> 31
  | Abstraction_bvadd -> 32
  | Abstraction_bvmul -> 33
  | Abstraction_bvudiv -> 34
  | Abstraction_bvurem -> 35
  | Abstraction_eq -> 36
  | Abstraction_ite -> 37
  | Preprocess -> 38
  | Pp_contr_ands -> 39
  | Pp_elim_extracts -> 40
  | Pp_elim_bvudiv -> 41
  | Pp_embedded -> 42
  | Pp_flatten_and -> 43
  | Pp_normalize -> 44
  | Pp_skeleton_preproc -> 45
  | Pp_variable_subst -> 46
  | Pp_variable_subst_norm_eq -> 47
  | Pp_variable_subst_norm_diseq -> 48
  | Pp_variable_subst_norm_bv_ineq -> 49
  | Dbg_rw_node_thresh -> 50
  | Dbg_pp_node_thresh -> 51
  | Check_model -> 52
  | Check_unsat_core -> 53
let bv_solver_to_string = function
  | Bitblast -> "bitblast"
  | Preprop -> "preprop"
  | Prop -> "prop"
let sat_solver_to_string = function
  | Cadical -> "cadical"
  | Cms -> "cms"
  | Kissat -> "kissat"
let prop_path_sel_to_string = function
  | Essential -> "essential"
  | Random -> "random"
let bv_solver_of_string = function
  | "bitblast" -> Bitblast
  | "preprop" -> Preprop
  | "prop" -> Prop
  | _ -> assert false
let sat_solver_of_string = function
  | "cadical" -> Cadical
  | "cms" -> Cms
  | "kissat" -> Kissat
  | _ -> assert false
let prop_path_sel_of_string = function
  | "essential" -> Essential
  | "random" -> Random
  | _ -> assert false
let default_value : type a. a key -> a = function
  | Log_level -> 0
  | Produce_models -> false
  | Produce_unsat_assumptions -> false
  | Produce_unsat_cores -> false
  | Seed -> 27644437
  | Verbosity -> 0
  | Time_limit_per -> 0
  | Memory_limit -> 0
  | Nthreads -> 1
  | Bv_solver -> Bitblast
  | Rewrite_level -> 2
  | Sat_solver -> Cadical
  | Write_aiger -> ""
  | Write_cnf -> ""
  | Prop_const_bits -> true
  | Prop_ineq_bounds -> true
  | Prop_nprops -> 0
  | Prop_nupdates -> 0
  | Prop_opt_lt_concat_sext -> false
  | Prop_path_sel -> Essential
  | Prop_prob_pick_rand_input -> 10
  | Prop_prob_pick_inv_value -> 990
  | Prop_sext -> true
  | Abstraction -> true
  | Abstraction_bv_size -> 33
  | Abstraction_eager_refine -> false
  | Abstraction_value_limit -> 8
  | Abstraction_value_only -> false
  | Abstraction_assert -> false
  | Abstraction_assert_refs -> 100
  | Abstraction_initial_lemmas -> false
  | Abstraction_inc_bitblast -> false
  | Abstraction_bvadd -> false
  | Abstraction_bvmul -> true
  | Abstraction_bvudiv -> true
  | Abstraction_bvurem -> true
  | Abstraction_eq -> false
  | Abstraction_ite -> false
  | Preprocess -> true
  | Pp_contr_ands -> false
  | Pp_elim_extracts -> false
  | Pp_elim_bvudiv -> false
  | Pp_embedded -> true
  | Pp_flatten_and -> true
  | Pp_normalize -> true
  | Pp_skeleton_preproc -> true
  | Pp_variable_subst -> true
  | Pp_variable_subst_norm_eq -> true
  | Pp_variable_subst_norm_diseq -> false
  | Pp_variable_subst_norm_bv_ineq -> false
  | Dbg_rw_node_thresh -> 0
  | Dbg_pp_node_thresh -> 0
  | Check_model -> false
  | Check_unsat_core -> false
let min : int key -> int = function
  | Log_level -> 0
  | Seed -> 0
  | Verbosity -> 0
  | Time_limit_per -> 0
  | Memory_limit -> 0
  | Nthreads -> 1
  | Rewrite_level -> 0
  | Prop_nprops -> 0
  | Prop_nupdates -> 0
  | Prop_prob_pick_rand_input -> 0
  | Prop_prob_pick_inv_value -> 0
  | Abstraction_bv_size -> 3
  | Abstraction_value_limit -> 0
  | Abstraction_assert_refs -> 1
  | Dbg_rw_node_thresh -> 0
  | Dbg_pp_node_thresh -> 0
let max : int key -> int = function
  | Log_level -> 3
  | Seed -> 4294967295
  | Verbosity -> 4
  | Time_limit_per -> 4611686018427387903
  | Memory_limit -> 4611686018427387903
  | Nthreads -> 4611686018427387903
  | Rewrite_level -> 2
  | Prop_nprops -> 4611686018427387903
  | Prop_nupdates -> 4611686018427387903
  | Prop_prob_pick_rand_input -> 1000
  | Prop_prob_pick_inv_value -> 1000
  | Abstraction_bv_size -> 4611686018427387903
  | Abstraction_value_limit -> 4611686018427387903
  | Abstraction_assert_refs -> 4611686018427387903
  | Dbg_rw_node_thresh -> 4611686018427387903
  | Dbg_pp_node_thresh -> 100
type t
external default : unit -> t = "ocaml_bitwuzla_cxx_options_new"
external set_numeric : t -> (int [@untagged])-> (int [@untagged]) -> unit = "ocaml_bitwuzla_cxx_options_set_numeric" "native_bitwuzla_cxx_options_set_numeric"
external set_mode : t -> (int [@untagged]) -> string -> unit = "ocaml_bitwuzla_cxx_options_set_mode" "native_bitwuzla_cxx_options_set_mode"
let set : type a. t -> a key -> a -> unit = fun t k v ->
  match k with
  | Log_level -> set_numeric t (to_cxx k) v
  | Produce_models -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Produce_unsat_assumptions -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Produce_unsat_cores -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Seed -> set_numeric t (to_cxx k) v
  | Verbosity -> set_numeric t (to_cxx k) v
  | Time_limit_per -> set_numeric t (to_cxx k) v
  | Memory_limit -> set_numeric t (to_cxx k) v
  | Nthreads -> set_numeric t (to_cxx k) v
  | Bv_solver -> set_mode t (to_cxx k) (bv_solver_to_string v)
  | Rewrite_level -> set_numeric t (to_cxx k) v
  | Sat_solver -> set_mode t (to_cxx k) (sat_solver_to_string v)
  | Write_aiger -> set_mode t (to_cxx k) v
  | Write_cnf -> set_mode t (to_cxx k) v
  | Prop_const_bits -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Prop_ineq_bounds -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Prop_nprops -> set_numeric t (to_cxx k) v
  | Prop_nupdates -> set_numeric t (to_cxx k) v
  | Prop_opt_lt_concat_sext -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Prop_path_sel -> set_mode t (to_cxx k) (prop_path_sel_to_string v)
  | Prop_prob_pick_rand_input -> set_numeric t (to_cxx k) v
  | Prop_prob_pick_inv_value -> set_numeric t (to_cxx k) v
  | Prop_sext -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Abstraction -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Abstraction_bv_size -> set_numeric t (to_cxx k) v
  | Abstraction_eager_refine -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Abstraction_value_limit -> set_numeric t (to_cxx k) v
  | Abstraction_value_only -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Abstraction_assert -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Abstraction_assert_refs -> set_numeric t (to_cxx k) v
  | Abstraction_initial_lemmas -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Abstraction_inc_bitblast -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Abstraction_bvadd -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Abstraction_bvmul -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Abstraction_bvudiv -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Abstraction_bvurem -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Abstraction_eq -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Abstraction_ite -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Preprocess -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_contr_ands -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_elim_extracts -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_elim_bvudiv -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_embedded -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_flatten_and -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_normalize -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_skeleton_preproc -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_variable_subst -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_variable_subst_norm_eq -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_variable_subst_norm_diseq -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_variable_subst_norm_bv_ineq -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Dbg_rw_node_thresh -> set_numeric t (to_cxx k) v
  | Dbg_pp_node_thresh -> set_numeric t (to_cxx k) v
  | Check_model -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Check_unsat_core -> set_numeric t (to_cxx k) (Bool.to_int v)
external get_numeric : t -> (int [@untagged])-> (int [@untagged]) = "ocaml_bitwuzla_cxx_options_get_numeric" "native_bitwuzla_cxx_options_get_numeric"
external get_mode : t -> (int [@untagged]) -> string = "ocaml_bitwuzla_cxx_options_get_mode" "native_bitwuzla_cxx_options_get_mode"
external get_string : t -> (int [@untagged]) -> string = "ocaml_bitwuzla_cxx_options_get_str" "native_bitwuzla_cxx_options_get_str"
let get : type a. t -> a key -> a = fun t k ->
  match k with
  | Log_level -> get_numeric t (to_cxx k)
  | Produce_models -> get_numeric t (to_cxx k) <> 0
  | Produce_unsat_assumptions -> get_numeric t (to_cxx k) <> 0
  | Produce_unsat_cores -> get_numeric t (to_cxx k) <> 0
  | Seed -> get_numeric t (to_cxx k)
  | Verbosity -> get_numeric t (to_cxx k)
  | Time_limit_per -> get_numeric t (to_cxx k)
  | Memory_limit -> get_numeric t (to_cxx k)
  | Nthreads -> get_numeric t (to_cxx k)
  | Bv_solver -> bv_solver_of_string (get_mode t (to_cxx k))
  | Rewrite_level -> get_numeric t (to_cxx k)
  | Sat_solver -> sat_solver_of_string (get_mode t (to_cxx k))
  | Write_aiger -> get_string t (to_cxx k)
  | Write_cnf -> get_string t (to_cxx k)
  | Prop_const_bits -> get_numeric t (to_cxx k) <> 0
  | Prop_ineq_bounds -> get_numeric t (to_cxx k) <> 0
  | Prop_nprops -> get_numeric t (to_cxx k)
  | Prop_nupdates -> get_numeric t (to_cxx k)
  | Prop_opt_lt_concat_sext -> get_numeric t (to_cxx k) <> 0
  | Prop_path_sel -> prop_path_sel_of_string (get_mode t (to_cxx k))
  | Prop_prob_pick_rand_input -> get_numeric t (to_cxx k)
  | Prop_prob_pick_inv_value -> get_numeric t (to_cxx k)
  | Prop_sext -> get_numeric t (to_cxx k) <> 0
  | Abstraction -> get_numeric t (to_cxx k) <> 0
  | Abstraction_bv_size -> get_numeric t (to_cxx k)
  | Abstraction_eager_refine -> get_numeric t (to_cxx k) <> 0
  | Abstraction_value_limit -> get_numeric t (to_cxx k)
  | Abstraction_value_only -> get_numeric t (to_cxx k) <> 0
  | Abstraction_assert -> get_numeric t (to_cxx k) <> 0
  | Abstraction_assert_refs -> get_numeric t (to_cxx k)
  | Abstraction_initial_lemmas -> get_numeric t (to_cxx k) <> 0
  | Abstraction_inc_bitblast -> get_numeric t (to_cxx k) <> 0
  | Abstraction_bvadd -> get_numeric t (to_cxx k) <> 0
  | Abstraction_bvmul -> get_numeric t (to_cxx k) <> 0
  | Abstraction_bvudiv -> get_numeric t (to_cxx k) <> 0
  | Abstraction_bvurem -> get_numeric t (to_cxx k) <> 0
  | Abstraction_eq -> get_numeric t (to_cxx k) <> 0
  | Abstraction_ite -> get_numeric t (to_cxx k) <> 0
  | Preprocess -> get_numeric t (to_cxx k) <> 0
  | Pp_contr_ands -> get_numeric t (to_cxx k) <> 0
  | Pp_elim_extracts -> get_numeric t (to_cxx k) <> 0
  | Pp_elim_bvudiv -> get_numeric t (to_cxx k) <> 0
  | Pp_embedded -> get_numeric t (to_cxx k) <> 0
  | Pp_flatten_and -> get_numeric t (to_cxx k) <> 0
  | Pp_normalize -> get_numeric t (to_cxx k) <> 0
  | Pp_skeleton_preproc -> get_numeric t (to_cxx k) <> 0
  | Pp_variable_subst -> get_numeric t (to_cxx k) <> 0
  | Pp_variable_subst_norm_eq -> get_numeric t (to_cxx k) <> 0
  | Pp_variable_subst_norm_diseq -> get_numeric t (to_cxx k) <> 0
  | Pp_variable_subst_norm_bv_ineq -> get_numeric t (to_cxx k) <> 0
  | Dbg_rw_node_thresh -> get_numeric t (to_cxx k)
  | Dbg_pp_node_thresh -> get_numeric t (to_cxx k)
  | Check_model -> get_numeric t (to_cxx k) <> 0
  | Check_unsat_core -> get_numeric t (to_cxx k) <> 0