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