search

mgudemann / iimc

Other
11 stars 6 forks source link

SIGSEV on HWMCC12 benchmark with satsweep tactic #2

Closed mgudemann closed 7 years ago

mgudemann commented 7 years ago 
iimc -v3 -t satsweep  bob12s04.aig 
Input File is bob12s04.aig
# iimc -v3 -t satsweep bob12s04.aig
ExprAttachment: building from file
CombAttachment: building
AIGAttachment: Building AIG for model bob12s04.aig
AIGAttachment: Done with building AIG
SAT Sweeping: Number of AIG nodes = 268210
SAT Sweeping: Running with a timeout of 10 seconds + 0 seconds of relayed time
SAT Sweeping: Performing initial refinement of classes
SAT Sweeping: Done with initial refinement
SAT Sweeping: Simulated 84 random vectors
fish: Job 1, “iimc -v3 -t satsweep  bob12s04.aig ” terminated by signal SIGSEGV (Address boundary error)
mgudemann commented 7 years ago

Problem seems to be in

Program received signal SIGSEGV, Segmentation fault.
Opt::buildClauses (aig=..., ref=ref@entry=228670, v=..., clauses=std::vector of length 525339, capacity 1048576 = {...}, idOfAigRef=std::unordered_map with 501118 elements = {...}, 
    satIdOfRef=satIdOfRef@entry=0x7fffffffd110, visited=std::vector of length 268210, capacity 268210 = {...}) at src/copt/AIGUtil.cpp:66

while NodeRef should be defined as unsigned long, something else is supplied here

mgudemann commented 7 years ago

solved by raising rlimit