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/theory_sets.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/theory_sets.h')
0 files changed, 0 insertions, 0 deletions