From f5511f4213e624ec43389e2c7ae50a06a652e52b Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 28 Mar 2018 18:01:29 +0200 Subject: [PATCH] removed obsolete 'inplace' setting for multiplier --- src/storm/settings/modules/MultiplierSettings.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/settings/modules/MultiplierSettings.cpp b/src/storm/settings/modules/MultiplierSettings.cpp index befa91086..d386bbf3a 100644 --- a/src/storm/settings/modules/MultiplierSettings.cpp +++ b/src/storm/settings/modules/MultiplierSettings.cpp @@ -15,7 +15,7 @@ namespace storm { const std::string MultiplierSettings::multiplierTypeOptionName = "type"; MultiplierSettings::MultiplierSettings() : ModuleSettings(moduleName) { - std::vector multiplierTypes = {"native", "inplace", "gmmxx"}; + std::vector multiplierTypes = {"native", "gmmxx"}; this->addOption(storm::settings::OptionBuilder(moduleName, multiplierTypeOptionName, true, "Sets which type of multiplier is preferred.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a multiplier.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(multiplierTypes)).setDefaultValueString("gmmxx").build()).build());