update doc (#5619)

The current help message for --bv-div-zero-const only mentions bvudiv (in which the result is -1) and not bvurem (in which the result is the first argument).
I think this is a bit misleading, because in practice, this option controls also the behavior of bvurem:
CVC4/src/theory/bv/theory_bv.cpp

Line 134 in 0309ef4

 if (options::bitvectorDivByZeroConst())
This PR is an attempt to provide a more accurate help message.

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index d2e3a61fd6f9d6613e4da2af430cf95f1b90a5c5..a7f8d439f2bc107eecfa80bc5cf8728c3562b4f2 100644 (file)
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -135,7 +135,7 @@ header = "options/bv_options.h"
   long       = "bv-div-zero-const"
   type       = "bool"
   default    = "true"
-  help       = "always return -1 on division by zero"
+  help       = "always return -1 on (bvudiv s 0) and s on (bvurem s 0)"
 
 [[option]]
   name       = "bvExtractArithRewrite"