4 files changed, 20 insertions, 3 deletions
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 7ceb64885..eb068152c 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -133,10 +133,10 @@ std::string Configuration::copyright() {
      << "See licenses/antlr3-LICENSE for copyright and licensing information."
      << "\n\n";
 
-  if (Configuration::isBuiltWithAbc()
-      || Configuration::isBuiltWithLfsc()
+  if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithLfsc()
       || Configuration::isBuiltWithCadical()
-      || Configuration::isBuiltWithCryptominisat())
+      || Configuration::isBuiltWithCryptominisat()
+      || Configuration::isBuiltWithSymFPU())
   {
     ss << "This version of CVC4 is linked against the following non-(L)GPL'ed\n"
        << "third party libraries.\n\n";
@@ -162,6 +162,12 @@ std::string Configuration::copyright() {
          << "  See https://github.com/msoos/cryptominisat for copyright "
          << "information.\n\n";
     }
+    if (Configuration::isBuiltWithSymFPU())
+    {
+      ss << "  SymFPU - The Symbolic Floating Point Unit\n"
+         << "  See https://github.com/martin-cs/symfpu/tree/CVC4 for copyright "
+         << "information.\n\n";
+    }
   }
 
   if (Configuration::isBuiltWithGmp())
@@ -256,6 +262,8 @@ bool Configuration::isBuiltWithLfsc() {
   return IS_LFSC_BUILD;
 }
 
+bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; }
+
 unsigned Configuration::getNumDebugTags() {
 #if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
   /* -1 because a NULL pointer is inserted as the last value */
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 897f234d7..f98111181 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -105,6 +105,8 @@ public:
 
   static bool isBuiltWithLfsc();
 
+  static bool isBuiltWithSymFPU();
+
   /* Return the number of debug tags */
   static unsigned getNumDebugTags();
   /* Return a sorted array of the debug tags name */
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index cf9117100..018c7f800 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -138,6 +138,12 @@ namespace CVC4 {
 #  define IS_READLINE_BUILD false
 #endif /* HAVE_LIBREADLINE */
 
+#ifdef CVC4_USE_SYMFPU
+#define IS_SYMFPU_BUILD true
+#else /* HAVE_SYMFPU_HEADERS */
+#define IS_SYMFPU_BUILD false
+#endif /* HAVE_SYMFPU_HEADERS */
+
 #if CVC4_GPL_DEPS
 #  define IS_GPL_BUILD true
 #else /* CVC4_GPL_DEPS */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 9b2eb1cb2..41378e245 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1693,6 +1693,7 @@ void OptionsHandler::showConfiguration(std::string option) {
   print_config_cond("gmp", Configuration::isBuiltWithGmp());
   print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
   print_config_cond("readline", Configuration::isBuiltWithReadline());
+  print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
   print_config_cond("tls", Configuration::isBuiltWithTlsSupport());
   
   exit(0);