From 31938565c64c8ae0226b35a0c9b166af510e4a70 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Tue, 12 Dec 2023 06:41:10 -0500
Subject: [PATCH] Work around bitwuzla/bitwuzla#96 on Ubuntu 20.04

Sadly, Ubuntu 20.04's version of `glibc` is susceptible to
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=58909. We work around the issue
by applying a workaround taken from
https://bbs.archlinux.org/viewtopic.php?pid=2022393#p2022393.
---
 .github/ci.sh                            |  7 ++++++
 .github/workflows/ci.yml                 |  4 +++
 patches/bitwuzla-T58909-workaround.patch | 31 ++++++++++++++++++++++++
 3 files changed, 42 insertions(+)
 create mode 100644 patches/bitwuzla-T58909-workaround.patch

diff --git a/.github/ci.sh b/.github/ci.sh
index 602ac24..4221635 100755
--- a/.github/ci.sh
+++ b/.github/ci.sh
@@ -44,6 +44,13 @@ build_abc() {
 
 build_bitwuzla() {
   pushd repos/bitwuzla
+  if [ "$GITHUB_MATRIX_OS" == 'ubuntu-20.04' ] ; then
+    # Ubuntu 20.04 uses an older version of glibc that is susceptible to
+    # https://gcc.gnu.org/bugzilla/show_bug.cgi?id=58909, so we must apply a
+    # crude workaround for it. Thankfully, this is not required for the version
+    # of glibc that ships with Ubuntu 22.04.
+    patch -p1 -i $PATCHES/bitwuzla-T58909-workaround.patch
+  fi
   ./configure.py
   cd build
   ninja -j4
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 4ec6418..a51db78 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -83,11 +83,15 @@ jobs:
       - name: build_solver (non-Windows)
         shell: bash
         run: .github/ci.sh build_${{ matrix.solver }}
+        env:
+          GITHUB_MATRIX_OS: ${{ matrix.os }}
         if: runner.os != 'Windows'
 
       - name: build_solver (Windows)
         shell: msys2 {0}
         run: .github/ci.sh build_${{ matrix.solver }}
+        env:
+          GITHUB_MATRIX_OS: ${{ matrix.os }}
         if: runner.os == 'Windows'
 
       - uses: actions/upload-artifact@v2
diff --git a/patches/bitwuzla-T58909-workaround.patch b/patches/bitwuzla-T58909-workaround.patch
new file mode 100644
index 0000000..b19deef
--- /dev/null
+++ b/patches/bitwuzla-T58909-workaround.patch
@@ -0,0 +1,31 @@
+diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp
+index 45238be4..f1ee25cb 100644
+--- a/src/main/time_limit.cpp
++++ b/src/main/time_limit.cpp
+@@ -6,6 +6,7 @@
+ #include <cstdlib>
+ #include <iostream>
+ #include <thread>
++#include <pthread.h>
+
+ namespace bzla::main {
+
+@@ -15,6 +16,18 @@ std::condition_variable cv;
+ std::mutex cv_m;
+ bool time_limit_set = false;
+
++// Work around https://gcc.gnu.org/bugzilla/show_bug.cgi?id=58909
++// on old versions of glibc
++void pthread_cond_bug() {
++  pthread_cond_signal((pthread_cond_t *) nullptr);
++  pthread_cond_init((pthread_cond_t *) nullptr,
++                    (const pthread_condattr_t *) nullptr);
++  pthread_cond_destroy((pthread_cond_t *) nullptr);
++  pthread_cond_timedwait((pthread_cond_t *) nullptr, (pthread_mutex_t *)
++                         nullptr, (const struct timespec *) nullptr);
++  pthread_cond_wait((pthread_cond_t *) nullptr, (pthread_mutex_t *) nullptr);
++}
++
+ void
+ timeout_reached()
+ {