diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp index 22dc7c753..7a1a9ab8d 100644 --- a/src/storage/dd/DdManager.cpp +++ b/src/storage/dd/DdManager.cpp @@ -108,13 +108,14 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> + template<> Add DdManager::getIdentity(storm::expressions::Variable const& variable) const { storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); Add result = this->getAddZero(); for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { storm::RationalFunction constantFunction(value); - result += this->getEncoding(variable, value).template toAdd() * this->getConstant(constantFunction); + result += this->getEncoding(variable, value).template toAdd() * this->getConstant(constantFunction); } return result; } diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp index c10235ca8..287fe55c3 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -131,12 +131,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const { - storm::RationalFunction rationalFunction = value; - storm_rational_function_ptr_struct helperStruct; - helperStruct.storm_rational_function = (void*)(&rationalFunction); - uint64_t terminalValue = (uint64_t)&helperStruct; - - return InternalAdd(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), terminalValue)); + return InternalAdd(this, sylvan::Mtbdd::stormRationalFunctionTerminal(value)); } #endif