projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b212e64) | patch
Do not call ppRewrite on Boolean equalities (#5762)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 13 Jan 2021 14:28:56 +0000 (08:28 -0600)
committerGitHub <noreply@github.com>
Wed, 13 Jan 2021 14:28:56 +0000 (08:28 -0600)
commitacbe543869918eb2d88779f0f98bfd18b82282d3
tree13c51723dcaf4c7c56da2f7cc076c45a034f214ctree
parentb212e64555954532b93db2b64a863d107a4a127dcommit | diff
Do not call ppRewrite on Boolean equalities (#5762)

Was causing arithmetic to process a Boolean equality when --arith-rewrite-equalities is true.

Fixes #5761.
src/preprocessing/passes/theory_rewrite_eq.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/arith/issue5761-ppr.smt2 [new file with mode: 0644] blob