From: yoni206 <yoni206@users.noreply.github.com>
Date: Wed, 9 Dec 2020 00:42:25 +0000 (-0800)
Subject: update doc (#5619)
X-Git-Tag: cvc5-1.0.0~2475
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=831bf3412fd4d95656539d7d61fe6d3f7150368c;p=cvc5.git

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 d2e3a61fd..a7f8d439f 100644
--- 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"