summaryrefslogtreecommitdiff
path: root/src/expr/proof_node_manager.cpp
diff options
context:
space:
mode:
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>2020-09-17 22:44:53 +0200
committerGitHub <noreply@github.com>2020-09-17 15:44:53 -0500
commit6cc837f99a37287bf583491649797486650f77e7 (patch)
tree22974bc24c4e5b93643ad5ed5acea3e2e4fcab36 /src/expr/proof_node_manager.cpp
parentbd6f48ec9ecdd0547b77e9e8a49d3028f4281fe0 (diff)
(cad-solver) Fix square-free-basis computation (#5085)
This PR fixes a subtle issue when making the polynomials of two subsequent (overlapping) intervals relative square-free. We now make sure that the resulting polynomials are ignored (if constant) or pushed to the lower dimension (if lower main variable). Also, we now appropriately update the main polynomials of the corresponding intervals.
Diffstat (limited to 'src/expr/proof_node_manager.cpp')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback