[launch.sh] args:  /home/biere/hwmcc15/solvers/pdtrav/single.pdtravthrd /home/biere/hwmcc15/benchmarks/all/selection/random/intel024.aig
[launch.sh] host:  atom04 (atom04)
[launch.sh] start: Sat Sep 19 21:40:07 CEST 2015
[launch.sh] jobid: 7196269
[launch.sh] name:  intel024pdtravthrd
[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/7196269.1.queue/intel024.aig
c [single.pdtravthrd] copying /home/biere/hwmcc15/benchmarks/all/selection/random/intel024.aig to /tmp/7196269.1.queue/intel024.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 intel024.aig 
## Running Date: Sat Sep 19 21:40:11 CEST 2015
## Hostname: atom04
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.
CREATING SYN Thread (father 8460 - 612ab880)

Thread SYN activated
CREATED Thread (8460 - ffa1c700)
-- 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 3 ENGINES: PDRPFL ITPPFL BMCPFL
-- FSM Manager Init.

Running PDRPFL ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 8460 - 612ab880)

Thread PDRPFL activated
CREATED Thread (8460 - 4a1e700)
INITIALIZING 2 ENGINES: PDR PDR2-- FSM Manager Init.

-- FSM Manager Init.

Running ITPPFL ...
-- FSM Manager Init.

Running PDR ...
-- FSM Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 8460 - 612ab880)

Thread ITPPFL activated
CREATED Thread (8460 - 5a1f700)
INITIALIZING 2 ENGINES: ITP IGR
-- FSM Manager Init.
-- FSM Manager Init.

Running BMCPFL ...
-- FSM Manager Init.

Running ITP ...
-- FSM Manager Init.
CREATING Thread (father 8460 - 4a1e700)

Thread PDR activated
-- FSM Manager Init.

Running PDR2 ...
-- FSM Manager Init.
CREATED Thread (8460 - 6a20700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
STATS NUM: 4
-- DDI Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 8460 - 5a1f700)

Thread ITP activated
-- FSM Manager Init.

Running IGR ...
-- FSM Manager Init.
CREATING Thread (father 8460 - 612ab880)
CREATED Thread (8460 - 7a21700)
-- MC Manager Init.

Thread BMCPFL activated
CREATED Thread (8460 - 15002700)
INITIALIZING 3 ENGINES: BMC SIM BMC2
-- FSM Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.

Running BMC ...
-- FSM Manager Init.
CREATING Thread (father 8460 - 4a1e700)

Thread PDR2 activated
CREATED Thread (8460 - 16003700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
STATS NUM: 4
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 8460 - 5a1f700)

Thread IGR activated
CREATED Thread (8460 - 17004700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
CREATING Thread (father 8460 - 15002700)

Thread BMC activated
CREATED Thread (8460 - 21001700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- FSM Manager Init.

Running SIM ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 8460 - 15002700)

Thread SIM activated
-- FSM Manager Init.

Running BMC2 ...
-- FSM Manager Init.
CREATED Thread (8460 - 22002700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- DDI Manager Init.
Invariant verification TERMINATED with -2 [SIM]
CREATING Thread (father 8460 - 15002700)

Thread BMC2 activated
CREATED Thread (8460 - 23003700)
BLOCKED START (BMC2 - 1 - 9)
Invariant verification aborted by engine: SIM
RESULT: -2 (SYN - 15 - 0)
FWD ITP fix-point at depth 11
Invariant verification TERMINATED with 0 [IGR]

Invariant verification completed by engine: IGR

Invariant verification completed by engine: ITPPFL
Verification result (PASS) written to file intel024.pdtrav.out
Total used memory: 35.00 MBytes
Total Verification Time: 0.8
Total Execution Time: 2.13 s (norm 1.45 s)
## PdTRAV End.
[launch.sh] stop:  Sat Sep 19 21:40:41 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:40:45 CEST 2015
[launch.sh] out: cat /tmp/7196269.1.queue/intel024.pdtrav.out
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
0
[launch.sh] done: Sat Sep 19 21:40:45 CEST 2015
