From 0b895adcfd54c906d608eadbce32d6735f653cae Mon Sep 17 00:00:00 2001
From: coord_e <me@coord-e.com>
Date: Thu, 24 Sep 2026 21:05:08 +0900
Subject: [PATCH 1/3] Use latest PCSat

---
 .github/workflows/ci.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 781b3513..3333892e 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -50,8 +50,8 @@ jobs:
           tar --strip-components=1 -xf thrust-pcsat-wrapper.tar.gz
           mv thrust-pcsat-wrapper "$GITHUB_WORKSPACE/tests/thrust-pcsat-wrapper"
         env:
-          PCSAT_URL: https://thrust-ci-public.s3.ap-northeast-1.amazonaws.com/pcsat/thrust-pcsat-wrapper-873d558c6a.tar.gz
-          PCSAT_SHA256: cae6829b40cfde196ae231f4a97eed5b873756cb59619f580934b488c1e7a11a
+          PCSAT_URL: https://thrust-ci-public.s3.ap-northeast-1.amazonaws.com/pcsat/thrust-pcsat-wrapper-49ed9fe340.tar.gz
+          PCSAT_SHA256: 7a606b60050e8e04aece7a58297fcd80055783084996d2f1c9fa99d9d51d6114
       - run: rustup show
       - uses: Swatinem/rust-cache@v2
       - run: cargo test

From c8f600abf435e59ec8df580f0be286dd11246cba Mon Sep 17 00:00:00 2001
From: coord_e <me@coord-e.com>
Date: Thu, 24 Sep 2026 21:05:36 +0900
Subject: [PATCH 2/3] Revert "Remove unstable slice_split_first_mut_loop.rs
 cases for now"

This reverts commit 7d886e09d5647e3dfd22dcc9597b516bc95c7a5c.
---
 tests/ui/fail/slice_split_first_mut_loop.rs | 27 +++++++++++++++++++++
 tests/ui/pass/slice_split_first_mut_loop.rs | 27 +++++++++++++++++++++
 2 files changed, 54 insertions(+)
 create mode 100644 tests/ui/fail/slice_split_first_mut_loop.rs
 create mode 100644 tests/ui/pass/slice_split_first_mut_loop.rs

diff --git a/tests/ui/fail/slice_split_first_mut_loop.rs b/tests/ui/fail/slice_split_first_mut_loop.rs
new file mode 100644
index 00000000..4a068d38
--- /dev/null
+++ b/tests/ui/fail/slice_split_first_mut_loop.rs
@@ -0,0 +1,27 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).len() == 2
+        && (*result)[0] == 10
+        && (*result)[1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+#[thrust::callable]
+fn check() {
+    let sl = slice();
+    let mut s = &mut *sl;
+    while let Some((first, rest)) = s.split_first_mut() {
+        *first = 0;
+        s = rest;
+    }
+    assert!(sl[0] != 0);
+}
+
+fn main() {}
diff --git a/tests/ui/pass/slice_split_first_mut_loop.rs b/tests/ui/pass/slice_split_first_mut_loop.rs
new file mode 100644
index 00000000..ba47b2fe
--- /dev/null
+++ b/tests/ui/pass/slice_split_first_mut_loop.rs
@@ -0,0 +1,27 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).len() == 2
+        && (*result)[0] == 10
+        && (*result)[1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+#[thrust::callable]
+fn check() {
+    let sl = slice();
+    let mut s = &mut *sl;
+    while let Some((first, rest)) = s.split_first_mut() {
+        *first = 0;
+        s = rest;
+    }
+    assert!(sl[0] == 0);
+}
+
+fn main() {}

From bf7ddd3a3ebe3ee1186921535a058f44a20cc2a7 Mon Sep 17 00:00:00 2001
From: coord_e <me@coord-e.com>
Date: Thu, 24 Sep 2026 21:16:50 +0900
Subject: [PATCH 3/3] Extend timeout

---
 tests/ui/fail/slice_split_first_mut_loop.rs | 1 +
 tests/ui/pass/seq_subsequence.rs            | 1 +
 2 files changed, 2 insertions(+)

diff --git a/tests/ui/fail/slice_split_first_mut_loop.rs b/tests/ui/fail/slice_split_first_mut_loop.rs
index 4a068d38..62d8392b 100644
--- a/tests/ui/fail/slice_split_first_mut_loop.rs
+++ b/tests/ui/fail/slice_split_first_mut_loop.rs
@@ -1,6 +1,7 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -C debug-assertions=off
 //@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+//@rustc-env: THRUST_SOLVER_TIMEOUT_SECS=60
 
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
diff --git a/tests/ui/pass/seq_subsequence.rs b/tests/ui/pass/seq_subsequence.rs
index fc1564db..e762be63 100644
--- a/tests/ui/pass/seq_subsequence.rs
+++ b/tests/ui/pass/seq_subsequence.rs
@@ -1,6 +1,7 @@
 //@check-pass
 //@compile-flags: -C debug-assertions=off
 //@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+//@rustc-env: THRUST_SOLVER_TIMEOUT_SECS=60
 
 use thrust_models::model::{Int, Seq};