search

conp-solutions / riss

Riss SAT Solver
GNU Lesser General Public License v2.1
8 stars 5 forks source link

Memory error crash, reproducible #18

Open msoos opened 3 years ago

msoos commented 3 years ago

File included at the bottom (gzipped, because .cnf is not supported by GitHub). Valgrind spits out a bunch of nonsense, so I can't give you more detailed information about the issue. But it's certainly 100% reproducible and the CNF is 100% valid. I'm running latest Arch Linux, compiled with gcc (GCC) 11.1.0

soos@tiresias:ccanr-cscc$ ./coprocessor stuff.cnf model_193741 -enabled_cp3 -cp3_undo=cp3_undo_193741 -dimacs=cp3_tmpCNF_193741 -enabled_cp3 -cp3_stats -up -subsimp -bve -no-bve_gates -no-bve_strength -bve_red_lits=1 -cp3_bve_heap=1 -bve_heap_updates=1 -bve_totalG -bve_cgrow_t=1000 -bve_cgrow=10
c ====================[ Coprocessor 7.1.0  satcomp-2020-11-g4be9296-dirty ]================================
c | Norbert Manthey. The use of the tool is limited to research only!                                     |
c | Contributors:                                                                                         |
c |     Kilian Gebhard                                                                                    |
c |     Lucas Kahlert, Franziska Krüger, Aaron Stephan                                                    |
c ============================[ Problem Statistics ]=======================================================
c |                                                                                                       |
c |  Number of variables:        161280                                                                  |
c |  Number of clauses:          604800                                                                   |
c |  Parse time:                   0.07 s                                                                 |
c [STAT] CP3 2.08749 s-ppTime, 0 s-ipTime, 2.1455 s-ppwTime, 0 s-ipwTime, 148.23 MB, ok 0.079133 s-ohTime, 
c [STAT] CP3(2) 605760 cls, 0 learnts, -1010 rem-cls, 0 rem-learnts, 
c [STAT] UP 1.5e-05 s, 0 units, 0 cls, 7 lits
c [STAT] SuSi(1) 0.040444 s, 0 cls,  with 0 lits, 0 strengthed 
c [STAT] SuSi(2) 3393526 subs-steps, 4232935 strenght-steps, 0 increases, 0.070528s strengthening 
c [STAT] EE 0.513001 s, 0 steps 0 ee-lits 0 removedCls, 0 removedSubCls,
c [STAT] EE-gate 0.068885 s, 0 steps, 0.372971 extractGateTime, 
c [STAT] BVE(1) 0.054383 s, 0.000386 s spent on subsimp, 161939 vars tested, 161936 anticipations, 2258 vars skipped, 1145787 checks, 
c [STAT] BVE(2) 5934 rem cls, with 18266 lits, 0 learnts rem, with 0 lits, 6944 new cls, with 31994 lits, 0 new learnts, with 0 lits, 
c [STAT] BVE(3) 447 vars eliminated, 0 units enqueued, 0 BC removed, with 0 lits, 0 blocked learnts removed, with 0 lits, 
c [STAT] BVE(4) 0 gateDefs, 0 usedGates, 0 gateSeconds, 
c [STAT] BVE(5) 50 incElims, 0 keepElims, 397 decElims, 1010 totalAdds,
c [STAT] UNHIDE 0.649535 s, 0 cls, 0 totalLits, 0 lits 
c [STAT] UNHIDE(2) 0 prSecs, 0 prSteps, 0 L1units, 0 L2units, 0 L3units, 0 L4units, 0 L5units, 
c [STAT] UNHIDE(3) 0 EE-checks, 0 EE-cands, 0 EEs 
c [STAT] XOR 0.075353s, 0.067971 parse-s, 0.006614 reason-s, 
c [STAT] XOR(2) 0 xors, 0 subXors, 0 resXors, 0 clauses, 0 resClauses, 0 resTauts, 0 resStrength, 1210502 findChecks, 
c [STAT] XOR(3) 0 steps, 322560 empties, 0 listUnits, 0 useLists, 0 xorUnits, 0 eqs, 
c [STAT] XOR(4) 605755 participating, 0.990291 ratio, 0 simDecisions, 0 xorProps, 0 clsProps, 
c [STAT] BCE 0.285556 seconds, 2610300 steps, 643294 testLits, 0 remBCE, 0 BCMs, 0 BCMcands, 0 BCMlits, 
c [STAT] CLE 0 remCLE, 0 cleUnits, 
c [STAT] BCE-CLA 0 seconds, 0 steps, 0 testLits, 0 extClss, 0 extLits, 0 possibles, 
c [STAT] FM 0.307754 s, 0.1546 amo-s, 1.34608 fm-s, 0.024457 amt-s, 1 amos, 0 amts, 0 sameUnits, 0 deducedUnits, 0 propUnits, 0 cls, 0 steps, 12000012 searchSteps, 0 addDups, 
c [STAT] FM(2) 0 irregulars, 0 pureAmoLits, 0 diff, 0 discards, 0 addedCs, 0 removedCs, 0 newAmos, 0 discardedNewAmos, 
c [STAT] FM(3) 0 newAmoBinCls, 0 newCls, 0 newAlos, 0 newAlks, 0 duplicates, 0 garbageCollecst, 
c [STAT] FM(4) 0.000579 2PrdTime, 0 2PrAmos, 0 2PrLits, 2e-06 dedAloTime, 0 dedAlos, 
c [STAT] FM(5) time: 0.115298 s,steps: 1805765 cards: 0 failed: 1341 extLits: 0 redDegree: 0 probes: 2682 conflictProbes: 0 savedPreCls: 0 savedPostCls: 0 units: 8032
c [STAT] DENSE 455 gaps
c |  Simplification time:          2.10 s                                                                 |
c |                                                                                                       |
c ==============================[ Writing DIMACS ]=========================================================
double free or corruption (!prev)
Aborted (core dumped)

The cmake ran like this: (note that there is completely unrelated bug here somewhere about git HEAD not working):

soos@tiresias:build$ cmake -D CMAKE_BUILD_TYPE=Release ..
-- The C compiler identification is GNU 11.1.0
-- The CXX compiler identification is GNU 11.1.0
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/lib/ccache/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/lib/ccache/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
fatal: ambiguous argument 'v7.1.0..HEAD': unknown revision or path not in the working tree.
Use '--' to separate paths from revisions, like this:
'git <command> [<revision>...] -- [<file>...]'
-- Build type Release
-- Static binaries ON
-- Verbose warnings ON
-- Compile with -fpic OFF
-- Compile for gprof profiling OFF
-- Quiet OFF
-- DRAT proofs OFF
-- Found Git: /usr/bin/git (found version "2.32.0") 
-- enable verbose compiler warnings
-- Performing Test HAVE_FLAG_-Wno-delete-non-virtual-dtor
-- Performing Test HAVE_FLAG_-Wno-delete-non-virtual-dtor - Success
-- Performing Test HAVE_FLAG_-Wno-unused-but-set-variable
-- Performing Test HAVE_FLAG_-Wno-unused-but-set-variable - Success
-- Performing Test HAVE_FLAG_-Wno-class-memaccess
-- Performing Test HAVE_FLAG_-Wno-class-memaccess - Success
-- Found ZLIB: /usr/lib/libz.so (found version "1.2.11") 
-- Looking for pthread.h
-- Looking for pthread.h - found
-- Performing Test CMAKE_HAVE_LIBC_PTHREAD
-- Performing Test CMAKE_HAVE_LIBC_PTHREAD - Failed
-- Looking for pthread_create in pthreads
-- Looking for pthread_create in pthreads - not found
-- Looking for pthread_create in pthread
-- Looking for pthread_create in pthread - found
-- Found Threads: TRUE  
-- Libs: /usr/lib/libz.so /usr/lib/librt.so -lpthread
-- Generating signature riss-version from git
-- Generating signature coprocessor-version from git
-- Found Doxygen: /usr/bin/doxygen (found version "1.9.1") found components: doxygen dot 
-- Configuring done
-- Generating done
-- Build files have been written to: /home/soos/development/sat_solvers/riss/build

stuff.cnf.gz

msoos commented 3 years ago

Ah, even a standard CNF (mizh-md5-47-3.cnf), running in standard mode crashes. Hmmm strange!

soos@tiresias:ccanr-cscc$ ./coprocessor mizh-md5-47-3.cnf 
c ====================[ Coprocessor 7.1.0  satcomp-2020-11-g4be9296-dirty ]================================
c | Norbert Manthey. The use of the tool is limited to research only!                                     |
c | Contributors:                                                                                         |
c |     Kilian Gebhard                                                                                    |
c |     Lucas Kahlert, Franziska Krüger, Aaron Stephan                                                    |
c ============================[ Problem Statistics ]=======================================================
c |                                                                                                       |
c |  Number of variables:         65604                                                                  |
c |  Number of clauses:          234719                                                                   |
c |  Parse time:                   0.02 s                                                                 |
c [STAT] CP3 1.61866 s-ppTime, 0 s-ipTime, 1.6942 s-ppwTime, 0 s-ipwTime, 72.6562 MB, ok 0.031385 s-ohTime, 
c [STAT] CP3(2) 175673 cls, 0 learnts, 57784 rem-cls, 0 rem-learnts, 
c [STAT] UP 0.000617 s, 0 units, 721 cls, 1162 lits
c [STAT] SuSi(1) 0.047942 s, 29337 cls,  with 116770 lits, 3243 strengthed 
c [STAT] SuSi(2) 5441248 subs-steps, 9813833 strenght-steps, 0 increases, 0.098028s strengthening 
c [STAT] EE 0.328172 s, 0 steps 10996 ee-lits 46579 removedCls, 0 removedSubCls,
c [STAT] EE-gate 0.059512 s, 230464 steps, 0.167844 extractGateTime, 
c [STAT] BVE(1) 0.322302 s, 0.15879 s spent on subsimp, 51087 vars tested, 51087 anticipations, 24156 vars skipped, 1255677 checks, 
c [STAT] BVE(2) 176311 rem cls, with 487690 lits, 0 learnts rem, with 0 lits, 177310 new cls, with 666207 lits, 0 new learnts, with 0 lits, 
c [STAT] BVE(3) 27906 vars eliminated, 0 units enqueued, 0 BC removed, with 0 lits, 0 blocked learnts removed, with 0 lits, 
c [STAT] BVE(4) 27904 gateDefs, 26184 usedGates, 0.026078 gateSeconds, 
c [STAT] BVE(5) 1863 incElims, 965 keepElims, 25078 decElims, 999 totalAdds,
c [STAT] UNHIDE 0.370982 s, 1581 cls, 14075 totalLits, 7203 lits 
c [STAT] UNHIDE(2) 0 prSecs, 0 prSteps, 0 L1units, 0 L2units, 0 L3units, 0 L4units, 0 L5units, 
c [STAT] UNHIDE(3) 0 EE-checks, 0 EE-cands, 0 EEs 
c [STAT] XOR 0.111484s, 0.06535 parse-s, 0.040402 reason-s, 
c [STAT] XOR(2) 30342 xors, 0 subXors, 0 resXors, 0 clauses, 0 resClauses, 0 resTauts, 0 resStrength, 416131 findChecks, 
c [STAT] XOR(3) 40781 steps, 78411 empties, 0 listUnits, 1621 useLists, 0 xorUnits, 1487 eqs, 
c [STAT] XOR(4) 182677 participating, 0.999447 ratio, 0 simDecisions, 0 xorProps, 0 clsProps, 
c [STAT] BCE 0.135266 seconds, 2919785 steps, 128816 testLits, 0 remBCE, 0 BCMs, 0 BCMcands, 0 BCMlits, 
c [STAT] CLE 120 remCLE, 0 cleUnits, 
c [STAT] BCE-CLA 0 seconds, 0 steps, 0 testLits, 0 extClss, 0 extLits, 0 possibles, 
c [STAT] FM 0.310014 s, 0.048883 amo-s, 1.01196 fm-s, 0.039746 amt-s, 10 amos, 0 amts, 0 sameUnits, 0 deducedUnits, 0 propUnits, 57453 cls, 120717 steps, 2878729 searchSteps, 7796 addDups, 
c [STAT] FM(2) 0 irregulars, 32023 pureAmoLits, 42391 diff, 30289 discards, 35660 addedCs, 43657 removedCs, 0 newAmos, 0 discardedNewAmos, 
c [STAT] FM(3) 0 newAmoBinCls, 3308 newCls, 6397 newAlos, 0 newAlks, 51089 duplicates, 0 garbageCollecst, 
c [STAT] FM(4) 0.00034 2PrdTime, 0 2PrAmos, 0 2PrLits, 8.9e-05 dedAloTime, 0 dedAlos, 
c [STAT] FM(5) time: 0.129226 s,steps: 1381540 cards: 5641 failed: 5324 extLits: 5639 redDegree: 2 probes: 37911 conflictProbes: 6046 savedPreCls: 63 savedPostCls: 10094 units: 75822
c [STAT] DENSE 44442 gaps
c |  Simplification time:          1.63 s                                                                 |
c |                                                                                                       |
double free or corruption (!prev)
Aborted (core dumped)

I wonder if the newer gcc is causing this? Do you know what could be happening?

Mate

conp-solutions commented 2 years ago

Thanks Mate. I'll finally have a look into this.