[launch.sh] args:  /home/biere/hwmcc15/solvers/pdtrav/single.pdtravdeep /home/biere/hwmcc15/benchmarks/all/selection/random/bob12s03.aig
[launch.sh] host:  atom21 (atom21)
[launch.sh] start: Sun Sep 20 16:57:55 CEST 2015
[launch.sh] jobid: 7197596
[launch.sh] name:  bob12s03pdtravdeep
[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/7197596.1.queue/bob12s03.aig
c [single.pdtravdeep] copying /home/biere/hwmcc15/benchmarks/all/selection/random/bob12s03.aig to /tmp/7197596.1.queue/bob12s03.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 bob12s03.aig 
## Running Date: Sun Sep 20 16:57:58 CEST 2015
## Hostname: atom21
CPU time adjustment: 0.66 s (norm 0.66 s) - scale factor: 1.482222
-- DDI Manager Init.
-- FSM Manager Init.
-- FSM Loading.
# CONSTRAINTS: 0
Property: !o0.
Design Statistics: 617 Inputs / 5174 State Vars / 36599 AIG Gates
|Constraint|=0 nodes.
|Constraint|=0 nodes.
-- FSM Manager Init.

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

Running reductions...(phase 1)
compacting deltas (EQ prop): 36600 -> 36330
compacting miters (EQ prop): 1433 -> 1237
Checking for Equivalence Property: OK (189/213 Equivalences Found).

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

Running reductions...(phase 3)
COI Reduction Performed: Kept 2423 State Vars out of 5176.
Ternary Simulation: TSIM found 15 EQUIVALENCES
COI Reduction Performed: Kept 2402 State Vars out of 2408.

Running reductions...(phase 4)
(null)       : i/o =  495/    1  lat = 2400  and =  23304  lev =185
(null)       : i/o =  495/    1  lat =  869  and =   7232  lev = 30
(null)       : i/o =  495/    1  lat =  869  and =   7136  lev = 29
Delta: 2400 -> 869
Lambda: 1 -> 1
latches: 869 -> 869
inputs: 495 -> 371
|Constraint|=0 nodes.
-- 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 13981 - 625cf880)

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

Running BMC ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 13981 - fefa3700)

Thread BMC activated
CREATED Thread (13981 - fffa4700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- FSM Manager Init.

Running BMC2 ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 13981 - fefa3700)

Thread BMC2 activated
CREATED Thread (13981 - 9001700)
BLOCKED START (BMC2 - 1 - 2)
BMC failure at bound 7.
Total SAT time: 0.42 s (norm 0.42 s), total BMC time: 0.42 s (norm 0.42 s).
Invariant verification TERMINATED with 1 [BMC]

cex written to: /tmp/bob12s03.pdtrav.out.1.cex
CEX validated by aigsim

Invariant verification completed by engine: BMC

Invariant verification completed by engine: BMCPFL
Verification result (FAIL) written to file bob12s03.pdtrav.out
CMD: cat /tmp/bob12s03.pdtrav.out.1.cex >> bob12s03.pdtrav.out
Total used memory: 49.00 MBytes
Total Verification Time: 13.7
Total Execution Time: 21.25 s (norm 14.40 s)
## PdTRAV End.
[launch.sh] stop:  Sun Sep 20 16:58:23 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: Sun Sep 20 16:58:26 CEST 2015
[launch.sh] out: cat /tmp/7197596.1.queue/bob12s03.pdtrav.out
u1
u3
u5
u7
u9
u11
1
b0
[encoded data, 15046 characters]
.
[launch.sh] done: Sun Sep 20 16:58:26 CEST 2015
