Repository: chrjabs/rustsat (language: python)

Issue:
Get solvers to build under windows
Getting the solvers to build under windows seems to be a challenge, since many of them use some GCC / Unix specific features. Get as many of them to compile in windows as possible, and include checks and tests in the CI.


Discussion / hints:
Cadical and Kissat are hard to provide on Windows ([Kissat issue](https://github.com/arminbiere/kissat/issues/7) and [Cadical instructions](https://github.com/arminbiere/cadical/blob/master/BUILD.md)), but Minisat would be a good start so people can still use the crate :)

Fix patch:
diff --git a/.github/workflows/pr-lints.yml b/.github/workflows/pr-lints.yml
index 3eaf6ddd..c6f6daea 100644
--- a/.github/workflows/pr-lints.yml
+++ b/.github/workflows/pr-lints.yml
@@ -1,4 +1,4 @@
-name: Rust
+name: Lints
 
 on:
   pull_request:
diff --git a/README.md b/README.md
index ab82a3f1..b0507aaa 100644
--- a/README.md
+++ b/README.md
@@ -13,7 +13,8 @@ let l1 = instance.new_lit();
 let l2 = instance.new_lit();
 instance.add_binary(l1, l2);
 instance.add_binary(!l1, l2);
-let mut solver = rustsat_cadical::CaDiCaL::default();
+instance.add_unit(l1);
+let mut solver = rustsat_minisat::core::Minisat::default();
 solver.add_cnf(instance.as_cnf().0).unwrap();
 let res = solver.solve().unwrap();
 assert_eq!(res, SolverResult::Sat);
diff --git a/cadical/README.md b/cadical/README.md
index 8103d70f..7a687e44 100644
--- a/cadical/README.md
+++ b/cadical/README.md
@@ -12,16 +12,8 @@ Armin Biere's SAT solver [CaDiCaL](https://github.com/arminbiere/cadical) to be
 ## CaDiCaL Versions
 
 CaDiCaL versions can be selected via cargo crate features.
-The following CaDiCaL versions are available:
-- `v1-7-0`: [Version 1.7.0](https://github.com/arminbiere/cadical/releases/tag/rel-1.7.0)
-- `v1-6-0`: [Version 1.6.0](https://github.com/arminbiere/cadical/releases/tag/rel-1.6.0)
-- `v1-5-6`: [Version 1.5.6](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.6)
-- `v1-5-5`: [Version 1.5.5](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.5)
-- `v1-5-4`: [Version 1.5.4](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.4)
-- `v1-5-3`: [Version 1.5.3](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.3)
-- `v1-5-2`: [Version 1.5.2](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.2)
-- `v1-5-1`: [Version 1.5.1](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.1)
-- `v1-5-0`: [Version 1.5.0](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.0)
+All CaDiCaL versions up to [Version 1.9.4](https://github.com/arminbiere/cadical/releases/tag/rel-1.9.4) are available.
+For the full list of versions and the changelog see [the CaDiCaL releases](https://github.com/arminbiere/cadical/releases).
 
 Without any features selected, the newest version will be used.
 If conflicting CaDiCaL versions are requested, the newest requested version will be selected.
\ No newline at end of file
diff --git a/glucose/Cargo.toml b/glucose/Cargo.toml
index b3d953fa..55275cc4 100644
--- a/glucose/Cargo.toml
+++ b/glucose/Cargo.toml
@@ -14,6 +14,7 @@ build = "build.rs"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [features]
+debug = []
 glucose4-1 = []
 
 [dependencies]
diff --git a/glucose/README.md b/glucose/README.md
index e1776cde..71698769 100644
--- a/glucose/README.md
+++ b/glucose/README.md
@@ -2,6 +2,10 @@
 
 The Glucose SAT solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
 
+## Features
+
+- `debug`: if this feature is enables, the C++ library will be built with debug and check functionality if the Rust project is built in debug mode
+
 ## Glucose Version
 
 The version of Glucose in this crate is Version 4.2.1.
diff --git a/glucose/build.rs b/glucose/build.rs
index 9306b651..6f9ac3a9 100644
--- a/glucose/build.rs
+++ b/glucose/build.rs
@@ -7,7 +7,7 @@ fn main() {
     build(
         "https://github.com/chrjabs/glucose4.git",
         "main",
-        "ce988a0cdc0a7085a8ec08fdc1a67bf19acf70d2",
+        "257eeb2951a481a12d72f83a37d484360cabdcad",
     );
 
     let out_dir = env::var("OUT_DIR").unwrap();
@@ -28,7 +28,12 @@ fn build(repo: &str, branch: &str, commit: &str) {
             .join("libglucose4.a")
             .exists()
     {
-        cmake::build(glucose_dir);
+        let mut conf = cmake::Config::new(glucose_dir);
+        conf.define("BUILD_SYRUP", "OFF");
+        if cfg!(not(feature = "debug")) {
+            conf.profile("Release");
+        }
+        conf.build();
     };
 
     println!("cargo:rustc-link-lib=static=glucose4");
@@ -36,7 +41,7 @@ fn build(repo: &str, branch: &str, commit: &str) {
     #[cfg(target_os = "macos")]
     println!("cargo:rustc-flags=-l dylib=c++");
 
-    #[cfg(not(target_os = "macos"))]
+    #[cfg(not(any(target_os = "macos", target_os = "windows")))]
     println!("cargo:rustc-flags=-l dylib=stdc++");
 }
 
diff --git a/minisat/Cargo.toml b/minisat/Cargo.toml
index 73418a18..42db3d0c 100644
--- a/minisat/Cargo.toml
+++ b/minisat/Cargo.toml
@@ -13,6 +13,9 @@ build = "build.rs"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
+[features]
+debug = []
+
 [dependencies]
 cpu-time = "1.0.0"
 rustsat = { version = "0.4.0", path = "../rustsat", default-features = false }
diff --git a/minisat/README.md b/minisat/README.md
index c5f6f2e9..f54b00e1 100644
--- a/minisat/README.md
+++ b/minisat/README.md
@@ -2,6 +2,10 @@
 
 The Minisat SAT solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
 
+## Features
+
+- `debug`: if this feature is enables, the C++ library will be built with debug and check functionality if the Rust project is built in debug mode
+
 ## Minisat Version
 
 The version of minisat in this crate is Version 2.2.0.
diff --git a/minisat/build.rs b/minisat/build.rs
index 8beead56..557f315c 100644
--- a/minisat/build.rs
+++ b/minisat/build.rs
@@ -7,7 +7,7 @@ fn main() {
     build(
         "https://github.com/chrjabs/minisat.git",
         "master",
-        "f34c822a9106ffed26c429015914b927d4da455c",
+        "f64a4f78eea61927dec9f151650504defba490c1",
     );
 
     let out_dir = env::var("OUT_DIR").unwrap();
@@ -28,7 +28,11 @@ fn build(repo: &str, branch: &str, commit: &str) {
             .join("libminisat.a")
             .exists()
     {
-        cmake::build(minisat_dir);
+        let mut conf = cmake::Config::new(minisat_dir);
+        if cfg!(not(feature = "debug")) {
+            conf.profile("Release");
+        }
+        conf.build();
     };
 
     println!("cargo:rustc-link-lib=static=minisat");
@@ -36,7 +40,7 @@ fn build(repo: &str, branch: &str, commit: &str) {
     #[cfg(target_os = "macos")]
     println!("cargo:rustc-flags=-l dylib=c++");
 
-    #[cfg(not(target_os = "macos"))]
+    #[cfg(not(any(target_os = "macos", target_os = "windows")))]
     println!("cargo:rustc-flags=-l dylib=stdc++");
 }
 
diff --git a/rustsat/Cargo.toml b/rustsat/Cargo.toml
index 6aa489a0..2b37d064 100644
--- a/rustsat/Cargo.toml
+++ b/rustsat/Cargo.toml
@@ -31,7 +31,7 @@ pyo3-build-config = { version = "0.20.0", optional = true }
 
 [dev-dependencies]
 inline-c = "0.1.7"
-rustsat-cadical = { version = "0.2.1", path = "../cadical" }
+rustsat-minisat = { version = "0.2.1", path = "../minisat" }
 
 [features]
 default = [
@@ -52,7 +52,6 @@ all = [
   "compression",
   "rand",
   "fxhash",
-  "pyapi"
 ]
 
 [lib]
diff --git a/rustsat/src/capi.rs b/rustsat/src/capi.rs
index aa83a243..6cb3e63f 100644
--- a/rustsat/src/capi.rs
+++ b/rustsat/src/capi.rs
@@ -227,7 +227,8 @@ pub mod encodings {
             drop(unsafe { Box::from_raw(tot) })
         }
 
-        #[cfg(test)]
+        // TODO: figure out how to get these to work on windows
+        #[cfg(all(test, not(target_os = "windows")))]
         mod tests {
             use inline_c::assert_c;
 
@@ -419,7 +420,8 @@ pub mod encodings {
             drop(unsafe { Box::from_raw(dpw) })
         }
 
-        #[cfg(test)]
+        // TODO: figure out how to get these to work on windows
+        #[cfg(all(test, not(target_os = "windows")))]
         mod tests {
             use inline_c::assert_c;
 
diff --git a/rustsat/src/solvers.rs b/rustsat/src/solvers.rs
index 2b7762d4..82e24ff2 100644
--- a/rustsat/src/solvers.rs
+++ b/rustsat/src/solvers.rs
@@ -135,7 +135,7 @@ pub trait Solve: Extend<Clause> {
     /// ```
     /// # use rustsat::{lit, solvers::{SolverResult, Solve}};
     /// // any other solver crate works the same way
-    /// let mut solver = rustsat_cadical::CaDiCaL::default();
+    /// let mut solver = rustsat_minisat::core::Minisat::default();
     /// solver.add_unit(lit![0]).unwrap();
     /// let res = solver.solve().unwrap();
     /// debug_assert_eq!(res, SolverResult::Sat);
@@ -188,7 +188,7 @@ pub trait Solve: Extend<Clause> {
     /// ```
     /// # use rustsat::{lit, solvers::Solve, types::TernaryVal};
     /// // any other solver crate works the same way
-    /// let mut solver = rustsat_cadical::CaDiCaL::default();
+    /// let mut solver = rustsat_minisat::core::Minisat::default();
     /// solver.add_unit(lit![0]).unwrap();
     /// let res = solver.solve().unwrap();
     /// debug_assert_eq!(solver.lit_val(lit![0]).unwrap(), TernaryVal::True);
diff --git a/tools/Cargo.toml b/tools/Cargo.toml
index 26f5c17b..21889135 100644
--- a/tools/Cargo.toml
+++ b/tools/Cargo.toml
@@ -13,7 +13,8 @@ readme = "README.md"
 
 [dependencies]
 rustsat = { version = "0.4.0", path = "../rustsat", features = ["compression", "multiopt", "rand", "internals"] }
-rustsat-cadical = { version = "0.2.1", path = "../cadical" }
+rustsat-cadical = { version = "0.2.1", path = "../cadical", optional = true }
+rustsat-minisat = { version = "0.2.1", path = "../minisat", optional = true }
 clap = { version = "4.2.4", features = ["derive", "cargo"] }
 concolor-clap = { version = "0.1.0" }
 termcolor = { version = "1.2.0" }
@@ -22,6 +23,11 @@ nom = "7.1.3"
 rand = "0.8.5"
 rand_chacha = "0.3.1"
 
+[features]
+default = ["minisat"]
+minisat = ["dep:rustsat-minisat"]
+cadical = ["dep:rustsat-cadical"]
+
 [[bin]]
 name = "enumerator"
 
diff --git a/tools/src/bin/enumerator.rs b/tools/src/bin/enumerator.rs
index 3f110b8b..b885503f 100644
--- a/tools/src/bin/enumerator.rs
+++ b/tools/src/bin/enumerator.rs
@@ -52,7 +52,7 @@ fn main() {
         SatInstance::from_dimacs_path(in_path).expect("error parsing the input file");
     let (cnf, vm) = inst.as_cnf();
 
-    let mut solver = rustsat_cadical::CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     solver
         .reserve(vm.max_var().expect("no variables in instance"))
         .expect("error reserving memory in solver");
diff --git a/tools/src/lib.rs b/tools/src/lib.rs
index 5c9923c9..c72fe0e1 100644
--- a/tools/src/lib.rs
+++ b/tools/src/lib.rs
@@ -8,3 +8,8 @@ pub mod encodings {
     pub mod clustering;
     pub mod knapsack;
 }
+
+#[cfg(feature = "cadical")]
+pub type Solver = rustsat_cadical::CaDiCaL<'static, 'static>;
+#[cfg(all(not(feature = "cadical"), feature = "minisat"))]
+pub type Solver = rustsat_minisat::core::Minisat;


Test patch:
diff --git a/.github/workflows/check-test.yml b/.github/workflows/check-test.yml
index c4901efb..ceba3811 100644
--- a/.github/workflows/check-test.yml
+++ b/.github/workflows/check-test.yml
@@ -1,4 +1,4 @@
-name: Rust
+name: Check & Test
 
 on:
   push:
@@ -10,11 +10,11 @@ env:
   CARGO_TERM_COLOR: always
 
 jobs:
-  check:
-    name: Check
+  check-test:
+    name: Build and test
     strategy:
       matrix:
-        os: [ubuntu-latest, macos-latest]
+        os: [ubuntu-latest, macos-latest, windows-latest]
     runs-on: ${{ matrix.os }}
     steps:
       - name: Checkout sources
@@ -22,25 +22,22 @@ jobs:
       - name: Install stable toolchain
         uses: dtolnay/rust-toolchain@stable
       - uses: Swatinem/rust-cache@v2
-      - name: Run cargo check
-        run: cargo check --workspace --verbose --features=all
-          
-  test:
-    name: Test suite
-    strategy:
-      matrix:
-        os: [ubuntu-latest, macos-latest]
-    runs-on: ${{ matrix.os }}
-    steps:
-      - name: Checkout sources
-        uses: actions/checkout@v4
-      - name: Install stable toolchain
-        uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
-      - name: Build project
-        run: cargo build
-      - name: Run cargo test suite
-        run: cargo test --workspace --verbose
+      - name: Cargo build
+        shell: bash
+        run: |
+          if [ "$RUNNER_OS" == "Windows" ]; then
+            cargo build --workspace --verbose --features=all --exclude rustsat-kissat --exclude rustsat-cadical
+          else 
+            cargo build --workspace --verbose --features=all
+          fi
+      - name: Cargo test
+        shell: bash
+        run: |
+          if [ "$RUNNER_OS" == "Windows" ]; then
+            RUST_BACKTRACE=1 cargo test --workspace --verbose --features=all --exclude rustsat-kissat --exclude rustsat-cadical
+          else 
+            RUST_BACKTRACE=1 cargo test --workspace --verbose --features=all
+          fi
 
   doc:
     name: Doc
diff --git a/tools/tests/am1_encodings.rs b/tools/tests/am1_encodings.rs
index bb3bcfe7..7fbc2ccd 100644
--- a/tools/tests/am1_encodings.rs
+++ b/tools/tests/am1_encodings.rs
@@ -9,12 +9,11 @@ use rustsat::{
     types::Lit,
     var,
 };
-use rustsat_cadical::CaDiCaL;
 
-use rustsat_tools::{test_all, test_assignment};
+use rustsat_tools::{test_all, test_assignment, Solver};
 
 fn test_am1<AM1: Encode + From<Vec<Lit>>>() {
-    let mut solver = CaDiCaL::default();
+    let mut solver = Solver::default();
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![3]);
 
diff --git a/tools/tests/card_encodings.rs b/tools/tests/card_encodings.rs
index e47b95f8..ced34457 100644
--- a/tools/tests/card_encodings.rs
+++ b/tools/tests/card_encodings.rs
@@ -13,11 +13,10 @@ use rustsat::{
     types::Lit,
     var,
 };
-use rustsat_cadical::CaDiCaL;
 
 fn test_inc_both_card<CE: BoundBothIncremental + Extend<Lit> + Default>() {
     // Set up instance
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     solver.add_clause(clause![lit![0], lit![1]]).unwrap();
     solver.add_clause(clause![lit![1]]).unwrap();
     solver.add_clause(clause![lit![1], lit![2]]).unwrap();
@@ -81,7 +80,7 @@ fn test_inc_both_card<CE: BoundBothIncremental + Extend<Lit> + Default>() {
 
 fn test_inc_ub_card<CE: BoundUpperIncremental + Extend<Lit> + Default>() {
     // Set up instance
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     solver.add_clause(clause![lit![0], lit![1]]).unwrap();
     solver.add_clause(clause![lit![1]]).unwrap();
     solver.add_clause(clause![lit![1], lit![2]]).unwrap();
@@ -141,7 +140,7 @@ fn test_inc_ub_card<CE: BoundUpperIncremental + Extend<Lit> + Default>() {
 
 fn test_both_card<CE: BoundBoth + From<Vec<Lit>>>() {
     // Set up instance
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     solver.add_clause(clause![lit![0], lit![1]]).unwrap();
     solver.add_clause(clause![lit![1]]).unwrap();
     solver.add_clause(clause![lit![1], lit![2]]).unwrap();
@@ -174,7 +173,7 @@ fn test_both_card<CE: BoundBoth + From<Vec<Lit>>>() {
 /// Requires a cardinality encoding with upper and lower bounding functionality
 fn test_both_card_min_enc<CE: BoundBoth + From<Vec<Lit>>>() {
     // Set up instance
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![4]);
 
@@ -270,7 +269,7 @@ fn dbtot_inc_ub() {
 use rustsat_tools::{test_all, test_assignment};
 
 fn test_ub_exhaustive<CE: BoundUpperIncremental + From<Vec<Lit>>>() {
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     let mut enc = CE::from(vec![lit![0], lit![1], lit![2], lit![3]]);
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![4]);
@@ -392,7 +391,7 @@ fn test_ub_exhaustive<CE: BoundUpperIncremental + From<Vec<Lit>>>() {
 }
 
 fn test_both_exhaustive<CE: BoundBothIncremental + From<Vec<Lit>>>() {
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     let mut enc = CE::from(vec![lit![0], lit![1], lit![2], lit![3]]);
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![4]);
diff --git a/tools/tests/cnf.rs b/tools/tests/cnf.rs
index 07d65207..06787e1e 100644
--- a/tools/tests/cnf.rs
+++ b/tools/tests/cnf.rs
@@ -7,20 +7,19 @@ use rustsat::{
     },
     types::Lit,
 };
-use rustsat_cadical::CaDiCaL;
-use rustsat_tools::{test_all, test_assignment};
+use rustsat_tools::{test_all, test_assignment, Solver};
 
 #[test]
 fn cnf_implications() {
     let mut cnf = Cnf::new();
     cnf.add_lit_impl_lit(lit![0], lit![1]);
-    let mut solver = CaDiCaL::default();
+    let mut solver = Solver::default();
     solver.add_cnf(cnf).unwrap();
     test_all!(solver, Vec::<Lit>::new(), Sat, Unsat, Sat, Sat);
 
     let mut cnf = Cnf::new();
     cnf.add_lit_impl_clause(lit![0], &[lit![1], lit![2]]);
-    let mut solver = CaDiCaL::default();
+    let mut solver = Solver::default();
     solver.add_cnf(cnf).unwrap();
     test_all!(
         solver,
@@ -37,7 +36,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_lit_impl_cube(lit![0], &[lit![1], lit![2]]);
-    let mut solver = CaDiCaL::default();
+    let mut solver = Solver::default();
     solver.add_cnf(cnf).unwrap();
     test_all!(
         solver,
@@ -54,7 +53,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_cube_impl_lit(&[lit![0], lit![1]], lit![2]);
-    let mut solver = CaDiCaL::default();
+    let mut solver = Solver::default();
     solver.add_cnf(cnf).unwrap();
     test_all!(
         solver,
@@ -71,7 +70,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_clause_impl_lit(&[lit![0], lit![1]], lit![2]);
-    let mut solver = CaDiCaL::default();
+    let mut solver = Solver::default();
     solver.add_cnf(cnf).unwrap();
     test_all!(
         solver,
@@ -88,7 +87,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_cube_impl_clause(&[lit![0], lit![1]], &[lit![2], lit![3]]);
-    let mut solver = CaDiCaL::default();
+    let mut solver = Solver::default();
     solver.add_cnf(cnf).unwrap();
     test_all!(
         solver,
@@ -113,7 +112,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_clause_impl_clause(&[lit![0], lit![1]], &[lit![2], lit![3]]);
-    let mut solver = CaDiCaL::default();
+    let mut solver = Solver::default();
     solver.add_cnf(cnf).unwrap();
     test_all!(
         solver,
@@ -138,7 +137,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_clause_impl_cube(&[lit![0], lit![1]], &[lit![2], lit![3]]);
-    let mut solver = CaDiCaL::default();
+    let mut solver = Solver::default();
     solver.add_cnf(cnf).unwrap();
     test_all!(
         solver,
@@ -163,7 +162,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_cube_impl_cube(&[lit![0], lit![1]], &[lit![2], lit![3]]);
-    let mut solver = CaDiCaL::default();
+    let mut solver = Solver::default();
     solver.add_cnf(cnf).unwrap();
     test_all!(
         solver,
diff --git a/tools/tests/compression.rs b/tools/tests/compression.rs
index 1f831c6b..057d57f2 100644
--- a/tools/tests/compression.rs
+++ b/tools/tests/compression.rs
@@ -3,25 +3,25 @@ use rustsat::{
     solvers::Solve,
     solvers::SolverResult,
 };
-use rustsat_cadical::CaDiCaL;
 
 #[test]
 fn small_sat_instance_gzip() {
     let inst: SatInstance<BasicVarManager> =
         SatInstance::from_dimacs_path("./data/AProVE11-12.cnf.gz").unwrap();
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     solver.add_cnf(inst.as_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Sat);
 }
 
 #[test]
+#[ignore]
 fn small_unsat_instance_gzip() {
     let inst: SatInstance<BasicVarManager> = SatInstance::from_dimacs_path(
         "./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf.gz",
     )
     .unwrap();
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     solver.add_cnf(inst.as_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Unsat);
@@ -31,19 +31,20 @@ fn small_unsat_instance_gzip() {
 fn small_sat_instance_bz2() {
     let inst: SatInstance<BasicVarManager> =
         SatInstance::from_dimacs_path("./data/AProVE11-12.cnf.bz2").unwrap();
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     solver.add_cnf(inst.as_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Sat);
 }
 
 #[test]
+#[ignore]
 fn small_unsat_instance_bz2() {
     let inst: SatInstance<BasicVarManager> = SatInstance::from_dimacs_path(
         "./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf.bz2",
     )
     .unwrap();
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     solver.add_cnf(inst.as_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Unsat);
diff --git a/tools/tests/constraints.rs b/tools/tests/constraints.rs
index 0b63d5c9..37aa58e7 100644
--- a/tools/tests/constraints.rs
+++ b/tools/tests/constraints.rs
@@ -7,7 +7,6 @@ use rustsat::{
         RsHashMap,
     },
 };
-use rustsat_cadical::CaDiCaL;
 
 macro_rules! test_card {
     ( $constr:expr, $sat_assump:expr, $unsat_assump:expr ) => {{
@@ -15,7 +14,7 @@ macro_rules! test_card {
         inst.add_card_constr($constr);
         let (cnf, _) = inst.as_cnf();
         println!("{:?}", cnf);
-        let mut solver = CaDiCaL::default();
+        let mut solver = rustsat_tools::Solver::default();
         solver.add_cnf(cnf).unwrap();
         assert_eq!(
             solver.solve_assumps($sat_assump).unwrap(),
@@ -34,7 +33,7 @@ macro_rules! test_pb {
         inst.add_pb_constr($constr);
         let (cnf, _) = inst.as_cnf();
         println!("{:?}", cnf);
-        let mut solver = CaDiCaL::default();
+        let mut solver = rustsat_tools::Solver::default();
         solver.add_cnf(cnf).unwrap();
         assert_eq!(
             solver.solve_assumps($sat_assump).unwrap(),
diff --git a/tools/tests/opb.rs b/tools/tests/opb.rs
index 3749ad16..8eadd4d4 100644
--- a/tools/tests/opb.rs
+++ b/tools/tests/opb.rs
@@ -2,7 +2,6 @@ use rustsat::{
     instances::{fio::opb::Options, SatInstance},
     solvers::{Solve, SolverResult},
 };
-use rustsat_cadical::CaDiCaL;
 
 use rustsat::instances::MultiOptInstance;
 use rustsat::types::RsHashMap;
@@ -17,7 +16,7 @@ macro_rules! opb_test {
         let inst: SatInstance = SatInstance::from_opb_path($path, Options::default()).unwrap();
         let (cnf, _) = inst.as_cnf();
         println!("{:?}", cnf);
-        let mut solver = CaDiCaL::default();
+        let mut solver = rustsat_tools::Solver::default();
         solver.add_cnf(cnf).unwrap();
         assert_eq!(solver.solve().unwrap(), $expect);
     }};
diff --git a/tools/tests/pb_encodings.rs b/tools/tests/pb_encodings.rs
index c7f2b9c2..a688cd14 100644
--- a/tools/tests/pb_encodings.rs
+++ b/tools/tests/pb_encodings.rs
@@ -17,11 +17,10 @@ use rustsat::{
     types::{Lit, RsHashMap},
     var,
 };
-use rustsat_cadical::CaDiCaL;
 
 fn test_inc_pb_ub<PBE: BoundUpperIncremental + Extend<(Lit, usize)> + Default>() {
     // Set up instance
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     solver.add_clause(clause![lit![0], lit![1]]).unwrap();
     solver.add_clause(clause![lit![1]]).unwrap();
     solver.add_clause(clause![lit![1], lit![2]]).unwrap();
@@ -100,7 +99,7 @@ fn test_inc_pb_ub<PBE: BoundUpperIncremental + Extend<(Lit, usize)> + Default>()
 
 fn test_pb_eq<PBE: BoundBothIncremental + From<RsHashMap<Lit, usize>>>() {
     // Set up instance
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![3]);
 
@@ -155,7 +154,7 @@ fn test_pb_eq<PBE: BoundBothIncremental + From<RsHashMap<Lit, usize>>>() {
 
 fn test_pb_lb<PBE: BoundLower + From<RsHashMap<Lit, usize>>>() {
     // Set up instance
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     solver
         .add_clause(clause![!lit![0], !lit![1], !lit![2]])
         .unwrap();
@@ -184,7 +183,7 @@ fn test_pb_lb<PBE: BoundLower + From<RsHashMap<Lit, usize>>>() {
 
 fn test_pb_ub_min_enc<PBE: BoundUpper + From<RsHashMap<Lit, usize>>>() {
     // Set up instance
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![4]);
 
@@ -282,7 +281,7 @@ fn test_ub_exhaustive<PBE: BoundUpperIncremental + From<RsHashMap<Lit, usize>>>(
     weights: [usize; 4],
     decreasing: bool,
 ) {
-    let mut solver = CaDiCaL::default();
+    let mut solver = rustsat_tools::Solver::default();
     let mut lits = RsHashMap::default();
     lits.insert(lit![0], weights[0]);
     lits.insert(lit![1], weights[1]);