diff --git a/yices-cryptominisat.patch b/yices-cryptominisat.patch
index 78d4a74..be1cc37 100644
--- a/yices-cryptominisat.patch
+++ b/yices-cryptominisat.patch
@@ -5,7 +5,7 @@
  
  #ifdef HAVE_CADICAL
 -#include "ccadical.h"
-+#include <cadical/ccadical.h>
++#include <ccadical.h>
  #endif
  
  #ifdef HAVE_CRYPTOMINISAT
diff --git a/yices.spec b/yices.spec
index 7b990a7..8f5caac 100644
--- a/yices.spec
+++ b/yices.spec
@@ -34,33 +34,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 +58,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
@@ -181,7 +169,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.7*
 
 %files devel
 %{_includedir}/%{name}/