sat-heritage / docker-images

SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers
MIT License
38 stars 3 forks source link

dk-sat11_1:2013 has non-standard returncode #22

Open pauleve opened 3 years ago

pauleve commented 3 years ago
 + docker run --name satex23230 --rm -e TIMEOUT=10 -v /home/runner/work/docker-images/docker-images/tests:/data satex/dk-sat11_1:2013 aim-200-1_6-yes1-1.cnf
cnf...#### dk-sat11_1:2013 ####
+ cd /solvers/dk-SAT11
+ set +x
+ timeout 10 .//dk-run.sh /data/aim-200-1_6-yes1-1.cnf
c size 3
c running 3-SAT solver
c (200 variables, 320 clauses, 959 literals successfully read)
s SATISFIABLE
v 107 67 186 37 94 194 1 -36 -187 -87 -159 -29 -63 18 -3 147 13 -84 69 89 -66 38 -21 -160 126 83 55 -70 -144 121 -196 20 -120 -117 4 143 -102 -135 -161 51 7 183 74 131 -42 97 27 179 -127 -122 145 92 -100 82 -181 119 -68 -25 -62 -184 -166 198 53 -153 134 109 -98 -195 170 177 116 192 -193 141 -110 -149 169 104 167 -130 54 150 -22 -88 15 -73 93 16 -32 -146 185 -49 197 -168 71 157 -113 56 -48 139 -43 65 95 19 10 105 81 90 171 52 -174 154 -5 41 -133 142 -123 114 28 190 11 6 -200 -115 -60 111 191 -61 -91 -124 -118 -40 39 76 137 132 -80 172 -162 -79 9 180 148 46 45 173 -64 33 152 -24 156 -178 101 -99 30 -85 155 35 96 75 108 182 -47 176 17 -158 -128 125 -129 -2 199 -23 26 -44 -163 -138 -165 78 -164 151 -72 -106 31 77 14 -175 189 136 -12 -50 -57 8 -58 112 86 -59 -34 -140 -103 -188 0
c Altogether 12091+2772284 mems, 118500 bytes, 199 nodes.
ERROR Solver failed with return code 58