From: yoni206 <yoni206@users.noreply.github.com>
Date: Mon, 22 Jun 2020 15:33:46 +0000 (-0700)
Subject: fix (#4637)
X-Git-Tag: cvc5-1.0.0~3186
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4bd54ef0cc862ae8736c97ecca07f80ab31396df;p=cvc5.git

fix (#4637)

The help message of --bv-print-consts-as-indexed-symbols seems wrong to me, and this PR suggests a fix.
---

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index a72c7d92a..517d864d3 100644
--- 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"