diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-09-04 00:58:03 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-03 17:58:03 -0500 |
commit | 19ff08d652de2890eee4674d2a6debe10e879f1f (patch) | |
tree | a1e10e4c354fd44bd1073683b2e4edea8a054e41 /src/theory/sets/solver_state.h | |
parent | 8828e545cfb838d806a0ad382671a9af131e8431 (diff) |
Added a new rule to simplify (bvugt (bvurem T x) x) (#4993)
Motivated by #4936, this PR adds a new BV rewrite rule:
(bvugt (bvurem T x) x) ==> (ite (= x 0) (bvugt T 0) false)
Fixes #4936.
Diffstat (limited to 'src/theory/sets/solver_state.h')
0 files changed, 0 insertions, 0 deletions