From abcb54e7d5447e7385371438d546fa26eca9ea2d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 25 Jul 2024 09:27:10 +0200
Subject: [PATCH] Maintain test execution performance with newer CaDiCaL
 versions (#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                              | 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());