projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d07c779) | patch
Improve error message for unsupported exponents (#4852)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 5 Aug 2020 18:55:00 +0000 (20:55 +0200)
committerGitHub <noreply@github.com>
Wed, 5 Aug 2020 18:55:00 +0000 (13:55 -0500)
commit47f003828a8ba0cd8edd362accaef8b2449b0c46
treed67941c0c017262dc287fda36b1a9818302e4d30tree
parentd07c7796f75e32e46698f4f0af90a8b99577323fcommit | diff
Improve error message for unsupported exponents (#4852)

We have had a few issues where essentially users misinterpreted the error message about which types of exponents are supported for (^ base exp). Given that this is rewritten to a multiplication of length exp, we only support reasonably small natural numbers.
This PR improves the error message.
Fixes #4692
src/theory/arith/arith_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/arith/bug716.1.cvc diff | blob | history
test/regress/regress1/arith/bug716.2.cvc [new file with mode: 0644] blob