From f7491d86a428a7402f5e432276a595781ba0753c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 20 Jan 2021 21:58:43 -0700 Subject: [PATCH] Add -dup-decl patch to fix FTBFS with recent LFSC versions. --- cvc4-dup-decl.patch | 18 ++++++++++++++++++ cvc4.spec | 7 ++++++- 2 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 cvc4-dup-decl.patch diff --git a/cvc4-dup-decl.patch b/cvc4-dup-decl.patch new file mode 100644 index 0000000..a330a9c --- /dev/null +++ b/cvc4-dup-decl.patch @@ -0,0 +1,18 @@ +--- proofs/signatures/th_bv.plf.orig 2020-06-19 10:59:27.000000000 -0600 ++++ proofs/signatures/th_bv.plf 2021-01-20 14:56:16.883629683 -0700 +@@ -72,7 +72,6 @@ + + (declare bvand bvop2) + (declare bvor bvop2) +-(declare bvor bvop2) + (declare bvxor bvop2) + (declare bvnand bvop2) + (declare bvnor bvop2) +@@ -88,7 +87,6 @@ + (declare bvshl bvop2) + (declare bvlshr bvop2) + (declare bvashr bvop2) +-(declare concat bvop2) + + ; bit vector unary operators + (define bvop1 diff --git a/cvc4.spec b/cvc4.spec index d599b98..aff1ebb 100644 --- a/cvc4.spec +++ b/cvc4.spec @@ -3,7 +3,7 @@ Name: cvc4 Version: 1.8 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Automatic theorem prover for SMT problems # License breakdown: @@ -21,6 +21,8 @@ Source0: https://github.com/CVC4/CVC4/archive/%{version}/%{name}-%{versio Patch0: %{name}-flags.patch # Adapt to cryptominisat 5.7 Patch1: %{name}-cryptominisat.patch +# Remove duplicate declarations, leads to errors with recent LFSC versions +Patch2: %{name}-dup-decl.patch BuildRequires: abc-devel BuildRequires: antlr3-C-devel @@ -245,6 +247,9 @@ export LD_LIBRARY_PATH=%{buildroot}%{_libdir} %{python3_sitearch}/pycvc4* %changelog +* Wed Jan 20 2021 Jerry James - 1.8-3 +- Add -dup-decl patch to fix FTBFS with recent LFSC versions + * Fri Nov 27 2020 Jerry James - 1.8-2 - Rebuild for cryptominisat 5.8.0