diff --git a/cvc4-drat.patch b/cvc4-drat.patch
new file mode 100644
index 0000000..234068e
--- /dev/null
+++ b/cvc4-drat.patch
@@ -0,0 +1,20 @@
+--- 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.spec b/cvc4.spec
index 0328f69..967ccf6 100644
--- a/cvc4.spec
+++ b/cvc4.spec
@@ -3,7 +3,7 @@
 
 Name:           cvc4
 Version:        1.7
-Release:        5%{?dist}
+Release:        6%{?dist}
 Summary:        Automatic theorem prover for SMT problems
 
 # License breakdown:
@@ -23,6 +23,9 @@ Patch0:         %{name}-abc.patch
 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
 
 BuildRequires:  abc-devel
 BuildRequires:  antlr3-C-devel
@@ -217,6 +220,9 @@ make check
 %{python3_sitearch}/__pycache__/CVC4.*
 
 %changelog
+* Mon Sep  9 2019 Jerry James <loganjerry@gmail.com> - 1.7-6
+- Add -drat patch to fix build with latest lfsc
+
 * Mon Aug 19 2019 Miro Hrončok <mhroncok@redhat.com> - 1.7-5
 - Rebuilt for Python 3.8