search

msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
817 stars 181 forks source link

seg fault with latest master #261

Closed aodinaev closed 9 years ago

aodinaev commented 9 years ago 
(gdb) run
Starting program: /home/aodinaye/projects/cminisat/build/cryptominisat4 data/puz8.cnf
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib64/libthread_db.so.1".
c Outputting solution to console
c CryptoMiniSat version 4.5.3
c CryptoMiniSat SHA revision 2b0012ae833bcdb7d54c2b55e89a4c3b3b7ad41a
c CryptoMiniSat compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -std=c++11 -pthread -g -Wall -Wextra -Wunused -pedantic -Wsign-compare -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -fvisibility=hidden -Wpointer-arith -Wformat-nonliteral -Winit-self -Wunreachable-code -fPIC | COMPILE_DEFINES =  -DBOOST_TEST_DYN_LINK -DUSE_ZLIB | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = 1 | TBB_FOUND =  | STATS = OFF | MYSQL_FOUND =  | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND = FALSE | ENABLE_TESTING = OFF | M4RI_FOUND = FALSE | SLOW_DEBUG = OFF | PYTHON_EXECUTABLE = /usr/bin/python2.7 | PYTHON_LIBRARY = /usr/lib64/libpython2.7.so | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | compilation date time = Sep 14 2015 21:12:53
c compiled with gcc version 4.8.3 20140911 (Red Hat 4.8.3-7)
c Executed with command line: /home/aodinaye/projects/cminisat/build/cryptominisat4 data/puz8.cnf
c Reading file 'data/puz8.cnf'
c -- header says num vars:          43476
c -- header says num clauses:     2088140
c -- clauses added: 2088140
c -- xor clauses added: 0
c -- vars added 43476
c Parsing time: 0.49 s
c --> Executing strategy token: sub-impl
c [impl sub] bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.08 T-out: N w-visit: 86952
c --> Executing strategy token: scc-vrepl
c [clean] T: 0.0278 s
c [simp] mem usage for occur of irred     35 MB
c [simp] mem usage for occur of red        3 MB
c [simp] Not linked in red 0/0 (0.00 %)
c Mem for watch alloc      : 54          MB (66.68     %)
c Mem for watch array      : 1           MB (2.41      %)
c --> Executing OCC strategy token: occ-backw-sub-str
c [sub] tri upI: 69267 subs w bin: 0 str w bin: 0 subs w tri: 24 str w tri: 6 tried: 2046034 str: 0 toDecrease: 315296382 0-depth ass: 0 T: 0.46 T-out: N T-r: 15.76%
c [sub] rem cl: 0 tried: 370890/37089 (1000.0%) T: 0.12 T-out: N
c [str] sub: 0 str: 0 tried: 111267/37089 (300.0)  T: 0.05 T-out: N
c sub_str_with sub: 0 str: 0 T: 0.00
c --> Executing OCC strategy token: occ-clean-implicit
c --> Executing OCC strategy token: occ-bve
c Empty resolvent elimed: 61 T: 0.03 T-out: N
c sub_str_with sub: 0 str: 0 T: 0.00
c impls_sub_lits  T: 0.13
c iter v-elim 9925
c  #try to eliminate: 43217
c  #var-elim: 9925
c  #T-o: Y
c  #T-r: -0.00%
c  #T: 0.91
c --> Executing OCC strategy token: 
c [clean] T: 0.0300 s
c [occur] 0.1021 is overhead
c [v-elim] elimed: 9986 / 30294 / 43278 T: 0.91 T-out: Y
c [v-elim] cl-new: 25191 tried: 9925 tested: 43217 (0.0000 % aggressive)
c [v-elim] subs: 26 red-bin rem: 0 red-tri rem: 0 red-long rem: 0 v-fix:    0
c [simp] link-in T: 0.0487 cleanup T: 0.0534
c [scc] new: 0 BP 1M T: 0.01
c calculated reachability. T: 0.000
c [polar] default polars -  pos:   15663 neg:   17629 undec:   10184 T: 0.01
c     0     0   33292   31K   114 2008K 64.58  2.98     0     0     0  0.00  0.00
c  rest  conf freevar  IrrL  IrrT  IrrB   l/c  RedL  RedT  RedB   l/c
c    29  7001   33177   31K   114 2008K 64.58  2.98  6741     4    91 1030.43 1016.14
c [w-sort]  T: 0.03
c [blk-lit-opt]  T: 0.04
c    52 14002   33046   31K   114 2008K 64.57  2.98 13489     6   119 965.03 956.19
c    75   21K   33036   31K   114 2008K 64.57  2.98   20K    14   163 918.56 910.61
c [DBclean] locked:0 marked: 9984 glue: 116 ttl:4155 locked_solver:32
c [mem] Consolidated memory  cls   46K old size 12293K new size 6484K T: 0.09
c  rest  conf freevar  IrrL  IrrT  IrrB   l/c  RedL  RedT  RedB   l/c
c   105   28K   33021   31K   189 1968K 64.02  2.98 16931    23   209 691.16 681.84
c [DBclean] locked:0 marked: 9950 glue: 789 ttl:1877 locked_solver:104
c [mem] Consolidated memory  cls   44K old size 9946K new size 5693K T: 0.08
c   147   35K   33015   31K   170 1968K 64.03  2.98 13724    26   244 673.70 660.75
c   172   42K   33007   31K   170 1968K 64.03  2.98   20K    35   270 754.83 743.79
c [DBclean] locked:0 marked: 9974 glue: 1135 ttl:2462 locked_solver:57
c [mem] Consolidated memory  cls   45K old size 10501K new size 6109K T: 0.09
c  rest  conf freevar  IrrL  IrrT  IrrB   l/c  RedL  RedT  RedB   l/c
c   212   49K   33007   31K   185 1967K 64.07  2.98 17223    43   306 725.66 711.29
c [DBclean] locked:0 marked: 9981 glue: 1450 ttl:2161 locked_solver:39
c [mem] Consolidated memory  cls   45K old size 10125K new size 5374K T: 0.08
c   255   56K   32998   31K   126 1967K 64.07  2.98 13947    45   334 596.97 581.23
c   295   63K   32981   31K   126 1967K 64.07  2.98   20K    51   369 628.66 616.17
c [DBclean] locked:0 marked: 9988 glue: 1861 ttl:2306 locked_solver:28
c [mem] Consolidated memory  cls   45K old size 8985K new size 4759K T: 0.08
c recursive minimization too costly: 412079Kcost/(% lits removed) --> disabling
c --> Executing strategy token: handle-comps
c --> Executing strategy token: scc-vrepl
c [scc] new: 144 BP 1M T: 0.02
c [clean] T: 0.0380 s
c [vrep] vars 141 lits 98616 rem-bin-cls 570 rem-tri-cls 0 rem-long-cls 259 BP 0M T: 0.28
c --> Executing strategy token: cache-clean
c [cache] cleaned. Updated:       0 K Cleaned:       0 K Freed:       0 K T: 0.00
c --> Executing strategy token: cache-tryboth
c [bcache]  0-depth ass: 13 BXprop: 0 T: 0.01
c --> Executing strategy token: sub-impl
c [impl sub] bin: 215 tri: 4 (stamp: 0, cache: 0) T: 0.09 T-out: N w-visit: 86952
c --> Executing strategy token: intree-probe
c [clean] T: 0.0372 s
c [scc] new: 0 BP 1M T: 0.02
c [clean] T: 0.0370 s
c [vrep] vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 BP 0M T: 0.05
c [intree] Set 11 vars hyper-added: 317149 trans-irred::368 trans-red::1845 T: 0.90 T-out: Y T-r: -0.33%
c --> Executing strategy token: probe
c [clean] T: 0.0413 s
c [probe] lits : 11.41M act vars: 32.81K BP+HP todo: 960.00M
c [probe] NumProps after perf multi: 960.00M after numcall multi: 960.00M (<- final)
c [clean] T: 0.0449 s
c [probe] 0-depth assigns: 67 bsame: 2 Flit: 28 Visited: 49239/65620(75.0%)
c [probe] probed: 1454(2.2%) hyperBin:212341 transR-Irred:844 transR-Red:14975
c [probe] BP: 613.6M HP: 341.0M T: 1.96 T-out: Y T-r: -0.00%
c [probe] time spent updating cache during probing: 0.0%
c --> Executing strategy token: sub-str-cls-with-bin
c [clean] T: 0.0479 s
c [clean] T: 0.0479 s
c [distill] cache-based irred--  cl tried    20037 cl-sh   482 cl-rem  599 lit-rem   1252 T: 0.29 T-out: Y
c [distill] cache-based   red--  cl tried     5141 cl-sh  1024 cl-rem  150 lit-rem  67089 T: 0.22 T-out: Y
c --> Executing strategy token: distill-cls
c [distill] longirred tried: 522/30307 cl-r:258 lit-r:385 T: 0.21 T-out: Y T-r: 100.43%
c [distill] tri+long useful: 281/522/30558 lits-rem: 408 0-depth-assigns: 0 T: 0.21 T-out: Y
c --> Executing strategy token: scc-vrepl
c [scc] new: 1909 BP 1M T: 0.02
c [clean] T: 0.0469 s
c [vrep] vars 1533 lits 2306691 rem-bin-cls 6863 rem-tri-cls 4 rem-long-cls 1527 BP 6M T: 0.36
c --> Executing strategy token: sub-impl
c [impl sub] bin: 20456 tri: 26 (stamp: 0, cache: 0) T: 0.09 T-out: Y w-visit: 67731
c --> Executing strategy token: str-impl
c [clean] T: 0.0456 s
c [simp] mem usage for occur of irred     30 MB
c [simp] mem usage for occur of red      142 MB
c [simp] Not linked in red 7153/15937 (44.88 %)
c Mem for watch alloc      : 73          MB (36.34     %)
c Mem for watch array      : 1           MB (0.99      %)
c --> Executing OCC strategy token: occ-backw-sub-str
c [sub] tri upI: 1344 subs w bin: 0 str w bin: 30220 subs w tri: 4 str w tri: 61 tried: 2852216 str: 0 toDecrease: -82019 0-depth ass: 0 T: 0.47 T-out: Y T-r: -0.00%
c [sub] rem cl: 2148 tried: 297269/45501 (653.3%) T: 0.33 T-out: Y
c [str] sub: 13 str: 2361 tried: 135814/45501 (298.5)  T: 0.21 T-out: Y

Program received signal SIGSEGV, Segmentation fault.
CMSat::SubsumeStrengthen::strengthen_subsume_and_unlink_and_markirred (this=this@entry=0x63f920, offset=1287283)
    at /home/aodinaye/projects/cminisat/src/subsumestrengthen.cpp:139
139     );
Missing separate debuginfos, use: debuginfo-install boost-program-options-1.54.0-12.fc20.x86_64 glibc-2.18-19.fc20.x86_64 libgcc-4.8.3-7.fc20.x86_64 libstdc++-4.8.3-7.fc20.x86_64 zlib-1.2.8-3.fc20.x86_64
(gdb) bt
#0  CMSat::SubsumeStrengthen::strengthen_subsume_and_unlink_and_markirred (this=this@entry=0x63f920, offset=1287283)
    at /home/aodinaye/projects/cminisat/src/subsumestrengthen.cpp:139
#1  0x00007ffff7ad210c in CMSat::SubsumeStrengthen::handle_sub_str_with (this=0x63f920) at /home/aodinaye/projects/cminisat/src/subsumestrengthen.cpp:451
#2  0x00007ffff7ac44e8 in CMSat::OccSimplifier::backward_sub_str (this=this@entry=0x64fa10) at /home/aodinaye/projects/cminisat/src/occsimplifier.cpp:1022
#3  0x00007ffff7acb976 in CMSat::OccSimplifier::execute_simplifier_sched (this=this@entry=0x64fa10, 
    strategy="occ-backw-sub-str, occ-xor, occ-clean-implicit, occ-bve, occ-bva, occ-gates, ") at /home/aodinaye/projects/cminisat/src/occsimplifier.cpp:918
#4  0x00007ffff7acbf15 in CMSat::OccSimplifier::simplify (this=0x64fa10, _startup=_startup@entry=false, 
    schedule="occ-backw-sub-str, occ-xor, occ-clean-implicit, occ-bve, occ-bva, occ-gates, ") at /home/aodinaye/projects/cminisat/src/occsimplifier.cpp:993
#5  0x00007ffff7b0198a in CMSat::Solver::execute_inprocess_strategy (this=this@entry=0x649690, startup=startup@entry=false, 
    strategy="handle-comps,scc-vrepl, cache-clean, cache-tryboth,sub-impl, intree-probe, probe,sub-str-cls-with-bin, distill-cls, scc-vrepl, sub-impl, occ-backw-sub-str, occ-xor, occ-clean-implicit, occ-bve, occ-bv"...) at /home/aodinaye/projects/cminisat/src/solver.cpp:1618
#6  0x00007ffff7b023f3 in CMSat::Solver::simplify_problem (this=this@entry=0x649690, startup=startup@entry=false) at /home/aodinaye/projects/cminisat/src/solver.cpp:1766
#7  0x00007ffff7b02a6a in CMSat::Solver::iterate_until_solved (this=this@entry=0x649690) at /home/aodinaye/projects/cminisat/src/solver.cpp:1559
#8  0x00007ffff7b040ac in CMSat::Solver::solve (this=this@entry=0x649690) at /home/aodinaye/projects/cminisat/src/solver.cpp:1343
#9  0x00007ffff7b3b380 in solve_with_assumptions (_assumptions=0x0, this=0x649690) at /home/aodinaye/projects/cminisat/src/solver.h:429
#10 CMSat::SATSolver::solve (this=0x635450, assumptions=assumptions@entry=0x0) at /home/aodinaye/projects/cminisat/src/cryptominisat.cpp:551
#11 0x000000000040c450 in Main::solve (this=this@entry=0x7fffffffdb40) at /home/aodinaye/projects/cminisat/src/main.cpp:1223
#12 0x0000000000406dbc in main (argc=<optimized out>, argv=<optimized out>) at /home/aodinaye/projects/cminisat/src/main.cpp:1319
(gdb)
aodinaev commented 9 years ago

same cnf on OSX give different stack trace

Program received signal EXC_BAD_ACCESS, Could not access memory.
Reason: KERN_INVALID_ADDRESS at address: 0x0000001101aa7fe8
0x000000010014308a in CMSat::vec<CMSat::Watched, unsigned int>::size () at /Users/aodinayev/projects/cminisat/src/subsumestrengthen.cpp:427
427                 + solver->watches[(~cl[i]).toInt()].size();
(gdb) bt
#0  0x000000010014308a in CMSat::vec<CMSat::Watched, unsigned int>::size () at /Users/aodinayev/projects/cminisat/src/subsumestrengthen.cpp:427
#1  0x000000010014308a in CMSat::watch_subarray::size () at /Users/aodinayev/projects/cminisat/src/watcharray.h:59
#2  0x000000010014308a in CMSat::SubsumeStrengthen::findStrengthened<CMSat::Clause> (this=0x100413950, offset=1287560, cl=@0x1098d2c40, abs=33684, out_subsumed=@0x1004139b8, out_lits=@0x1004139d0) at /Users/aodinayev/projects/cminisat/src/subsumestrengthen.cpp:427
#3  0x000000010013fe6c in std::__1::vector<unsigned int, std::__1::allocator<unsigned int> >::size () at /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/include/c++/v1/vector:133
#4  0x000000010013fe6c in CMSat::SubsumeStrengthen::strengthen_subsume_and_unlink_and_markirred (this=0x100413950, offset=1287560) at /Users/aodinayev/projects/cminisat/src/subsumestrengthen.cpp:427
#5  0x0000000100141619 in CMSat::SubsumeStrengthen::handle_sub_str_with (this=0x100413950) at /Users/aodinayev/projects/cminisat/src/subsumestrengthen.cpp:451
#6  0x0000000100132d9c in std::__1::vector<unsigned int, std::__1::allocator<unsigned int> >::begin () at /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/include/c++/v1/vector:1022
#7  CMSat::OccSimplifier::free_clauses_to_free () at /Users/aodinayev/projects/cminisat/src/occsimplifier.h:858
#8  0x0000000100132d9c in CMSat::OccSimplifier::backward_sub_str (this=0x100413400) at /Users/aodinayev/projects/cminisat/src/occsimplifier.cpp:427
#9  0x00000001001327d8 in CMSat::OccSimplifier::execute_simplifier_sched (this=0x100413400, strategy=<value temporarily unavailable, due to optimizations>) at /Users/aodinayev/projects/cminisat/src/occsimplifier.cpp:918
#10 0x00000001001331cb in CMSat::OccSimplifier::simplify (this=0x100413400, _startup=<value temporarily unavailable, due to optimizations>, schedule={<std::__1::__basic_string_common<true>> = {<No data fields>}, __r_ = {<std::__1::__libcpp_compressed_pair_imp<std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> >::__rep, std::__1::allocator<char>, 2>> = {<std::__1::allocator<char>> = {<No data fields>}, __first_ = {{__l = {__cap_ = 81, __size_ = 77, __data_ = 0x107d8b310 "occ-backw-sub-str, occ-xor, occ-clean-implicit, occ-bve, occ-bva, occ-gates, "}, __s = {{__size_ = 81 'Q', __lx = 81 'Q'}, __data_ = "\000\000\000\000\000\000\000M\000\000\000\000\000\000\000\020??\a\001\000\000"}, __r = {__words = {81, 77, 4426609424}}}}}, <No data fields>}, static npos = <optimized out>}) at /Users/aodinayev/projects/cminisat/src/occsimplifier.cpp:993
#11 0x000000010016d0d3 in CMSat::Solver::execute_inprocess_strategy () at /Users/aodinayev/projects/cminisat/src/solver.cpp:1618
#12 0x000000010016b69a in CMSat::Solver::simplify_problem (this=0x101002c00, startup=<value temporarily unavailable, due to optimizations>) at /Users/aodinayev/projects/cminisat/src/solver.cpp:1766
#13 0x000000010016bd00 in CMSat::Solver::iterate_until_solved (this=0x101002c00) at /Users/aodinayev/projects/cminisat/src/solver.cpp:1559
#14 0x000000010016abc6 in CMSat::Solver::solve (this=0x101002c00) at /Users/aodinayev/projects/cminisat/src/solver.cpp:1343
#15 0x00000001001ab49c in CMSat::Solver::solve_with_assumptions (this=0x101002c00, _assumptions=<value temporarily unavailable, due to optimizations>) at solver.h:429
#16 0x00000001001aa64d in CMSat::SATSolver::solve (this=0x10040b7f0, assumptions=0x0) at /Users/aodinayev/projects/cminisat/src/cryptominisat.cpp:551
#17 0x000000010001945f in Main::solve () at /Users/aodinayev/projects/cminisat/src/main.cpp:1223
#18 0x0000000100019c0a in main (argc=<value temporarily unavailable, due to optimizations>, argv=<value temporarily unavailable, due to optimizations>) at main.h:1319
(gdb)
aodinaev commented 9 years ago

I attached test cnf

https://github.com/aodinaev/cryptominisat/blob/segfault/file/tests/cnf-files/sf.cnf.gz

capiman commented 9 years ago

I can reproduce this problem/crash (MinGW64 4.8.1 on Windows):

D:\cryptominisat-20150914\src>gdb --args cryptominisat64 --input=sf.cnf --dumpres=sf.res GNU gdb (GDB) 7.6 Copyright (C) 2013 Free Software Foundation, Inc. License GPLv3+: GNU GPL version 3 or later http://gnu.org/licenses/gpl.html This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law. Type "show copying" and "show warranty" for details. This GDB was configured as "x86_64-w64-mingw32". For bug reporting instructions, please see: http://www.gnu.org/software/gdb/bugs/... Reading symbols from D:\cryptominisat-20150914\src\cryptominisat64.exe...done. (gdb) run Starting program: D:\cryptominisat-20150914\src\cryptominisat64.exe "--input=sf.cnf" "--dumpres=sf.res" [New Thread 4012.0xf20] c Outputting solution to console c CryptoMiniSat version c CryptoMiniSat SHA revision c CryptoMiniSat compilation env c compiled with gcc version 4.8.1 c Executed with command line: D:\cryptominisat-20150914\src\cryptominisat64.exe --input=sf.cnf --dumpres=sf.res c Reading file 'sf.cnf' c -- header says num vars: 43476 c -- header says num clauses: 2088140 c -- clauses added: 2088140 c -- xor clauses added: 0 c -- vars added 43476 c Parsing time: 3.81 s c --> Executing strategy token: sub-impl c [impl sub] bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.40 T-out: N w-visit: 86952 c --> Executing strategy token: scc-vrepl c [clean] T: 0.0740 s c [simp] mem usage for occur of irred 35 MB c [simp] mem usage for occur of red 3 MB c [simp] Not linked in red 0/0 (0.00 %) c Mem for watch alloc : 54 MB (0.00 %) c Mem for watch array : 1 MB (0.00 %) c --> Executing OCC strategy token: occ-backw-sub-str c [sub] tri upI: 69267 subs w bin: 0 str w bin: 0 subs w tri: 24 str w tri: 6 tried: 2046034 str: 0 toDecrease: 315296382 0-d epth ass: 0 T: 1.00 T-out: N T-r: 15.76% c [sub] rem cl: 0 tried: 370890/37089 (1000.0%) T: 0.24 T-out: N c [str] sub: 0 str: 0 tried: 111267/37089 (300.0) T: 0.11 T-out: N c sub_str_with sub: 0 str: 0 T: 0.00 c --> Executing OCC strategy token: occ-clean-implicit c --> Executing OCC strategy token: occ-bve c Empty resolvent elimed: 61 T: 0.09 T-out: N c sub_str_with sub: 0 str: 0 T: 0.00 c impls_sub_lits T: 0.28 c iter v-elim 9925 c #try to eliminate: 43217 c #var-elim: 9925 c #T-o: Y c #T-r: -0.00% c #T: 4.64 c --> Executing OCC strategy token: c [clean] T: 0.0830 s c [occur] 0.4290 is overhead c [v-elim] elimed: 9986 / 30294 / 43278 T: 4.64 T-out: Y c [v-elim] cl-new: 25191 tried: 9925 tested: 43217 (0.0000 % aggressive) c [v-elim] subs: 26 red-bin rem: 0 red-tri rem: 0 red-long rem: 0 v-fix: 0 c [simp] link-in T: 0.2740 cleanup T: 0.1550 c [scc] new: 0 BP 1M T: 0.03 c calculated reachability. T: 0.001 c [polar] default polars - pos: 15663 neg: 17629 undec: 10184 T: 0.03 c 0 0 33292 31K 114 2008K 64.58 2.98 0 0 0 0.00 0.00 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 26 7001 33151 31K 114 2008K 64.58 2.98 6754 2 77 814.92 805.52 c [w-sort] T: 0.08 c [blk-lit-opt] T: 0.08 c 57 14002 33021 31K 114 2008K 64.57 2.98 13503 8 115 806.54 799.28 c 87 21K 32906 31K 114 2008K 64.57 2.98 20K 11 143 895.47 888.73 c [DBclean] locked:0 marked: 9984 glue: 114 ttl:4037 locked_solver:37 c [mem] Consolidated memory cls 46K old size 12285K new size 7181K T: 0.28 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 121 28K 32887 31K 93 1952K 63.76 2.98 17005 16 150 817.84 809.95 c [DBclean] locked:0 marked: 9976 glue: 639 ttl:2009 locked_solver:48 c [mem] Consolidated memory cls 44K old size 11505K new size 6794K T: 0.25 c 136 35K 32875 31K 103 1951K 63.84 2.98 13740 20 160 890.29 878.80 c 166 42K 32860 31K 103 1951K 63.84 2.98 20K 25 201 900.92 891.10 c [DBclean] locked:0 marked: 9950 glue: 778 ttl:2094 locked_solver:102 c [mem] Consolidated memory cls 44K old size 11259K new size 6035K T: 0.24 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 206 49K 32841 31K 183 1950K 64.01 2.98 17295 32 221 825.09 813.22 c [DBclean] locked:0 marked: 9957 glue: 1138 ttl:2599 locked_solver:87 c 246 56K 32826 31K 183 1950K 64.01 2.98 14095 39 259 687.85 673.65 c [mem] Consolidated memory cls 45K old size 11111K new size 6221K T: 0.24 c 290 63K 32816 31K 216 1949K 64.08 2.98 20K 47 285 691.40 680.58 c [DBclean] locked:0 marked: 9983 glue: 1724 ttl:2224 locked_solver:34 c [mem] Consolidated memory cls 45K old size 9756K new size 5003K T: 0.22 c newZeroDepthAss : 493 c [clean] T: 0.0960 s c recursive minimization too costly: 434074Kcost/(% lits removed) --> disabling c --> Executing strategy token: handle-comps c --> Executing strategy token: scc-vrepl c [scc] new: 142 BP 1M T: 0.03 c [clean] T: 0.1010 s c [vrep] vars 142 lits 129835 rem-bin-cls 568 rem-tri-cls 1 rem-long-cls 252 BP 0M T: 0.59 c --> Executing strategy token: cache-clean c [cache] cleaned. Updated: 0 K Cleaned: 0 K Freed: 0 K T: 0.00 c --> Executing strategy token: cache-tryboth c [bcache] 0-depth ass: 19 BXprop: 0 T: 0.03 c --> Executing strategy token: sub-impl c [impl sub] bin: 209 tri: 9 (stamp: 0, cache: 0) T: 0.43 T-out: N w-visit: 86952 c --> Executing strategy token: intree-probe c [clean] T: 0.1050 s c [scc] new: 2 BP 1M T: 0.03 c [clean] T: 0.1070 s c [vrep] vars 2 lits 729 rem-bin-cls 8 rem-tri-cls 0 rem-long-cls 0 BP 0M T: 0.18 c [clean] T: 0.1020 s c [scc] new: 0 BP 1M T: 0.03 c [clean] T: 0.1090 s c [vrep] vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 BP 0M T: 0.14 c [intree] Set 30 vars hyper-added: 284198 trans-irred::314 trans-red::1223 T: 2.48 T-out: Y T-r: -0.05% c --> Executing strategy token: probe c [clean] T: 0.1210 s c [probe] lits : 12.25M act vars: 32.60K BP+HP todo: 960.00M c [probe] NumProps after perf multi: 960.00M after numcall multi: 960.00M (<- final) c [clean] T: 0.1470 s c [probe] cleaning up after T: 0.15 s c [probe] 0-depth assigns: 171 bsame: 0 Flit: 24 Visited: 49108/65206(75.3%) c [probe] probed: 1448(2.2%) hyperBin:228346 transR-Irred:1342 transR-Red:15588 c [probe] BP: 619.4M HP: 338.4M T: 5.30 T-out: Y T-r: -0.37% c [probe] time spent updating cache during probing: 0.0% c --> Executing strategy token: sub-str-cls-with-bin c [clean] T: 0.1320 s c [clean] T: 0.1250 s c [distill] cache-based irred-- cl tried 20501 cl-sh 445 cl-rem 545 lit-rem 1347 T: 0.74 T-out: Y c [distill] cache-based red-- cl tried 4602 cl-sh 953 cl-rem 154 lit-rem 62564 T: 0.50 T-out: Y c --> Executing strategy token: distill-cls c [distill] longirred tried: 431/30042 cl-r:203 lit-r:278 T: 0.55 T-out: Y T-r: 100.28% c [distill] tri+long useful: 215/431/30237 lits-rem: 290 0-depth-assigns: 0 T: 0.55 T-out: Y c --> Executing strategy token: scc-vrepl c [scc] new: 1666 BP 1M T: 0.05 c [clean] T: 0.1240 s c [vrep] vars 1393 lits 2232536 rem-bin-cls 6102 rem-tri-cls 6 rem-long-cls 1425 BP 6M T: 0.89 c --> Executing strategy token: sub-impl c [impl sub] bin: 20400 tri: 10 (stamp: 0, cache: 0) T: 0.39 T-out: Y w-visit: 43408 c --> Executing strategy token: str-impl c [clean] T: 0.1350 s c [simp] mem usage for occur of irred 29 MB c [simp] mem usage for occur of red 155 MB c [simp] Not linked in red 7627/16221 (47.02 %) c Mem for watch alloc : 72 MB (0.00 %) c Mem for watch array : 1 MB (0.00 %) c --> Executing OCC strategy token: occ-backw-sub-str c [sub] tri upI: 1320 subs w bin: 5 str w bin: 31965 subs w tri: 0 str w tri: 101 tried: 2844645 str: 0 toDecrease: -81698 0- depth ass: 0 T: 1.05 T-out: Y T-r: -0.00% c [sub] rem cl: 2094 tried: 294878/45587 (646.8%) T: 0.98 T-out: Y c [str] sub: 27 str: 2899 tried: 127470/45587 (279.6) T: 0.48 T-out: Y

Program received signal SIGSEGV, Segmentation fault. CMSat::SubsumeStrengthen::strengthen_subsume_and_unlink_and_markirred (this=this@entry=0x33b9090, offset=1287217) at subsumestrengthen.cpp:139 139 ); (gdb) bt

0 CMSat::SubsumeStrengthen::strengthen_subsume_and_unlink_and_markirred (this=this@entry=0x33b9090, offset=1287217)

at subsumestrengthen.cpp:139

1 0x0000000000454a1d in CMSat::SubsumeStrengthen::handle_sub_str_with (this=0x33b9090) at subsumestrengthen.cpp:451

2 0x000000000047ea67 in CMSat::OccSimplifier::backward_sub_str (this=this@entry=0x33ac740) at occsimplifier.cpp:1022

3 0x0000000000486004 in fu1577ZSt4cout () at occsimplifier.cpp:918

4 0x0000000000486555 in CMSat::OccSimplifier::simplify (this=0x33ac740, _startup=_startup@entry=false,

schedule="occ-backw-sub-str, occ-xor, occ-clean-implicit, occ-bve, occ-bva, occ-gates, ") at occsimplifier.cpp:993

5 0x000000000041537f in fu1788ZTVSt9basic_iosIcSt11char_traitsIcEE () at solver.cpp:1618

6 0x0000000000415f31 in CMSat::Solver::simplify_problem (this=this@entry=0x33b2fa0, startup=startup@entry=false)

at solver.cpp:1766

7 0x000000000041642a in CMSat::Solver::iterate_until_solved (this=this@entry=0x33b2fa0) at solver.cpp:1559

8 0x0000000000417ade in fu342ZSt4cout () at solver.cpp:1343

9 0x0000000000464cbb in solve_with_assumptions (_assumptions=0x0, this=0x33b2fa0) at solver.h:429

10 CMSat::SATSolver::solve (this=0x339ab70, assumptions=assumptions@entry=0x0) at cryptominisat.cpp:551

11 0x0000000000402914 in fu74ZSt4cout () at main.cpp:1223

12 0x00000000004e0117 in main (argc=3, argv=0x3b2640) at main.cpp:1319

msoos commented 9 years ago

Thanks to both of you! I can reproduce it, debugging now :) Also, by the way, the .cnf.gz is usually uploaded to git gist: http://gist.github.com/ It's more for that kind of thing, I think.

msoos commented 9 years ago

5176fdc771702804b98512c4cf56d82c30b41344 fixes this issue. Thanks for everyone, it was really helpful!