From 56cce94522c01ed0201bf8b3d66b5eebfb5c66be Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Sat, 22 Jan 2022 16:14:49 -0700
Subject: [PATCH] Add -const-map-key patch to fix FTBFS.

---
 cvc4-const-map-key.patch | 47 ++++++++++++++++++++++++++++++++++++++++
 cvc4.rpmlintrc           |  8 -------
 cvc4.spec                |  7 +++++-
 3 files changed, 53 insertions(+), 9 deletions(-)
 create mode 100644 cvc4-const-map-key.patch
 delete mode 100644 cvc4.rpmlintrc

diff --git a/cvc4-const-map-key.patch b/cvc4-const-map-key.patch
new file mode 100644
index 0000000..ad64595
--- /dev/null
+++ b/cvc4-const-map-key.patch
@@ -0,0 +1,47 @@
+--- src/context/cdinsert_hashmap.h.orig	2020-06-19 10:59:27.000000000 -0600
++++ src/context/cdinsert_hashmap.h	2022-01-22 15:49:35.129038124 -0700
+@@ -57,7 +57,7 @@ private:
+   /** A list of the keys in the map maintained as a stack. */
+   KeyVec d_keys;
+ 
+-  using HashMap = std::unordered_map<const Key, const Data, HashFcn>;
++  using HashMap = std::unordered_map<Key, const Data, HashFcn>;
+   /** The hash_map used for element lookup. */
+   HashMap d_hashMap;
+ 
+@@ -95,7 +95,7 @@ public:
+    * See hash_map::find()
+    */
+   const_iterator find(const Key& k) const{
+-    return d_hashMap.find(k);
++    return d_hashMap.find(const_cast<Key&>(k));
+   }
+ 
+   /** Returns an iterator to the start of the set of keys. */
+@@ -114,7 +114,7 @@ public:
+ 
+   /** Returns true if k is a mapped key. */
+   bool contains(const Key& k) const {
+-    return find(k) != end();
++    return find(const_cast<Key&>(k)) != end();
+   }
+ 
+   /**
+@@ -122,7 +122,7 @@ public:
+    * This must succeed.
+    */
+   const Data& operator[](const Key& k) const {
+-    const_iterator ci = find(k);
++    const_iterator ci = find(const_cast<Key&>(k));
+     Assert(ci != end());
+     return (*ci).second;
+   }
+@@ -361,7 +361,7 @@ public:
+     * the context.
+     */
+   const_iterator find(const Key& k) const {
+-    return d_insertMap->find(k);
++    return d_insertMap->find(const_cast<Key&>(k));
+   }
+ 
+   /**
diff --git a/cvc4.rpmlintrc b/cvc4.rpmlintrc
deleted file mode 100644
index da0309f..0000000
--- a/cvc4.rpmlintrc
+++ /dev/null
@@ -1,8 +0,0 @@
-# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON
-# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors
-
-# The dictionary lacks some technical words
-addFilter(r'spelling-error .* (dually|prover|satisfiability)')
-
-# Documentation is in the main package
-addFilter(r'^cvc4-(java|libs|python3)\.[^:]+: W: no-documentation')
diff --git a/cvc4.spec b/cvc4.spec
index 87471c1..461be9d 100644
--- a/cvc4.spec
+++ b/cvc4.spec
@@ -25,12 +25,14 @@ Patch0:         %{name}-flags.patch
 Patch1:         %{name}-cryptominisat.patch
 # Remove duplicate declarations, leads to errors with recent LFSC versions
 Patch2:         %{name}-dup-decl.patch
-
 # Just use the default linker specied by the distro. ld.gold was the
 # new kid on the block a while ago, primarily offering higher link
 # speeds. But it has aged, and has less features than ld.bfd. Let's
 # use ld.bfd so that package notes work without workarounds.
 Patch3:         %{name}-do-not-use-gold.diff
+# Change map keys from const to non-const
+# https://bugzilla.redhat.com/show_bug.cgi?id=2043767
+Patch4:         %{name}-const-map-key.patch
 
 BuildRequires:  abc-devel
 BuildRequires:  antlr3-C-devel
@@ -260,6 +262,9 @@ export LD_LIBRARY_PATH=%{buildroot}%{_libdir}
 %{python3_sitearch}/pycvc4*
 
 %changelog
+* Sat Jan 22 2022 Jerry James <loganjerry@gmail.com> - 1.8-8
+- Add -const-map-key patch to fix FTBFS
+
 * Thu Jan 20 2022 Fedora Release Engineering <releng@fedoraproject.org> - 1.8-8
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
 - Use the default linker