From 6e2e3d452d637058b5c4a08ab20d06b4d82d2dad Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 18 Jul 2018 16:54:34 +0200 Subject: [PATCH] minor fixes in counterexample generation --- .../counterexamples/SMTMinimalLabelSetGenerator.h | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 4a829b9cb..ce0b94204 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1200,8 +1200,8 @@ namespace storm { solver.add(variableInformation.auxiliaryVariables.back()); variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(solver, variableInformation, ++currentBound)); assumption = !variableInformation.auxiliaryVariables.back(); - if (currentBound > (1 << variableInformation.minimalityLabelVariables.size())) { - STORM_LOG_DEBUG("Constraint system fully explored: Bound exceeds maximum of " << (1 << variableInformation.minimalityLabelVariables.size())); + if (currentBound > variableInformation.minimalityLabelVariables.size()) { + STORM_LOG_DEBUG("Constraint system fully explored: Bound exceeds maximum of " << variableInformation.minimalityLabelVariables.size()); return boost::none; } } @@ -1525,11 +1525,6 @@ namespace storm { } - if (rewardName) { - auto const &origRewModel = model.getRewardModel(rewardName.get()); - assert(origRewModel.hasOnlyStateRewards()); - } - std::shared_ptr> resultModel; if (model.isOfType(storm::models::ModelType::Dtmc)) { resultModel = std::make_shared>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling()), model.getRewardModels());