From bc94f69c0bad0e5ce2b9e1b0e7f0fbb95c9217be Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 13 Nov 2013 15:07:20 +0100 Subject: [PATCH] Resolved some ambiguities that produced problems under Linux. Added option USE_LIBCXX to CMakeLists.txt to also use libc++ under Linux. Former-commit-id: 2e06d7adf6686d271794a8ca40a376ee077c3bfc --- CMakeLists.txt | 3 ++- src/adapters/Z3ExpressionAdapter.h | 4 ++-- src/counterexamples/SMTMinimalCommandSetGenerator.h | 2 +- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 9bb6e10da..51a4b9004 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -31,6 +31,7 @@ option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be li option(USE_INTELTBB "Sets whether the Intel TBB Extensions should be used." OFF) option(STORM_USE_COTIRE "Sets whether Cotire should be used (for building precompiled headers)." OFF) option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF) +option(USE_LIBCXX "Sets whether the standard library is libc++." OFF) set(GUROBI_ROOT "" CACHE STRING "The root directory of Gurobi (if available).") set(Z3_ROOT "" CACHE STRING "The root directory of Z3 (if available).") set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") @@ -138,7 +139,7 @@ else(CLANG) set (CLANG ON) # Set standard flags for clang set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O3") - if(UNIX AND NOT APPLE) + if(UNIX AND NOT APPLE AND NOT USE_LIBCXX) set(CLANG_STDLIB libstdc++) message(STATUS "StoRM - Linking against libstdc++") else() diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 6a6ce210a..09bc1dac4 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -166,11 +166,11 @@ namespace storm { << ". Integer constant '" << expression->getConstantName() << "' is undefined."; } - stack.push(context.int_val(expression->getValue())); + stack.push(context.int_val(static_cast(expression->getValue()))); } virtual void visit(ir::expressions::IntegerLiteralExpression* expression) { - stack.push(context.int_val(expression->getValueAsInt(nullptr))); + stack.push(context.int_val(static_cast(expression->getValueAsInt(nullptr)))); } virtual void visit(ir::expressions::UnaryBooleanFunctionExpression* expression) { diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 645ba0268..6ab3e5bc0 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -555,7 +555,7 @@ namespace storm { } for (uint_fast64_t index = 0; index < programVariableInformation.integerVariables.size(); ++index) { storm::ir::IntegerVariable const& variable = programVariableInformation.integerVariables[index]; - initialStateExpression = initialStateExpression && (solverVariables.at(variable.getName()) == localContext.int_val(std::get<1>(*initialState).at(programVariableInformation.integerVariableToIndexMap.at(variable.getName())))); + initialStateExpression = initialStateExpression && (solverVariables.at(variable.getName()) == localContext.int_val(static_cast(std::get<1>(*initialState).at(programVariableInformation.integerVariableToIndexMap.at(variable.getName()))))); } // Store the found implications in a container similar to the preceding label sets.