[launch.sh] args:  /home/biere/hwmcc15/solvers/pdtrav/single.pdtravthrd /home/biere/hwmcc15/benchmarks/all/selection/random/intel045.aig
[launch.sh] host:  atom23 (atom23)
[launch.sh] start: Sat Sep 19 23:47:27 CEST 2015
[launch.sh] jobid: 7196397
[launch.sh] name:  intel045pdtravthrd
[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/7196397.1.queue/intel045.aig
c [single.pdtravthrd] copying /home/biere/hwmcc15/benchmarks/all/selection/random/intel045.aig to /tmp/7196397.1.queue/intel045.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 intel045.aig 
## Running Date: Sat Sep 19 23:47:30 CEST 2015
## Hostname: atom23
CPU time adjustment: 0.67 s (norm 0.67 s) - scale factor: 1.508889
-- DDI Manager Init.
-- FSM Manager Init.
-- FSM Loading.
# CONSTRAINTS: 0
Property: !o0.
Design Statistics: 642 Inputs / 647 State Vars / 6853 AIG Gates
|Constraint|=0 nodes.
|Constraint|=0 nodes.
CREATING SYN Thread (father 10184 - 622ff880)

Thread SYN activated
CREATED Thread (10184 - 12513700)
-- FSM Manager Init.

Running reductions...(phase 0)
Clock pair found; Names: l2570 - l2572.

Running reductions...(phase 1)
SCC0: l2578.
Implied Constraint l2574.

Running reductions...(phase 2)
Custom Reduction: Delta size 3887 (num = 290).
Constraint: AND[501].
Equivalence Found For l1826-l1848.
Equivalence Found For l1828-l1846.
Equivalence Found For l2536-l2542.
Equivalence Found For l2538-l2540.
Equivalence Found For l1840-l2348.
Equivalence Found For l1854-l2530.
Equivalence Found For l1288-l2572.
Complement.
Equivalence Found For l1288-l2572.
Complement.
Equivalence Found For l1854-l2530.
Equivalence Found For l1840-l2348.
Equivalence Found For l2538-l2540.
Equivalence Found For l2536-l2542.
Equivalence Found For l1826-l1848.
Equivalence Found For l1828-l1846.
44/290 relational latches left.
custom reduction DONE - delta size 2683 (num: 290).
-- FSM Manager Init.

Running reductions...(phase 3)
COI Reduction Performed: Kept 273 State Vars out of 290.
Ternary Simulation: TSIM found 216 EQUIVALENCES
COI Reduction Performed: Kept 232 State Vars out of 254.
-- 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 10184 - 622ff880)

Thread PDRPFL activated
CREATED Thread (10184 - 17515700)
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 10184 - 622ff880)

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

Running BMCPFL ...
-- FSM Manager Init.

Running ITP ...
-- FSM Manager Init.
CREATING Thread (father 10184 - 17515700)

Thread PDR activated
CREATED Thread (10184 - 26003700)
-- FSM Manager Init.
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
STATS NUM: 4

Running PDR2 ...
-- FSM Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 10184 - 622ff880)

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

Running BMC ...
-- FSM Manager Init.
CREATING Thread (father 10184 - 25002700)
CREATING Thread (father 10184 - 17515700)

Thread PDR2 activated

Thread ITP activated
-- FSM Manager Init.
CREATED Thread (10184 - 36003700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
STATS NUM: 4

Running IGR ...
-- FSM Manager Init.
CREATED Thread (10184 - 35002700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 10184 - 27004700)

Thread BMC activated
-- FSM Manager Init.
CREATED Thread (10184 - 37004700)

Running SIM ...
-- FSM Manager Init.
CREATING Thread (father 10184 - 25002700)

Thread IGR activated
CREATED Thread (10184 - 41001700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- DDI Manager Init.
CREATING Thread (father 10184 - 27004700)

Thread SIM activated
CREATED Thread (10184 - 42002700)
-- FSM Manager Init.
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.

Running BMC2 ...
-- FSM Manager Init.
Invariant verification TERMINATED with -2 [SIM]
-- DDI Manager Init.
CREATING Thread (father 10184 - 27004700)

Thread BMC2 activated
Invariant verification aborted by engine: SIM
CREATED Thread (10184 - 43003700)
BLOCKED START (BMC2 - 1 - 9)
RESULT: -2 (SYN - 15 - 0)
CEX of failure
Number of forced suspensions: 0
Invariant verification TERMINATED with 1 [PDR]
Invariant verification ABORTED by 7 ...
Invariant verification TERMINATED with -2 [IGR]
Invariant verification aborted by engine: IGR
CEX of failure
Number of forced suspensions: 0
Invariant verification TERMINATED with 1 [PDR2]
FWD ITP fix-point at depth 1
Invariant verification TERMINATED with 0 [ITP]

Invariant verification completed by engine: ITP

Invariant verification completed by engine: ITPPFL
Verification result (PASS) written to file intel045.pdtrav.out
Total used memory: 36.57 MBytes
Total Verification Time: 1.2
Total Execution Time: 2.48 s (norm 1.80 s)
## PdTRAV End.
[launch.sh] stop:  Sat Sep 19 23:55:51 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 23:55:54 CEST 2015
[launch.sh] out: cat /tmp/7196397.1.queue/intel045.pdtrav.out
[Armin Biere: manually commented out since above FATAL error message not caught]
cu4
cu6
cu8
cu10
cu12
cu14
cu16
cu18
cu20
cu22
cu24
cu26
cu28
cu30
cu32
cu34
cu36
cu38
cu40
cu42
cu44
cu46
cu48
cu50
cu52
cu54
cu56
cu58
cu60
cu62
c0
[launch.sh] done: Sat Sep 19 23:55:54 CEST 2015
