summaryrefslogtreecommitdiff
path: root/src/lib
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2021-04-21 10:21:34 -0700
committerGitHub <noreply@github.com>2021-04-21 10:21:34 -0700
commitae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 (patch)
treea7c2ab8013f46dbea75fcd6e7da3fb83e2012b2f /src/lib
parent86aa9bc35ba9dc9a57913a2ffc71619c7657cc35 (diff)
Goodbye CVC4, hello cvc5! (#6371)
This commits changes the build system to cvc5 and removes the remaining occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
Diffstat (limited to 'src/lib')
-rw-r--r--src/lib/ffs.h2
-rw-r--r--src/lib/replacements.h12
2 files changed, 8 insertions, 6 deletions
diff --git a/src/lib/ffs.h b/src/lib/ffs.h
index c9ad5422e..eb66e4172 100644
--- a/src/lib/ffs.h
+++ b/src/lib/ffs.h
@@ -19,7 +19,7 @@
#define CVC5__LIB__FFS_H
//We include this for HAVE_FFS
-#include "cvc4autoconfig.h"
+#include "base/cvc5config.h"
#ifdef HAVE_FFS
diff --git a/src/lib/replacements.h b/src/lib/replacements.h
index ad868d7c6..26749daf6 100644
--- a/src/lib/replacements.h
+++ b/src/lib/replacements.h
@@ -16,17 +16,19 @@
#ifndef CVC5__LIB__REPLACEMENTS_H
#define CVC5__LIB__REPLACEMENTS_H
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
+#if (defined(__BUILDING_CVC5LIB) || defined(__BUILDING_CVC5LIB_UNIT_TEST)) \
+ && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
#include "cvc5_private.h"
#else
-# if defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST)
+#if defined(__BUILDING_CVC5PARSERLIB) \
+ || defined(__BUILDING_CVC5PARSERLIB_UNIT_TEST)
#include "cvc5parser_private.h"
# else
-#if defined(__BUILDING_CVC4DRIVER) || defined(__BUILDING_CVC5_SYSTEM_TEST) \
+#if defined(__BUILDING_CVC5DRIVER) || defined(__BUILDING_CVC5_SYSTEM_TEST) \
|| defined(__BUILDING_STATISTICS_FOR_EXPORT)
-# include "cvc4autoconfig.h"
+#include "base/cvc5config.h"
# else
-# error Must be building libcvc4 or libcvc4parser to use replacement functions. This is because replacement function headers should never be publicly-depended upon, as they should not be installed on user machines with 'make install'.
+# error Must be building libcvc5 or libcvc5parser to use replacement functions. This is because replacement function headers should never be publicly-depended upon, as they should not be installed on user machines with 'make install'.
# endif
# endif
#endif
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback