diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-16 16:38:38 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-16 16:38:38 -0800 |
| commit | 78d7485639cdf0769c13606b8ad3f5e9455153f1 (patch) | |
| tree | fa32eeda005c7ef774bdf9e7a210d43bc9b33ffa /src/options/bv_options.toml | |
| parent | 60b5ac4c6488014feb4820a98e663cc5fdbad5c1 (diff) | |
Add option to print BV constants in binary (#2805)
This commit adds the option `--bv-print-consts-in-binary` to print
bit-vector constants in binary, e.g. `#b0001`, instead of decimal, e.g.
`(_ bv1 4)`). The option is on by default to match the behavior of Z3
and Boolector.
Diffstat (limited to 'src/options/bv_options.toml')
| -rw-r--r-- | src/options/bv_options.toml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 0422ae06f..c4541f4e4 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -232,3 +232,11 @@ header = "options/bv_options.h" type = "bool" default = "true" help = "algebraic inferences for extended functions" + +[[option]] + name = "bvPrintConstsInBinary" + category = "regular" + long = "bv-print-consts-in-binary" + type = "bool" + default = "false" + help = "print bit-vector constants in binary (e.g. #b0001) instead of decimal (e.g. (_ bv1 4)), applies to SMT-LIB 2.x" |