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 36d0e6d1166919882998c57fd10453d76ca97706..2ecafdaa208f269a2538d9bdc8298aae8d9d2a57 100644 (file)
--- 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 4ffe4421e1b907170726332c321d14cb7ac1ffaf..4ef2a64c77a3f0c66950a5999bca895dd3acd0ab 100644 (file)
--- 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 (file)
index 0000000..b540c63
--- /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)
+