From 6d08b20ba87657b2e82ace29f1fa43114861615c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 24 Jul 2024 19:48:08 +0000
Subject: [PATCH] Maintain test execution performance with newer CaDiCaL
 versions

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                              | 1 +
 tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs           | 2 ++
 tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs         | 2 ++
 tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs | 2 ++
 tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs | 2 ++
 tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs           | 2 ++
 tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs           | 2 ++
 tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs         | 2 ++
 tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs         | 2 ++
 tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs         | 2 ++
 10 files changed, 19 insertions(+)

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