diff --git a/cvc4-abc.patch b/cvc4-abc.patch deleted file mode 100644 index 9541634..0000000 --- a/cvc4-abc.patch +++ /dev/null @@ -1,54 +0,0 @@ ---- cmake/FindABC.cmake.orig 2019-04-09 10:14:31.000000000 -0600 -+++ cmake/FindABC.cmake 2019-04-16 16:01:44.519958231 -0600 -@@ -2,7 +2,6 @@ - # ABC_FOUND - system has ABC lib - # ABC_INCLUDE_DIR - the ABC include directory - # ABC_LIBRARIES - Libraries needed to use ABC --# ABC_ARCH_FLAGS - Platform specific compile flags - - - # Check default location of ABC built with contrib/get-abc. -@@ -14,28 +13,19 @@ endif() - # install rule. - find_path(ABC_INCLUDE_DIR - NAMES base/abc/abc.h -- PATHS ${ABC_HOME}/src -+ PATHS /usr/include/abc - NO_DEFAULT_PATH) - find_library(ABC_LIBRARIES - NAMES abc -- PATHS ${ABC_HOME} -- NO_DEFAULT_PATH) --find_program(ABC_ARCH_FLAGS_PROG -- NAMES arch_flags -- PATHS ${ABC_HOME} -+ PATHS /usr/lib64 /usr/lib - NO_DEFAULT_PATH) - --if(ABC_ARCH_FLAGS_PROG) -- execute_process(COMMAND ${ABC_ARCH_FLAGS_PROG} -- OUTPUT_VARIABLE ABC_ARCH_FLAGS) --endif() -- - include(FindPackageHandleStandardArgs) - find_package_handle_standard_args(ABC - DEFAULT_MSG -- ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS) -+ ABC_INCLUDE_DIR ABC_LIBRARIES) - --mark_as_advanced(ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS) -+mark_as_advanced(ABC_INCLUDE_DIR ABC_LIBRARIES) - if(ABC_LIBRARIES) - message(STATUS "Found ABC libs: ${ABC_LIBRARIES}") - endif() ---- CMakeLists.txt.orig 2019-04-09 10:14:31.000000000 -0600 -+++ CMakeLists.txt 2019-04-16 15:54:30.334111544 -0600 -@@ -379,7 +379,7 @@ endif() - if(USE_ABC) - set(ABC_HOME "${ABC_DIR}") - find_package(ABC REQUIRED) -- add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS}) -+ add_definitions(-DCVC4_USE_ABC) - endif() - - if(USE_CADICAL) diff --git a/cvc4-cryptominisat.patch b/cvc4-cryptominisat.patch index 33b43d5..b13316b 100644 --- a/cvc4-cryptominisat.patch +++ b/cvc4-cryptominisat.patch @@ -1,8 +1,8 @@ ---- src/prop/cryptominisat.cpp.orig 2019-04-09 10:14:31.000000000 -0600 -+++ src/prop/cryptominisat.cpp 2020-04-26 14:04:26.086833393 -0600 -@@ -68,15 +68,8 @@ CryptoMinisatSolver::CryptoMinisatSolver - d_okay(true), - d_statistics(registry, name) +--- src/prop/cryptominisat.cpp.orig 2020-06-19 10:59:27.000000000 -0600 ++++ src/prop/cryptominisat.cpp 2020-06-21 11:51:21.496211208 -0600 +@@ -73,15 +73,8 @@ CryptoMinisatSolver::CryptoMinisatSolver + + void CryptoMinisatSolver::init() { - d_true = newVar(); - d_false = newVar(); @@ -10,15 +10,15 @@ - std::vector clause(1); - clause[0] = CMSat::Lit(d_true, false); - d_solver->add_clause(clause); -- +- - clause[0] = CMSat::Lit(d_false, true); - d_solver->add_clause(clause); + d_true = undefSatVariable; + d_false = undefSatVariable; } - -@@ -154,10 +147,32 @@ SatVariable CryptoMinisatSolver::newVar + CryptoMinisatSolver::~CryptoMinisatSolver() {} +@@ -158,10 +151,32 @@ SatVariable CryptoMinisatSolver::newVar } SatVariable CryptoMinisatSolver::trueVar() { diff --git a/cvc4-drat.patch b/cvc4-drat.patch deleted file mode 100644 index 234068e..0000000 --- a/cvc4-drat.patch +++ /dev/null @@ -1,20 +0,0 @@ ---- proofs/signatures/drat.plf.orig 2019-04-09 10:14:31.000000000 -0600 -+++ proofs/signatures/drat.plf 2019-09-09 17:42:41.118932870 -0600 -@@ -322,7 +322,7 @@ - - - ; Do unit propagation on `f`, constructing a UP model for it. --(program build_up_model ((f cnf)) clause -+(program build_up_model ((f cnf)) UPConstructionResult - (match (unit_search f) - (USRBottom UPCRBottom) - (USRNoUnit (UPCRModel cln)) -@@ -335,7 +335,7 @@ - - ; Given some starting assignment (`up_model`), continue UP to construct a larger - ; model. --(program extend_up_model ((f cnf) (up_model clause)) clause -+(program extend_up_model ((f cnf) (up_model clause)) UPConstructionResult - (do (clause_into_global up_model) - (let result (build_up_model f) - (do (clause_undo_into_global up_model) diff --git a/cvc4-flags.patch b/cvc4-flags.patch index c26da0b..bb83c33 100644 --- a/cvc4-flags.patch +++ b/cvc4-flags.patch @@ -1,18 +1,16 @@ ---- cmake/ConfigProduction.cmake.orig 2019-04-09 10:14:31.000000000 -0600 -+++ cmake/ConfigProduction.cmake 2020-04-26 17:24:03.338855205 -0600 -@@ -1,7 +1,7 @@ +--- cmake/ConfigProduction.cmake.orig 2020-06-19 10:59:27.000000000 -0600 ++++ cmake/ConfigProduction.cmake 2020-06-21 11:47:20.134513759 -0600 +@@ -1,5 +1,5 @@ -# OPTLEVEL=3 -+# OPTLEVEL=2 - # enable_optimized=yes - cvc4_set_option(ENABLE_OPTIMIZED ON) -set(OPTIMIZATION_LEVEL 3) ++# OPTLEVEL=2 +set(OPTIMIZATION_LEVEL 2) # enable_debug_symbols=no cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF) # enable_statistics=yes ---- CMakeLists.txt.orig 2019-04-09 10:14:31.000000000 -0600 -+++ CMakeLists.txt 2020-04-26 17:23:30.427884359 -0600 -@@ -125,7 +125,7 @@ option(BUILD_BINDINGS_PYTHON "Build Pyth +--- CMakeLists.txt.orig 2020-06-19 10:59:27.000000000 -0600 ++++ CMakeLists.txt 2020-06-21 11:45:03.767689990 -0600 +@@ -175,7 +175,7 @@ option(BUILD_BINDINGS_PYTHON "Build Pyth #-----------------------------------------------------------------------------# # Internal cmake variables @@ -21,9 +19,9 @@ set(GPL_LIBS "") #-----------------------------------------------------------------------------# ---- src/parser/CMakeLists.txt.orig 2019-04-09 10:14:31.000000000 -0600 -+++ src/parser/CMakeLists.txt 2019-04-17 11:21:41.680050119 -0600 -@@ -81,10 +81,6 @@ foreach(lang Cvc Smt1 Smt2 Tptp) +--- src/parser/CMakeLists.txt.orig 2020-06-19 10:59:27.000000000 -0600 ++++ src/parser/CMakeLists.txt 2020-06-21 11:45:48.007632818 -0600 +@@ -81,10 +81,6 @@ foreach(lang Cvc Smt2 Tptp) set_source_files_properties(${gen_src_files} PROPERTIES LANGUAGE CXX) set_source_files_properties(${gen_src_files} PROPERTIES GENERATED TRUE) @@ -34,8 +32,8 @@ # Add generated source files to the parser source files list(APPEND libcvc4parser_src_files ${gen_src_files}) endforeach() ---- src/prop/bvminisat/mtl/template.mk.orig 2019-04-09 10:14:31.000000000 -0600 -+++ src/prop/bvminisat/mtl/template.mk 2019-04-17 11:22:27.662986017 -0600 +--- src/prop/bvminisat/mtl/template.mk.orig 2020-06-19 10:59:27.000000000 -0600 ++++ src/prop/bvminisat/mtl/template.mk 2020-06-21 11:46:23.831586522 -0600 @@ -22,7 +22,7 @@ CXX ?= g++ CFLAGS ?= -Wall -Wno-parentheses LFLAGS ?= -Wall @@ -45,8 +43,8 @@ CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS LFLAGS += -lz ---- src/prop/minisat/mtl/template.mk.orig 2019-04-09 10:14:31.000000000 -0600 -+++ src/prop/minisat/mtl/template.mk 2019-04-17 11:22:15.879002442 -0600 +--- src/prop/minisat/mtl/template.mk.orig 2020-06-19 10:59:27.000000000 -0600 ++++ src/prop/minisat/mtl/template.mk 2020-06-21 11:46:37.670568635 -0600 @@ -22,7 +22,7 @@ CXX ?= g++ CFLAGS ?= -Wall -Wno-parentheses LFLAGS ?= -Wall diff --git a/cvc4-swig4.patch b/cvc4-swig4.patch deleted file mode 100644 index 710e744..0000000 --- a/cvc4-swig4.patch +++ /dev/null @@ -1,44 +0,0 @@ ---- src/bindings/java/CMakeLists.txt.orig 2019-04-09 10:14:31.000000000 -0600 -+++ src/bindings/java/CMakeLists.txt 2019-06-06 11:58:39.836849929 -0600 -@@ -131,6 +131,7 @@ set(gen_java_files - ${CMAKE_CURRENT_BINARY_DIR}/LastExceptionBuffer.java - ${CMAKE_CURRENT_BINARY_DIR}/LogicException.java - ${CMAKE_CURRENT_BINARY_DIR}/LogicInfo.java -+ ${CMAKE_CURRENT_BINARY_DIR}/Map_ExprExpr.java - ${CMAKE_CURRENT_BINARY_DIR}/ModalException.java - ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java - ${CMAKE_CURRENT_BINARY_DIR}/Options.java -@@ -177,7 +178,6 @@ set(gen_java_files - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpq_class.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpz_class.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__istream.java -- ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__mapT_CVC4__Expr_CVC4__Expr_t.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__ostream.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__shared_ptrT_CVC4__SygusPrintCallback_t.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__string.java -@@ -204,12 +204,12 @@ set(gen_java_files - ${CMAKE_CURRENT_BINARY_DIR}/StatisticsBase.java - ${CMAKE_CURRENT_BINARY_DIR}/StringType.java - ${CMAKE_CURRENT_BINARY_DIR}/SygusConstraintCommand.java -- ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java - ${CMAKE_CURRENT_BINARY_DIR}/SygusGTerm.java - ${CMAKE_CURRENT_BINARY_DIR}/SygusInvConstraintCommand.java - ${CMAKE_CURRENT_BINARY_DIR}/SygusPrintCallback.java - ${CMAKE_CURRENT_BINARY_DIR}/SymbolTable.java - ${CMAKE_CURRENT_BINARY_DIR}/SymbolType.java -+ ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java - ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java - ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java - ${CMAKE_CURRENT_BINARY_DIR}/Timer.java ---- src/smt/smt_engine.i.orig 2019-04-09 10:14:31.000000000 -0600 -+++ src/smt/smt_engine.i 2019-06-06 11:24:53.214450924 -0600 -@@ -42,6 +42,9 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acs - swigCPtr = 0; - } - } -+ -+%template(Map_ExprExpr) std::map; -+ - #endif // SWIGJAVA - - %ignore CVC4::SmtEngine::setLogic(const char*); diff --git a/cvc4.spec b/cvc4.spec index 42f10b8..9e98889 100644 --- a/cvc4.spec +++ b/cvc4.spec @@ -2,8 +2,8 @@ # we currently build without glpk support. Name: cvc4 -Version: 1.7 -Release: 15%{?dist} +Version: 1.8 +Release: 1%{?dist} Summary: Automatic theorem prover for SMT problems # License breakdown: @@ -17,17 +17,10 @@ Summary: Automatic theorem prover for SMT problems License: Boost and BSD and MIT URL: http://cvc4.cs.stanford.edu/ Source0: https://github.com/CVC4/CVC4/archive/%{version}/%{name}-%{version}.tar.gz -# Fix detection of ABC -Patch0: %{name}-abc.patch # Do not override Fedora flags -Patch1: %{name}-flags.patch -# Adapt to swig 4 -Patch2: %{name}-swig4.patch -# Fix drat signature wrt side condition return types -# https://github.com/CVC4/CVC4/commit/57524fd9f204f8e85e5e37af1444a6f76d809aee -Patch3: %{name}-drat.patch +Patch0: %{name}-flags.patch # Adapt to cryptominisat 5.7 -Patch4: %{name}-cryptominisat.patch +Patch1: %{name}-cryptominisat.patch BuildRequires: abc-devel BuildRequires: antlr3-C-devel @@ -35,28 +28,28 @@ BuildRequires: antlr3-tool BuildRequires: boost-devel BuildRequires: cadical-devel BuildRequires: cmake -BuildRequires: cryptominisat-devel +BuildRequires: cmake(cryptominisat5) BuildRequires: cxxtest BuildRequires: drat2er-devel +BuildRequires: drat-trim-devel BuildRequires: gcc-c++ BuildRequires: ghostscript BuildRequires: gmp-devel BuildRequires: java-devel -BuildRequires: jpackage-utils +BuildRequires: javapackages-tools +BuildRequires: kissat-devel BuildRequires: lfsc-devel BuildRequires: libtool BuildRequires: perl-interpreter +BuildRequires: pkgconfig(readline) BuildRequires: python3-devel -BuildRequires: readline-devel +BuildRequires: %{py3_dist cython} +BuildRequires: %{py3_dist toml} BuildRequires: swig BuildRequires: symfpu-devel Requires: %{name}-libs%{?_isa} = %{version}-%{release} -# This can be removed when Fedora 30 reaches EOL -Obsoletes: %{name}-doc < 1.7 -Provides: %{name}-doc = %{version}-%{release} - %description CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove @@ -92,7 +85,7 @@ SMT problems. Summary: Java interface to %{name} Requires: %{name}-libs%{?_isa} = %{version}-%{release} Requires: java-headless -Requires: jpackage-utils +Requires: javapackages-tools %description java Java interface to %{name}. @@ -107,6 +100,12 @@ Python 3 interface to %{name}. %prep %autosetup -p0 -n CVC4-%{version} +# Adapt to way kissat is packaged for Fedora +sed -i 's,#include ,#include ,' src/prop/kissat.h + +# We want to know about use of deprecated interfaces +sed -i '/Wno-deprecated/d' CMakeLists.txt + # The Java interface uses type punning sed -i '/include_directories/aadd_compile_options("-fno-strict-aliasing")' \ src/bindings/java/CMakeLists.txt @@ -116,12 +115,13 @@ sed -i 's/\${CMAKE_INSTALL_PREFIX}/\\$ENV{DESTDIR}&/' src/CMakeLists.txt # Fix installation directory on 64-bit arches if [ "%{_lib}" = "lib64" ]; then - sed -i 's/DESTINATION lib/&64/' src/CMakeLists.txt src/parser/CMakeLists.txt + sed -i 's/LIBRARY_INSTALL_DIR lib/&64/' CMakeLists.txt fi # Python extensions should not link against libpython; see # https://github.com/python/cpython/pull/12946 -sed -i 's/ \${PYTHON_LIBRARIES}//' src/bindings/python/CMakeLists.txt +sed -i 's/ \${PYTHON_LIBRARIES}//' src/bindings/python/CMakeLists.txt \ + src/api/python/CMakeLists.txt # One test exhausts all memory on 32-bit platforms; skip it %ifarch %{arm} %{ix86} @@ -134,32 +134,32 @@ pylib=$(ls -1 %{_libdir}/libpython3.*.so) export CFLAGS="%{optflags} -fsigned-char -DABC_USE_STDINT_H -I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -I%{_includedir}/abc" export CXXFLAGS="$CFLAGS" %cmake \ - -DCMAKE_SKIP_RPATH:BOOL=YES \ - -DCMAKE_SKIP_INSTALL_RPATH:BOOL=YES \ - -DBUILD_BINDINGS_JAVA:BOOL=ON \ -DBUILD_BINDINGS_PYTHON:BOOL=ON \ + -DBUILD_SWIG_BINDINGS_JAVA:BOOL=ON \ + -DBUILD_SWIG_BINDINGS_PYTHON:BOOL=ON \ + -DCMAKE_JAVA_COMPILE_FLAGS:STRING="-source;1.8;-target;1.8" \ -DENABLE_GPL:BOOL=ON \ - -DENABLE_OPTIMIZED:STRING=ON \ - -DENABLE_PORTFOLIO:STRING=ON \ - -DENABLE_PROOFS:STRING=ON \ - -DENABLE_SHARED:STRING=ON \ - -DUSE_ABC:STRING=ON \ - -DABC_DIR:STRING=%{_prefix} \ + -DENABLE_OPTIMIZED:BOOL=ON \ + -DENABLE_PORTFOLIO:BOOL=ON \ + -DENABLE_PROOFS:BOOL=ON \ + -DENABLE_SHARED:BOOL=ON \ + -DUSE_ABC:BOOL=ON \ + -DABC_ARCH_FLAGS:FILEPATH="-I%{_includedir}/abc" \ -DUSE_CADICAL:BOOL=ON \ - -DCADICAL_DIR:STRING=%{_prefix} \ -DUSE_CRYPTOMINISAT:BOOL=ON \ - -DCRYPTOMINISAT_DIR:STRING=%{_prefix} \ + -DCryptoMiniSat_INCLUDE_DIR:FILEPATH=%{_includedir}/cryptominisat5 \ -DUSE_DRAT2ER:BOOL=ON \ - -DDRAT2ER_DIR:STRING=%{_prefix} \ - -DDrat2Er_INCLUDE_DIR:STRING=%{_includedir}/drat2er \ + -DDrat2Er_INCLUDE_DIR:FILEPATH=%{_includedir} \ -DDrat2Er_LIBRARIES:STRING=-ldrat2er \ - -DDratTrim_LIBRARIES:STRING=-ldrat2er \ + -DDratTrim_LIBRARIES:STRING=-ldrat-trim \ + -DUSE_KISSAT:BOOL=ON \ + -DKissat_INCLUDE_DIR:FILEPATH=%{_includedir} \ + -DKissat_LIBRARIES:STRING=-lkissat \ -DUSE_LFSC:BOOL=ON \ - -DLFSC_DIR:STRING=%{_prefix} \ -DUSE_PYTHON3:BOOL=ON \ - -DUSE_READLINE:STRING=ON \ + -DUSE_READLINE:BOOL=ON \ -DUSE_SYMFPU:BOOL=ON \ - -DSYMFPU_DIR:STRING=%{_prefix} \ + -DSYMFPU_DIR:FILEPATH=%{_prefix} \ -DPYTHON_EXECUTABLE:FILEPATH=%{_bindir}/python%{python3_version} \ -DPYTHON_LIBRARY:FILEPATH=$pylib \ -DPYTHON_INCLUDE_DIR:FILEPATH=$pyinc \ @@ -167,19 +167,32 @@ export CXXFLAGS="$CFLAGS" # Tell swig to build for python 3 sed -i 's/swig -python/& -py3/' \ - src/bindings/python/CMakeFiles/CVC4_swig_compilation.dir/build.make + %{__cmake_builddir}/src/bindings/python/CMakeFiles/CVC4_swig_compilation.dir/build.make -make %{?_smp_mflags} +%cmake_build make doc %install -%make_install +# The Python API install target ignores DESTDIR, so force the issue. +sed -e 's,"%{_prefix}","%{buildroot}%{_prefix}",g' \ + -e 's,--prefix=%{_prefix},--prefix=%{buildroot}%{_prefix},' \ + -i %{__cmake_builddir}/src/api/python/cmake_install.cmake -# BUG: CVC4 1.7 does not install the Java interface -mkdir -p %{buildroot}%{_javadir} -cp -p src/bindings/java/CVC4.jar %{buildroot}%{_javadir} +%cmake_install + +# Link the JNI interface to where Fedora mandates it should go mkdir -p %{buildroot}%{_jnidir}/%{name} -cp -p src/bindings/java/libcvc4jni.so %{buildroot}%{_jnidir}/%{name} +ln -s ../../%{_lib}/libcvc4jni.so %{buildroot}%{_jnidir}/%{name} + +# Fix a symlink that points to the build directory +rm %{buildroot}%{_javadir}/%{name}/CVC4.jar +ln -s CVC4-%{version}.jar %{buildroot}%{_javadir}/%{name}/CVC4.jar + +# The cython interface is installed into the wrong directory +if [ "%{python3_sitelib}" != "%{python3_sitearch}" ]; then + mv %{buildroot}%{python3_sitelib}/pycvc4* %{buildroot}%{python3_sitearch} + rm -fr %{buildroot}%{prefix}/lib/python3* +fi %check # The tests use a large amount of stack space. @@ -194,38 +207,43 @@ sed 's,loadLibrary("cvc4jni"),load("%{buildroot}%{_jnidir}/%{name}/libcvc4jni.so export LC_ALL=C.UTF-8 export LD_LIBRARY_PATH=%{buildroot}%{_libdir} -make check +%cmake_build --target check %files %doc AUTHORS NEWS README.md THANKS %{_bindir}/%{name} -%{_bindir}/p%{name} %{_datadir}/%{name}/ %{_mandir}/man1/%{name}.1* -%{_mandir}/man1/p%{name}.1* %{_mandir}/man5/%{name}.5* %files libs -%license COPYING licenses/channel.h-LICENSE -%{_libdir}/lib%{name}.so.6 -%{_libdir}/lib%{name}parser.so.6 +%license COPYING +%{_libdir}/lib%{name}.so.7 +%{_libdir}/lib%{name}parser.so.7 %files devel %{_includedir}/%{name}/ %{_libdir}/lib%{name}.so %{_libdir}/lib%{name}parser.so +%{_libdir}/cmake/CVC4/ %{_mandir}/man3/* %files java -%{_javadir}/CVC4.jar +%{_javadir}/%{name}/ %{_jnidir}/%{name}/ +%{_libdir}/libcvc4jni.so %files python3 %{python3_sitearch}/CVC4.py %{python3_sitearch}/_CVC4.so %{python3_sitearch}/__pycache__/CVC4.* +%{python3_sitearch}/pycvc4* %changelog +* Mon Aug 3 2020 Jerry James - 1.8-1 +- Version 1.8 +- Drop upstreamed patches: -abc, -swig4, -drat + * Sat Aug 01 2020 Fedora Release Engineering - 1.7-15 - Second attempt - Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild diff --git a/sources b/sources index 3b9fac1..dbdd34c 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (cvc4-1.7.tar.gz) = b91dfac7ddf979a3474f562eb98f2d6f17a53efa38c1be5502429309a0c059e1f2b0d85ee95e5aee17d35f34c825f01f879ec4aaf26025b1fcac835c33a867c6 +SHA512 (cvc4-1.8.tar.gz) = 19e318a62f0a6dfeea4db5225b150550f1e7afcf42a3547bad1ff2030aca7a7713fe29e7059f2dc391eaa18b0cd4183f99ab2dca5008979cb8881b46b8dc01f2