diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake index 731758830..a23bb46f6 100644 --- a/resources/3rdparty/include_cudd.cmake +++ b/resources/3rdparty/include_cudd.cmake @@ -23,7 +23,7 @@ ExternalProject_Add( PREFIX ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 PATCH_COMMAND ${AUTORECONF} CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --with-pic=yes --prefix=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 --libdir=${CUDD_LIB_DIR} CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} - BUILD_COMMAND make "CFLAGS=-O2 -w" + BUILD_COMMAND make "CFLAGS=-O3 -w" INSTALL_COMMAND make install BUILD_IN_SOURCE 0 LOG_CONFIGURE ON @@ -49,4 +49,4 @@ else() list(APPEND STORM_DEP_TARGETS cudd_STATIC) endif() -message(STATUS "Storm - Linking with CUDD ${CUDD_VERSION_STRING}.") \ No newline at end of file +message(STATUS "Storm - Linking with CUDD ${CUDD_VERSION_STRING}.") diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index 84d7bcd15..c8dd1f1f3 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -58,7 +58,7 @@ namespace storm { // Solve the equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.0) * maybeStatesAdd, subvector); + storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.0), subvector); return statesWithProbability01.second.template toAdd() + result; } else { @@ -175,7 +175,7 @@ namespace storm { // Solve the equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.0) * maybeStatesAdd, subvector); + storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.0), subvector); return infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), result); } else { diff --git a/src/storm/solver/SymbolicLinearEquationSolver.h b/src/storm/solver/SymbolicLinearEquationSolver.h index 1b64c1d55..13686d3f4 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.h +++ b/src/storm/solver/SymbolicLinearEquationSolver.h @@ -83,7 +83,7 @@ namespace storm { protected: // The matrix defining the coefficients of the linear equation system. - storm::dd::Add const& A; + storm::dd::Add A; // A BDD characterizing all rows of the equation system. storm::dd::Bdd const& allRows;