From b89f8f8de433ef1fb5bf09a41b36e422db022235 Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Wed, 24 Apr 2019 12:55:18 +0200
Subject: [PATCH] Refactoring of SMT tests

---
 .../storm-dft/api/DftModelCheckerTest.cpp     | 19 --------------
 src/test/storm-dft/api/DftSmtTest.cpp         | 26 +++++++++++++++++++
 2 files changed, 26 insertions(+), 19 deletions(-)
 create mode 100644 src/test/storm-dft/api/DftSmtTest.cpp

diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp
index 454c94f36..65e1e05d2 100644
--- a/src/test/storm-dft/api/DftModelCheckerTest.cpp
+++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp
@@ -2,7 +2,6 @@
 #include "storm-config.h"
 
 #include "storm-dft/api/storm-dft.h"
-#include "storm-dft/modelchecker/dft/DFTASFChecker.h"
 #include "storm-parsers/api/storm-parsers.h"
 
 namespace {
@@ -72,17 +71,6 @@ namespace {
             return boost::get<double>(results[0]);
         }
 
-        storm::solver::SmtSolver::CheckResult analyzeSMT(std::string const &file) {
-            std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
-            EXPECT_TRUE(storm::api::isWellFormed(*dft));
-            storm::modelchecker::DFTASFChecker smtChecker(*dft);
-            smtChecker.convert();
-            smtChecker.toSolver();
-            std::vector<storm::solver::SmtSolver::CheckResult> results;
-
-            return smtChecker.checkTleNeverFailed();
-        }
-
         double analyzeReliability(std::string const &file, double bound) {
             std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
             EXPECT_TRUE(storm::api::isWellFormed(*dft));
@@ -211,11 +199,4 @@ namespace {
         double result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1.0);
         EXPECT_FLOAT_EQ(result, 0.00021997582);
     }
-
-    TYPED_TEST(DftModelCheckerTest, SmtTest) {
-        storm::solver::SmtSolver::CheckResult result = this->analyzeSMT(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
-        EXPECT_EQ(result, storm::solver::SmtSolver::CheckResult::Unsat);
-        result = this->analyzeSMT(STORM_TEST_RESOURCES_DIR "/dft/pand.dft");
-        EXPECT_EQ(result, storm::solver::SmtSolver::CheckResult::Sat);
-    }
 }
diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp
new file mode 100644
index 000000000..ac350b3d5
--- /dev/null
+++ b/src/test/storm-dft/api/DftSmtTest.cpp
@@ -0,0 +1,26 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "storm-dft/api/storm-dft.h"
+
+namespace {
+    TEST(DftSmtTest, AndTest) {
+        std::shared_ptr<storm::storage::DFT<double>> dft =
+                storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
+        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        storm::modelchecker::DFTASFChecker smtChecker(*dft);
+        smtChecker.convert();
+        smtChecker.toSolver();
+        EXPECT_EQ(smtChecker.checkTleNeverFailed(), storm::solver::SmtSolver::CheckResult::Unsat);
+    }
+
+    TEST(DftSmtTest, PandTest) {
+        std::shared_ptr<storm::storage::DFT<double>> dft =
+                storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/pand.dft");
+        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        storm::modelchecker::DFTASFChecker smtChecker(*dft);
+        smtChecker.convert();
+        smtChecker.toSolver();
+        EXPECT_EQ(smtChecker.checkTleNeverFailed(), storm::solver::SmtSolver::CheckResult::Sat);
+    }
+}
\ No newline at end of file