From 6e17dd6d5e3ec043e5edd097ac6a736f6a41c753 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Mon, 24 Feb 2020 19:58:01 -0800 Subject: bv_to_int preprocessing pass Introduces a preprocessing pass that translates bv problems to integer problems. --- src/options/smt_options.toml | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/options/smt_options.toml') diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index f78dbb3b8..024530224 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -664,6 +664,15 @@ header = "options/smt_options.h" read_only = true help = "Force no CPU limit when dumping models and proofs" +[[option]] + name = "solveBVAsInt" + category = "undocumented" + long = "solve-bv-as-int=N" + type = "uint32_t" + default = "0" + read_only = true + help = "attempt to solve BV formulas by translation to integer arithmetic (experimental)" + [[option]] name = "solveIntAsBV" category = "undocumented" -- cgit v1.2.3