do not export reward model if we find a counterexample for a probability property

src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h

@@ -2121,7 +2121,11 @@ namespace storm {
 
 
                 if (symbolicModel.isPrismProgram()) {
-                    return std::make_shared<HighLevelCounterexample>(symbolicModel.asPrismProgram().restrictCommands(labelSets[0]));
+                    storm::prism::Program program = symbolicModel.asPrismProgram().restrictCommands(labelSets[0]);
+                    if(formula->isProbabilityOperatorFormula()) {
+                        program.removeRewardModels();
+                    }
+                    return std::make_shared<HighLevelCounterexample>(program);
                 } else {
                     STORM_LOG_ASSERT(symbolicModel.isJaniModel(), "Unknown symbolic model description type.");
                     return std::make_shared<HighLevelCounterexample>(symbolicModel.asJaniModel().restrictEdges(labelSets[0]));

src/storm/storage/prism/Program.cpp

@@ -732,6 +732,11 @@ namespace storm {
             STORM_LOG_THROW(it != this->labels.end(), storm::exceptions::InvalidArgumentException, "Canno remove unknown label '" << name << "'.");
             this->labels.erase(it);
         }
+
+        void Program::removeRewardModels() {
+            this->rewardModels.clear();
+            this->rewardModelToIndexMap.clear();
+        }
         
         void Program::filterLabels(std::set<std::string> const& labelSet) {
             std::vector<storm::prism::Label> newLabels;

src/storm/storage/prism/Program.h

@@ -575,6 +575,8 @@ namespace storm {
              */
             void filterLabels(std::set<std::string> const& labelSet);
 
+            void removeRewardModels();
+
             /*!
              * Retrieves all observation labels that are defined by this program
              *