.gitignore

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

sources

@@ -1,2 +1,2 @@
-SHA512 (yices-2.7.0.tar.gz) = 0ed9811bfc505793078aa87afd86177a79bb5b9a4ec579fa0c43076cc997ff432d66588e996c1303d91bfb2163110312f30f1fc75a4d2f60d5786499bdd26b92
+SHA512 (Yices-2.6.5.tar.gz) = 8f01c6d516f2aa901b30e9248c3df78930e670c8e1a795b1bb112561f4e338e6e11eadfc2e6cbfc089f6593561b5874fbe816be677dd09c0834a01829c5cf490
 SHA512 (cudd-3.0.0.tar.gz) = a26728fedc3033ae2a842000f43f215b4abc914cd00fe0097fd483e59dc630568bfa6a115baa93af94b2f70f3d538761a12143fdb757167e90395c9fd244318c

yices-cryptominisat.patch

@@ -5,7 +5,7 @@
  
  #ifdef HAVE_CADICAL
 -#include "ccadical.h"
-+#include <cadical/ccadical.h>
++#include <ccadical.h>
  #endif
  
  #ifdef HAVE_CRYPTOMINISAT
@@ -68,12 +68,12 @@
  
  static smt_status_t cryptominisat_check(void *solver) {
 -  switch (cmsat_solve(solver)) {
--  case CMSAT_SAT: return YICES_STATUS_SAT;
--  case CMSAT_UNSAT: return YICES_STATUS_UNSAT;
+-  case CMSAT_SAT: return STATUS_SAT;
+-  case CMSAT_UNSAT: return STATUS_UNSAT;
 +  switch (cmsat_solve((SATSolver *)solver).x) {
-+  case L_TRUE: return YICES_STATUS_SAT;
-+  case L_FALSE: return YICES_STATUS_UNSAT;
-   default: return YICES_STATUS_UNKNOWN;
++  case L_TRUE: return STATUS_SAT;
++  case L_FALSE: return STATUS_UNSAT;
+   default: return STATUS_UNKNOWN;
    }
  }
 @@ -356,28 +356,23 @@ static smt_status_t cryptominisat_check(

yices.spec

@@ -1,23 +1,21 @@
-%global giturl  https://github.com/SRI-CSL/yices2
-
 Name:           yices
-Version:        2.7.0
+Version:        2.6.5
 Release:        %autorelease
 Summary:        SMT solver
 
 # 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/
-VCS :           git:%{giturl}.git
-Source0:        %{giturl}/archive/yices-%{version}.tar.gz
+VCS:            https://github.com/SRI-CSL/yices2
+Source0:        %{vcs}/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
 # Adapt to newer versions of cryptominisat
-Patch:          %{name}-cryptominisat.patch
+Patch0:         %{name}-cryptominisat.patch
 # Get rid of an implicit-int function declaration in a configure check.
-Patch:          implicit-int.patch
+Patch1:         implicit-int.patch
 
 # See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval
 ExcludeArch:    %{ix86}
@@ -34,33 +32,21 @@ BuildRequires:  libpoly-devel
 BuildRequires:  libtool
 BuildRequires:  make
 BuildRequires:  %{py3_dist sphinx}
-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
+BuildRequires:  tex(latex)
 
 # 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.
 
@@ -70,8 +56,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
@@ -117,19 +103,14 @@ BuildArch:      noarch
 This package contains yices documentation.
 
 %prep
-%autosetup -n yices2-yices-%{version} -a 1 -p1
+%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
 
-# 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
@@ -149,6 +130,9 @@ cd cudd-cudd-3.0.0
 %make_build
 cd -
 
+#bv64_interval_abstraction depends on wrapping for signed overflow
+export CFLAGS='%{build_cflags} -fwrapv'
+export CXXFLAGS='%{build_cxxflags} -fwrapv'
 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'
@@ -181,7 +165,7 @@ make check MODE=debug
 %files
 %doc doc/SMT-LIB-LANGUAGE doc/YICES-LANGUAGE
 %license copyright.txt LICENSE.txt
-%{_libdir}/libyices.so.2.7{,.*}
+%{_libdir}/libyices.so.2*
 
 %files devel
 %{_includedir}/%{name}/