[launch.sh] args:  /home/biere/hwmcc15/solvers/pdtrav/single.pdtravthrd /home/biere/hwmcc15/benchmarks/all/selection/random/6s177.aig
[launch.sh] host:  atom07 (atom07)
[launch.sh] start: Fri Sep 18 19:43:59 CEST 2015
[launch.sh] jobid: 7194221
[launch.sh] name:  h6s177pdtravthrd
[launch.sh] round 1: killall abcpdr avy avybmc navy
[launch.sh] round 2: killall abcpdr avy avybmc navy
[launch.sh] round 3: killall abcpdr avy avybmc navy
c [single.pdtravthrd] removing /tmp/7194221.1.queue/6s177.aig
c [single.pdtravthrd] copying /home/biere/hwmcc15/benchmarks/all/selection/random/6s177.aig to /tmp/7194221.1.queue/6s177.aig
c [single.pdtravthrd] sync
c [single.pdtravthrd] starting actual solver

## Tool Version: PdTRAV 3.2.0
## DD Version: Cudd-2.5.0
## Compile Date: Tue Sep 15 13:18:00 CEST 2015
## Command: /home/biere/hwmcc15/solvers/pdtrav/pdtrav -strategy thrd 6s177.aig 
## Running Date: Fri Sep 18 19:44:02 CEST 2015
## Hostname: atom07
CPU time adjustment: 0.69 s (norm 0.69 s) - scale factor: 1.542222
-- DDI Manager Init.
-- FSM Manager Init.
-- FSM Loading.
# CONSTRAINTS: 0
Property: !o0.
Design Statistics: 13 Inputs / 160 State Vars / 800 AIG Gates
|Constraint|=0 nodes.
|Constraint|=0 nodes.
CREATING SYN Thread (father 9049 - 6272c880)

Thread SYN activated
CREATED Thread (9049 - ed4fc700)
-- FSM Manager Init.

Running reductions...(phase 0)
Clock found; Name: l194

Running reductions...(phase 1)

Running reductions...(phase 2)
-- FSM Manager Init.

Running reductions...(phase 3)
COI Reduction Performed: Kept 149 State Vars out of 150.
Ternary Simulation: TSIM found 123 EQUIVALENCES
COI Reduction Performed: Kept 130 State Vars out of 131.

Running reductions...(phase 4)
(null)       : i/o =   30/    1  lat =  128  and =   1201  lev = 18
RESULT: -2 (SYN - 15 - 0)
(null)       : i/o =   30/    1  lat =  125  and =   1048  lev = 18
(null)       : i/o =   30/    1  lat =  125  and =   1031  lev = 18
Delta: 128 -> 125
Lambda: 1 -> 1
latches: 125 -> 125
inputs: 30 -> 29
|Constraint|=0 nodes.
-- TRAV Manager Init.
INITIALIZING THREADED ENGINES (stacksize = 16777216)
INITIALIZING 4 ENGINES: BDD PDRPFL ITPPFL BMCPFL
-- FSM Manager Init.

Running BDD ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 9049 - 6272c880)

Thread BDD activated
CREATED Thread (9049 - f24fe700)
-- FSM Manager Init.
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.

Running PDRPFL ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 9049 - 6272c880)

Thread PDRPFL activated
CREATED Thread (9049 - f34ff700)
INITIALIZING 2 ENGINES: PDR PDR2-- FSM Manager Init.


Running ITPPFL ...
-- FSM Manager Init.
-- FSM Manager Init.

Running PDR ...
-- FSM Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 9049 - 6272c880)

Thread ITPPFL activated
CREATED Thread (9049 - fd001700)
INITIALIZING 2 ENGINES:-- FSM Manager Init.
 ITP IGR

Running BMCPFL ...
-- FSM Manager Init.
-- FSM Manager Init.

Running ITP ...
-- FSM Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 9049 - f34ff700)

Thread PDR activated
-- FSM Manager Init.

Running PDR2 ...
-- FSM Manager Init.
CREATED Thread (9049 - fe002700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
STATS NUM: 4
CREATING Thread (father 9049 - 6272c880)

Thread BMCPFL activated
CREATED Thread (9049 - ff003700)
INITIALIZING 3 ENGINES: BMC SIM BMC2
-- FSM Manager Init.

Running BMC ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 9049 - fd001700)

Thread ITP activated
-- FSM Manager Init.

Running IGR ...
-- FSM Manager Init.
CREATED Thread (9049 - d002700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 9049 - f34ff700)

Thread PDR2 activated
CREATED Thread (9049 - e003700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
STATS NUM: 4
CREATING Thread (father 9049 - fd001700)

Thread IGR activated
CREATED Thread (9049 - f004700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
CREATING Thread (father 9049 - ff003700)

Thread BMC activated
CREATED Thread (9049 - 1d002700)
-- FSM Manager Init.
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.

Running SIM ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 9049 - ff003700)

Thread SIM activated
-- FSM Manager Init.

Running BMC2 ...
-- FSM Manager Init.
CREATED Thread (9049 - 1e003700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
(null)       : i/o =   21/    1  lat =  126  and =   1080  lev = 19
-- DDI Manager Init.
CREATING Thread (father 9049 - ff003700)

Thread BMC2 activated
CREATED Thread (9049 - 1f004700)
BLOCKED START (BMC2 - 1 - 10)
|Tr| = 22599 #Part = 42
UNBLOCKED START (BMC2 - 1 - 10)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
Number of forced suspensions: 0
Invariant verification TERMINATED with -2 [PDR]
Invariant verification aborted by engine: PDR
Simulated 20 frames for 163578 rounds with 1635 restarts.  Reached timeout (4000 sec).
There is no current CEX.
Invariant verification TERMINATED with -2 [SIM]
Invariant verification aborted by engine: SIM
[launch.sh] stop:  Fri Sep 18 20:44:02 CEST 2015
[launch.sh] round 1: killall abcpdr avy avybmc navy
[launch.sh] round 2: killall abcpdr avy avybmc navy
[launch.sh] round 3: killall abcpdr avy avybmc navy
[launch.sh] sync: Fri Sep 18 20:44:05 CEST 2015
[launch.sh] out: cat /tmp/7194221.1.queue/6s177.pdtrav.out
u4
u6
u8
u10
u12
u14
u16
u18
u20
u22
u24
u26
u28
u30
u32
u34
u36
u38
u40
u42
u44
u46
u48
u50
u52
u54
u56
u58
u60
u62
u64
u66
u68
u70
u72
u74
u76
u78
u80
u82
u84
u86
u88
u90
u92
u94
u96
u98
u100
u102
u104
u106
u108
u110
u112
u114
u116
u118
u120
u122
u124
u126
u128
u130
u132
u134
u136
u138
u140
u142
u144
u146
u148
u150
u152
u154
u156
u158
u160
u162
u164
u166
u168
u170
u172
u174
u176
u178
u180
u182
u184
u186
u188
u190
u192
u194
u196
u198
u200
u202
u204
u206
u208
u210
u212
u214
u216
u218
u220
u222
u224
u226
u228
u230
u232
u234
u236
u238
u240
u242
u244
u246
u248
u250
u252
u254
u256
u258
u260
u262
u264
u266
u268
u270
u272
u274
u276
u278
u280
u282
u284
u286
u288
u290
u292
u294
u296
u298
u300
u302
u304
u306
u308
u310
u312
u314
u316
u318
u320
u322
u324
u326
u328
u330
u332
u334
u336
u338
u340
u342
u344
u346
u348
u350
u352
u354
u356
u358
u360
u362
u364
u366
u368
u370
u372
u374
u376
u378
u380
u382
u384
u386
u388
u390
u392
u394
u396
u398
u400
u402
u404
u406
u408
u410
u412
u414
u416
u418
u420
u422
u424
u426
u428
u430
u432
u434
u436
u438
u440
u442
u444
u446
u448
u450
u452
u454
u456
u458
u460
u462
u464
u466
u468
u470
u472
u474
u476
u478
u480
u482
u484
u486
u488
u490
u492
u494
u496
u498
u500
u502
u504
u506
u508
u510
u512
u514
u516
u518
u520
u522
u524
u526
u528
u530
u532
[launch.sh] done: Fri Sep 18 20:44:05 CEST 2015
