Add -drat patch to fix build with latest lfsc.
This commit is contained in:
parent
b65b6a9a07
commit
e32cd51007
|
@ -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)
|
|
@ -3,7 +3,7 @@
|
||||||
|
|
||||||
Name: cvc4
|
Name: cvc4
|
||||||
Version: 1.7
|
Version: 1.7
|
||||||
Release: 5%{?dist}
|
Release: 6%{?dist}
|
||||||
Summary: Automatic theorem prover for SMT problems
|
Summary: Automatic theorem prover for SMT problems
|
||||||
|
|
||||||
# License breakdown:
|
# License breakdown:
|
||||||
|
@ -23,6 +23,9 @@ Patch0: %{name}-abc.patch
|
||||||
Patch1: %{name}-flags.patch
|
Patch1: %{name}-flags.patch
|
||||||
# Adapt to swig 4
|
# Adapt to swig 4
|
||||||
Patch2: %{name}-swig4.patch
|
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: abc-devel
|
||||||
BuildRequires: antlr3-C-devel
|
BuildRequires: antlr3-C-devel
|
||||||
|
@ -217,6 +220,9 @@ make check
|
||||||
%{python3_sitearch}/__pycache__/CVC4.*
|
%{python3_sitearch}/__pycache__/CVC4.*
|
||||||
|
|
||||||
%changelog
|
%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
|
* Mon Aug 19 2019 Miro Hrončok <mhroncok@redhat.com> - 1.7-5
|
||||||
- Rebuilt for Python 3.8
|
- Rebuilt for Python 3.8
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue