diff options
Diffstat (limited to 'src/theory/fp/fp_converter.cpp')
| -rw-r--r-- | src/theory/fp/fp_converter.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 3b5a115c8..1d124045b 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -648,7 +648,7 @@ symbolicBitVector<false> symbolicBitVector<isSigned>::toUnsigned(void) const template <> symbolicBitVector<true> symbolicBitVector<true>::extend(bwt extension) const { - NodeBuilder<> construct(kind::BITVECTOR_SIGN_EXTEND); + NodeBuilder construct(kind::BITVECTOR_SIGN_EXTEND); construct << NodeManager::currentNM()->mkConst<BitVectorSignExtend>( BitVectorSignExtend(extension)) << *this; @@ -659,7 +659,7 @@ symbolicBitVector<true> symbolicBitVector<true>::extend(bwt extension) const template <> symbolicBitVector<false> symbolicBitVector<false>::extend(bwt extension) const { - NodeBuilder<> construct(kind::BITVECTOR_ZERO_EXTEND); + NodeBuilder construct(kind::BITVECTOR_ZERO_EXTEND); construct << NodeManager::currentNM()->mkConst<BitVectorZeroExtend>( BitVectorZeroExtend(extension)) << *this; @@ -673,7 +673,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::contract( { Assert(this->getWidth() > reduction); - NodeBuilder<> construct(kind::BITVECTOR_EXTRACT); + NodeBuilder construct(kind::BITVECTOR_EXTRACT); construct << NodeManager::currentNM()->mkConst<BitVectorExtract>( BitVectorExtract((this->getWidth() - 1) - reduction, 0)) << *this; @@ -724,7 +724,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract( { Assert(upper >= lower); - NodeBuilder<> construct(kind::BITVECTOR_EXTRACT); + NodeBuilder construct(kind::BITVECTOR_EXTRACT); construct << NodeManager::currentNM()->mkConst<BitVectorExtract>( BitVectorExtract(upper, lower)) << *this; |