diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 37d8847a4..43128aa0d 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -183,6 +183,9 @@ Z3Solver::getNextConfiguration() { Dirty = true; } + if (Solver->check() == z3::unsat) { + return UNSAT; + } return getCurrentConfiguration(); } @@ -236,9 +239,6 @@ Z3Solver::setBinaryFeatureConstraints(const feature::BinaryFeature &Feature, } Result Z3Solver::excludeCurrentConfiguration() { - if (Solver->check() == z3::unsat) { - return UNSAT; - } const z3::model M = Solver->get_model(); z3::expr Expr = Context.bool_val(false); for (const auto &Entry : OptionToVariableMapping) { @@ -260,9 +260,6 @@ Result Z3Solver::excludeCurrentConfiguration() { Result> Z3Solver::getCurrentConfiguration() { - if (Solver->check() == z3::unsat) { - return UNSAT; - } const z3::model M = Solver->get_model(); auto Config = std::make_unique(); diff --git a/unittests/Solver/ConfigurationFactory.cpp b/unittests/Solver/ConfigurationFactory.cpp index 2a095ea34..84988998f 100644 --- a/unittests/Solver/ConfigurationFactory.cpp +++ b/unittests/Solver/ConfigurationFactory.cpp @@ -72,6 +72,25 @@ TEST(ConfigurationFactory, GetAllConfigurations2) { EXPECT_EQ(Configs.size(), UniqueConfigs.size()); } +TEST(ConfigurationFactory, GetAllConfigurations3) { + auto FM = feature::loadFeatureModel( + getTestResource("test_msmr.xml")); + auto ConfigResult = ConfigurationFactory::getAllConfigs(*FM); + EXPECT_TRUE(ConfigResult); + auto Configs = ConfigResult.extractValue(); + + EXPECT_EQ(Configs.size(), 16); + + auto ConfigsStrings = std::vector(); + for (auto &config : Configs) { + ConfigsStrings.push_back(config.get()->dumpToString()); + } + + auto UniqueConfigs = + std::set(ConfigsStrings.begin(), ConfigsStrings.end()); + EXPECT_EQ(Configs.size(), UniqueConfigs.size()); +} + TEST(ConfigurationFactory, GetNConfigurations) { auto FM = getFeatureModel(); auto ConfigResult = ConfigurationFactory::getNConfigs(*FM, 100); diff --git a/unittests/resources/CMakeLists.txt b/unittests/resources/CMakeLists.txt index 5d47f4336..dbf71e528 100644 --- a/unittests/resources/CMakeLists.txt +++ b/unittests/resources/CMakeLists.txt @@ -32,6 +32,7 @@ set(FEATURE_LIB_TEST_FILES xml/test_hsqldb_num.xml xml/test_member_offset.xml xml/test_mixed_constraints.xml + xml/test_msmr.xml xml/test_numbers.xml xml/test_only_children.xml xml/test_only_parents.xml diff --git a/unittests/resources/xml/test_msmr.xml b/unittests/resources/xml/test_msmr.xml new file mode 100644 index 000000000..20f41419e --- /dev/null +++ b/unittests/resources/xml/test_msmr.xml @@ -0,0 +1,48 @@ + + + + + + root + + False + + + Slow + --slow + root + True + + + Header + --header + root + True + + + Extern + --extern + root + True + + + src/MultiSharedMultipleRegions/FeatureHeader.cpp + + 3 + 6 + + + 3 + 18 + + + + + + Cpp + --cpp + root + True + + + \ No newline at end of file