projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8cf0942) | patch
Fix reduction for arc trig functions (#8289)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 11 Mar 2022 17:40:16 +0000 (11:40 -0600)
committerGitHub <noreply@github.com>
Fri, 11 Mar 2022 17:40:16 +0000 (17:40 +0000)
commit3f09cf86d8a0129c12afc6ee63445c2a714ce5f6
treec828688fa568a46145e863696326e5f87d2b46e5tree
parent8cf0942ec99e61c92befd1a08eb2aba8d6072781commit | diff
Fix reduction for arc trig functions (#8289)

We were not guarding the case where the argument was out of the bounds, e.g. arccos(x) requires -1 <= x <= 1.

Fixes cvc5/cvc5-projects#485.
src/theory/arith/operator_elim.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/nta/proj-issue483-arccos-oob.smt2 [new file with mode: 0644] blob
test/regress/regress1/nl/sugar-ident.smt2 diff | blob | history