projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 60b5ac4) | patch
Add option to print BV constants in binary (#2805)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 17 Jan 2019 00:38:38 +0000 (16:38 -0800)
committerGitHub <noreply@github.com>
Thu, 17 Jan 2019 00:38:38 +0000 (16:38 -0800)
commit78d7485639cdf0769c13606b8ad3f5e9455153f1
treefa32eeda005c7ef774bdf9e7a210d43bc9b33ffatree
parent60b5ac4c6488014feb4820a98e663cc5fdbad5c1commit | 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.
src/options/bv_options.toml diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/printer/bv_consts_bin.smt2 [new file with mode: 0644] blob
test/regress/regress0/printer/bv_consts_dec.smt2 [new file with mode: 0644] blob