Comments (2)
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.
Thanks Mate. I'll finally have a look into this.
from riss.
Related Issues (3)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
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.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from riss.