projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 3bc4a54)
fix (#4637)
authoryoni206 <yoni206@users.noreply.github.com>
Mon, 22 Jun 2020 15:33:46 +0000 (08:33 -0700)
committerGitHub <noreply@github.com>
Mon, 22 Jun 2020 15:33:46 +0000 (10:33 -0500)
The help message of --bv-print-consts-as-indexed-symbols seems wrong to me, and this PR suggests a fix.

src/options/bv_options.toml patch | blob | history

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index a72c7d92a6d9eb64311380f4f824b097bc1c26c2..517d864d3eb722da839953c65573dfa171eff051 100644 (file)
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -291,4 +291,4 @@ header = "options/bv_options.h"
   long       = "bv-print-consts-as-indexed-symbols"
   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"
+  help       = "print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x"