Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild

Using the current date breaks build reproducibility.

.gitignore

@@ -1,2 +1,3 @@
 /Yices-*.tar.gz
+/yices-*.tar.gz
 /cudd-*.tar.gz

README.md

@@ -0,0 +1,11 @@
+# yices
+
+[Yices 2](https://yices.csl.sri.com/) is a solver for
+[Satisfiability Modulo Theories](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)
+(SMT) problems.  Yices 2 can process input written in the SMT-LIB language, or
+in Yices' own specification language.  The package provides a
+[C API](https://github.com/SRI-CSL/yices2/blob/master/src/include/yices.h).
+Separately, bindings for [Java](https://github.com/SRI-CSL/yices2_java_bindings),
+[Python](https://github.com/SRI-CSL/yices2_python_bindings),
+[Go](https://github.com/SRI-CSL/yices2_go_bindings), and
+[OCaml](https://github.com/SRI-CSL/yices2_ocaml_bindings) are available.

changelog

@@ -0,0 +1,109 @@
+* Tue Feb 20 2024 Jerry James <loganjerry@gmail.com> - 2.6.4-12
+- Fix the SPDX expression
+
+* Fri Feb  9 2024 Jerry James <loganjerry@gmail.com> - 2.6.4-11
+- Rebuild for cryptominisat 5.11.21
+
+* Wed Jan 31 2024 Jerry James <loganjerry@gmail.com> - 2.6.4-10
+- Rebuild for cryptominisat 5.11.15
+
+* Sat Jan 27 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-9
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
+
+* Wed Jan 10 2024 Jerry James <loganjerry@gmail.com> - 2.6.4-8
+- Rebuild for cadical 1.9.4
+- Update font licenses from LPPL-1.0 to LPPL-1.3a
+- Stop building for 32-bit x86
+
+* Sat Jul 22 2023 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-7
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
+
+* Sat Jan 21 2023 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-6
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
+
+* Mon Nov 28 2022 Jerry James <loganjerry@gmail.com> - 2.6.4-5
+- Regenerate the cudd configure script to fix FTBFS
+- Convert License tag to SPDX
+
+* Mon Nov 28 2022 Timm Bäder <tbaeder@redhat.com> - 2.6.4-5
+- Get rid of an implicit int function declaration in a configure check
+
+* Sat Jul 23 2022 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-4
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
+
+* Sat Jan 22 2022 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
+
+* Tue Jan 11 2022 Jerry James <loganjerry@gmail.com> - 2.6.4-2
+- Build with kissat support
+
+* Mon Oct 25 2021 Jerry James <loganjerry@gmail.com> - 2.6.4-1
+- Version 2.6.4
+- Drop upstreamed -big-endian and -sphinx3 patches
+- Enable tests on 32-bit platforms
+
+* Fri Jul 23 2021 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2-8
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
+
+* Thu Jan 28 2021 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2-7
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
+
+* Fri Nov 27 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-6
+- Rebuild for cryptominisat 5.8.0
+
+* Mon Aug  3 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-5
+- Rebuild for cadical 1.3.0
+
+* Wed Jul 29 2020 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2-4
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
+
+* Sat Apr 25 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-3
+- Rebuild for cryptominisat 5.7.0
+- Switch to upstream's solution for sphinx 3 support
+
+* Thu Apr 16 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-2
+- Use native sphinx 3 support for enum instead of cenum extension (bz 1823515)
+
+* Thu Mar 26 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-1
+- Version 2.6.2
+- Drop upstreamed -missing-typedef patch
+- Add -big-endian patch to fix s390x build
+- Add -cryptominisat5 patch to fix build with recent cryptominisat releases
+- Skip tests on 32-bit platforms; some tests fail due to the limited size of a
+  C integer
+
+* Fri Jan 31 2020 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-6
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
+
+* Thu Jan 23 2020 Jerry James <loganjerry@gmail.com> - 2.6.1-5
+- Add -missing-typedef patch to fix FTBFS with gcc 10
+- Set -doc subpackage to noarch
+
+* Fri Nov 22 2019 Jerry James <loganjerry@gmail.com> - 2.6.1-4
+- Add -fwrapv to build flags; thanks to Jeff Law for the diagnosis
+
+* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
+
+* Sun Feb 03 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
+
+* Tue Oct 30 2018 Jerry James <loganjerry@gmail.com> - 2.6.1-1
+- New upstream version
+
+* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
+
+* Wed Jul  4 2018 Jerry James <loganjerry@gmail.com> - 2.6.0-1
+- New upstream version
+
+* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.4-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
+
+* Tue Jan  2 2018 Jerry James <loganjerry@gmail.com> - 2.5.4-2
+- Add a -doc subpackage
+- Fix end of line encodings
+- Fix permissions on yices_debug_version.c
+
+* Mon Jan  1 2018 Jerry James <loganjerry@gmail.com> - 2.5.4-1
+- Initial RPM

implicit-int.patch

@@ -0,0 +1,12 @@
+diff -ruN yices2-Yices-2.6.4/cudd-cudd-3.0.0/configure.ac yices2-Yices-2.6.4.orig/cudd-cudd-3.0.0/configure.ac
+--- a/cudd-cudd-3.0.0/configure.ac	2016-01-20 23:59:33.000000000 +0100
++++ b/cudd-cudd-3.0.0/configure.ac	2022-11-28 12:32:24.297791070 +0100
+@@ -131,7 +131,7 @@
+ AC_CACHE_VAL(ac_cv_have_ieee_754,
+ [ AC_TRY_RUN([
+ #include <math.h>
+-main(void)
++int main(void)
+ {
+     if (HUGE_VAL != HUGE_VAL * 3 || HUGE_VAL != HUGE_VAL / 3) return 1;
+     return 0;

sources

@@ -1,2 +1,2 @@
-SHA512 (Yices-2.6.2.tar.gz) = 58990cff2a70d4fae797efdf3c52a15772eb824bc6865682fa64e63b571054eb042a252e52b67b2f89fb191444543f0ad55f9b34086bdd8bcd083ef10422d388
+SHA512 (yices-2.7.0.tar.gz) = 0ed9811bfc505793078aa87afd86177a79bb5b9a4ec579fa0c43076cc997ff432d66588e996c1303d91bfb2163110312f30f1fc75a4d2f60d5786499bdd26b92
 SHA512 (cudd-3.0.0.tar.gz) = a26728fedc3033ae2a842000f43f215b4abc914cd00fe0097fd483e59dc630568bfa6a115baa93af94b2f70f3d538761a12143fdb757167e90395c9fd244318c

yices-big-endian.patch

@@ -1,78 +0,0 @@
---- a/configure.ac
-+++ b/configure.ac
-@@ -152,15 +152,9 @@ dnl
- dnl Check for endianness
- dnl --------------------
- dnl
--dnl The neorationals code is little-endian only for now.
--dnl TODO: support big-endian architectures at some point
--dnl For now, we check here and fail.
--dnl
--bigendian=""
--AC_C_BIGENDIAN([bigendian=yes],[bigendian=no],[bigendian=yes])
--if test "x$bigendian" = xyes ; then
--   AC_MSG_ERROR([Can't build for your architecture. Yices builds only on little-endian hardware. Please file an issue at $repo_url])
--fi
-+WORDS_BIGENDIAN=""
-+AC_C_BIGENDIAN([WORDS_BIGENDIAN=yes],[WORDS_BIGENDIAN=no],[WORDS_BIGENDIAN=yes])
-+AC_SUBST(WORDS_BIGENDIAN)
- 
- dnl
- dnl CHECK_THREAD_LOCAL
---- a/make.include.in
-+++ b/make.include.in
-@@ -66,6 +66,7 @@ RANLIB=@RANLIB@
- GPERF=@GPERF@
- STRIP=@STRIP@
- NO_STACK_PROTECTOR=@NO_STACK_PROTECTOR@
-+WORDS_BIGENDIAN=@WORDS_BIGENDIAN@
- 
- # thread-safe build
- HAVE_TLS=@HAVE_TLS@
---- a/src/Makefile
-+++ b/src/Makefile
-@@ -595,6 +595,13 @@ libyices_def=libyices.def
- ###########################
- 
- #
-+# Whether we are building for a big endian architecture
-+#
-+ifeq ($(WORDS_BIGENDIAN),yes)
-+  CPPFLAGS += -DWORDS_BIGENDIAN
-+endif
-+
-+#
- # Whether we have support for mcsat
- #
- ifeq ($(ENABLE_MCSAT),yes)
---- a/src/terms/rationals.h
-+++ b/src/terms/rationals.h
-@@ -47,8 +47,13 @@
-  * signed numerator, and a 31 bit unsigned denominator.
-  */
- typedef struct {
-+#ifdef WORDS_BIGENDIAN
-+  int32_t  num;
-+  uint32_t den;
-+#else
-   uint32_t den;
-   int32_t  num;
-+#endif
- } rat32_t;
- 
- typedef struct {
---- a/tests/unit/Makefile
-+++ b/tests/unit/Makefile
-@@ -84,6 +84,12 @@ static_tests := $(src_c:%.c=$(static_bin
- libyices := $(libdir)/libyices.a
- static_libyices := $(static_libdir)/libyices.a
- 
-+#
-+# Whether we are building for a big endian architecture
-+#
-+ifeq ($(WORDS_BIGENDIAN),yes)
-+  CPPFLAGS += -DWORDS_BIGENDIAN
-+endif
- 
- #
- # Whether we have support for mcsat

yices-cryptominisat.patch

@@ -5,7 +5,7 @@
  
  #ifdef HAVE_CADICAL
 -#include "ccadical.h"
-+#include <ccadical.h>
++#include <cadical/ccadical.h>
  #endif
  
  #ifdef HAVE_CRYPTOMINISAT
@@ -13,8 +13,8 @@
 +#include <cryptominisat5/cryptominisat_c.h>
  #endif
  
- #include "solvers/cdcl/delegate.h"
-@@ -293,44 +293,44 @@ static void cadical_as_delegate(delegate
+ #ifdef HAVE_KISSAT
+@@ -308,44 +308,44 @@ static void cadical_as_delegate(delegate
  
  #if HAVE_CRYPTOMINISAT
  static void cryptominisat_add_empty_clause(void *solver) {
@@ -68,15 +68,15 @@
  
  static smt_status_t cryptominisat_check(void *solver) {
 -  switch (cmsat_solve(solver)) {
--  case CMSAT_SAT: return STATUS_SAT;
--  case CMSAT_UNSAT: return STATUS_UNSAT;
+-  case CMSAT_SAT: return YICES_STATUS_SAT;
+-  case CMSAT_UNSAT: return YICES_STATUS_UNSAT;
 +  switch (cmsat_solve((SATSolver *)solver).x) {
-+  case L_TRUE: return STATUS_SAT;
-+  case L_FALSE: return STATUS_UNSAT;
-   default: return STATUS_UNKNOWN;
++  case L_TRUE: return YICES_STATUS_SAT;
++  case L_FALSE: return YICES_STATUS_UNSAT;
+   default: return YICES_STATUS_UNKNOWN;
    }
  }
-@@ -341,28 +341,23 @@ static smt_status_t cryptominisat_check(
+@@ -356,28 +356,23 @@ static smt_status_t cryptominisat_check(
   * that cryptominisat always produces a full truth assignment.
   */
  static bval_t cryptominisat_get_value(void *solver, bvar_t x) {

yices-sphinx3.patch

@@ -1,57 +0,0 @@
---- a/doc/sphinx/source/basic-usage.rst
-+++ b/doc/sphinx/source/basic-usage.rst
-@@ -263,7 +263,7 @@ Running this example should produce some
- 
-    To avoid these issues, we recommend compiling with mingw.
-    It is still possible to use Visual Studio or other compilers on Windows,
--   as long as you avoid functions in the Yices API that take a :c:type:`FILE *`
-+   as long as you avoid functions in the Yices API that take a `FILE *`
-    argument. File :file:`examples/example1b.c` in the distribution shows
-    how to use alternative functions for pretty printing. You can also
-    download this file  :download:`here <_static/example1b.c>`.
---- a/doc/sphinx/source/conf.py
-+++ b/doc/sphinx/source/conf.py
-@@ -14,6 +14,7 @@
- 
- import sys
- import os
-+from sphinx import version_info
- 
- # If extensions (or modules to document with autodoc) are in another directory,
- # add these directories to sys.path here. If the directory is relative to the
-@@ -33,7 +34,7 @@ needs_sphinx = '1.0'
- #
- # mathjax_path = 'https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML'
- #
--extensions = ['cenum']
-+extensions = [] if version_info[0] >= 3 else ['cenum']
- 
- # Add any paths that contain templates here, relative to this directory.
- templates_path = ['_templates']
---- a/doc/sphinx/source/error-reports.rst
-+++ b/doc/sphinx/source/error-reports.rst
-@@ -41,7 +41,7 @@ The following functions give access to t
-    be used for diagnostic.
- 
- 
--.. c:function:: int32_t yices_print_error(int fd)
-+.. c:function:: int32_t yices_print_error_fd(int fd)
- 
-    This is a variant of the previous function that writes to file
-    descriptor *fd* instead of an output stream. The file must be open
---- a/doc/sphinx/source/_static/classic.css
-+++ b/doc/sphinx/source/_static/classic.css
-@@ -199,11 +199,13 @@ span.raw-html {
- }
- 
- table {
-+  border: 1px solid black;
-   border-collapse: collapse;
-   margin: 0 -0.5em 0 -0.5em;
- }
- 
- table td, table th {
-+  border: 1px solid black;
-   padding: 0.2em 0.5em 0.2em 0.5em;
- }
- 

yices.rpmlintrc

@@ -1,8 +0,0 @@
-# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON
-# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors
-
-# The dictionary is missing some technical terms
-addFilter(r'W: spelling-error .* (bitvectors|satisfiability|tuples)')
-
-# Documentation is in the -doc subpackage
-addFilter(r'yices-devel\.[^:]+: W: no-documentation')

yices.spec

@@ -1,24 +1,26 @@
+%global giturl  https://github.com/SRI-CSL/yices2
+
 Name:           yices
-Version:        2.6.2
-Release:        6%{?dist}
+Version:        2.7.0
+Release:        %autorelease
 Summary:        SMT solver
 
-# The yices code is GPLv3+.  The cudd code is BSD.
-License:        GPLv3+ and BSD
+# The yices code is GPL-3.0-or-later.  The cudd code is BSD-3-Clause.
+License:        GPL-3.0-or-later AND BSD-3-Clause
 URL:            http://yices.csl.sri.com/
-Source0:        https://github.com/SRI-CSL/yices2/archive/Yices-%{version}.tar.gz
+VCS :           git:%{giturl}.git
+Source0:        %{giturl}/archive/yices-%{version}.tar.gz
 # The CUDD web site disappeared in 2018.  The Fedora package was retired in 2019
 # when there were no more Fedora users.  Instead of resurrecting the package for
 # the sole use of yices, we bundle a snapshot of the last released version.
 Source1:        https://github.com/ivmai/cudd/archive/cudd-3.0.0.tar.gz
-# Fix the build on big endian machines
-# https://github.com/SRI-CSL/yices2/pull/185
-Patch0:         %{name}-big-endian.patch
 # Adapt to newer versions of cryptominisat
-Patch1:         %{name}-cryptominisat.patch
-# Adapt to sphinx 3.x
-# https://github.com/SRI-CSL/yices2/commit/52d025a6b0ae2af55bf8f537ddeb9cd8f2519237
-Patch2:         %{name}-sphinx3.patch
+Patch:          %{name}-cryptominisat.patch
+# Get rid of an implicit-int function declaration in a configure check.
+Patch:          implicit-int.patch
+
+# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval
+ExcludeArch:    %{ix86}
 
 BuildRequires:  cadical-devel
 BuildRequires:  cryptominisat-devel
@@ -26,26 +28,39 @@ BuildRequires:  gcc
 BuildRequires:  gcc-c++
 BuildRequires:  gmp-devel
 BuildRequires:  gperf
+BuildRequires:  kissat-devel
 BuildRequires:  latexmk
 BuildRequires:  libpoly-devel
 BuildRequires:  libtool
 BuildRequires:  make
 BuildRequires:  %{py3_dist sphinx}
-BuildRequires:  tex(latex)
+BuildRequires:  tex(amsfonts.sty)
+BuildRequires:  tex(cite.sty)
+BuildRequires:  tex(epstopdf.sty)
+BuildRequires:  tex(listings.sty)
+BuildRequires:  tex(xcolor.sty)
+BuildRequires:  texlive-bibtex
+BuildRequires:  texlive-cm
+BuildRequires:  texlive-courier
+BuildRequires:  texlive-ec
+BuildRequires:  texlive-helvetic
+BuildRequires:  texlive-latex
+BuildRequires:  texlive-makeindex
+BuildRequires:  texlive-times
 
 # See Source1 comment
 Provides:       bundled(cudd) = 3.0.0
 
 %description
-Yices 2 is an efficient SMT solver that decides the satisfiability of
-formulas containing uninterpreted function symbols with equality, linear
-real and integer arithmetic, bitvectors, scalar types, and tuples.
+Yices 2 is an efficient SMT solver that decides the satisfiability of formulas
+containing uninterpreted function symbols with equality, linear real and
+integer arithmetic, bitvectors, scalar types, and tuples.
 
-Yices 2 can process input written in the SMT-LIB notation (both versions
-2.0 and 1.2 are supported).
+Yices 2 can process input written in the SMT-LIB notation (both versions 2.0
+and 1.2 are supported).
 
-Alternatively, you can write specifications using the Yices 2
-specification language, which includes tuples and scalar types.
+Alternatively, you can write specifications using the Yices 2 specification
+language, which includes tuples and scalar types.
 
 Yices 2 can also be used as a library in other software.
 
@@ -55,8 +70,8 @@ Requires:       %{name}%{?_isa} = %{version}-%{release}
 Requires:       gmp-devel%{?_isa}
 
 %description devel
-This package contains the header files necessary for developing programs
-which use yices.
+This package contains the header files necessary for developing programs which
+use yices.
 
 %package tools
 Summary:        Command line tools that use the yices library
@@ -66,6 +81,35 @@ Requires:       %{name}%{?_isa} = %{version}-%{release}
 Command line tools that use the yices library.
 
 %package doc
+# The content is GPL-3.0-or-later.  Other licenses are due to files copied in
+# by Sphinx and due to fonts embedded in PDFs.
+# Sphinx file licenses:
+# _static/_sphinx_javascript_frameworks_compat.js: BSD-2-Clause
+# _static/basic.css: BSD-2-Clause
+# _static/classic.css: BSD-2-Clause
+# _static/default.css: BSD-2-Clause
+# _static/doctools.js: BSD-2-Clause
+# _static/documentation_options.js: BSD-2-Clause
+# _static/epub.css: BSD-2-Clause
+# _static/file.png: BSD-2-Clause
+# _static/jquery*.js: MIT
+# _static/language_data.js: BSD-2-Clause
+# _static/minus.png: BSD-2-Clause
+# _static/plus.png: BSD-2-Clause
+# _static/searchtools.js: BSD-2-Clause
+# _static/sidebar.js: BSD-2-Clause
+# _static/underscore*.js: MIT
+# genindex.html: BSD-2-Clause
+# search.html: BSD-2-Clause
+# searchindex.js: BSD-2-Clause
+#
+# Font licenses:
+# AMS: OFL-1.1-RFN
+# CM: Knuth-CTAN
+# DejaVu: LPPL-1.3a
+# LaTeX: LPPL-1.3a
+# Nimbus: AGPL-3.0-only
+License:        GPL-3.0-or-later AND BSD-2-Clause AND MIT AND OFL-1.1-RFN AND Knuth-CTAN AND LPPL-1.3a AND AGPL-3.0-only
 Summary:        Documentation for yices
 BuildArch:      noarch
 
@@ -73,17 +117,24 @@ BuildArch:      noarch
 This package contains yices documentation.
 
 %prep
-%autosetup -n yices2-Yices-%{version} -p1
-%setup -q -n yices2-Yices-%{version} -T -D -a 1
+%autosetup -n yices2-yices-%{version} -a 1 -p1
 
+%conf
 # Do not try to avoid -fstack-protector
 sed -i 's/@NO_STACK_PROTECTOR@//' make.include.in
 
 # Do not override our build flags
 sed -i 's/ -O3//;s/ -fomit-frame-pointer//' src/Makefile tests/unit/Makefile
 
-# Generate the configure script
+# Use $SOURCE_DATE_EPOCH (or current date)
+sed -i "s/^now=.*/now=$(date +%Y-%m-%d ${SOURCE_DATE_EPOCH:+--date=@$SOURCE_DATE_EPOCH})/" \
+  utils/make_source_version
+
+# Generate the configure scripts
 autoreconf -fi
+cd cudd-cudd-3.0.0
+autoreconf -fi
+cd -
 
 # Fix end of line encodings
 sed -i 's/\r//' examples/{jinpeng,problem_with_input}.ys
@@ -94,16 +145,13 @@ sed -i 's/cp/install -m 0644/' utils/make_source_version
 %build
 # Build cudd
 cd cudd-cudd-3.0.0
-%configure CFLAGS="%{optflags} -fPIC" CXXFLAGS="%{optflags} -fPIC"
+%configure CFLAGS='%{build_cflags} -fPIC' CXXFLAGS='%{build_cxxflags} -fPIC'
 %make_build
 cd -
 
-#bv64_interval_abstraction depends on wrapping for signed overflow
-%global optflags %{optflags} -fwrapv
-
-export CPPFLAGS="-I$PWD/cudd-cudd-3.0.0/cudd -DHAVE_CADICAL -DHAVE_CRYPTOMINISAT"
-export LDFLAGS="$RPM_LD_FLAGS -L$PWD/cudd-cudd-3.0.0/cudd/.libs"
-export LIBS="-lcadical -lcryptominisat5"
+export CPPFLAGS="-I$PWD/cudd-cudd-3.0.0/cudd -DHAVE_CADICAL -DHAVE_CRYPTOMINISAT -DHAVE_KISSAT"
+export LDFLAGS="%{build_ldflags} -L$PWD/cudd-cudd-3.0.0/cudd/.libs"
+export LIBS='-lcadical -lcryptominisat5 -lkissat'
 %configure --enable-mcsat
 
 guess=$(./config.guess)
@@ -127,88 +175,31 @@ rm -f %{buildroot}%{_libdir}/libyices.a
 mkdir -p %{buildroot}%{_mandir}/man1
 cp -p doc/*.1 %{buildroot}%{_mandir}/man1
 
-%ifnarch %{ix86} %{arm}
 %check
 make check MODE=debug
-%endif
 
 %files
 %doc doc/SMT-LIB-LANGUAGE doc/YICES-LANGUAGE
 %license copyright.txt LICENSE.txt
-%{_libdir}/*.so.2*
+%{_libdir}/libyices.so.2.7{,.*}
 
 %files devel
 %{_includedir}/%{name}/
-%{_libdir}/*.so
+%{_libdir}/libyices.so
 
 %files tools
 %{_bindir}/yices
 %{_bindir}/yices-sat
 %{_bindir}/yices-smt
 %{_bindir}/yices-smt2
-%{_mandir}/man1/*
+%{_mandir}/man1/yices.1*
+%{_mandir}/man1/yices-sat.1*
+%{_mandir}/man1/yices-smt.1*
+%{_mandir}/man1/yices-smt2.1*
 
 %files doc
 %doc doc/manual/manual.pdf doc/sphinx/build/html examples
 %license copyright.txt LICENSE.txt
 
 %changelog
-* Fri Nov 27 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-6
-- Rebuild for cryptominisat 5.8.0
-
-* Mon Aug  3 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-5
-- Rebuild for cadical 1.3.0
-
-* Wed Jul 29 2020 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2-4
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
-
-* Sat Apr 25 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-3
-- Rebuild for cryptominisat 5.7.0
-- Switch to upstream's solution for sphinx 3 support
-
-* Thu Apr 16 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-2
-- Use native sphinx 3 support for enum instead of cenum extension (bz 1823515)
-
-* Thu Mar 26 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-1
-- Version 2.6.2
-- Drop upstreamed -missing-typedef patch
-- Add -big-endian patch to fix s390x build
-- Add -cryptominisat5 patch to fix build with recent cryptominisat releases
-- Skip tests on 32-bit platforms; some tests fail due to the limited size of a
-  C integer
-
-* Fri Jan 31 2020 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-6
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
-
-* Thu Jan 23 2020 Jerry James <loganjerry@gmail.com> - 2.6.1-5
-- Add -missing-typedef patch to fix FTBFS with gcc 10
-- Set -doc subpackage to noarch
-
-* Fri Nov 22 2019 Jerry James <loganjerry@gmail.com> - 2.6.1-4
-- Add -fwrapv to build flags; thanks to Jeff Law for the diagnosis
-
-* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-3
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
-
-* Sun Feb 03 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
-
-* Tue Oct 30 2018 Jerry James <loganjerry@gmail.com> - 2.6.1-1
-- New upstream version
-
-* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.0-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
-
-* Wed Jul  4 2018 Jerry James <loganjerry@gmail.com> - 2.6.0-1
-- New upstream version
-
-* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.4-3
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
-
-* Tue Jan  2 2018 Jerry James <loganjerry@gmail.com> - 2.5.4-2
-- Add a -doc subpackage
-- Fix end of line encodings
-- Fix permissions on yices_debug_version.c
-
-* Mon Jan  1 2018 Jerry James <loganjerry@gmail.com> - 2.5.4-1
-- Initial RPM
+%autochangelog