diff options
| -rw-r--r-- | src/expr/expr_manager.i | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index 2736e9135..7cc635259 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -52,7 +52,6 @@ %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateRight>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::IntToBitVector>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPoint>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RoundingMode>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointSize>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPIEEEBitVector>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPFloatingPoint>; @@ -77,12 +76,14 @@ * case into mkBoolConst. */ %template(mkBoolConst) CVC4::ExprManager::mkConst<bool>; +%template(mkRoundingMode) CVC4::ExprManager::mkConst<RoundingMode>; // These cases have trouble too. Remove them for now. //%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>; #else %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>; %template(mkConst) CVC4::ExprManager::mkConst<bool>; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RoundingMode>; #endif %include "expr/expr_manager.h" |