Revert "Test performance with CBMC using CaDiCaL 2.0.0"

This reverts commit b7b3b15.
tautschnig · Jul 31, 2024 · 2de6464 · 2de6464
1 parent c968d65
commit 2de6464
Show file tree

Hide file tree

Showing 11 changed files with 1 addition and 20 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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());