Resolved some ambiguities that produced problems under Linux. Added option USE_LIBCXX to CMakeLists.txt to also use libc++ under Linux.

Former-commit-id: 2e06d7adf6

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()

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<int>(expression->getValue())));
             }
             
             virtual void visit(ir::expressions::IntegerLiteralExpression* expression) {
-                stack.push(context.int_val(expression->getValueAsInt(nullptr)));
+                stack.push(context.int_val(static_cast<int>(expression->getValueAsInt(nullptr))));
             }
             
             virtual void visit(ir::expressions::UnaryBooleanFunctionExpression* expression) {

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<int>(std::get<1>(*initialState).at(programVariableInformation.integerVariableToIndexMap.at(variable.getName())))));
                 }
                 
                 // Store the found implications in a container similar to the preceding label sets.