diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index bc918b48c..9cef9ab3c 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -31,14 +31,19 @@ namespace storm { storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(critical1)); storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2)); - auto latticeCopy = new Lattice(lattice); std::vector> assumptions; - auto myMap = createAssumptions(var1, var2, latticeCopy, assumptions); + auto myMap = createAssumptions(var1, var2, new Lattice(lattice), assumptions); result.insert(myMap.begin(), myMap.end()); std::vector> assumptions2; - myMap = createAssumptions(var2, var1, lattice, assumptions2); + myMap = createAssumptions(var2, var1, new Lattice(lattice), assumptions2); result.insert(myMap.begin(), myMap.end()); + if (result.size() == 0) { + // No assumptions could be made, all not valid based on sampling, therefore returning original lattice + result.insert(std::pair>>(lattice, emptySet)); + } else { + delete lattice; + } } return result; }