From: yoni206 Date: Thu, 2 Jun 2022 03:26:45 +0000 (+0300) Subject: Restricting the bit-width in int-to-bv (#8814) X-Git-Tag: cvc5-1.0.1~78 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3003ba4636a5de1425869082cf4f497a256f4968;p=cvc5.git Restricting the bit-width in int-to-bv (#8814) `cvc5` only supports bit-widths of `unsigned` size for BitVector sorts (see, e.g., [here](https://github.com/cvc5/cvc5/blob/4338d9d49a41022d34cd4cbabf17a66fdf39efae/src/expr/node_manager_template.cpp#L178)). This checks that the provided bit-width for the `int-to-bv` option is in the right range. Fixes https://github.com/cvc5/cvc5-projects/issues/425 and includes a regression that is based on the test from the issue. --- diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 36d0e6d11..2ecafdaa2 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -404,6 +404,7 @@ name = "SMT Layer" long = "solve-int-as-bv=N" type = "uint64_t" default = "0" + maximum = "4294967295" help = "attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)" [[option]] diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 4ffe4421e..4ef2a64c7 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -868,6 +868,7 @@ set(regress_0_tests regress0/nl/pow2-pow.smt2 regress0/nl/pow2-pow-isabelle.smt2 regress0/nl/proj-issue-348.smt2 + regress0/nl/proj-issue-425.smt2 regress0/nl/proj-issue-444-memout-eqelim.smt2 regress0/nl/proj-issue-451-ran-combination-1.smt2 regress0/nl/proj-issue-451-ran-combination-2.smt2 diff --git a/test/regress/cli/regress0/nl/proj-issue-425.smt2 b/test/regress/cli/regress0/nl/proj-issue-425.smt2 new file mode 100644 index 000000000..b540c638b --- /dev/null +++ b/test/regress/cli/regress0/nl/proj-issue-425.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --solve-int-as-bv=5524936381719514648 +; ERROR-SCRUBBER: sed -e '.*Error in option parsing.*/d' +; DISABLE-TESTER: dump +; EXIT: 1 +(set-logic QF_NIA) +(declare-fun x () Int) +(declare-fun y () Int) +(assert (= (* x x) y)) +(check-sat) +