Maintain test execution performance with newer CaDiCaL versions (mode…

…l-checking#3381)

CBMC using CaDiCaL 1.9.2 and later have substantially worse performance
on these tests than CaDiCaL 1.7.2, which CBMC 5.95.1 uses. Using MiniSat
will make sure performance remains consistent.

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

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());

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());

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());

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());

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());

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());

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());

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());

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());