Use latest PCSat

.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

tests/ui/fail/slice_split_first_mut_loop.rs

@@ -0,0 +1,28 @@
+//@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)]
+#[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() {}

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};
 

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() {}