summaryrefslogtreecommitdiff
path: root/src/options/smt_options.toml
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/smt_options.toml')
-rw-r--r--src/options/smt_options.toml9
1 files changed, 9 insertions, 0 deletions
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
@@ -665,6 +665,15 @@ header = "options/smt_options.h"
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"
long = "solve-int-as-bv=N"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback