Support for conjunction over empty set

7 years ago · e8a950d9d7
1 changed files with 8 additions and 4 deletions
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
@ -107,11 +107,15 @@ namespace storm {

            std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
                std::stringstream sstr;
-                sstr << "(and";
-                for(auto const& c : constraints) {
-                    sstr << " " << c->toSmtlib2(varNames);
+                if (constraints.empty()) {
+                    sstr << "true";
+                } else {
+                    sstr << "(and";
+                    for(auto const& c : constraints) {
+                        sstr << " " << c->toSmtlib2(varNames);
+                    }
+                    sstr << ")";
                }
-                sstr << ")";
                return sstr.str();
            }