automatic import of cvc5HEADmasterf38f37

8 files changed, 468 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
index e69de29..01793ac 100644
--- a/.gitignore
+++ b/.gitignore
@@ -0,0 +1,2 @@
+/a04093e60036b83681c6f2cf5cca42bb631b6ce4.zip
+/cvc5-1.0.5.tar.gz
diff --git a/cvc5-antlr3.patch b/cvc5-antlr3.patch
new file mode 100644
index 0000000..31f4f3b
--- /dev/null
+++ b/cvc5-antlr3.patch
@@ -0,0 +1,44 @@
+--- cvc5-cvc5-1.0.5/cmake/FindANTLR3.cmake.orig	2023-03-13 10:15:58.000000000 -0600
++++ cvc5-cvc5-1.0.5/cmake/FindANTLR3.cmake	2023-07-14 13:38:14.961596481 -0600
+@@ -18,12 +18,14 @@
+ 
+ include(deps-helper)
+ 
+-find_file(ANTLR3_JAR NAMES antlr-3.4-complete.jar PATH_SUFFIXES share/java/)
++find_file(ANTLR3_JAR NAMES antlr3.jar PATH_SUFFIXES share/java/)
++find_file(ANTLR3_RUNTIME_JAR NAMES antlr3-runtime.jar PATH_SUFFIXES share/java/)
++find_file(ST4_JAR NAMES ST4.jar PATH_SUFFIXES share/java/stringtemplate4/)
+ find_path(ANTLR3_INCLUDE_DIR NAMES antlr3.h)
+ find_library(ANTLR3_LIBRARIES NAMES antlr3c)
+ 
+ set(ANTLR3_FOUND_SYSTEM FALSE)
+-if(ANTLR3_JAR AND ANTLR3_INCLUDE_DIR AND ANTLR3_LIBRARIES)
++if(ANTLR3_JAR AND ANTLR3_RUNTIME_JAR AND ST4_JAR AND ANTLR3_INCLUDE_DIR AND ANTLR3_LIBRARIES)
+     set(ANTLR3_FOUND_SYSTEM TRUE)
+ 
+     # Parse ANTLR3 version
+@@ -154,7 +156,7 @@ set(ANTLR3_FOUND TRUE)
+ # This may not be a single binary: the EP has a whole commandline
+ # We thus do not make this an executable target.
+ # Just call ${ANTLR3_COMMAND} instead.
+-set(ANTLR3_COMMAND ${Java_JAVA_EXECUTABLE} -cp "${ANTLR3_JAR}" org.antlr.Tool
++set(ANTLR3_COMMAND ${Java_JAVA_EXECUTABLE} -cp "${ANTLR3_JAR}:${ANTLR3_RUNTIME_JAR}:${ST4_JAR}" org.antlr.Tool
+     CACHE STRING "run ANTLR3" FORCE)
+ 
+ add_library(ANTLR3 STATIC IMPORTED GLOBAL)
+@@ -172,11 +174,15 @@ mark_as_advanced(ANTLR3_FOUND)
+ mark_as_advanced(ANTLR3_FOUND_SYSTEM)
+ mark_as_advanced(ANTLR3_INCLUDE_DIR)
+ mark_as_advanced(ANTLR3_JAR)
++mark_as_advanced(ANTLR3_RUNTIME_JAR)
++mark_as_advanced(ST4_JAR)
+ mark_as_advanced(ANTLR3_LIBRARIES)
+ 
+ if(ANTLR3_FOUND_SYSTEM)
+     message(STATUS "Found ANTLR3 runtime: ${ANTLR3_LIBRARIES}")
+     message(STATUS "Found ANTLR3 JAR: ${ANTLR3_JAR}")
++    message(STATUS "Found ANTLR3 Runtime JAR: ${ANTLR3_RUNTIME_JAR}")
++    message(STATUS "Found ST4 JAR: ${ST4_JAR}")
+ else()
+     message(STATUS "Building ANTLR3 runtime: ${ANTLR3_LIBRARIES}")
+     message(STATUS "Downloading ANTLR3 JAR: ${ANTLR3_JAR}")
diff --git a/cvc5-do-not-use-gold.patch b/cvc5-do-not-use-gold.patch
new file mode 100644
index 0000000..909898d
--- /dev/null
+++ b/cvc5-do-not-use-gold.patch
@@ -0,0 +1,22 @@
+--- cvc5-cvc5-1.0.5/CMakeLists.txt.orig	2023-07-14 13:37:21.195405688 -0600
++++ cvc5-cvc5-1.0.5/CMakeLists.txt	2023-07-14 13:38:52.441032407 -0600
+@@ -230,19 +230,6 @@ if (WIN32)
+ endif ()
+ 
+ #-----------------------------------------------------------------------------#
+-# Use ld.gold if available
+-
+-execute_process(COMMAND ${CMAKE_C_COMPILER}
+-                -fuse-ld=gold
+-                -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_VERSION)
+-if ("${LD_VERSION}" MATCHES "GNU gold")
+-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -fuse-ld=gold")
+-  string(APPEND CMAKE_SHARED_LINKER_FLAGS " -fuse-ld=gold")
+-  string(APPEND CMAKE_MODULE_LINKER_FLAGS " -fuse-ld=gold")
+-  message(STATUS "Using GNU gold linker.")
+-endif ()
+-
+-#-----------------------------------------------------------------------------#
+ # Use interprocedural optimization if requested
+ 
+ if(ENABLE_IPO)
diff --git a/cvc5-flags.patch b/cvc5-flags.patch
new file mode 100644
index 0000000..10450ca
--- /dev/null
+++ b/cvc5-flags.patch
@@ -0,0 +1,81 @@
+--- cvc5-cvc5-1.0.5/cmake/ConfigProduction.cmake.orig	2023-03-13 10:15:58.000000000 -0600
++++ cvc5-cvc5-1.0.5/cmake/ConfigProduction.cmake	2023-07-14 13:37:21.194405703 -0600
+@@ -12,7 +12,7 @@
+ ##
+ 
+ # OPTLEVEL=3
+-set(OPTIMIZATION_LEVEL 3)
++set(OPTIMIZATION_LEVEL 2)
+ # enable_debug_symbols=no
+ cvc5_set_option(ENABLE_DEBUG_SYMBOLS OFF)
+ # enable_statistics=yes
+--- cvc5-cvc5-1.0.5/cmake/FindCaDiCaL.cmake.orig	2023-03-13 10:15:58.000000000 -0600
++++ cvc5-cvc5-1.0.5/cmake/FindCaDiCaL.cmake	2023-07-14 13:37:21.195405688 -0600
+@@ -53,7 +53,7 @@ if(NOT CaDiCaL_FOUND_SYSTEM)
+   # avoid configure script and instantiate the makefile manually the configure
+   # scripts unnecessarily fails for cross compilation thus we do the bare
+   # minimum from the configure script here
+-  set(CXXFLAGS "-fPIC -O3 -DNDEBUG -DQUIET -std=c++11")
++  set(CXXFLAGS "-fPIC -O2 -DNDEBUG -DQUIET -std=c++11")
+   if(CMAKE_CROSSCOMPILING_MACOS)
+     set(CXXFLAGS "${CXXFLAGS} -arch ${CMAKE_OSX_ARCHITECTURES}")
+   endif()
+--- cvc5-cvc5-1.0.5/CMakeLists.txt.orig	2023-03-13 10:15:58.000000000 -0600
++++ cvc5-cvc5-1.0.5/CMakeLists.txt	2023-07-14 13:37:21.195405688 -0600
+@@ -158,7 +158,7 @@ endif()
+ #-----------------------------------------------------------------------------#
+ # Internal cmake variables
+ 
+-set(OPTIMIZATION_LEVEL 3)
++set(OPTIMIZATION_LEVEL 2)
+ set(GPL_LIBS "")
+ 
+ #-----------------------------------------------------------------------------#
+--- cvc5-cvc5-1.0.5/src/api/python/CMakeLists.txt.orig	2023-03-13 10:15:58.000000000 -0600
++++ cvc5-cvc5-1.0.5/src/api/python/CMakeLists.txt	2023-07-14 13:37:21.195405688 -0600
+@@ -143,10 +143,6 @@ target_link_libraries(cvc5_python_base c
+ 
+ # Disable -Werror and other warnings for code generated by Cython.
+ set(PY_SRC_FLAGS "")
+-check_cxx_compiler_flag("-Werror" HAVE_CXX_FLAGWerror)
+-if(HAVE_CXX_FLAGWerror)
+-  set(PY_SRC_FLAGS "${PY_SRC_FLAGS} -Wno-error")
+-endif()
+ check_cxx_compiler_flag("-Wshadow" HAVE_CXX_FLAGWshadow)
+ if(HAVE_CXX_FLAGWshadow)
+   set(PY_SRC_FLAGS "${PY_SRC_FLAGS} -Wno-shadow")
+--- cvc5-cvc5-1.0.5/src/parser/CMakeLists.txt.orig	2023-03-13 10:15:58.000000000 -0600
++++ cvc5-cvc5-1.0.5/src/parser/CMakeLists.txt	2023-07-14 13:37:21.195405688 -0600
+@@ -116,17 +116,8 @@ if(WIN32)
+   set(FLEX_INCLUDE_DIRS ${CMAKE_CURRENT_BINARY_DIR}/flex)
+ endif()
+ 
+-# We don't want to enable -Wall for code generated by Flex.
+ set(gen_src_files ${CMAKE_CURRENT_BINARY_DIR}/smt2/smt2_lexer.cpp)
+ set(GEN_SRC_FLAGS "")
+-check_cxx_compiler_flag("-Wall" HAVE_CXX_FLAGWall)
+-if(HAVE_CXX_FLAGWall)
+-  set(GEN_SRC_FLAGS "${GEN_SRC_FLAGS} -Wno-all")
+-endif()
+-check_cxx_compiler_flag("-Werror" HAVE_CXX_FLAGWerror)
+-if(HAVE_CXX_FLAGWerror)
+-  set(GEN_SRC_FLAGS "${GEN_SRC_FLAGS} -Wno-error")
+-endif()
+ set_source_files_properties(
+   ${gen_src_files} PROPERTIES COMPILE_FLAGS "${GEN_SRC_FLAGS}")
+ # Add generated source files to the parser source files
+@@ -166,14 +157,6 @@ foreach(lang Smt2 Tptp)
+ 
+   # We don't want to enable -Wall for code generated by ANTLR.
+   set(GEN_SRC_FLAGS "")
+-  check_cxx_compiler_flag("-Wall" HAVE_CXX_FLAGWall)
+-  if(HAVE_CXX_FLAGWall)
+-    set(GEN_SRC_FLAGS "${GEN_SRC_FLAGS} -Wno-all")
+-  endif()
+-  check_cxx_compiler_flag("-Werror" HAVE_CXX_FLAGWerror)
+-  if(HAVE_CXX_FLAGWerror)
+-    set(GEN_SRC_FLAGS "${GEN_SRC_FLAGS} -Wno-error")
+-  endif()
+   set_source_files_properties(
+     ${gen_src_files} PROPERTIES COMPILE_FLAGS "${GEN_SRC_FLAGS}")
+ 
diff --git a/cvc5-rpath.patch b/cvc5-rpath.patch
new file mode 100644
index 0000000..30809f4
--- /dev/null
+++ b/cvc5-rpath.patch
@@ -0,0 +1,27 @@
+--- cvc5-cvc5-1.0.5/CMakeLists.txt.orig	2023-07-14 13:38:52.441032407 -0600
++++ cvc5-cvc5-1.0.5/CMakeLists.txt	2023-07-14 13:39:28.449490458 -0600
+@@ -248,24 +248,6 @@ endif()
+ #-----------------------------------------------------------------------------#
+ # Shared/static libraries
+ 
+-# Embed the installation prefix as an RPATH in the executable such that the
+-# linker can find our libraries (such as libcvc5parser) when executing the
+-# cvc5 binary. This is for example useful when installing cvc5 with a custom
+-# prefix on macOS (e.g. when using homebrew in a non-standard directory). If
+-# we do not set this option, then the linker will not be able to find the
+-# required libraries when trying to run cvc5.
+-#
+-# Also embed the installation prefix of the installed contrib libraries as an
+-# RPATH. This allows to install a dynamically linked binary that depends on
+-# dynamically linked libraries. This is dangerous, as the installed binary
+-# breaks if the contrib library is removed or changes in other ways, we thus
+-# print a big warning and only allow if installing to a custom installation
+-# prefix.
+-#
+-# More information on RPATH in CMake:
+-# https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling
+-set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR};${PROJECT_SOURCE_DIR}/deps/install/lib")
+-
+ # Set visibility to default if unit tests are enabled. If unit tests are
+ # enabled, we also check if we can execute white box unit tests (some versions
+ # of Clang have issues with the required flag).
diff --git a/cvc5-toml.patch b/cvc5-toml.patch
new file mode 100644
index 0000000..3087a1b
--- /dev/null
+++ b/cvc5-toml.patch
@@ -0,0 +1,50 @@
+--- cvc5-cvc5-1.0.5/INSTALL.rst.orig	2023-03-13 10:15:58.000000000 -0600
++++ cvc5-cvc5-1.0.5/INSTALL.rst	2023-07-14 13:39:57.097059304 -0600
+@@ -118,8 +118,8 @@ versions; more recent versions should be
+ - `GNU C and C++ (gcc and g++, >= 7) <https://gcc.gnu.org>`_
+   or `Clang (>= 5) <https://clang.llvm.org>`_
+ - `CMake >= 3.9 <https://cmake.org>`_
+-- `Python >= 3.6 <https://www.python.org>`_
+-  + module `toml <https://pypi.org/project/toml/>`_
++- `Python >= 3.6 and <= 3.10 <https://www.python.org>`_
++  + module `tomli <https://pypi.org/project/tomli/>`_
+ - `GMP v6.1 (GNU Multi-Precision arithmetic library) <https://gmplib.org>`_
+ - `ANTLR 3.4 <http://www.antlr3.org/>`_
+ - `CaDiCaL (SAT solver) <https://github.com/arminbiere/cadical>`_
+--- cvc5-cvc5-1.0.5/src/CMakeLists.txt.orig	2023-03-13 10:15:58.000000000 -0600
++++ cvc5-cvc5-1.0.5/src/CMakeLists.txt	2023-07-14 13:39:57.097059304 -0600
+@@ -1251,7 +1251,9 @@ include_directories(. ${CMAKE_CURRENT_BI
+ #-----------------------------------------------------------------------------#
+ # Take care of options
+ 
+-check_python_module("toml")
++if (Python_VERSION VERSION_LESS "3.11.0")
++  check_python_module("tomli")
++endif()
+ 
+ set(options_toml_files
+   options/arith_options.toml
+--- cvc5-cvc5-1.0.5/src/options/mkoptions.py.orig	2023-03-13 10:15:58.000000000 -0600
++++ cvc5-cvc5-1.0.5/src/options/mkoptions.py	2023-07-14 13:39:57.098059289 -0600
+@@ -50,7 +50,10 @@ import os
+ import re
+ import sys
+ import textwrap
+-import toml
++try:
++    import tomllib
++except ImportError:
++    import tomli as tomllib
+ 
+ ### Allowed attributes for module/option
+ 
+@@ -1162,7 +1165,8 @@ def mkoptions_main():
+     checker = Checker()
+     modules = []
+     for filename in filenames:
+-        data = toml.load(filename)
++        with open(filename, "rb") as f:
++            data = tomllib.load(f)
+         module = checker.check_module(data, filename)
+         if 'option' in data:
+             module.options = sorted(
diff --git a/cvc5.spec b/cvc5.spec
new file mode 100644
index 0000000..944f26a
--- /dev/null
+++ b/cvc5.spec
@@ -0,0 +1,240 @@
+# CVC5 wants a modified glpk (glpk-cut-log), unavailable in Fedora.  Therefore,
+# we currently build without glpk support.
+
+# The cvc5_pythonic_api project needs cvc5 to build, and cvc5 needs
+# cvc5_pythonic_api to build.  See cmake/FindCVC5PythonicAPI.cmake for the git
+# commit needed by this version of cvc5.
+%global pcommit a04093e60036b83681c6f2cf5cca42bb631b6ce4
+
+Name:           cvc5
+Version:        1.0.5
+Release:        %autorelease
+Summary:        Automatic theorem prover for SMT problems
+
+# BSD-3-Clause: the project as a whole, including cvc5_pythonic_api
+# MIT: the bundled version of minisat2 in src/prop/minisat, and the
+#      cvc5_pythonic_api code derived from Z3
+License:        BSD-3-Clause AND MIT
+URL:            https://cvc5.github.io/
+Source0:        https://github.com/cvc5/cvc5/archive/%{name}-%{version}.tar.gz
+Source1:        https://github.com/cvc5/cvc5_pythonic_api/archive/%{pcommit}/%{pcommit}.zip
+# Do not override Fedora flags
+Patch0:         %{name}-flags.patch
+# Adapt to the way ANTLR3 is packaged in Fedora
+Patch1:         %{name}-antlr3.patch
+# Just use the default linker specified by the distro. ld.gold was the
+# new kid on the block a while ago, primarily offering higher link
+# speeds. But it has aged, and has less features than ld.bfd. Let's
+# use ld.bfd so that package notes work without workarounds.
+Patch2:         %{name}-do-not-use-gold.patch
+# Do not add rpaths to libraries and executables
+Patch3:         %{name}-rpath.patch
+# Use tomllib instead of the deprecated toml package
+Patch4:         %{name}-toml.patch
+
+# ANTLR 3 is not available on i686
+# See https://fedoraproject.org/wiki/Changes/Drop_i686_JDKs
+ExclusiveArch:  %{java_arches}
+
+BuildRequires:  abc-devel
+BuildRequires:  antlr3-C-devel
+BuildRequires:  antlr3-tool
+BuildRequires:  cadical
+BuildRequires:  cadical-devel
+BuildRequires:  chrpath
+BuildRequires:  cmake
+BuildRequires:  cmake(cryptominisat5)
+BuildRequires:  cocoalib-devel
+BuildRequires:  drat2er-devel
+BuildRequires:  drat-trim-devel
+BuildRequires:  flex
+BuildRequires:  gcc-c++
+BuildRequires:  git-core
+BuildRequires:  java-devel
+BuildRequires:  javapackages-tools
+BuildRequires:  kissat-devel
+BuildRequires:  lfsc-devel
+BuildRequires:  libfl-devel
+BuildRequires:  libpoly-devel
+BuildRequires:  pkgconfig(gmp)
+BuildRequires:  pkgconfig(libedit)
+BuildRequires:  pkgconfig(m4ri)
+BuildRequires:  pkgconfig(sqlite3)
+BuildRequires:  procps-ng
+BuildRequires:  python3-devel
+BuildRequires:  %{py3_dist cython}
+BuildRequires:  %{py3_dist pyparsing}
+BuildRequires:  %{py3_dist scikit-build}
+BuildRequires:  %{py3_dist setuptools}
+BuildRequires:  symfpu-devel
+
+Requires:       %{name}-libs%{?_isa} = %{version}-%{release}
+
+# Minisat has been altered for better integration with CVC5
+# See src/prop/minisat/CVC4-README
+Provides:       bundled(minisat2) = 2.2.0
+
+# This can be removed when F42 reaches EOL
+Obsoletes:      cvc4 < 1.9
+
+%description
+CVC5 is a tool for determining the satisfiability of a first order
+formula modulo a first order theory (or a combination of such theories).
+It is the fifth in the Cooperating Validity Checker family of tools
+(CVC, CVC Lite, CVC3, CVC4) but does not directly incorporate code from
+any previous version prior to CVC4.
+
+CVC5 is intended to be an open and extensible SMT engine.  It can be
+used as a stand-alone tool or as a library.  It has been designed to
+increase the performance and reduce the memory overhead of its
+predecessors.
+
+%package        devel
+Summary:        Headers and other files for developing with %{name}
+Requires:       %{name}-libs%{?_isa} = %{version}-%{release}
+Requires:       gmp-devel%{?_isa}
+Requires:       symfpu-devel%{?_isa}
+
+# This can be removed when F42 reaches EOL
+Obsoletes:      cvc4-devel < 1.9
+
+%description    devel
+Header files and library links for developing applications that use %{name}.
+
+%package        libs
+Summary:        Library containing an automatic theorem prover for SMT problems
+
+# This can be removed when F42 reaches EOL
+Obsoletes:      cvc4-libs < 1.9
+
+%description    libs
+Library containing the core of the %{name} automatic theorem prover for
+SMT problems.
+
+%package        java
+Summary:        Java interface to %{name}
+Requires:       %{name}-libs%{?_isa} = %{version}-%{release}
+Requires:       java-headless
+Requires:       javapackages-tools
+
+# This can be removed when F42 reaches EOL
+Obsoletes:      cvc4-java < 1.9
+
+%description    java
+Java interface to %{name}.
+
+%package     -n python3-cvc5
+Summary:        Python 3 interface to %{name}
+Requires:       %{name}-libs%{?_isa} = %{version}-%{release}
+
+# This can be removed when F42 reaches EOL
+Obsoletes:      cvc4-python3 < 1.9
+
+%description -n python3-cvc5
+Python 3 interface to %{name}.
+
+%prep
+%autosetup -n %{name}-%{name}-%{version} -p1
+mkdir -p %{_vpath_builddir}/deps/src/CVC5PythonicAPI
+cp -p %{SOURCE1} %{_vpath_builddir}/deps/src
+
+# FIXME: cmake fails to find a version in the Fedora cryptominisat package
+# cmake files, causing the version check to fail
+sed -i 's/ \${CryptoMiniSat_FIND_VERSION}//' cmake/FindCryptoMiniSat.cmake
+
+# The Fedora editline library does not need libbsd
+sed -i 's/ bsd//' cmake/FindEditline.cmake
+
+# Adapt to the way kissat is packaged for Fedora
+sed -i 's,#include <kissat/kissat\.h>,#include <kissat.h>,' src/prop/kissat.h
+sed -i 's,kissat/kissat\.h,kissat.h,' cmake/FindKissat.cmake
+
+# The header file installation script does not know about DESTDIR
+sed -i 's/\${CMAKE_INSTALL_PREFIX}/\\$ENV{DESTDIR}&/' src/CMakeLists.txt
+
+# Build the Java interface so that JDK 1.8 can use it
+sed -i 's/\${Java_JAVAC_EXECUTABLE}/& -source 1.8 -target 1.8/' \
+  src/api/java/CMakeLists.txt
+
+# Allow use of python 3.12
+sed -i 's/3\.10\.999/3.12.999/' cmake/Helpers.cmake
+
+%generate_buildrequires
+ln -s . src/api/python/cvc5
+ln -s . src/api/python/pythonic
+cd src/api/python
+sed -e 's/\${CVC5_VERSION}/%{version}/' \
+    -e "s,\${CMAKE_CURRENT_BINARY_DIR},$PWD," \
+    setup.py.in > setup.py
+%pyproject_buildrequires
+rm -fr cvc5 cvc5.egg-info pythonic setup.py
+
+%build
+export CFLAGS='%{build_cflags} -DABC_USE_STDINT_H -I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -I%{_includedir}/abc -I%{_includedir}/cryptominisat5'
+export CXXFLAGS="$CFLAGS"
+%cmake --debug-find \
+  -DBUILD_BINDINGS_JAVA:BOOL=ON \
+  -DBUILD_BINDINGS_PYTHON:BOOL=ON \
+  -DBUILD_DOCS:BOOL=OFF \
+  -DBUILD_SHARED_LIBS:BOOL=ON \
+  -DENABLE_GPL:BOOL=ON \
+  -DENABLE_IPO:BOOL=ON \
+  -DUSE_COCOA:BOOL=ON \
+  -DUSE_CRYPTOMINISAT:BOOL=ON \
+  -DUSE_EDITLINE:BOOL=ON \
+  -DUSE_KISSAT:BOOL=ON \
+  -DUSE_POLY:BOOL=ON
+%cmake_build
+
+# Build the python interface the Fedora way
+cd %{_vpath_builddir}/src/api/python
+%pyproject_wheel
+cd -
+
+%install
+%cmake_install
+
+# Link the JNI interface to where Fedora mandates it should go
+mkdir -p %{buildroot}%{_jnidir}/%{name}
+ln -s ../../%{_lib}/libcvc5jni.so %{buildroot}%{_jnidir}/%{name}
+
+# Install the python interface the Fedora way
+cd %{_vpath_builddir}/src/api/python
+%pyproject_install
+cd -
+
+# The python interface is incorrectly installed in the noarch directory
+if [ "%{_lib}" != "lib" ]; then
+  mv %{buildroot}%{_prefix}/lib/python* %{buildroot}%{_libdir}
+fi
+
+# FIXME: What is causing an rpath to be added in the first place?
+chrpath -d %{buildroot}%{python3_sitearch}/cvc5/*.so
+
+%files
+%doc AUTHORS NEWS.md README.md THANKS
+%{_bindir}/%{name}
+
+%files libs
+%license COPYING
+%{_libdir}/libcvc5.so.1
+%{_libdir}/libcvc5parser.so.1
+
+%files devel
+%{_includedir}/%{name}/
+%{_libdir}/libcvc5.so
+%{_libdir}/libcvc5parser.so
+%{_libdir}/cmake/%{name}/
+
+%files java
+%{_javadir}/cvc5.jar
+%{_javadir}/cvc5-%{version}.jar
+%{_jnidir}/%{name}/
+%{_libdir}/libcvc5jni.so
+
+%files -n python3-cvc5
+%{python3_sitearch}/cvc5/
+%{python3_sitearch}/cvc5-%{version}.dist-info/
+
+%changelog
+%autochangelog
diff --git a/sources b/sources
new file mode 100644
index 0000000..0373da8
--- /dev/null
+++ b/sources
@@ -0,0 +1,2 @@
+48797f3718b3124dc6b121bcb80c20da  a04093e60036b83681c6f2cf5cca42bb631b6ce4.zip
+57717622ec2afbc8664b6865c4142833  cvc5-1.0.5.tar.gz