[launch.sh] args:  /home/biere/hwmcc15/solvers/pdtrav/single.pdtravthrd /home/biere/hwmcc15/benchmarks/all/selection/random/bobsmhdlc1.aig
[launch.sh] host:  atom32 (atom32)
[launch.sh] start: Sat Sep 19 04:57:23 CEST 2015
[launch.sh] jobid: 7195005
[launch.sh] name:  bobsmhdlc1pdtravthrd
[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/7195005.1.queue/bobsmhdlc1.aig
c [single.pdtravthrd] copying /home/biere/hwmcc15/benchmarks/all/selection/random/bobsmhdlc1.aig to /tmp/7195005.1.queue/bobsmhdlc1.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 bobsmhdlc1.aig 
## Running Date: Sat Sep 19 04:57:26 CEST 2015
## Hostname: atom32
CPU time adjustment: 0.67 s (norm 0.67 s) - scale factor: 1.504444
-- DDI Manager Init.
-- FSM Manager Init.
-- FSM Loading.
# CONSTRAINTS: 0
Property: !o0.
Design Statistics: 61 Inputs / 290 State Vars / 1965 AIG Gates
|Constraint|=0 nodes.
|Constraint|=0 nodes.
CREATING SYN Thread (father 3028 - 61399880)

Thread SYN activated
CREATED Thread (3028 - 38a93700)
-- FSM Manager Init.

Running reductions...(phase 0)

Running reductions...(phase 1)
compacting deltas (EQ prop): 1966 -> 1934
compacting miters (EQ prop): 163 -> 163
Checking for Equivalence Property: OK (5/10 Equivalences Found).

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

Running reductions...(phase 3)
COI Reduction Performed: Kept 292 State Vars out of 292.
Ternary Simulation: TSIM found 1 EQUIVALENCES
COI Reduction Performed: Kept 287 State Vars out of 287.

Running reductions...(phase 4)
(null)       : i/o =   48/    1  lat =  285  and =   1633  lev = 17
(null)       : i/o =   48/    1  lat =  285  and =   1602  lev = 15
-- TRAV Manager Init.
INITIALIZING THREADED ENGINES (stacksize = 16777216)
INITIALIZING 4 ENGINES: LMS PDRPFL ITPPFL BMCPFL
-- FSM Manager Init.

Running LMS ...
-- FSM Manager Init.
-- DDI Manager Init.
CREATING Thread (father 3028 - 61399880)

Thread LMS activated
CREATED Thread (3028 - 3da95700)

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

Running PDRPFL ...
-- FSM Manager Init.
COI Reduction Performed: Kept 287 State Vars out of 287.
Ternary Simulation: -- DDI Manager Init.
TSIM found 1 EQUIVALENCES
COI Reduction Performed: Kept 287 State Vars out of 287.
CREATING Thread (father 3028 - 61399880)

Thread PDRPFL activated
CREATED Thread (3028 - 3ea96700)
INITIALIZING 2 ENGINES: PDR PDR2
-- FSM Manager Init.

Running ITPPFL ...
-- FSM Manager Init.
-- FSM Manager Init.
ACTIVE GATES: 1910/1967 - shortEdges: 317, shortEdgeCuts: 317

Running PDR ...
-- FSM Manager Init.
TOTAL 267 paths found (253 vars, 32 PO vars)
path len - avg: 3, min: 1, max: 10
TOTAL path len - avg: 7, min: 1, max: 18
-- DDI Manager Init.
-- DDI Manager Init.
MINCUT: input=127, intern=140, auxv=140
AUXSIZE: 1021
BASESIZE: 1120
Shared Variables between Cut Regions: 21.
CREATING Thread (father 3028 - 3ea96700)

Thread PDR activated
-- FSM Manager Init.

Running PDR2 ...
-- FSM Manager Init.
CREATED Thread (3028 - 3fa97700)
CREATING Thread (father 3028 - 61399880)
-- MC Manager Init.

Thread ITPPFL activated
CREATED Thread (3028 - 49001700)
-- TRAV Manager Init.
INITIALIZING 2 ENGINES:-- TR Manager Init.
 ITP IGR
-- FSM Manager Init.

Running BMCPFL ...
-- FSM Manager Init.
STATS NUM: 4
-- FSM Manager Init.

Running ITP ...
-- FSM Manager Init.
-- DDI Manager Init.
MINREG retiming from 287 toto 276 regs.
CREATING Thread (father 3028 - 3ea96700)

Thread PDR2 activated
CREATED Thread (3028 - 4a002700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
STATS NUM: 4
COI Reduction Performed: Kept 276 State Vars out of 276.
Ternary Simulation: -- DDI Manager Init.
-- DDI Manager Init.
TSIM found 1 EQUIVALENCES
CREATING Thread (father 3028 - 61399880)

Thread BMCPFL activated
CREATED Thread (3028 - 4b003700)
INITIALIZING 3 ENGINES: BMC SIM BMC2
-- FSM Manager Init.

Running BMC ...
-- FSM Manager Init.
CREATING Thread (father 3028 - 49001700)

Thread ITP activated
-- FSM Manager Init.

Running IGR ...
-- FSM Manager Init.
COI Reduction Performed: Kept 276 State Vars out of 276.
CREATED Thread (3028 - 5d003700)
ACTIVE GATES: 1918/1972 - shortEdges: 317, shortEdgeCuts: 317
TOTAL 257 paths found (254 vars, 20 PO vars)
path len - avg: 4, min: 1, max: 13
TOTAL path len - avg: 7, min: 1, max: 18
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- DDI Manager Init.
-- DDI Manager Init.
RESULT: -2 (SYN - 15 - 0)
CREATING Thread (father 3028 - 4b003700)
MINCUT: input=87, intern=170, auxv=170
AUXSIZE: 1577
BASESIZE: 745

Thread BMC activated
CREATED Thread (3028 - 5e004700)
-- FSM Manager Init.

Running SIM ...
-- FSM Manager Init.
-- MC Manager Init.
Shared Variables between Cut Regions: 70.
-- TRAV Manager Init.
-- TR Manager Init.
CREATING Thread (father 3028 - 49001700)

Thread IGR activated
CREATED Thread (3028 - 5f005700)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
-- DDI Manager Init.
MINREG retiming from 276 toto 268 regs.
CREATING Thread (father 3028 - 4b003700)

Thread SIM activated
CREATED Thread (3028 - 71002700)
-- FSM Manager Init.

Running BMC2 ...
-- FSM Manager Init.
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
COI Reduction Performed: Kept 268 State Vars out of 268.
-- DDI Manager Init.
Ternary Simulation: TSIM found 1 EQUIVALENCES
COI Reduction Performed: Kept 268 State Vars out of 268.
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
CREATING Thread (father 3028 - 4b003700)

Thread BMC2 activated
CREATED Thread (3028 - 72003700)
BLOCKED START (BMC2 - 1 - 10)
(null)       : i/o =   48/    1  lat =  285  and =   1633  lev = 17
*** Gen. lemmas iteration 0 ***
Simulation time: 0.03 s (norm 0.03 s)
Potential eq.: 0+1
Proved equiv.: 0+1 in 0.01 s (1 iter, 1 total run)
Rewriting: |delta| = 2078 -> 2077.
Rewriting: |lambda| = 3 -> 3.
*** Gen. lemmas iteration 0 ***
Simulation time: 0.45 s (norm 0.45 s)
Potential eq.: 1246+425
Remaining eq.: 1246+425 in 0.02 s (1 iter, 1 total run, 0.00 s)
*** Gen. lemmas iteration 1 ***
Potential eq.: 1246+425
Proved equiv.: 1+1 in 2.30 s (42 iter, 579 total run)
Potential eq.: 1244+425
Remaining eq.: 1244+425 in 0.04 s (1 iter, 1 total run, 0.01 s)
*** Gen. lemmas iteration 2 ***
Potential eq.: 1244+425
Proved equiv.: 0+0 in 3.65 s (41 iter, 610 total run)
Potential eq.: 1244+425
Remaining eq.: 1244+425 in 0.04 s (1 iter, 1 total run, 0.01 s)
*** Gen. lemmas iteration 3 ***
Potential eq.: 1244+425
Remaining eq.: 1244+425 in 0.07 s (1 iter, 1 total run, 0.01 s)
*** Gen. lemmas iteration 4 ***
Potential eq.: 1244+425
Proved equiv.: 0+0 in 8.24 s (47 iter, 695 total run)
Potential eq.: 1244+425
Remaining eq.: 1236+420 in 0.33 s (4 iter, 1 total run, 0.07 s)
*** Gen. lemmas iteration 5 ***
Potential eq.: 1236+420
Remaining eq.: 1229+413 in 0.31 s (3 iter, 1 total run, 0.06 s)
*** Gen. lemmas iteration 6 ***
Potential eq.: 1229+413
Proved equiv.: 0+0 in 9.54 s (37 iter, 652 total run)
Potential eq.: 1229+413
Remaining eq.: 1209+421 in 0.24 s (2 iter, 1 total run, 0.06 s)
*** Gen. lemmas iteration 7 ***
Potential eq.: 1209+421
Remaining eq.: 1193+424 in 0.55 s (4 iter, 1 total run, 0.14 s)
*** Gen. lemmas iteration 8 ***
Potential eq.: 1193+424
Proved equiv.: 0+0 in 18.96 s (46 iter, 633 total run)
Potential eq.: 1193+424
Remaining eq.: 1188+424 in 0.54 s (3 iter, 1 total run, 0.12 s)
*** Gen. lemmas iteration 9 ***
Potential eq.: 1188+424
Remaining eq.: 1186+425 in 0.40 s (2 iter, 1 total run, 0.09 s)
*** Gen. lemmas iteration 10 ***
Potential eq.: 1186+425
Proved equiv.: 0+0 in 24.00 s (44 iter, 617 total run)
Potential eq.: 1186+425
Remaining eq.: 913+661 in 0.96 s (4 iter, 1 total run, 0.26 s)
*** Gen. lemmas iteration 11 ***
Potential eq.: 913+661
Remaining eq.: 672+717 in 1.26 s (4 iter, 1 total run, 0.46 s)
*** Gen. lemmas iteration 12 ***
Potential eq.: 672+717
Proved equiv.: 0+0 in 27.01 s (32 iter, 552 total run)
Rewriting: |delta| = 2077 -> 2076.
Rewriting: |lambda| = 3 -> 1.
Total lemma generation time: 149.06 s (norm 99.00 s).
-- TR Manager Init.
UNBLOCKED START (BMC2 - 1 - 10)
-- MC Manager Init.
-- TRAV Manager Init.
-- TR Manager Init.
Simulated 20 frames for 84762 rounds with 847 restarts.  Reached timeout (4000 sec).
There is no current CEX.
Invariant verification TERMINATED with -2 [SIM]
Invariant verification aborted by engine: SIM
[launch.sh] stop:  Sat Sep 19 05:57:26 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 05:57:29 CEST 2015
[launch.sh] out: cat /tmp/7195005.1.queue/bobsmhdlc1.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
u34
u35
u36
u37
[launch.sh] done: Sat Sep 19 05:57:29 CEST 2015
