conp-solutions / riss Goto Github PK

(echo "p cnf 0 1" && echo "0"  ) | riss
...
c CPU time              : 0.000156 s

s UNSATISFIABLE

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)

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