From e8a950d9d77b17b7dad0aac6d6780fd10d689882 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 24 Nov 2017 18:27:32 +0100
Subject: [PATCH] Support for conjunction over empty set

---
 src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
index 94b6c308c..35afa7cb8 100644
--- 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();
             }