projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d0bab2e) | patch
Refactor how arith rewriting checks for mult-by-zero (#7962)
authorGereon Kremer <gkremer@stanford.edu>
Mon, 24 Jan 2022 19:23:41 +0000 (11:23 -0800)
committerGitHub <noreply@github.com>
Mon, 24 Jan 2022 19:23:41 +0000 (19:23 +0000)
commitdfc685b86237a56b1a54801bafa343b5139aaac0
treed6634d8b37185f2e65702a48e79a88ac887ad328tree
parentd0bab2e969c3557596516f3460eede4f28e468a1commit | diff
Refactor how arith rewriting checks for mult-by-zero (#7962)

This adds an explicit check for a zero factor in the post rewriter for multiplication.
src/theory/arith/arith_rewriter.cpp diff | blob | history