projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cd1a802) | patch
Handle rewrite to bool in BoundInference (#5311)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 20 Oct 2020 15:01:30 +0000 (17:01 +0200)
committerGitHub <noreply@github.com>
Tue, 20 Oct 2020 15:01:30 +0000 (10:01 -0500)
commit5e714e365dbbd51bbf04305867c4bcdc3d5a4d83
tree7f37e2c514e24cb263ca07a9bf34277b254d22detree
parentcd1a8023502b0d6d268dafd22328d06840d04324commit | diff
Handle rewrite to bool in BoundInference (#5311)

The BoundInference class did not properly handle rewrites that yield constant Booleans. This PR fixes this issue by explicitly checking for this case.
src/theory/arith/bound_inference.cpp diff | blob | history
src/theory/arith/nl/icp/icp_solver.cpp diff | blob | history