projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c1569c9) | patch
Fix issue with dropping non-reduced sine terms (#8211)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 2 Mar 2022 23:09:24 +0000 (17:09 -0600)
committerGitHub <noreply@github.com>
Wed, 2 Mar 2022 23:09:24 +0000 (23:09 +0000)
commita30458a2a3e21f40e893fe545c6e9c2c73e32707
tree27f982ddbacbbab33ff09b681c81b07af8b14f77tree
parentc1569c97f1d2a08c528ebddb86454bfa6ea58611commit | diff
Fix issue with dropping non-reduced sine terms (#8211)

Fixes #8208.

A spurious "break" was leftover from when this code was a loop, this meant when the first reduced term was encountered, it ignored the remainder.
src/theory/arith/nl/transcendental/sine_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_state.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/nta/issue8208-red-nred.smt2 [new file with mode: 0644] blob