projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2b504cd) | patch
Fix tangent plane lemmas (#5455)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 17 Nov 2020 13:43:15 +0000 (14:43 +0100)
committerGitHub <noreply@github.com>
Tue, 17 Nov 2020 13:43:15 +0000 (14:43 +0100)
commit3bbdafbc3f5683d04786efdd86db7f478f2ae522
tree9f07f2861ae819534ea55ddb7c5b189473c4c1e4tree
parent2b504cd20b7cbbd0a3e7473162c7640907faf04dcommit | diff
Fix tangent plane lemmas (#5455)

The previous refactoring of tangent plane lemmas introduced incorrect lemmas.
This PR fixes this issue and actually generated the lemmas described in the comment.
Fixes #5452.
src/theory/arith/nl/ext/tangent_plane_check.cpp diff | blob | history