diff options
Diffstat (limited to 'src/theory/bv/bitblaster_template.h')
| -rw-r--r-- | src/theory/bv/bitblaster_template.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 0a7d165a2..aa5ae9c16 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -404,6 +404,9 @@ template <class T> void TBitblaster<T>::initTermBBStrategies() { d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB<T>; d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB<T>; d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB<T>; + d_termBBStrategies [ kind::BITVECTOR_ULTBV ] = DefaultUltbvBB<T>; + d_termBBStrategies [ kind::BITVECTOR_SLTBV ] = DefaultSltbvBB<T>; + d_termBBStrategies [ kind::BITVECTOR_ITE ] = DefaultIteBB<T>; d_termBBStrategies [ kind::BITVECTOR_EXTRACT ] = DefaultExtractBB<T>; d_termBBStrategies [ kind::BITVECTOR_REPEAT ] = DefaultRepeatBB<T>; d_termBBStrategies [ kind::BITVECTOR_ZERO_EXTEND ] = DefaultZeroExtendBB<T>; |