[launch.sh] args:  /home/biere/hwmcc15/solvers/pdtrav/single.pdtravdeep /home/biere/hwmcc15/benchmarks/all/selection/random/intel024.aig
[launch.sh] host:  atom19 (atom19)
[launch.sh] start: Sat Sep 19 21:37:27 CEST 2015
[launch.sh] jobid: 7196268
[launch.sh] name:  intel024pdtravdeep
[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.pdtravdeep] removing /tmp/7196268.1.queue/intel024.aig
c [single.pdtravdeep] copying /home/biere/hwmcc15/benchmarks/all/selection/random/intel024.aig to /tmp/7196268.1.queue/intel024.aig
c [single.pdtravdeep] sync
c [single.pdtravdeep] 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 deep intel024.aig 
## Running Date: Sat Sep 19 21:37:30 CEST 2015
## Hostname: atom19
CPU time adjustment: 0.68 s (norm 0.68 s) - scale factor: 1.513333
-- DDI Manager Init.
-- FSM Manager Init.
-- FSM Loading.
# CONSTRAINTS: 0
Property: !o0.
Design Statistics: 352 Inputs / 357 State Vars / 5705 AIG Gates
|Constraint|=0 nodes.
|Constraint|=0 nodes.
-- FSM Manager Init.

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

Running reductions...(phase 1)
SCC0: l1416.
Implied Constraint l1414.

Running reductions...(phase 2)
Custom Reduction: Delta size 3164 (num = 192).
Constraint: AND[437].
Equivalence Found For l842-l1090.
Equivalence Found For l844-l1262.
Equivalence Found For l1044-l1252.
Equivalence Found For l976-l1244.
Equivalence Found For l894-l1042.
Equivalence Found For l1052-l1254.
Equivalence Found For l916-l986.
Equivalence Found For l900-l902.
Equivalence Found For l848-l972.
Equivalence Found For l850-l1124.
Equivalence Found For l852-l1128.
Equivalence Found For l854-l1132.
Equivalence Found For l856-l1136.
Equivalence Found For l858-l1140.
Equivalence Found For l860-l966.
Equivalence Found For l950-l956.
Equivalence Found For l952-l1148.
Equivalence Found For l832-l866.
Equivalence Found For l834-l1280.
Equivalence Found For l810-l826.
Equivalence Found For l812-l830.
Equivalence Found For l1062-l1246.
Equivalence Found For l846-l958.
Equivalence Found For l1066-l1248.
Equivalence Found For l770-l824.
Equivalence Found For l794-l892.
Equivalence Found For l808-l828.
Equivalence Found For l806-l822.
Equivalence Found For l946-l948.
Equivalence Found For l818-l820.
Equivalence Found For l818-l820.
Equivalence Found For l946-l948.
Equivalence Found For l806-l822.
Equivalence Found For l808-l828.
Equivalence Found For l794-l892.
Equivalence Found For l770-l824.
Equivalence Found For l1066-l1248.
Equivalence Found For l846-l958.
Equivalence Found For l1062-l1246.
Equivalence Found For l812-l830.
Equivalence Found For l810-l826.
Equivalence Found For l834-l1280.
Equivalence Found For l832-l866.
Equivalence Found For l952-l1148.
Equivalence Found For l950-l956.
Equivalence Found For l860-l966.
Equivalence Found For l858-l1140.
Equivalence Found For l856-l1136.
Equivalence Found For l854-l1132.
Equivalence Found For l852-l1128.
Equivalence Found For l850-l1124.
Equivalence Found For l848-l972.
Equivalence Found For l900-l902.
Equivalence Found For l916-l986.
Equivalence Found For l1052-l1254.
Equivalence Found For l894-l1042.
Equivalence Found For l976-l1244.
Equivalence Found For l1044-l1252.
Equivalence Found For l842-l1090.
Equivalence Found For l844-l1262.
68/192 relational latches left.
custom reduction DONE - delta size 2550 (num: 192).
-- FSM Manager Init.

Running reductions...(phase 3)
COI Reduction Performed: Kept 169 State Vars out of 192.
Ternary Simulation: COI Reduction Performed: Kept 165 State Vars out of 165.
-- TRAV Manager Init.
INITIALIZING THREADED ENGINES (stacksize = 16777216)
INITIALIZING 1 ENGINES: BMCPFL
-- FSM Manager Init.

Running BMCPFL ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 7249 - 61b7c880)

Thread BMCPFL activated
CREATED Thread (7249 - f2928700)
INITIALIZING 2 ENGINES: BMC BMC2
-- FSM Manager Init.

Running BMC ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 7249 - f2928700)

Thread BMC activated
CREATED Thread (7249 - f3929700)
-- MC Manager Init.
-- FSM Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.

Running BMC2 ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 7249 - f2928700)

Thread BMC2 activated
CREATED Thread (7249 - fd001700)
[launch.sh] stop:  Sat Sep 19 21:54:21 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: Sat Sep 19 21:54:24 CEST 2015
[launch.sh] out: cat /tmp/7196268.1.queue/intel024.pdtrav.out
u4
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
[launch.sh] done: Sat Sep 19 21:54:24 CEST 2015
