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/solvertests/src/lib.rs b/solvertests/src/lib.rs index 8f5ab589..e20b8afd 100644 --- a/solvertests/src/lib.rs +++ b/solvertests/src/lib.rs @@ -99,6 +99,14 @@ pub fn base_tests(tokens: TokenStream) -> TokenStream { test_inst!(#slv, "./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf", rustsat::solvers::SolverResult::Unsat); } }); + let ignore = ignoretok(2); + ts.extend(quote! { + #[test] + #ignore + fn minisat_segfault() { + test_inst!(#slv, "./data/minisat-segfault.cnf", rustsat::solvers::SolverResult::Unsat); + } + }); ts.into() }