diff --git a/tests/expected/shadow/slices/slice_of_array/test.rs b/tests/expected/shadow/slices/slice_of_array/test.rs
index b5ac3abae126..39d2956753c0 100644
--- a/tests/expected/shadow/slices/slice_of_array/test.rs
+++ b/tests/expected/shadow/slices/slice_of_array/test.rs
@@ -13,7 +13,7 @@ const N: usize = 16;
 static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(false);
 
 #[kani::proof]
-#[kani::unwind(31)]
+#[kani::unwind(17)]
 fn check_slice_init() {
     let arr: [char; N] = kani::any();
     // tag every element of the array as initialized
diff --git a/tests/kani/FloatingPoint/main.rs b/tests/kani/FloatingPoint/main.rs
index f8ebccdac02a..93a29f169f27 100644
--- a/tests/kani/FloatingPoint/main.rs
+++ b/tests/kani/FloatingPoint/main.rs
@@ -26,6 +26,7 @@ macro_rules! test_floats {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn main() {
     assert!(1.1 == 1.1 * 1.0);
     assert!(1.1 != 1.11 / 1.0);
diff --git a/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs b/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs
index 09c630aa94a7..642d984a7e2b 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs
@@ -45,6 +45,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_inf() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -53,6 +54,7 @@ fn test_towards_inf() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs b/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs
index 0560a2c55064..54ad74c33430 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs
@@ -45,6 +45,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_neg_inf() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -53,6 +54,7 @@ fn test_towards_neg_inf() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs
index 25e02f45a943..7ffdb5f28747 100644
--- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs
@@ -50,6 +50,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_nearest() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
@@ -88,6 +89,7 @@ fn test_towards_nearest() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_half_one() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs
index 589a44a4d1ac..bf656512562e 100644
--- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs
@@ -50,6 +50,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_nearest() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -88,6 +89,7 @@ fn test_towards_nearest() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_half_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs
index 79a0a4f9be2c..53d9d7d5fc73 100644
--- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs
@@ -55,6 +55,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_nearest() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
@@ -93,6 +94,7 @@ fn test_towards_nearest() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_half_one() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs
index 8c8ea583a2d5..de608e7cdb9f 100644
--- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs
@@ -55,6 +55,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_nearest() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -93,6 +94,7 @@ fn test_towards_nearest() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_half_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs b/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs
index 8a8780878925..04893727dcfa 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs
@@ -39,6 +39,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_closer() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
@@ -61,6 +62,7 @@ fn test_towards_closer() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_half_one() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs b/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs
index ddafc45a2e9e..cd61e9607646 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs
@@ -39,6 +39,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_closer() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -61,6 +62,7 @@ fn test_towards_closer() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_half_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs b/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs
index 5fcc8c80606d..a8a80672e36b 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs
@@ -38,6 +38,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_zero() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -50,6 +51,7 @@ fn test_towards_zero() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());