From 2de6464500c660c358d7abdfd3cec874e28efea3 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 31 Jul 2024 07:45:51 +0000
Subject: [PATCH] Revert "Test performance with CBMC using CaDiCaL 2.0.0"

This reverts commit b7b3b156c1f22f50f009209a4c2847357d95cc4b.
---
 tests/expected/shadow/slices/slice_of_array/test.rs           | 2 +-
 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 --
 11 files changed, 1 insertion(+), 20 deletions(-)

diff --git a/tests/expected/shadow/slices/slice_of_array/test.rs b/tests/expected/shadow/slices/slice_of_array/test.rs
index 39d2956753c0..b5ac3abae126 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(17)]
+#[kani::unwind(31)]
 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 93a29f169f27..f8ebccdac02a 100644
--- a/tests/kani/FloatingPoint/main.rs
+++ b/tests/kani/FloatingPoint/main.rs
@@ -26,7 +26,6 @@ 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 642d984a7e2b..09c630aa94a7 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs
@@ -45,7 +45,6 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
-#[kani::solver(minisat)]
 fn test_towards_inf() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -54,7 +53,6 @@ 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 54ad74c33430..0560a2c55064 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs
@@ -45,7 +45,6 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
-#[kani::solver(minisat)]
 fn test_towards_neg_inf() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -54,7 +53,6 @@ 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 7ffdb5f28747..25e02f45a943 100644
--- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs
@@ -50,7 +50,6 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
-#[kani::solver(minisat)]
 fn test_towards_nearest() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
@@ -89,7 +88,6 @@ 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 bf656512562e..589a44a4d1ac 100644
--- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs
@@ -50,7 +50,6 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
-#[kani::solver(minisat)]
 fn test_towards_nearest() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -89,7 +88,6 @@ 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 53d9d7d5fc73..79a0a4f9be2c 100644
--- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs
@@ -55,7 +55,6 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
-#[kani::solver(minisat)]
 fn test_towards_nearest() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
@@ -94,7 +93,6 @@ 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 de608e7cdb9f..8c8ea583a2d5 100644
--- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs
@@ -55,7 +55,6 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
-#[kani::solver(minisat)]
 fn test_towards_nearest() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -94,7 +93,6 @@ 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 04893727dcfa..8a8780878925 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs
@@ -39,7 +39,6 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
-#[kani::solver(minisat)]
 fn test_towards_closer() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
@@ -62,7 +61,6 @@ 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 cd61e9607646..ddafc45a2e9e 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs
@@ -39,7 +39,6 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
-#[kani::solver(minisat)]
 fn test_towards_closer() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -62,7 +61,6 @@ 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 a8a80672e36b..5fcc8c80606d 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs
@@ -38,7 +38,6 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
-#[kani::solver(minisat)]
 fn test_towards_zero() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -51,7 +50,6 @@ fn test_towards_zero() {
 }
 
 #[kani::proof]
-#[kani::solver(minisat)]
 fn test_diff_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());