Git Product home page Git Product logo

Comments (2)

msoos avatar msoos commented on August 24, 2024

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

from riss.

conp-solutions avatar conp-solutions commented on August 24, 2024

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

from riss.

Related Issues (3)

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.