diff --git a/CMakeLists.txt b/CMakeLists.txt
index a5689009e..7aa6647b2 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -51,8 +51,26 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
 include(EthOptions)
 configure_project(TESTS)
 
+find_package(Z3 4.6.0)
+if (${Z3_FOUND})
+  add_definitions(-DHAVE_Z3)
+  message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
+endif()
+
+find_package(CVC4 QUIET)
+if (${CVC4_FOUND})
+  add_definitions(-DHAVE_CVC4)
+  message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.")
+endif()
+
+if (NOT (${Z3_FOUND} OR ${CVC4_FOUND}))
+  message("No SMT solver found (or it has been forcefully disabled). Optional SMT checking will not be available.\
+  \nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).")
+endif()
+
 add_subdirectory(libsolutil)
 add_subdirectory(liblangutil)
+add_subdirectory(libsmtutil)
 add_subdirectory(libevmasm)
 add_subdirectory(libyul)
 add_subdirectory(libsolidity)
diff --git a/libsolidity/formal/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp
similarity index 98%
rename from libsolidity/formal/CHCSmtLib2Interface.cpp
rename to libsmtutil/CHCSmtLib2Interface.cpp
index 4b52b7d5a..d5895fc69 100644
--- a/libsolidity/formal/CHCSmtLib2Interface.cpp
+++ b/libsmtutil/CHCSmtLib2Interface.cpp
@@ -15,7 +15,7 @@
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
 
-#include <libsolidity/formal/CHCSmtLib2Interface.h>
+#include <libsmtutil/CHCSmtLib2Interface.h>
 
 #include <libsolutil/Keccak256.h>
 
diff --git a/libsolidity/formal/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h
similarity index 95%
rename from libsolidity/formal/CHCSmtLib2Interface.h
rename to libsmtutil/CHCSmtLib2Interface.h
index d184cd9a4..9fd1489a4 100644
--- a/libsolidity/formal/CHCSmtLib2Interface.h
+++ b/libsmtutil/CHCSmtLib2Interface.h
@@ -21,9 +21,9 @@
 
 #pragma once
 
-#include <libsolidity/formal/CHCSolverInterface.h>
+#include <libsmtutil/CHCSolverInterface.h>
 
-#include <libsolidity/formal/SMTLib2Interface.h>
+#include <libsmtutil/SMTLib2Interface.h>
 
 namespace solidity::frontend::smt
 {
diff --git a/libsolidity/formal/CHCSolverInterface.h b/libsmtutil/CHCSolverInterface.h
similarity index 96%
rename from libsolidity/formal/CHCSolverInterface.h
rename to libsmtutil/CHCSolverInterface.h
index 91198e1a8..588e42ce1 100644
--- a/libsolidity/formal/CHCSolverInterface.h
+++ b/libsmtutil/CHCSolverInterface.h
@@ -21,7 +21,7 @@
 
 #pragma once
 
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsmtutil/SolverInterface.h>
 
 namespace solidity::frontend::smt
 {
diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt
new file mode 100644
index 000000000..d5df3633f
--- /dev/null
+++ b/libsmtutil/CMakeLists.txt
@@ -0,0 +1,34 @@
+set(sources
+	CHCSmtLib2Interface.cpp
+	CHCSmtLib2Interface.h
+	SMTLib2Interface.cpp
+	SMTLib2Interface.h
+	SMTPortfolio.cpp
+	SMTPortfolio.h
+	SolverInterface.h
+	Sorts.cpp
+	Sorts.h
+)
+
+if (${Z3_FOUND})
+  set(z3_SRCS Z3Interface.cpp Z3Interface.h Z3CHCInterface.cpp Z3CHCInterface.h)
+else()
+  set(z3_SRCS)
+endif()
+
+if (${CVC4_FOUND})
+  set(cvc4_SRCS CVC4Interface.cpp CVC4Interface.h)
+else()
+  set(cvc4_SRCS)
+endif()
+
+add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS})
+target_link_libraries(smtutil PUBLIC langutil solutil Boost::boost)
+
+if (${Z3_FOUND})
+  target_link_libraries(smtutil PUBLIC z3::libz3)
+endif()
+
+if (${CVC4_FOUND})
+  target_link_libraries(smtutil PUBLIC CVC4::CVC4)
+endif()
diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp
similarity index 99%
rename from libsolidity/formal/CVC4Interface.cpp
rename to libsmtutil/CVC4Interface.cpp
index 86688e0b1..71ab81f51 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsmtutil/CVC4Interface.cpp
@@ -15,7 +15,7 @@
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
 
-#include <libsolidity/formal/CVC4Interface.h>
+#include <libsmtutil/CVC4Interface.h>
 
 #include <liblangutil/Exceptions.h>
 #include <libsolutil/CommonIO.h>
diff --git a/libsolidity/formal/CVC4Interface.h b/libsmtutil/CVC4Interface.h
similarity index 97%
rename from libsolidity/formal/CVC4Interface.h
rename to libsmtutil/CVC4Interface.h
index b5c2a3fd6..2399dc453 100644
--- a/libsolidity/formal/CVC4Interface.h
+++ b/libsmtutil/CVC4Interface.h
@@ -17,7 +17,7 @@
 
 #pragma once
 
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsmtutil/SolverInterface.h>
 #include <boost/noncopyable.hpp>
 
 #if defined(__GLIBC__)
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp
similarity index 99%
rename from libsolidity/formal/SMTLib2Interface.cpp
rename to libsmtutil/SMTLib2Interface.cpp
index 97ccc2c91..081d87f61 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsmtutil/SMTLib2Interface.cpp
@@ -15,7 +15,7 @@
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
 
-#include <libsolidity/formal/SMTLib2Interface.h>
+#include <libsmtutil/SMTLib2Interface.h>
 
 #include <libsolutil/Keccak256.h>
 
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsmtutil/SMTLib2Interface.h
similarity index 98%
rename from libsolidity/formal/SMTLib2Interface.h
rename to libsmtutil/SMTLib2Interface.h
index 5310f7e95..1acbcde2c 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsmtutil/SMTLib2Interface.h
@@ -17,7 +17,7 @@
 
 #pragma once
 
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsmtutil/SolverInterface.h>
 
 #include <libsolidity/interface/ReadFile.h>
 #include <liblangutil/Exceptions.h>
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp
similarity index 96%
rename from libsolidity/formal/SMTPortfolio.cpp
rename to libsmtutil/SMTPortfolio.cpp
index 2ce698bdf..67cb3803c 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsmtutil/SMTPortfolio.cpp
@@ -15,15 +15,15 @@
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
 
-#include <libsolidity/formal/SMTPortfolio.h>
+#include <libsmtutil/SMTPortfolio.h>
 
 #ifdef HAVE_Z3
-#include <libsolidity/formal/Z3Interface.h>
+#include <libsmtutil/Z3Interface.h>
 #endif
 #ifdef HAVE_CVC4
-#include <libsolidity/formal/CVC4Interface.h>
+#include <libsmtutil/CVC4Interface.h>
 #endif
-#include <libsolidity/formal/SMTLib2Interface.h>
+#include <libsmtutil/SMTLib2Interface.h>
 
 using namespace std;
 using namespace solidity;
diff --git a/libsolidity/formal/SMTPortfolio.h b/libsmtutil/SMTPortfolio.h
similarity index 97%
rename from libsolidity/formal/SMTPortfolio.h
rename to libsmtutil/SMTPortfolio.h
index 7799f2268..1ffce37ee 100644
--- a/libsolidity/formal/SMTPortfolio.h
+++ b/libsmtutil/SMTPortfolio.h
@@ -18,7 +18,7 @@
 #pragma once
 
 
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsmtutil/SolverInterface.h>
 #include <libsolidity/interface/ReadFile.h>
 #include <libsolutil/FixedHash.h>
 
diff --git a/libsolidity/formal/SolverInterface.h b/libsmtutil/SolverInterface.h
similarity index 99%
rename from libsolidity/formal/SolverInterface.h
rename to libsmtutil/SolverInterface.h
index 4532c1b3e..078eaef73 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsmtutil/SolverInterface.h
@@ -17,7 +17,7 @@
 
 #pragma once
 
-#include <libsolidity/formal/Sorts.h>
+#include <libsmtutil/Sorts.h>
 
 #include <libsolidity/ast/Types.h>
 #include <libsolidity/interface/ReadFile.h>
diff --git a/libsolidity/formal/Sorts.cpp b/libsmtutil/Sorts.cpp
similarity index 95%
rename from libsolidity/formal/Sorts.cpp
rename to libsmtutil/Sorts.cpp
index 195048e56..dba0dc4b7 100644
--- a/libsolidity/formal/Sorts.cpp
+++ b/libsmtutil/Sorts.cpp
@@ -16,7 +16,7 @@
 */
 
 
-#include <libsolidity/formal/Sorts.h>
+#include <libsmtutil/Sorts.h>
 
 using namespace std;
 
diff --git a/libsolidity/formal/Sorts.h b/libsmtutil/Sorts.h
similarity index 100%
rename from libsolidity/formal/Sorts.h
rename to libsmtutil/Sorts.h
diff --git a/libsolidity/formal/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp
similarity index 98%
rename from libsolidity/formal/Z3CHCInterface.cpp
rename to libsmtutil/Z3CHCInterface.cpp
index c64da2edc..3be40d396 100644
--- a/libsolidity/formal/Z3CHCInterface.cpp
+++ b/libsmtutil/Z3CHCInterface.cpp
@@ -15,7 +15,7 @@
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
 
-#include <libsolidity/formal/Z3CHCInterface.h>
+#include <libsmtutil/Z3CHCInterface.h>
 
 #include <liblangutil/Exceptions.h>
 #include <libsolutil/CommonIO.h>
diff --git a/libsolidity/formal/Z3CHCInterface.h b/libsmtutil/Z3CHCInterface.h
similarity index 93%
rename from libsolidity/formal/Z3CHCInterface.h
rename to libsmtutil/Z3CHCInterface.h
index a7b7d6aeb..bc0e6cf92 100644
--- a/libsolidity/formal/Z3CHCInterface.h
+++ b/libsmtutil/Z3CHCInterface.h
@@ -21,8 +21,8 @@
 
 #pragma once
 
-#include <libsolidity/formal/CHCSolverInterface.h>
-#include <libsolidity/formal/Z3Interface.h>
+#include <libsmtutil/CHCSolverInterface.h>
+#include <libsmtutil/Z3Interface.h>
 
 namespace solidity::frontend::smt
 {
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp
similarity index 99%
rename from libsolidity/formal/Z3Interface.cpp
rename to libsmtutil/Z3Interface.cpp
index d49314b6c..4303c76ac 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsmtutil/Z3Interface.cpp
@@ -15,7 +15,7 @@
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
 
-#include <libsolidity/formal/Z3Interface.h>
+#include <libsmtutil/Z3Interface.h>
 
 #include <liblangutil/Exceptions.h>
 #include <libsolutil/CommonIO.h>
diff --git a/libsolidity/formal/Z3Interface.h b/libsmtutil/Z3Interface.h
similarity index 97%
rename from libsolidity/formal/Z3Interface.h
rename to libsmtutil/Z3Interface.h
index 3791af4c5..282b87a09 100644
--- a/libsolidity/formal/Z3Interface.h
+++ b/libsmtutil/Z3Interface.h
@@ -17,7 +17,7 @@
 
 #pragma once
 
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsmtutil/SolverInterface.h>
 #include <boost/noncopyable.hpp>
 #include <z3++.h>
 
diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt
index 7b66e533e..8e930b6ab 100644
--- a/libsolidity/CMakeLists.txt
+++ b/libsolidity/CMakeLists.txt
@@ -94,22 +94,12 @@ set(sources
 	formal/BMC.h
 	formal/CHC.cpp
 	formal/CHC.h
-	formal/CHCSmtLib2Interface.cpp
-	formal/CHCSmtLib2Interface.h
-	formal/CHCSolverInterface.h
 	formal/EncodingContext.cpp
 	formal/EncodingContext.h
 	formal/ModelChecker.cpp
 	formal/ModelChecker.h
 	formal/SMTEncoder.cpp
 	formal/SMTEncoder.h
-	formal/SMTLib2Interface.cpp
-	formal/SMTLib2Interface.h
-	formal/SMTPortfolio.cpp
-	formal/SMTPortfolio.h
-	formal/SolverInterface.h
-	formal/Sorts.cpp
-	formal/Sorts.h
 	formal/SSAVariable.cpp
 	formal/SSAVariable.h
 	formal/SymbolicState.cpp
@@ -144,36 +134,6 @@ set(sources
 	parsing/Token.h
 )
 
-find_package(Z3 4.6.0)
-if (${Z3_FOUND})
-  add_definitions(-DHAVE_Z3)
-  message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
-  set(z3_SRCS formal/Z3Interface.cpp formal/Z3Interface.h formal/Z3CHCInterface.cpp formal/Z3CHCInterface.h)
-else()
-  set(z3_SRCS)
-endif()
+add_library(solidity ${sources})
+target_link_libraries(solidity PUBLIC yul evmasm langutil smtutil solutil Boost::boost)
 
-find_package(CVC4 QUIET)
-if (${CVC4_FOUND})
-  add_definitions(-DHAVE_CVC4)
-  message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.")
-  set(cvc4_SRCS formal/CVC4Interface.cpp formal/CVC4Interface.h)
-else()
-  set(cvc4_SRCS)
-endif()
-
-if (NOT (${Z3_FOUND} OR ${CVC4_FOUND}))
-  message("No SMT solver found (or it has been forcefully disabled). Optional SMT checking will not be available.\
-  \nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).")
-endif()
-
-add_library(solidity ${sources} ${z3_SRCS} ${cvc4_SRCS})
-target_link_libraries(solidity PUBLIC yul evmasm langutil solutil Boost::boost)
-
-if (${Z3_FOUND})
-  target_link_libraries(solidity PUBLIC z3::libz3)
-endif()
-
-if (${CVC4_FOUND})
-  target_link_libraries(solidity PUBLIC CVC4::CVC4)
-endif()
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index 952eb1c50..7c2bc4818 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -17,10 +17,11 @@
 
 #include <libsolidity/formal/BMC.h>
 
-#include <libsolidity/formal/SMTPortfolio.h>
 #include <libsolidity/formal/SymbolicState.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
+#include <libsmtutil/SMTPortfolio.h>
+
 using namespace std;
 using namespace solidity;
 using namespace solidity::util;
diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h
index 8b30f073d..16ef665c0 100644
--- a/libsolidity/formal/BMC.h
+++ b/libsolidity/formal/BMC.h
@@ -30,9 +30,10 @@
 
 #include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/SMTEncoder.h>
-#include <libsolidity/formal/SolverInterface.h>
 
 #include <libsolidity/interface/ReadFile.h>
+
+#include <libsmtutil/SolverInterface.h>
 #include <liblangutil/ErrorReporter.h>
 
 #include <set>
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index f30959972..9cc01e26e 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -17,16 +17,15 @@
 
 #include <libsolidity/formal/CHC.h>
 
-#include <libsolidity/formal/CHCSmtLib2Interface.h>
-
 #ifdef HAVE_Z3
-#include <libsolidity/formal/Z3CHCInterface.h>
+#include <libsmtutil/Z3CHCInterface.h>
 #endif
 
 #include <libsolidity/formal/SymbolicTypes.h>
 
 #include <libsolidity/ast/TypeProvider.h>
 
+#include <libsmtutil/CHCSmtLib2Interface.h>
 #include <libsolutil/Algorithms.h>
 
 using namespace std;
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
index 87f902732..9315da70f 100644
--- a/libsolidity/formal/CHC.h
+++ b/libsolidity/formal/CHC.h
@@ -32,10 +32,10 @@
 
 #include <libsolidity/formal/SMTEncoder.h>
 
-#include <libsolidity/formal/CHCSolverInterface.h>
-
 #include <libsolidity/interface/ReadFile.h>
 
+#include <libsmtutil/CHCSolverInterface.h>
+
 #include <set>
 
 namespace solidity::frontend
diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h
index d62de055d..e8cf48ed0 100644
--- a/libsolidity/formal/EncodingContext.h
+++ b/libsolidity/formal/EncodingContext.h
@@ -17,10 +17,11 @@
 
 #pragma once
 
-#include <libsolidity/formal/SolverInterface.h>
 #include <libsolidity/formal/SymbolicState.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 
+#include <libsmtutil/SolverInterface.h>
+
 #include <unordered_map>
 #include <set>
 
diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h
index 546f2df86..663bae869 100644
--- a/libsolidity/formal/ModelChecker.h
+++ b/libsolidity/formal/ModelChecker.h
@@ -25,9 +25,10 @@
 #include <libsolidity/formal/BMC.h>
 #include <libsolidity/formal/CHC.h>
 #include <libsolidity/formal/EncodingContext.h>
-#include <libsolidity/formal/SolverInterface.h>
 
 #include <libsolidity/interface/ReadFile.h>
+
+#include <libsmtutil/SolverInterface.h>
 #include <liblangutil/ErrorReporter.h>
 
 namespace solidity::langutil
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 44bec4d85..7a62199b2 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -18,10 +18,11 @@
 #include <libsolidity/formal/SMTEncoder.h>
 
 #include <libsolidity/ast/TypeProvider.h>
-#include <libsolidity/formal/SMTPortfolio.h>
 #include <libsolidity/formal/SymbolicState.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
+#include <libsmtutil/SMTPortfolio.h>
+
 #include <boost/range/adaptors.hpp>
 #include <boost/range/adaptor/reversed.hpp>
 
diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h
index 380bfda51..087ea9985 100644
--- a/libsolidity/formal/SymbolicState.h
+++ b/libsolidity/formal/SymbolicState.h
@@ -17,10 +17,11 @@
 
 #pragma once
 
-#include <libsolidity/formal/Sorts.h>
-#include <libsolidity/formal/SolverInterface.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 
+#include <libsmtutil/Sorts.h>
+#include <libsmtutil/SolverInterface.h>
+
 namespace solidity::frontend::smt
 {
 
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index 3f5379d9b..46d3520cf 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -17,10 +17,11 @@
 
 #pragma once
 
-#include <libsolidity/formal/SolverInterface.h>
 #include <libsolidity/formal/SSAVariable.h>
 #include <libsolidity/ast/Types.h>
 #include <libsolidity/ast/TypeProvider.h>
+
+#include <libsmtutil/SolverInterface.h>
 #include <memory>
 
 namespace solidity::frontend::smt
diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h
index 96dbc4f04..fbd32b382 100644
--- a/libsolidity/interface/CompilerStack.h
+++ b/libsolidity/interface/CompilerStack.h
@@ -27,7 +27,8 @@
 #include <libsolidity/interface/OptimiserSettings.h>
 #include <libsolidity/interface/Version.h>
 #include <libsolidity/interface/DebugSettings.h>
-#include <libsolidity/formal/SolverInterface.h>
+
+#include <libsmtutil/SolverInterface.h>
 
 #include <liblangutil/ErrorReporter.h>
 #include <liblangutil/EVMVersion.h>
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index 1834d3b30..6c6d12c1e 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -188,7 +188,7 @@ add_executable(soltest ${sources}
     ${libsolidity_util_sources}
     ${yul_phaser_sources}
 )
-target_link_libraries(soltest PRIVATE libsolc yul solidity yulInterpreter evmasm solutil Boost::boost Boost::filesystem Boost::program_options Boost::unit_test_framework evmc)
+target_link_libraries(soltest PRIVATE libsolc yul solidity yulInterpreter evmasm smtutil solutil Boost::boost Boost::filesystem Boost::program_options Boost::unit_test_framework evmc)
 
 
 # Special compilation flag for Visual Studio (version 2019 at least affected)
diff --git a/test/libsolidity/SMTCheckerTest.h b/test/libsolidity/SMTCheckerTest.h
index ad38af25c..674564f57 100644
--- a/test/libsolidity/SMTCheckerTest.h
+++ b/test/libsolidity/SMTCheckerTest.h
@@ -19,7 +19,7 @@
 
 #include <test/libsolidity/SyntaxTest.h>
 
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsmtutil/SolverInterface.h>
 
 #include <string>