[launch.sh] args:  /home/biere/hwmcc15/solvers/pdtrav/single.pdtravthrd /home/biere/hwmcc15/benchmarks/hwmcc14/single/6s274r.aig
[launch.sh] host:  atom06 (atom06)
[launch.sh] start: Tue Sep 15 23:11:59 CEST 2015
[launch.sh] jobid: 7190125
[launch.sh] name:  h6s274rpdtravthrd
[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/7190125.1.queue/6s274r.aig
c [single.pdtravthrd] copying /home/biere/hwmcc15/benchmarks/hwmcc14/single/6s274r.aig to /tmp/7190125.1.queue/6s274r.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 6s274r.aig 
## Running Date: Tue Sep 15 23:12:02 CEST 2015
## Hostname: atom06
CPU time adjustment: 0.68 s (norm 0.68 s) - scale factor: 1.517778
-- DDI Manager Init.
-- FSM Manager Init.
-- FSM Loading.
# CONSTRAINTS: 0
Property: !o0.
Design Statistics: 76 Inputs / 1712 State Vars / 10189 AIG Gates
|Constraint|=0 nodes.
|Constraint|=0 nodes.
CREATING SYN Thread (father 26476 - 62ac5880)

Thread SYN activated
CREATED Thread (26476 - 840d5700)
-- FSM Manager Init.

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

Running reductions...(phase 1)
compacting deltas (EQ prop): 10190 -> 10189
compacting miters (EQ prop): 12 -> 12
Checking for Equivalence Property: OK (1/1 Equivalences Found).

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

Running reductions...(phase 3)
COI Reduction Performed: Kept 1244 State Vars out of 1714.
Ternary Simulation: EQ refinements: 3797
EQ refinements: 0
SAT FOUND 44 EQUIVALENCES
COI Reduction Performed: Kept 1244 State Vars out of 1244.
EQ refinements: 3744
EQ refinements: 0
COI Reduction Performed: Kept 1244 State Vars out of 1244.
COI Reduction Performed: Kept 1244 State Vars out of 1244.
Ternary Simulation: EQ refinements: 3744
EQ refinements: 0
COI Reduction Performed: Kept 1244 State Vars out of 1244.

Running reductions...(phase 4)
(null)       : i/o =  150/    1  lat = 1242  and =   9769  lev = 31
RESULT: -2 (SYN - 15 - 0)
(null)       : i/o =  150/    1  lat = 1242  and =   8900  lev = 27
-- TRAV Manager Init.
INITIALIZING THREADED ENGINES (stacksize = 16777216)
INITIALIZING 4 ENGINES: LMS PDRPFL ITPPFL BMCPFL
-- FSM Manager Init.

Running LMS ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 26476 - 62ac5880)

Thread LMS activated
CREATED Thread (26476 - 890d7700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- FSM Manager Init.

Running PDRPFL ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 26476 - 62ac5880)

Thread PDRPFL activated
CREATED Thread (26476 - 8a0d8700)
INITIALIZING 2 ENGINES: PDR PDR2
-- FSM Manager Init.
-- FSM Manager Init.

Running PDR ...
-- FSM Manager Init.

Running ITPPFL ...
-- FSM Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 26476 - 8a0d8700)

Thread PDR activated
CREATED Thread (26476 - 8b0d9700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
STATS NUM: 4
-- FSM Manager Init.
CREATING Thread (father 26476 - 62ac5880)

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

Running BMCPFL ...
-- FSM Manager Init.

Running PDR2 ...
-- FSM Manager Init.

Running ITP ...
-- FSM Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 26476 - 95001700)

Thread ITP activated
-- FSM Manager Init.

Running IGR ...
-- FSM Manager Init.
CREATED Thread (26476 - 96002700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
CREATING Thread (father 26476 - 62ac5880)

Thread BMCPFL activated
CREATED Thread (26476 - 97003700)
INITIALIZING 3 ENGINES: BMC SIM BMC2
CREATING Thread (father 26476 - 8a0d8700)

Thread PDR2 activated
CREATED Thread (26476 - a5002700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
STATS NUM: 4
-- FSM Manager Init.

Running BMC ...
-- FSM Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 26476 - 95001700)

Thread IGR activated
CREATED Thread (26476 - a6003700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
CREATING Thread (father 26476 - 97003700)

Thread BMC activated
CREATED Thread (26476 - a7004700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- FSM Manager Init.

Running SIM ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 26476 - 97003700)

Thread SIM activated
CREATED Thread (26476 - c1004700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- FSM Manager Init.

Running BMC2 ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 26476 - 97003700)

Thread BMC2 activated
CREATED Thread (26476 - c2005700)
BLOCKED START (BMC2 - 1 - 10)
(null)       : i/o =  150/    1  lat = 1242  and =   9769  lev = 31
*** Gen. lemmas iteration 0 ***
Simulation time: 2.09 s (norm 1.41 s)
Potential eq.: 264+347
Proved equiv.: 0+1 in 2.12 s (8 iter, 316 total run)
Rewriting: |delta| = 11167 -> 11165.
Rewriting: |lambda| = 3 -> 3.
*** Gen. lemmas iteration 0 ***
Simulation time: 15.16 s (norm 10.03 s)
Potential eq.: 3171+2837
Remaining eq.: 3171+2837 in 0.13 s (1 iter, 1 total run, 0.00 s)
*** Gen. lemmas iteration 1 ***
Potential eq.: 3171+2837
Proved equiv.: 3+17 in 54.22 s (110 iter, 2120 total run)
Potential eq.: 3160+2828
Remaining eq.: 3160+2828 in 0.22 s (1 iter, 1 total run, 0.00 s)
*** Gen. lemmas iteration 2 ***
Potential eq.: 3160+2828
Proved equiv.: 0+13 in 97.75 s (113 iter, 1938 total run)
Potential eq.: 3147+2828
Remaining eq.: 3147+2828 in 0.51 s (1 iter, 1 total run, 0.00 s)
*** Gen. lemmas iteration 3 ***
Potential eq.: 3147+2828
Remaining eq.: 3147+2828 in 0.62 s (1 iter, 1 total run, 0.01 s)
*** Gen. lemmas iteration 4 ***
Potential eq.: 3147+2828
UNBLOCKED START (BMC2 - 1 - 10)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
Proved equiv.: 0+0 in 185.33 s (103 iter, 1946 total run)
Potential eq.: 3147+2828
Remaining eq.: 3147+2828 in 0.94 s (1 iter, 1 total run, 0.00 s)
*** Gen. lemmas iteration 5 ***
Potential eq.: 3147+2828
Remaining eq.: 3147+2828 in 1.11 s (1 iter, 1 total run, 0.01 s)
*** Gen. lemmas iteration 6 ***
Potential eq.: 3147+2828
Simulated 20 frames for 9018 rounds with 90 restarts.  Reached timeout (4000 sec).
There is no current CEX.
Invariant verification TERMINATED with -2 [SIM]
Invariant verification aborted by engine: SIM
Abort due to time limit
Rewriting: |delta| = 11165 -> 11132.
Rewriting: |lambda| = 3 -> 1.
Total lemma generation time: 912.64 s (norm 600.74 s).
-- TR Manager Init.
[launch.sh] stop:  Wed Sep 16 00:12: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: Wed Sep 16 00:12:05 CEST 2015
[launch.sh] out: cat /tmp/7190125.1.queue/6s274r.pdtrav.out
u1
u3
u5
u7
u9
u11
u13
u15
u17
u19
u21
u23
u25
u27
u29
u31
u33
u35
u37
u39
u41
u43
u45
u47
u49
u51
u53
u55
u57
u59
u61
u63
u65
u67
u69
u71
u73
u75
u77
u79
u81
u83
u85
u87
u89
u91
u93
u95
u97
u99
u101
u103
u105
u107
u109
u111
u113
u115
u117
u119
u121
u123
u125
u127
u129
u131
u133
u135
u137
u139
u141
u143
u145
u147
u149
u151
u153
u155
u157
u159
u161
u163
u165
u167
u169
u171
u173
u175
u177
u179
u181
u183
u185
u187
u189
u191
u193
u195
u197
u199
u201
u203
u205
u207
u209
u211
u213
u215
u217
u219
u221
u223
u225
u227
u229
u231
u233
u235
u237
u239
u241
u243
u245
u247
u249
u251
u253
u255
u257
u259
u261
u263
u265
u267
u269
u271
u273
u275
u277
u279
u281
u283
u285
u287
u289
u291
u293
u295
u297
u299
u301
u303
u305
u307
u309
u311
u313
u315
u317
u319
u321
u323
u325
u327
u329
u331
u333
u335
u337
u339
u341
u343
u345
u347
u349
u351
u353
u355
u357
u359
u361
u363
u365
u367
u369
u371
u373
u375
u377
u379
u381
u383
u385
u387
u389
u391
u393
u395
u397
u399
u401
u403
u405
u407
u409
u411
u413
u415
u417
u419
u421
u423
u425
u427
u429
u431
u433
u435
u437
u439
u441
u443
u445
u447
u449
u451
u453
u455
u457
u459
u461
u463
u465
u467
u469
u471
u473
u475
u477
u479
u481
u483
u485
u487
u489
u491
u493
u495
u497
u499
u501
u503
u505
u507
u509
u511
u513
u515
u517
u519
u521
u523
u525
u527
u529
u531
u533
u535
u537
u539
u541
u543
u545
u547
u549
u551
u553
u555
u557
u559
u561
u563
u565
u567
u569
u571
u573
u575
u577
u579
u581
u583
u585
u587
u589
u591
u593
u595
u597
u599
u601
u603
u605
u607
u609
u611
u613
u615
u617
u619
u621
u623
u625
u627
u629
u631
u633
u635
u637
u639
u641
u643
u645
u647
u649
u651
u653
u655
[launch.sh] done: Wed Sep 16 00:12:05 CEST 2015
