From 831bf3412fd4d95656539d7d61fe6d3f7150368c Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 8 Dec 2020 16:42:25 -0800 Subject: [PATCH] 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. --- src/options/bv_options.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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" -- 2.30.2