diff options
Diffstat (limited to 'src/theory/unconstrained_simplifier.cpp')
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 7509c7f4f..c2fc9929a 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -280,8 +280,8 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::BITVECTOR_SHL: case kind::BITVECTOR_LSHR: case kind::BITVECTOR_ASHR: - case kind::BITVECTOR_UDIV: - case kind::BITVECTOR_UREM: + case kind::BITVECTOR_UDIV_TOTAL: + case kind::BITVECTOR_UREM_TOTAL: case kind::BITVECTOR_SDIV: case kind::BITVECTOR_SREM: case kind::BITVECTOR_SMOD: { @@ -634,16 +634,13 @@ void UnconstrainedSimplifier::processUnconstrained() break; } - // These should have been rewritten up front - case kind::BITVECTOR_REPEAT: + // Do nothing + case kind::BITVECTOR_SIGN_EXTEND: case kind::BITVECTOR_ZERO_EXTEND: + case kind::BITVECTOR_REPEAT: case kind::BITVECTOR_ROTATE_LEFT: case kind::BITVECTOR_ROTATE_RIGHT: - Unreachable(); - break; - // Do nothing - case kind::BITVECTOR_SIGN_EXTEND: default: break; } |