Repository: chrjabs/rustsat (language: python)

Issue:
SatInstance::to_dimacs_path slow (unbuffered)
Some benchmarks on macOS (using a 23MB uncompressed CNF file):

This took ≈ 30 seconds:
```
instance.to_dimacs_path(filename)?;
```

This also took ≈ 30 seconds:
```
let mut f = File::create(filename)?;
instance.to_dimacs(&mut f)?;
```

But this was only ≈ 0.2 seconds:
```
let f = File::create(filename)?;
let mut f = BufWriter::new(f);
instance.to_dimacs(&mut f)?;
```

It looks like `to_dimacs_path` should wrap things in `BufWriter`; now it is apparently doing just `File::create` + `to_dimacs`, which can be very slow.
rustsat_minisat::simp segmentation fault
Sample code:

```
use rustsat::instances::SatInstance;
use rustsat::solvers::Solve;
use std::error::Error;
use std::result::Result;

fn main() -> Result<(), Box<dyn Error>> {
    let instance: SatInstance = SatInstance::from_dimacs_path("example.txt")?;
    let mut solver = rustsat_minisat::simp::Minisat::default();
    solver.add_cnf(instance.as_cnf().0)?;
    println!("solving...");
    let res = solver.solve()?;
    println!("{res}");
    Ok(())
}
```

Input file: [example.txt](https://github.com/chrjabs/rustsat/files/14796073/example.txt)

This seems to crash every time with a "Segmentation fault" right after it prints "solving...". Tried these systems, with the same result:
- Intel iMac with macOS 12.7.4
- Apple M3 MacBook Pro with macOS 14.4
- some random Intel x86 Linux 

It works fine if I change `rustsat_minisat::simp` to e.g. `rustsat_minisat::core` (or any other solver).

Versions:
- Rust 1.77.0
- rustsat 0.4.3
- rustsat-minisat 0.2.4


Discussion / hints:

Fix patch:
diff --git a/data/minisat-segfault.cnf b/data/minisat-segfault.cnf
new file mode 100755
index 00000000..d68bd433
--- /dev/null
+++ b/data/minisat-segfault.cnf
@@ -0,0 +1,465 @@
+c this instance caused a segfault in minisat simp
+c https://github.com/chrjabs/rustsat/issues/74
+p cnf 156 462
+2 0
+3 0
+4 0
+5 0
+7 0
+8 0
+9 0
+10 0
+12 0
+13 0
+14 0
+15 0
+21 22 23 24 0
+-1 -21 17 0
+-1 -22 18 0
+-1 -23 19 0
+-1 -24 20 0
+25 26 27 28 0
+-2 -25 17 0
+-2 -26 18 0
+-2 -27 19 0
+-2 -28 20 0
+29 30 31 32 0
+-3 -29 17 0
+-3 -30 18 0
+-3 -31 19 0
+-3 -32 20 0
+33 34 35 36 0
+-4 -33 17 0
+-4 -34 18 0
+-4 -35 19 0
+-4 -36 20 0
+41 42 43 44 0
+-5 -41 37 0
+-5 -42 38 0
+-5 -43 39 0
+-5 -44 40 0
+45 46 47 48 0
+-6 -45 37 0
+-6 -46 38 0
+-6 -47 39 0
+-6 -48 40 0
+49 50 51 52 0
+-7 -49 37 0
+-7 -50 38 0
+-7 -51 39 0
+-7 -52 40 0
+53 54 55 56 0
+-8 -53 37 0
+-8 -54 38 0
+-8 -55 39 0
+-8 -56 40 0
+61 62 63 64 0
+-9 -61 57 0
+-9 -62 58 0
+-9 -63 59 0
+-9 -64 60 0
+65 66 67 68 0
+-10 -65 57 0
+-10 -66 58 0
+-10 -67 59 0
+-10 -68 60 0
+69 70 71 72 0
+-11 -69 57 0
+-11 -70 58 0
+-11 -71 59 0
+-11 -72 60 0
+73 74 75 76 0
+-12 -73 57 0
+-12 -74 58 0
+-12 -75 59 0
+-12 -76 60 0
+81 82 83 84 0
+-13 -81 77 0
+-13 -82 78 0
+-13 -83 79 0
+-13 -84 80 0
+85 86 87 88 0
+-14 -85 77 0
+-14 -86 78 0
+-14 -87 79 0
+-14 -88 80 0
+89 90 91 92 0
+-15 -89 77 0
+-15 -90 78 0
+-15 -91 79 0
+-15 -92 80 0
+93 94 95 96 0
+-16 -93 77 0
+-16 -94 78 0
+-16 -95 79 0
+-16 -96 80 0
+-1 -21 -17 97 0
+-1 -21 -18 98 0
+-1 -21 -19 99 0
+-1 -21 -20 100 0
+-1 -22 -17 101 0
+-1 -22 -18 102 0
+-1 -22 -19 103 0
+-1 -22 -20 104 0
+-1 -23 -17 105 0
+-1 -23 -18 106 0
+-1 -23 -19 107 0
+-1 -23 -20 108 0
+-1 -24 -17 109 0
+-1 -24 -18 110 0
+-1 -24 -19 111 0
+-1 -24 -20 112 0
+-2 -25 -37 97 0
+-2 -25 -38 98 0
+-2 -25 -39 99 0
+-2 -25 -40 100 0
+-2 -26 -37 101 0
+-2 -26 -38 102 0
+-2 -26 -39 103 0
+-2 -26 -40 104 0
+-2 -27 -37 105 0
+-2 -27 -38 106 0
+-2 -27 -39 107 0
+-2 -27 -40 108 0
+-2 -28 -37 109 0
+-2 -28 -38 110 0
+-2 -28 -39 111 0
+-2 -28 -40 112 0
+-3 -29 -57 97 0
+-3 -29 -58 98 0
+-3 -29 -59 99 0
+-3 -29 -60 100 0
+-3 -30 -57 101 0
+-3 -30 -58 102 0
+-3 -30 -59 103 0
+-3 -30 -60 104 0
+-3 -31 -57 105 0
+-3 -31 -58 106 0
+-3 -31 -59 107 0
+-3 -31 -60 108 0
+-3 -32 -57 109 0
+-3 -32 -58 110 0
+-3 -32 -59 111 0
+-3 -32 -60 112 0
+-4 -33 -77 97 0
+-4 -33 -78 98 0
+-4 -33 -79 99 0
+-4 -33 -80 100 0
+-4 -34 -77 101 0
+-4 -34 -78 102 0
+-4 -34 -79 103 0
+-4 -34 -80 104 0
+-4 -35 -77 105 0
+-4 -35 -78 106 0
+-4 -35 -79 107 0
+-4 -35 -80 108 0
+-4 -36 -77 109 0
+-4 -36 -78 110 0
+-4 -36 -79 111 0
+-4 -36 -80 112 0
+-5 -41 -17 97 0
+-5 -41 -18 98 0
+-5 -41 -19 99 0
+-5 -41 -20 100 0
+-5 -42 -17 101 0
+-5 -42 -18 102 0
+-5 -42 -19 103 0
+-5 -42 -20 104 0
+-5 -43 -17 105 0
+-5 -43 -18 106 0
+-5 -43 -19 107 0
+-5 -43 -20 108 0
+-5 -44 -17 109 0
+-5 -44 -18 110 0
+-5 -44 -19 111 0
+-5 -44 -20 112 0
+-6 -45 -37 97 0
+-6 -45 -38 98 0
+-6 -45 -39 99 0
+-6 -45 -40 100 0
+-6 -46 -37 101 0
+-6 -46 -38 102 0
+-6 -46 -39 103 0
+-6 -46 -40 104 0
+-6 -47 -37 105 0
+-6 -47 -38 106 0
+-6 -47 -39 107 0
+-6 -47 -40 108 0
+-6 -48 -37 109 0
+-6 -48 -38 110 0
+-6 -48 -39 111 0
+-6 -48 -40 112 0
+-7 -49 -57 97 0
+-7 -49 -58 98 0
+-7 -49 -59 99 0
+-7 -49 -60 100 0
+-7 -50 -57 101 0
+-7 -50 -58 102 0
+-7 -50 -59 103 0
+-7 -50 -60 104 0
+-7 -51 -57 105 0
+-7 -51 -58 106 0
+-7 -51 -59 107 0
+-7 -51 -60 108 0
+-7 -52 -57 109 0
+-7 -52 -58 110 0
+-7 -52 -59 111 0
+-7 -52 -60 112 0
+-8 -53 -77 97 0
+-8 -53 -78 98 0
+-8 -53 -79 99 0
+-8 -53 -80 100 0
+-8 -54 -77 101 0
+-8 -54 -78 102 0
+-8 -54 -79 103 0
+-8 -54 -80 104 0
+-8 -55 -77 105 0
+-8 -55 -78 106 0
+-8 -55 -79 107 0
+-8 -55 -80 108 0
+-8 -56 -77 109 0
+-8 -56 -78 110 0
+-8 -56 -79 111 0
+-8 -56 -80 112 0
+-9 -61 -17 97 0
+-9 -61 -18 98 0
+-9 -61 -19 99 0
+-9 -61 -20 100 0
+-9 -62 -17 101 0
+-9 -62 -18 102 0
+-9 -62 -19 103 0
+-9 -62 -20 104 0
+-9 -63 -17 105 0
+-9 -63 -18 106 0
+-9 -63 -19 107 0
+-9 -63 -20 108 0
+-9 -64 -17 109 0
+-9 -64 -18 110 0
+-9 -64 -19 111 0
+-9 -64 -20 112 0
+-10 -65 -37 97 0
+-10 -65 -38 98 0
+-10 -65 -39 99 0
+-10 -65 -40 100 0
+-10 -66 -37 101 0
+-10 -66 -38 102 0
+-10 -66 -39 103 0
+-10 -66 -40 104 0
+-10 -67 -37 105 0
+-10 -67 -38 106 0
+-10 -67 -39 107 0
+-10 -67 -40 108 0
+-10 -68 -37 109 0
+-10 -68 -38 110 0
+-10 -68 -39 111 0
+-10 -68 -40 112 0
+-11 -69 -57 97 0
+-11 -69 -58 98 0
+-11 -69 -59 99 0
+-11 -69 -60 100 0
+-11 -70 -57 101 0
+-11 -70 -58 102 0
+-11 -70 -59 103 0
+-11 -70 -60 104 0
+-11 -71 -57 105 0
+-11 -71 -58 106 0
+-11 -71 -59 107 0
+-11 -71 -60 108 0
+-11 -72 -57 109 0
+-11 -72 -58 110 0
+-11 -72 -59 111 0
+-11 -72 -60 112 0
+-12 -73 -77 97 0
+-12 -73 -78 98 0
+-12 -73 -79 99 0
+-12 -73 -80 100 0
+-12 -74 -77 101 0
+-12 -74 -78 102 0
+-12 -74 -79 103 0
+-12 -74 -80 104 0
+-12 -75 -77 105 0
+-12 -75 -78 106 0
+-12 -75 -79 107 0
+-12 -75 -80 108 0
+-12 -76 -77 109 0
+-12 -76 -78 110 0
+-12 -76 -79 111 0
+-12 -76 -80 112 0
+-13 -81 -17 97 0
+-13 -81 -18 98 0
+-13 -81 -19 99 0
+-13 -81 -20 100 0
+-13 -82 -17 101 0
+-13 -82 -18 102 0
+-13 -82 -19 103 0
+-13 -82 -20 104 0
+-13 -83 -17 105 0
+-13 -83 -18 106 0
+-13 -83 -19 107 0
+-13 -83 -20 108 0
+-13 -84 -17 109 0
+-13 -84 -18 110 0
+-13 -84 -19 111 0
+-13 -84 -20 112 0
+-14 -85 -37 97 0
+-14 -85 -38 98 0
+-14 -85 -39 99 0
+-14 -85 -40 100 0
+-14 -86 -37 101 0
+-14 -86 -38 102 0
+-14 -86 -39 103 0
+-14 -86 -40 104 0
+-14 -87 -37 105 0
+-14 -87 -38 106 0
+-14 -87 -39 107 0
+-14 -87 -40 108 0
+-14 -88 -37 109 0
+-14 -88 -38 110 0
+-14 -88 -39 111 0
+-14 -88 -40 112 0
+-15 -89 -57 97 0
+-15 -89 -58 98 0
+-15 -89 -59 99 0
+-15 -89 -60 100 0
+-15 -90 -57 101 0
+-15 -90 -58 102 0
+-15 -90 -59 103 0
+-15 -90 -60 104 0
+-15 -91 -57 105 0
+-15 -91 -58 106 0
+-15 -91 -59 107 0
+-15 -91 -60 108 0
+-15 -92 -57 109 0
+-15 -92 -58 110 0
+-15 -92 -59 111 0
+-15 -92 -60 112 0
+-16 -93 -77 97 0
+-16 -93 -78 98 0
+-16 -93 -79 99 0
+-16 -93 -80 100 0
+-16 -94 -77 101 0
+-16 -94 -78 102 0
+-16 -94 -79 103 0
+-16 -94 -80 104 0
+-16 -95 -77 105 0
+-16 -95 -78 106 0
+-16 -95 -79 107 0
+-16 -95 -80 108 0
+-16 -96 -77 109 0
+-16 -96 -78 110 0
+-16 -96 -79 111 0
+-16 -96 -80 112 0
+115 116 0
+-97 -115 113 0
+-97 -116 114 0
+117 118 0
+-98 -117 113 0
+-98 -118 114 0
+119 120 0
+-99 -119 113 0
+-99 -120 114 0
+121 122 0
+-100 -121 113 0
+-100 -122 114 0
+125 126 0
+-101 -125 123 0
+-101 -126 124 0
+127 128 0
+-102 -127 123 0
+-102 -128 124 0
+129 130 0
+-103 -129 123 0
+-103 -130 124 0
+131 132 0
+-104 -131 123 0
+-104 -132 124 0
+135 136 0
+-105 -135 133 0
+-105 -136 134 0
+137 138 0
+-106 -137 133 0
+-106 -138 134 0
+139 140 0
+-107 -139 133 0
+-107 -140 134 0
+141 142 0
+-108 -141 133 0
+-108 -142 134 0
+145 146 0
+-109 -145 143 0
+-109 -146 144 0
+147 148 0
+-110 -147 143 0
+-110 -148 144 0
+149 150 0
+-111 -149 143 0
+-111 -150 144 0
+151 152 0
+-112 -151 143 0
+-112 -152 144 0
+-97 -115 -113 153 0
+-97 -115 -114 154 0
+-97 -116 -113 155 0
+-97 -116 -114 156 0
+-98 -117 -123 153 0
+-98 -117 -124 154 0
+-98 -118 -123 155 0
+-98 -118 -124 156 0
+-99 -119 -133 153 0
+-99 -119 -134 154 0
+-99 -120 -133 155 0
+-99 -120 -134 156 0
+-100 -121 -143 153 0
+-100 -121 -144 154 0
+-100 -122 -143 155 0
+-100 -122 -144 156 0
+-101 -125 -113 153 0
+-101 -125 -114 154 0
+-101 -126 -113 155 0
+-101 -126 -114 156 0
+-102 -127 -123 153 0
+-102 -127 -124 154 0
+-102 -128 -123 155 0
+-102 -128 -124 156 0
+-103 -129 -133 153 0
+-103 -129 -134 154 0
+-103 -130 -133 155 0
+-103 -130 -134 156 0
+-104 -131 -143 153 0
+-104 -131 -144 154 0
+-104 -132 -143 155 0
+-104 -132 -144 156 0
+-105 -135 -113 153 0
+-105 -135 -114 154 0
+-105 -136 -113 155 0
+-105 -136 -114 156 0
+-106 -137 -123 153 0
+-106 -137 -124 154 0
+-106 -138 -123 155 0
+-106 -138 -124 156 0
+-107 -139 -133 153 0
+-107 -139 -134 154 0
+-107 -140 -133 155 0
+-107 -140 -134 156 0
+-108 -141 -143 153 0
+-108 -141 -144 154 0
+-108 -142 -143 155 0
+-108 -142 -144 156 0
+-109 -145 -113 153 0
+-109 -145 -114 154 0
+-109 -146 -113 155 0
+-109 -146 -114 156 0
+-110 -147 -123 153 0
+-110 -147 -124 154 0
+-110 -148 -123 155 0
+-110 -148 -124 156 0
+-111 -149 -133 153 0
+-111 -149 -134 154 0
+-111 -150 -133 155 0
+-111 -150 -134 156 0
+-112 -151 -143 153 0
+-112 -151 -144 154 0
+-112 -152 -143 155 0
+-112 -152 -144 156 0
+-153 0
+-156 0
diff --git a/ipasir/src/lib.rs b/ipasir/src/lib.rs
index ebe6d5a6..1970d20f 100644
--- a/ipasir/src/lib.rs
+++ b/ipasir/src/lib.rs
@@ -98,7 +98,7 @@ impl Default for IpasirSolver<'_, '_> {
 
 impl IpasirSolver<'_, '_> {
     fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, InvalidApiReturn> {
-        let mut core = Vec::new();
+        let mut core = Vec::with_capacity(assumps.len());
         core.reserve(assumps.len());
         for a in assumps {
             match unsafe { ffi::ipasir_failed(self.handle, a.to_ipasir()) } {
diff --git a/minisat/build.rs b/minisat/build.rs
index 8c3850d0..1d90a38f 100644
--- a/minisat/build.rs
+++ b/minisat/build.rs
@@ -11,7 +11,7 @@ fn main() {
     build(
         "https://github.com/chrjabs/minisat.git",
         "master",
-        "f91df3ab8f9eeaebe351f4a1890cf92831b8b636",
+        "e168f6e72600f4b04769b0f3bbb7f89b1a200a67",
     );
 
     let out_dir = env::var("OUT_DIR").unwrap();
diff --git a/rustsat/src/bench.rs b/rustsat/src/bench.rs
index 478d5297..7bb79c5a 100644
--- a/rustsat/src/bench.rs
+++ b/rustsat/src/bench.rs
@@ -154,3 +154,22 @@ mod pb_enc {
         b.iter(|| build_full_ub::<DynamicPolyWatchdog>(&lits!()));
     }
 }
+
+mod fio {
+    extern crate test;
+
+    use test::Bencher;
+
+    use crate::instances::SatInstance;
+
+    fn read_write_dimacs() {
+        let inst: SatInstance =
+            SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap();
+        inst.to_dimacs_path("/tmp/rustsat-test.cnf").unwrap();
+    }
+
+    #[bench]
+    fn read_write(b: &mut Bencher) {
+        b.iter(|| read_write_dimacs());
+    }
+}
diff --git a/rustsat/src/instances/fio.rs b/rustsat/src/instances/fio.rs
index 1fa11360..3ee2cc9f 100644
--- a/rustsat/src/instances/fio.rs
+++ b/rustsat/src/instances/fio.rs
@@ -43,24 +43,26 @@ pub(crate) fn open_compressed_uncompressed_write<P: AsRef<Path>>(
     path: P,
 ) -> Result<Box<dyn io::Write>, io::Error> {
     let path = path.as_ref();
-    let raw_reader = File::create(path)?;
+    let raw_writer = File::create(path)?;
     #[cfg(feature = "compression")]
     if let Some(ext) = path.extension() {
         if ext.eq_ignore_ascii_case(std::ffi::OsStr::new("bz2")) {
-            return Ok(Box::new(bzip2::write::BzEncoder::new(
-                raw_reader,
+            return Ok(Box::new(io::BufWriter::new(bzip2::write::BzEncoder::new(
+                raw_writer,
                 bzip2::Compression::fast(),
-            )));
+            ))));
         }
         if ext.eq_ignore_ascii_case(std::ffi::OsStr::new("gz")) {
-            return Ok(Box::new(flate2::write::GzEncoder::new(
-                raw_reader,
+            return Ok(Box::new(io::BufWriter::new(flate2::write::GzEncoder::new(
+                raw_writer,
                 flate2::Compression::fast(),
-            )));
+            ))));
         }
         if ext.eq_ignore_ascii_case(std::ffi::OsStr::new("xz")) {
-            return Ok(Box::new(xz2::write::XzEncoder::new(raw_reader, 1)));
+            return Ok(Box::new(io::BufWriter::new(xz2::write::XzEncoder::new(
+                raw_writer, 1,
+            ))));
         }
     }
-    Ok(Box::new(raw_reader))
+    Ok(Box::new(io::BufWriter::new(raw_writer)))
 }
diff --git a/rustsat/src/instances/multiopt.rs b/rustsat/src/instances/multiopt.rs
index 41ca4a00..53ed0aa3 100644
--- a/rustsat/src/instances/multiopt.rs
+++ b/rustsat/src/instances/multiopt.rs
@@ -178,6 +178,10 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
     }
 
     /// Writes the instance to a DIMACS MCNF file at a path
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance.
     pub fn to_dimacs_path<P: AsRef<Path>>(self, path: P) -> Result<(), io::Error> {
         let mut writer = fio::open_compressed_uncompressed_write(path)?;
         self.to_dimacs(&mut writer)
@@ -211,6 +215,10 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
     }
 
     /// Writes the instance to an OPB file at a path
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance.
     pub fn to_opb_path<P: AsRef<Path>>(
         self,
         path: P,
diff --git a/rustsat/src/instances/opt.rs b/rustsat/src/instances/opt.rs
index 6bfb2608..84bbd64c 100644
--- a/rustsat/src/instances/opt.rs
+++ b/rustsat/src/instances/opt.rs
@@ -963,6 +963,10 @@ impl<VM: ManageVars> OptInstance<VM> {
     }
 
     /// Writes the instance to a DIMACS WCNF file at a path
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance.
     pub fn to_dimacs_path<P: AsRef<Path>>(self, path: P) -> Result<(), io::Error> {
         let mut writer = fio::open_compressed_uncompressed_write(path)?;
         self.to_dimacs(&mut writer)
@@ -996,6 +1000,10 @@ impl<VM: ManageVars> OptInstance<VM> {
     }
 
     /// Writes the instance to an OPB file at a path
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance.
     pub fn to_opb_path<P: AsRef<Path>>(
         self,
         path: P,
diff --git a/rustsat/src/instances/sat.rs b/rustsat/src/instances/sat.rs
index 244930aa..3a475205 100644
--- a/rustsat/src/instances/sat.rs
+++ b/rustsat/src/instances/sat.rs
@@ -710,6 +710,10 @@ impl<VM: ManageVars> SatInstance<VM> {
     }
 
     /// Writes the instance to a DIMACS CNF file at a path
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance.
     pub fn to_dimacs_path<P: AsRef<Path>>(self, path: P) -> Result<(), io::Error> {
         let mut writer = fio::open_compressed_uncompressed_write(path)?;
         self.to_dimacs(&mut writer)
@@ -742,6 +746,10 @@ impl<VM: ManageVars> SatInstance<VM> {
     }
 
     /// Writes the instance to an OPB file at a path
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance.
     pub fn to_opb_path<P: AsRef<Path>>(
         self,
         path: P,


Test patch:
diff --git a/cadical/tests/small.rs b/cadical/tests/small.rs
index 169fe6e9..5bd5d74c 100644
--- a/cadical/tests/small.rs
+++ b/cadical/tests/small.rs
@@ -21,6 +21,14 @@ fn small_unsat_instance<S: Solve>(mut solver: S) {
     assert_eq!(res, SolverResult::Unsat);
 }
 
+fn ms_segfault_instance<S: Solve>(mut solver: S) {
+    let inst: SatInstance<BasicVarManager> =
+        SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap();
+    solver.add_cnf(inst.as_cnf().0).unwrap();
+    let res = solver.solve().unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+}
+
 #[test]
 fn small_sat() {
     let solver = CaDiCaL::default();
@@ -33,6 +41,12 @@ fn small_unsat() {
     small_unsat_instance(solver);
 }
 
+#[test]
+fn ms_segfault() {
+    let solver = CaDiCaL::default();
+    ms_segfault_instance(solver);
+}
+
 #[test]
 fn sat_small_sat() {
     let mut solver = CaDiCaL::default();
@@ -51,6 +65,15 @@ fn sat_small_unsat() {
     small_unsat_instance(solver);
 }
 
+#[test]
+fn sat_ms_segfault() {
+    let mut solver = CaDiCaL::default();
+    solver
+        .set_configuration(rustsat_cadical::Config::SAT)
+        .unwrap();
+    ms_segfault_instance(solver);
+}
+
 #[test]
 fn unsat_small_sat() {
     let mut solver = CaDiCaL::default();
@@ -68,3 +91,12 @@ fn unsat_small_unsat() {
         .unwrap();
     small_unsat_instance(solver);
 }
+
+#[test]
+fn unsat_ms_segfault() {
+    let mut solver = CaDiCaL::default();
+    solver
+        .set_configuration(rustsat_cadical::Config::UNSAT)
+        .unwrap();
+    ms_segfault_instance(solver);
+}
diff --git a/glucose/tests/small.rs b/glucose/tests/small.rs
index ca02f36d..35c29c93 100644
--- a/glucose/tests/small.rs
+++ b/glucose/tests/small.rs
@@ -21,6 +21,14 @@ fn small_unsat_instance<S: Solve>(mut solver: S) {
     assert_eq!(res, SolverResult::Unsat);
 }
 
+fn ms_segfault_instance<S: Solve>(mut solver: S) {
+    let inst: SatInstance<BasicVarManager> =
+        SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap();
+    solver.add_cnf(inst.as_cnf().0).unwrap();
+    let res = solver.solve().unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+}
+
 #[test]
 fn core_small_sat() {
     let solver = core::Glucose::default();
@@ -35,6 +43,12 @@ fn core_small_unsat() {
     small_unsat_instance(solver);
 }
 
+#[test]
+fn core_ms_segfault() {
+    let solver = core::Glucose::default();
+    ms_segfault_instance(solver);
+}
+
 #[test]
 fn simp_small_sat() {
     let solver = simp::Glucose::default();
@@ -48,3 +62,9 @@ fn simp_small_unsat() {
     let solver = simp::Glucose::default();
     small_unsat_instance(solver);
 }
+
+#[test]
+fn simp_ms_segfault() {
+    let solver = simp::Glucose::default();
+    ms_segfault_instance(solver);
+}
diff --git a/kissat/tests/small.rs b/kissat/tests/small.rs
index b2a65dc3..f7ddd67c 100644
--- a/kissat/tests/small.rs
+++ b/kissat/tests/small.rs
@@ -21,6 +21,14 @@ fn small_unsat_instance<S: Solve>(mut solver: S) {
     assert_eq!(res, SolverResult::Unsat);
 }
 
+fn ms_segfault_instance<S: Solve>(mut solver: S) {
+    let inst: SatInstance<BasicVarManager> =
+        SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap();
+    solver.add_cnf(inst.as_cnf().0).unwrap();
+    let res = solver.solve().unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+}
+
 #[test]
 fn small_sat() {
     let solver = Kissat::default();
@@ -33,6 +41,12 @@ fn small_unsat() {
     small_unsat_instance(solver);
 }
 
+#[test]
+fn ms_segfault() {
+    let solver = Kissat::default();
+    ms_segfault_instance(solver);
+}
+
 #[test]
 fn sat_small_sat() {
     let mut solver = Kissat::default();
@@ -51,6 +65,15 @@ fn sat_small_unsat() {
     small_unsat_instance(solver);
 }
 
+#[test]
+fn sat_ms_segfault() {
+    let mut solver = Kissat::default();
+    solver
+        .set_configuration(rustsat_kissat::Config::SAT)
+        .unwrap();
+    ms_segfault_instance(solver);
+}
+
 #[test]
 fn unsat_small_sat() {
     let mut solver = Kissat::default();
@@ -68,3 +91,12 @@ fn unsat_small_unsat() {
         .unwrap();
     small_unsat_instance(solver);
 }
+
+#[test]
+fn unsat_ms_segfault() {
+    let mut solver = Kissat::default();
+    solver
+        .set_configuration(rustsat_kissat::Config::UNSAT)
+        .unwrap();
+    ms_segfault_instance(solver);
+}
diff --git a/minisat/tests/small.rs b/minisat/tests/small.rs
index 50a99f2c..154c2c09 100644
--- a/minisat/tests/small.rs
+++ b/minisat/tests/small.rs
@@ -27,6 +27,16 @@ fn core_small_unsat() {
     assert_eq!(res, SolverResult::Unsat);
 }
 
+#[test]
+fn core_ms_segfault() {
+    let mut solver = core::Minisat::default();
+    let inst: SatInstance<BasicVarManager> =
+        SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap();
+    solver.add_cnf(inst.as_cnf().0).unwrap();
+    let res = solver.solve().unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+}
+
 #[test]
 fn simp_small_sat() {
     let mut solver = simp::Minisat::default();
@@ -49,3 +59,13 @@ fn simp_small_unsat() {
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Unsat);
 }
+
+#[test]
+fn simp_ms_segfault() {
+    let mut solver = simp::Minisat::default();
+    let inst: SatInstance<BasicVarManager> =
+        SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap();
+    solver.add_cnf(inst.as_cnf().0).unwrap();
+    let res = solver.solve().unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+}