[launch.sh] args:  /home/biere/hwmcc15/solvers/pdtrav/single.pdtravthrd /home/biere/hwmcc15/benchmarks/all/selection/random/6s7.aig
[launch.sh] host:  atom08 (atom08)
[launch.sh] start: Sat Sep 19 13:46:15 CEST 2015
[launch.sh] jobid: 7195725
[launch.sh] name:  h6s7pdtravthrd
[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/7195725.1.queue/6s7.aig
c [single.pdtravthrd] copying /home/biere/hwmcc15/benchmarks/all/selection/random/6s7.aig to /tmp/7195725.1.queue/6s7.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 6s7.aig 
## Running Date: Sat Sep 19 13:46:18 CEST 2015
## Hostname: atom08
CPU time adjustment: 0.66 s (norm 0.66 s) - scale factor: 1.480000
-- DDI Manager Init.
-- FSM Manager Init.
-- FSM Loading.
# CONSTRAINTS: 0
Property: !o0.
Design Statistics: 45 Inputs / 504 State Vars / 2109 AIG Gates
|Constraint|=0 nodes.
|Constraint|=0 nodes.
CREATING SYN Thread (father 7430 - 60b77880)

Thread SYN activated
CREATED Thread (7430 - 95279700)
-- FSM Manager Init.

Running reductions...(phase 0)

Running reductions...(phase 1)

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

Running reductions...(phase 3)
COI Reduction Performed: Kept 505 State Vars out of 505.
Ternary Simulation: TSIM found 1 EQUIVALENCES
COI Reduction Performed: Kept 498 State Vars out of 498.
-- 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 7430 - 60b77880)

Thread BDD activated
CREATED Thread (7430 - 9a27b700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- FSM Manager Init.

Running PDRPFL ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 7430 - 60b77880)

Thread PDRPFL activated
CREATED Thread (7430 - 9b27c700)
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 7430 - 9b27c700)

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

Running PDR2 ...
-- FSM Manager Init.
CREATING Thread (father 7430 - 60b77880)

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

Running BMCPFL ...
-- FSM Manager Init.

Running ITP ...
-- FSM Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 7430 - 9b27c700)

Thread PDR2 activated
CREATED Thread (7430 - a7003700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
STATS NUM: 4
CREATING Thread (father 7430 - 60b77880)

Thread BMCPFL activated
CREATING Thread (father 7430 - a6002700)

Thread ITP activated
-- FSM Manager Init.
CREATED Thread (7430 - b5002700)
INITIALIZING 3 ENGINES:
Running IGR ...
-- FSM Manager Init.
CREATED Thread (7430 - b6003700)
-- MC Manager Init.
 BMC SIM BMC2
-- TRAV Manager Init.
-- TR Manager Init.
-- FSM Manager Init.

Running BMC ...
-- FSM Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
CREATING Thread (father 7430 - b5002700)

Thread BMC activated
-- FSM Manager Init.

Running SIM ...
-- FSM Manager Init.
CREATED Thread (7430 - b7004700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
CREATING Thread (father 7430 - a6002700)

Thread IGR activated
CREATED Thread (7430 - c1001700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- DDI Manager Init.
CREATING Thread (father 7430 - b5002700)

Thread SIM activated
-- FSM Manager Init.

Running BMC2 ...
-- FSM Manager Init.
CREATED Thread (7430 - c2002700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- DDI Manager Init.
CREATING Thread (father 7430 - b5002700)

Thread BMC2 activated
CREATED Thread (7430 - c3003700)
BLOCKED START (BMC2 - 1 - 10)
RESULT: -2 (SYN - 15 - 0)
(null)       : i/o =   45/    1  lat =  497  and =   3198  lev = 24
UNBLOCKED START (BMC2 - 1 - 10)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
Simulated 20 frames for 46663 rounds with 466 restarts.  Reached timeout (4000 sec).
There is no current CEX.
Invariant verification TERMINATED with -2 [SIM]
Invariant verification aborted by engine: SIM
Number of forced suspensions: 0
Invariant verification TERMINATED with -2 [PDR]
Invariant verification aborted by engine: PDR
BMC failure at bound 80.
Total SAT time: 364.60 s (norm 246.30 s), total BMC time: 364.60 s (norm 246.30 s).
Invariant verification TERMINATED with 1 [BMC2]

cex written to: /tmp/6s7.pdtrav.out.10.cex
CEX validated by aigsim

Invariant verification completed by engine: BMC2

Invariant verification completed by engine: BMCPFL
Verification result (FAIL) written to file 6s7.pdtrav.out
CMD: cat /tmp/6s7.pdtrav.out.10.cex >> 6s7.pdtrav.out
Total used memory: 33.60 MBytes
Total Verification Time: 0.3
Total Execution Time: 1.26 s (norm 0.94 s)
## PdTRAV End.
[launch.sh] stop:  Sat Sep 19 14:08:00 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 14:08:03 CEST 2015
[launch.sh] out: cat /tmp/7195725.1.queue/6s7.pdtrav.out
u1
u2
u3
u4
u5
u6
u7
u8
u9
u10
u11
u12
u13
u14
u15
u16
u17
u18
u19
u20
u21
u22
u23
u24
u25
u26
u27
u28
u29
u30
u31
u32
u33
1
b0
000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
001101000010000000000000011001000000010000000
xxxxxxxx0001100000xxxx00000101000x00x01000000
xxxxxxxx0000000001xxxx00111000000x10x10010010
xxxxxxxx0110000001xxxx10001100001x01x00010101
xxxxxxxx0000001001xxxx11101001000x00x00011000
xxxxxxxx0000011000xxxx00011000000x00x10000100
xxxxxxxx0000011001xxxx00011000001x00x11000010
xxxxxxxx0100011001xxxx00011100010x00x11000100
xxxxxxxx0000001000xxxx00011000010x10x11000000
xxxxxxxx0010100001xxxx00001000010x00x11000010
xxxxxxxx0100100011xxxx00001000000x10x10000010
xxxxxxxx0000010000xxxx00011100001x10x11000001
xxxxxxxx0000101001xxxx01011101000x10x10000000
xxxxxxxx0000000001xxxx00011001001x10x11000010
xxxxxxxx1000001000xxxx00100000000x10x10100000
xxxxxxxx0000101001xxxx00011000000x10x11110010
xxxxxxxx0000101001xxxx01001101000x10x10000000
xxxxxxxx0000011001xxxx00001000000x10x11001010
xxxxxxxx0000011001xxxx00100000000x10x10000010
xxxxxxxx0000011011xxxx00001000001x00x10110011
xxxxxxxx0000101001xxxx00001000001x10x10000011
xxxxxxxx0010101000xxxx00101000000x10x10010011
xxxxxxxx0000001001xxxx00101101001x11x10001011
xxxxxxxx0000011010xxxx00101101001x11x10010010
xxxxxxxx1100101001xxxx00111001000x10x10001010
xxxxxxxx0000101001xxxx01011100010x10x10000010
xxxxxxxx0010100001xxxx00110100010x10x10000011
xxxxxxxx0010001001xxxx00001000001x10x00000000
xxxxxxxx0000101000xxxx00111101010x00x10010010
xxxxxxxx0000100000xxxx00000001010x10x10010011
xxxxxxxx0000001000xxxx00111000100x10x10010011
xxxxxxxx0000101011xxxx00000101010x00x10000110
xxxxxxxx0010100000xxxx00100001011x00x10001010
xxxxxxxx0000010010xxxx00101101010x10x10001010
xxxxxxxx0000000011xxxx01101101010x00x10001011
xxxxxxxx0000000100xxxx01001100001x10x11000010
xxxxxxxx0000010001xxxx00100001000x00x10001110
xxxxxxxx0000101000xxxx00100101001x00x10000000
xxxxxxxx0000101000xxxx00100000100x00x10101110
xxxxxxxx0000000001xxxx01001101010x10x10001110
xxxxxxxx0000100001xxxx00101001001x00x00000011
xxxxxxxx0000001001xxxx00011000010x10x11011110
xxxxxxxx0000001000xxxx00011000010x10x10011000
xxxxxxxx0001001001xxxx01001001110x11x10000010
xxxxxxxx0000000001xxxx00001001000x10x11010010
xxxxxxxx0000000001xxxx00001001000x10x11001000
xxxxxxxx0100101001xxxx00011100000x10x10010001
xxxxxxxx0000001001xxxx01011000010x10x10011010
xxxxxxxx0000001001xxxx00001000001x10x10010010
xxxxxxxx0000001000xxxx00001001000x10x11001000
xxxxxxxx0100001011xxxx00001000011x10x10000010
xxxxxxxx0000000001xxxx00001000000x10x10000010
xxxxxxxx0001101001xxxx01001100000x10x10000110
xxxxxxxx0000001001xxxx00001001000x10x10000010
xxxxxxxx0010001001xxxx00001001001x10x10000010
xxxxxxxx0000000001xxxx00001001010x11x10000010
xxxxxxxx0010000000xxxx00101000010x10x10000110
xxxxxxxx0000001001xxxx00101001010x10x10000010
xxxxxxxx0000101001xxxx00001101000x10x10000000
xxxxxxxx0000001001xxxx00001000000x10x10000110
xxxxxxxx0000001000xxxx00001000001x10x10010010
xxxxxxxx0110001001xxxx00001001000x00x10000010
xxxxxxxx0000001001xxxx00001001001x10x10000010
xxxxxxxx0100001001xxxx00001001000x10x10001010
xxxxxxxx0100001001xxxx00001001011x10x10000010
xxxxxxxx0000001001xxxx00001001001x10x10001010
xxxxxxxx0000001001xxxx00001000000x10x10001110
xxxxxxxx0100101001xxxx00001100000x11x10000010
xxxxxxxx0000000001xxxx00011000000x11x10001010
xxxxxxxx0100001001xxxx00001001000x11x10000010
xxxxxxxx0100001001xxxx00001000010x11x10000010
xxxxxxxx0100000001xxxx00001000000x10x10000010
xxxxxxxx1010001000xxxx01000000000x11x11011010
xxxxxxxx1100001000xxxx00110001101x11x11000110
xxxxxxxx0000001000xxxx00101001010x10x10000110
xxxxxxxx0100001101xxxx00001001010x11x10011010
xxxxxxxx0000110001xxxx11001001110x11x10001101
xxxxxxxx0000100001xxxx00001101010x00x11011000
xxxxxxxx0000001001xxxx01001001110x11x10011000
xxxxxxxx0100001001xxxx01011000010x10x11101000
xxxxxxxx0000100001xxxx00101001001x00x10000011
xxxxxxxx1000111000xxxx11011010010x10x01001100
.
[launch.sh] done: Sat Sep 19 14:08:03 CEST 2015
