two more fixes for issues pointed out by Tim: concurrency bug in sylvan and bug in symbolic quantitative check result

resources/3rdparty/sylvan/src/sylvan_table.c

@@ -187,7 +187,7 @@ llmsset_lookup2(const llmsset_t dbs, uint64_t a, uint64_t b, int* created, const
         if (hash == (v & MASK_HASH)) {
             uint64_t d_idx = v & MASK_INDEX;
             uint64_t *d_ptr = ((uint64_t*)dbs->data) + 2*d_idx;
-            if (custom && is_custom_bucket(dbs, d_idx)) {
+            if (custom) {
                 if (dbs->equals_cb(a, b, d_ptr[0], d_ptr[1])) {
                     if (cidx != 0) {
                         dbs->destroy_cb(a, b);

src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp

@@ -24,17 +24,17 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         std::unique_ptr<CheckResult> SymbolicQuantitativeCheckResult<Type, ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const {
-            storm::dd::Bdd<Type> states;
+            storm::dd::Bdd<Type> states = this->states;
             if (comparisonType == storm::logic::ComparisonType::Less) {
-                states = values.less(bound);
+                states &= values.less(bound);
             } else if (comparisonType == storm::logic::ComparisonType::LessEqual) {
-                states = values.lessOrEqual(bound);
+                states &= values.lessOrEqual(bound);
             } else if (comparisonType == storm::logic::ComparisonType::Greater) {
-                states = values.greater(bound);
+                states &= values.greater(bound);
             } else if (comparisonType == storm::logic::ComparisonType::GreaterEqual) {
-                states = values.greaterOrEqual(bound);
+                states &= values.greaterOrEqual(bound);
             }
-            return std::unique_ptr<SymbolicQualitativeCheckResult<Type>>(new SymbolicQualitativeCheckResult<Type>(reachableStates, states));
+            return std::unique_ptr<SymbolicQualitativeCheckResult<Type>>(new SymbolicQualitativeCheckResult<Type>(reachableStates, this->states, states));
         }
         
         template<storm::dd::DdType Type, typename ValueType>

src/storm/utility/storm.h

@@ -268,6 +268,8 @@ namespace storm {
             
             STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models.");
             model = performBisimulationMinimization<ModelType>(model->template as<storm::models::sparse::Model<typename ModelType::ValueType>>(), formulas, bisimType);
+            
+            STORM_LOG_INFO("Quotient model has " << model->getNumberOfStates() << " states and " << model->getNumberOfTransitions() << " transitions.");
         }
         
         preprocessingWatch.stop();