[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/all/selection/random/6s413b398.aig
[launch.sh] host:  atom11 (atom11)
[launch.sh] start: Sun Sep 20 20:14:43 CEST 2015
[launch.sh] jobid: 7197861
[launch.sh] name:  h6s413b398avy
[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
Working directory /tmp/7197861.1.queue/avy-Zo7Pgn
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/all/selection/random/6s413b398.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/all/selection/random/6s413b398.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/all/selection/random/6s413b398.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7197861.1.queue/avy-Zo7Pgn/6s413b398.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/all/selection/random/6s413b398.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7197861.1.queue/avy-Zo7Pgn/6s413b398.pp.aig".

[pavy] finished pp, output=/tmp/7197861.1.queue/avy-Zo7Pgn/6s413b398.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/navy --reset-cover=1 --opt-bmc --kstep=1 --shallow-push=1 --min-suffix=1 --glucose --glucose-inc-mode=0 --sat-simp=0 --glucose_itp=1 --verbose=2 --cex=/tmp/7197861.1.queue/avy-Zo7Pgn/navy_avy0.cex /tmp/7197861.1.queue/avy-Zo7Pgn/6s413b398.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7197861.1.queue/avy-Zo7Pgn/abcpdr_avy1.cex /tmp/7197861.1.queue/avy-Zo7Pgn/6s413b398.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avy --reset-cover=1 -a --kstep=2 --shallow-push=1 --tr0=1 --min-suffix=1 --glucose --glucose-inc-mode=0 --min-core=1 --glucose_itp=1 --stick-error=1 --sat-simp=1 --verbose=2 --cex=/tmp/7197861.1.queue/avy-Zo7Pgn/avyabsmus_avy2.cex /tmp/7197861.1.queue/avy-Zo7Pgn/6s413b398.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7197861.1.queue/avy-Zo7Pgn/fib_avy3.cex /tmp/7197861.1.queue/avy-Zo7Pgn/6s413b398.pp.aig
[pavy] running: [16205, 16206, 16207, 16208]
[pavy] finished pid 16205 with code 0 and signal 0
[pavy] trying to kill  16206
[pavy] waiting for  16206
[pavy] trying to kill  16207
[pavy] waiting for  16207
[pavy] trying to kill  16208
[pavy] waiting for  16208
AVY PARAMETERS
	fName = /tmp/7197861.1.queue/avy-Zo7Pgn/6s413b398.pp.aig
	ipt = 0
	avy = 1
	stutter = 0
	reset-cover = 1
	shallow_push = 1
	min-core = 0
	abstraction = 0
	tr0 = 0
	pdr = 100000
	min-suffix = 1
	sat1 = 0
	minisat = 0
	glucose = 1
	minisat_itp = 0
	glucose_itp = 1
	sat_simp = 0
	itp_simp = 0
	proof_reorder = 0
	gen-conf-limit = 0
	kstep = 1
	stick-error = 0
	itp-simplify = 1
	max-frame = 100000
END
Starting ABC
	Reading AIG from '/tmp/7197861.1.queue/avy-Zo7Pgn/6s413b398.pp.aig'


************** BRUNCH STATS ***************** 
BRUNCH_STAT run.loop 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 1 core size: 2
UNSAT from BMC at frame: 0
itp             : pi =  1951  po =     1  and =       1  lev =   1
itp             : pi =  1951  po =     1  and =       1  lev =   1
FINDING NEEDED CONSTRAINTS: CoNum: 1 EquivNum: 1
. Done
Building PDR trace
3: 0 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 0
BRUNCH_STAT Frame 1
BRUNCH_STAT OrigItp 1
BRUNCH_STAT SimpItp 1
BRUNCH_STAT Aig_ManSimplifyComb 0.00
BRUNCH_STAT Glucose_solve 0.00
BRUNCH_STAT Pdr_solve 0.00
BRUNCH_STAT addCoverCubes 0.06
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT doBmc 0.00
BRUNCH_STAT doPdrTrace 0.12
BRUNCH_STAT doPdrTrace.last 0.12
BRUNCH_STAT doPdrTrace_part1 0.01
BRUNCH_STAT doPdrTrace_part2 0.07
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.11
BRUNCH_STAT findItpConstraints 0.00
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.00
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.00
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.00
BRUNCH_STAT run.loop 0.13
BRUNCH_STAT solveWithCore 0.00
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 2 of prefix
Assumption size: 2 core size: 2
UNSAT from BMC at frame: 1
itp             : pi =  1951  po =     2  and =       1  lev =   1
itp             : pi =  1951  po =     2  and =       1  lev =   1
FINDING NEEDED CONSTRAINTS: CoNum: 2 EquivNum: 2
..YESS
 Done
Building PDR trace
3: 0 5 2 
4: 0 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 1
BRUNCH_STAT Frame 2
BRUNCH_STAT OrigItp 1
BRUNCH_STAT SimpItp 1
BRUNCH_STAT Aig_ManSimplifyComb 0.01
BRUNCH_STAT Glucose_solve 0.00
BRUNCH_STAT Pdr_solve 0.00
BRUNCH_STAT addCoverCubes 0.16
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT computeNextTr 0.05
BRUNCH_STAT doBmc 0.06
BRUNCH_STAT doPdrTrace 0.28
BRUNCH_STAT doPdrTrace.last 0.16
BRUNCH_STAT doPdrTrace_part1 0.03
BRUNCH_STAT doPdrTrace_part2 0.19
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.21
BRUNCH_STAT findItpConstraints 0.04
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.01
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.00
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.00
BRUNCH_STAT run.loop 0.39
BRUNCH_STAT solveWithCore 0.06
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 3 of prefix
Assumption size: 3 core size: 2
UNSAT from BMC at frame: 2
itp             : pi =  1951  po =     3  and =       1  lev =   1
itp             : pi =  1951  po =     3  and =       1  lev =   1
FINDING NEEDED CONSTRAINTS: CoNum: 3 EquivNum: 3
..YESS
.YESS
 Done
Building PDR trace
4: 0 5 5 2 
4: 0 5 5 2 
5: 0 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 2
BRUNCH_STAT Frame 3
BRUNCH_STAT OrigItp 1
BRUNCH_STAT SimpItp 1
BRUNCH_STAT Aig_ManSimplifyComb 0.01
BRUNCH_STAT Glucose_solve 0.01
BRUNCH_STAT Pdr_solve 0.01
BRUNCH_STAT addCoverCubes 0.32
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT computeNextTr 0.10
BRUNCH_STAT doBmc 0.12
BRUNCH_STAT doPdrTrace 0.51
BRUNCH_STAT doPdrTrace.last 0.23
BRUNCH_STAT doPdrTrace_part1 0.06
BRUNCH_STAT doPdrTrace_part2 0.38
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.38
BRUNCH_STAT findItpConstraints 0.12
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.02
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.00
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.00
BRUNCH_STAT run.loop 0.76
BRUNCH_STAT solveWithCore 0.12
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 4 of prefix
Assumption size: 4 core size: 2
UNSAT from BMC at frame: 3
itp             : pi =  1951  po =     4  and =       1  lev =   1
itp             : pi =  1951  po =     4  and =       1  lev =   1
FINDING NEEDED CONSTRAINTS: CoNum: 4 EquivNum: 4
..YESS
.YESS
.YESS
 Done
Building PDR trace
5: 0 5 5 5 2 
5: 0 5 5 5 2 
5: 0 5 5 5 2 
6: 0 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 3
BRUNCH_STAT Frame 4
BRUNCH_STAT OrigItp 1
BRUNCH_STAT SimpItp 1
BRUNCH_STAT Aig_ManSimplifyComb 0.01
BRUNCH_STAT Glucose_solve 0.03
BRUNCH_STAT Pdr_solve 0.01
BRUNCH_STAT addCoverCubes 0.53
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT computeNextTr 0.17
BRUNCH_STAT doBmc 0.20
BRUNCH_STAT doPdrTrace 0.84
BRUNCH_STAT doPdrTrace.last 0.32
BRUNCH_STAT doPdrTrace_part1 0.10
BRUNCH_STAT doPdrTrace_part2 0.63
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.60
BRUNCH_STAT findItpConstraints 0.23
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.03
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.00
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.00
BRUNCH_STAT run.loop 1.28
BRUNCH_STAT solveWithCore 0.20
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 5 of prefix
Assumption size: 5 core size: 2
UNSAT from BMC at frame: 4
itp             : pi =  1951  po =     5  and =       1  lev =   1
itp             : pi =  1951  po =     5  and =       1  lev =   1
FINDING NEEDED CONSTRAINTS: CoNum: 5 EquivNum: 5
..YESS
.YESS
.YESS
.YESS
 Done
Building PDR trace
6: 0 5 5 5 5 2 
6: 0 5 5 5 5 2 
6: 0 5 5 5 5 2 
6: 0 5 5 5 5 2 
7: 0 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 4
BRUNCH_STAT Frame 5
BRUNCH_STAT OrigItp 1
BRUNCH_STAT SimpItp 1
BRUNCH_STAT Aig_ManSimplifyComb 0.02
BRUNCH_STAT Glucose_solve 0.05
BRUNCH_STAT Pdr_solve 0.02
BRUNCH_STAT addCoverCubes 0.80
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT computeNextTr 0.24
BRUNCH_STAT doBmc 0.29
BRUNCH_STAT doPdrTrace 1.22
BRUNCH_STAT doPdrTrace.last 0.39
BRUNCH_STAT doPdrTrace_part1 0.15
BRUNCH_STAT doPdrTrace_part2 0.94
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.87
BRUNCH_STAT findItpConstraints 0.38
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.04
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.01
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.01
BRUNCH_STAT run.loop 1.91
BRUNCH_STAT solveWithCore 0.29
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 6 of prefix
Assumption size: 6 core size: 2
UNSAT from BMC at frame: 5
itp             : pi =  1951  po =     6  and =       1  lev =   1
itp             : pi =  1951  po =     6  and =       1  lev =   1
FINDING NEEDED CONSTRAINTS: CoNum: 6 EquivNum: 6
..YESS
.YESS
.YESS
.YESS
.YESS
 Done
Building PDR trace
7: 0 7 5 5 5 5 2 
7: 0 7 5 5 5 5 2 
7: 0 7 5 5 5 5 2 
7: 0 7 5 5 5 5 2 
7: 0 7 5 5 5 5 2 
8: 0 7 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 5
BRUNCH_STAT Frame 6
BRUNCH_STAT OrigItp 1
BRUNCH_STAT SimpItp 1
BRUNCH_STAT Aig_ManSimplifyComb 0.02
BRUNCH_STAT Glucose_solve 0.07
BRUNCH_STAT Pdr_solve 0.03
BRUNCH_STAT addCoverCubes 1.12
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT computeNextTr 0.32
BRUNCH_STAT doBmc 0.39
BRUNCH_STAT doPdrTrace 1.70
BRUNCH_STAT doPdrTrace.last 0.48
BRUNCH_STAT doPdrTrace_part1 0.21
BRUNCH_STAT doPdrTrace_part2 1.32
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 1.20
BRUNCH_STAT findItpConstraints 0.56
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.06
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.01
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.01
BRUNCH_STAT run.loop 2.68
BRUNCH_STAT solveWithCore 0.39
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 7 of prefix
Assumption size: 7 core size: 2
UNSAT from BMC at frame: 6
itp             : pi =  1951  po =     7  and =       1  lev =   1
itp             : pi =  1951  po =     7  and =       1  lev =   1
FINDING NEEDED CONSTRAINTS: CoNum: 7 EquivNum: 7
..YESS
.YESS
.YESS
.YESS
.YESS
.YESS
 Done
Building PDR trace
8: 0 7 7 5 5 5 5 2 
8: 0 7 7 5 5 5 5 2 
8: 0 7 7 5 5 5 5 2 
8: 0 7 7 5 5 5 5 2 
8: 0 7 7 5 5 5 5 2 
8: 0 7 7 5 5 5 5 2 
9: 0 7 7 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 6
BRUNCH_STAT Frame 7
BRUNCH_STAT OrigItp 1
BRUNCH_STAT SimpItp 1
BRUNCH_STAT Aig_ManSimplifyComb 0.02
BRUNCH_STAT Glucose_solve 0.11
BRUNCH_STAT Pdr_solve 0.03
BRUNCH_STAT addCoverCubes 1.51
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT computeNextTr 0.41
BRUNCH_STAT doBmc 0.51
BRUNCH_STAT doPdrTrace 2.28
BRUNCH_STAT doPdrTrace.last 0.58
BRUNCH_STAT doPdrTrace_part1 0.28
BRUNCH_STAT doPdrTrace_part2 1.77
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 1.59
BRUNCH_STAT findItpConstraints 0.78
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.08
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.02
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.02
BRUNCH_STAT run.loop 3.59
BRUNCH_STAT solveWithCore 0.51
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 8 of prefix
Assumption size: 8 core size: 2
UNSAT from BMC at frame: 7
itp             : pi =  1951  po =     8  and =       1  lev =   1
itp             : pi =  1951  po =     8  and =       1  lev =   1
FINDING NEEDED CONSTRAINTS: CoNum: 8 EquivNum: 8
..YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
 Done
Building PDR trace
9: 0 7 7 7 5 5 5 5 2 
9: 0 7 7 7 5 5 5 5 2 
9: 0 7 7 7 5 5 5 5 2 
9: 0 7 7 7 5 5 5 5 2 
9: 0 7 7 7 5 5 5 5 2 
9: 0 7 7 7 5 5 5 5 2 
9: 0 7 7 7 5 5 5 5 2 
10: 0 7 7 7 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 7
BRUNCH_STAT Frame 8
BRUNCH_STAT OrigItp 1
BRUNCH_STAT SimpItp 1
BRUNCH_STAT Aig_ManSimplifyComb 0.02
BRUNCH_STAT Glucose_solve 0.14
BRUNCH_STAT Pdr_solve 0.04
BRUNCH_STAT addCoverCubes 1.94
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT computeNextTr 0.56
BRUNCH_STAT doBmc 0.71
BRUNCH_STAT doPdrTrace 2.94
BRUNCH_STAT doPdrTrace.last 0.66
BRUNCH_STAT doPdrTrace_part1 0.37
BRUNCH_STAT doPdrTrace_part2 2.29
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 2.04
BRUNCH_STAT findItpConstraints 1.03
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.13
BRUNCH_STAT getInterpolant 0.01
BRUNCH_STAT pushClauses 0.03
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.03
BRUNCH_STAT run.loop 4.72
BRUNCH_STAT solveWithCore 0.71
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 9 of prefix
Assumption size: 9 core size: 2
UNSAT from BMC at frame: 8
itp             : pi =  1951  po =     9  and =       1  lev =   1
itp             : pi =  1951  po =     9  and =       1  lev =   1
FINDING NEEDED CONSTRAINTS: CoNum: 9 EquivNum: 9
..YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
 Done
Building PDR trace
10: 0 7 7 7 7 5 5 5 5 2 
10: 0 7 7 7 7 5 5 5 5 2 
10: 0 7 7 7 7 5 5 5 5 2 
10: 0 7 7 7 7 5 5 5 5 2 
10: 0 7 7 7 7 5 5 5 5 2 
10: 0 7 7 7 7 5 5 5 5 2 
10: 0 7 7 7 7 5 5 5 5 2 
10: 0 7 7 7 7 5 5 5 5 2 
11: 0 7 7 7 7 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 8
BRUNCH_STAT Frame 9
BRUNCH_STAT OrigItp 1
BRUNCH_STAT SimpItp 1
BRUNCH_STAT Aig_ManSimplifyComb 0.03
BRUNCH_STAT Glucose_solve 0.18
BRUNCH_STAT Pdr_solve 0.05
BRUNCH_STAT addCoverCubes 2.43
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT computeNextTr 0.71
BRUNCH_STAT doBmc 0.92
BRUNCH_STAT doPdrTrace 3.67
BRUNCH_STAT doPdrTrace.last 0.73
BRUNCH_STAT doPdrTrace_part1 0.46
BRUNCH_STAT doPdrTrace_part2 2.87
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 2.53
BRUNCH_STAT findItpConstraints 1.32
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.19
BRUNCH_STAT getInterpolant 0.01
BRUNCH_STAT pushClauses 0.04
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.04
BRUNCH_STAT run.loop 5.95
BRUNCH_STAT solveWithCore 0.92
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 10 of prefix
Assumption size: 10 core size: 2
UNSAT from BMC at frame: 9
itp             : pi =  1951  po =    10  and =       1  lev =   1
itp             : pi =  1951  po =    10  and =       1  lev =   1
FINDING NEEDED CONSTRAINTS: CoNum: 10 EquivNum: 10
..YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
 Done
Building PDR trace
11: 0 8 7 7 7 7 5 5 5 5 2 
11: 0 8 7 7 7 7 5 5 5 5 2 
11: 0 8 7 7 7 7 5 5 5 5 2 
11: 0 8 7 7 7 7 5 5 5 5 2 
11: 0 8 7 7 7 7 5 5 5 5 2 
11: 0 8 7 7 7 7 5 5 5 5 2 
11: 0 8 7 7 7 7 5 5 5 5 2 
11: 0 8 7 7 7 7 5 5 5 5 2 
11: 0 8 7 7 7 7 5 5 5 5 2 
12: 0 8 7 7 7 7 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 9
BRUNCH_STAT Frame 10
BRUNCH_STAT OrigItp 1
BRUNCH_STAT SimpItp 1
BRUNCH_STAT Aig_ManSimplifyComb 0.03
BRUNCH_STAT Glucose_solve 0.22
BRUNCH_STAT Pdr_solve 0.06
BRUNCH_STAT addCoverCubes 2.99
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT computeNextTr 0.86
BRUNCH_STAT doBmc 1.14
BRUNCH_STAT doPdrTrace 4.50
BRUNCH_STAT doPdrTrace.last 0.84
BRUNCH_STAT doPdrTrace_part1 0.56
BRUNCH_STAT doPdrTrace_part2 3.52
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 3.09
BRUNCH_STAT findItpConstraints 1.65
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.24
BRUNCH_STAT getInterpolant 0.01
BRUNCH_STAT pushClauses 0.06
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.05
BRUNCH_STAT run.loop 7.33
BRUNCH_STAT solveWithCore 1.14
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.01
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 11 core size: 11
UNSAT from BMC at frame: 10
itp             : pi =  1951  po =    11  and =      98  lev =   9
itp             : pi =  1951  po =    11  and =      50  lev =   5
FINDING NEEDED CONSTRAINTS: CoNum: 11 EquivNum: 11
.......YESS
.YESS
.YESS
.YESS
.YESS
 Done
Building PDR trace
12: 0 12 8 8 8 7 5 5 5 5 2 0 
12: 0 12 11 8 8 8 7 5 5 5 5 2 
12: 0 12 11 8 8 8 7 5 5 5 5 2 
12: 0 12 11 8 8 8 7 5 5 5 5 2 
12: 0 12 11 8 8 8 7 5 5 5 5 2 
12: 0 12 11 8 8 8 7 5 5 5 5 2 
12: 0 12 11 8 8 8 7 5 5 5 5 2 
12: 0 12 11 8 8 8 7 5 5 5 5 2 
12: 0 12 11 8 8 8 7 5 5 5 5 2 
12: 0 12 11 8 8 8 7 5 5 5 5 2 
13: 0 12 11 8 8 8 7 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 10
BRUNCH_STAT Frame 11
BRUNCH_STAT OrigItp 98
BRUNCH_STAT SimpItp 50
BRUNCH_STAT Aig_ManSimplifyComb 0.04
BRUNCH_STAT Glucose_solve 0.43
BRUNCH_STAT Pdr_solve 0.07
BRUNCH_STAT addCoverCubes 3.58
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT computeNextTr 1.01
BRUNCH_STAT doBmc 1.53
BRUNCH_STAT doPdrTrace 5.38
BRUNCH_STAT doPdrTrace.last 0.88
BRUNCH_STAT doPdrTrace_part1 0.67
BRUNCH_STAT doPdrTrace_part2 4.21
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 3.69
BRUNCH_STAT findItpConstraints 2.02
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.29
BRUNCH_STAT getInterpolant 0.02
BRUNCH_STAT pushClauses 0.08
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.07
BRUNCH_STAT run.loop 8.99
BRUNCH_STAT solveWithCore 1.53
BRUNCH_STAT solveWithCore_minSuffix 0.15
BRUNCH_STAT solverAddClause 0.01
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 12 core size: 3
UNSAT from BMC at frame: 11
itp             : pi =  1951  po =    12  and =       6  lev =   5
itp             : pi =  1951  po =    12  and =       6  lev =   4
FINDING NEEDED CONSTRAINTS: CoNum: 12 EquivNum: 12
............ Done
Building PDR trace
13: 0 12 11 8 8 8 7 5 5 5 5 5 2 
14: 0 12 11 8 8 8 7 5 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 11
BRUNCH_STAT Frame 12
BRUNCH_STAT OrigItp 6
BRUNCH_STAT SimpItp 6
BRUNCH_STAT Aig_ManSimplifyComb 0.04
BRUNCH_STAT Glucose_solve 0.63
BRUNCH_STAT Pdr_solve 0.07
BRUNCH_STAT addCoverCubes 3.69
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT computeNextTr 1.16
BRUNCH_STAT doBmc 1.97
BRUNCH_STAT doPdrTrace 5.55
BRUNCH_STAT doPdrTrace.last 0.17
BRUNCH_STAT doPdrTrace_part1 0.69
BRUNCH_STAT doPdrTrace_part2 4.34
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 3.80
BRUNCH_STAT findItpConstraints 2.37
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.34
BRUNCH_STAT getInterpolant 0.03
BRUNCH_STAT pushClauses 0.08
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.08
BRUNCH_STAT run.loop 9.95
BRUNCH_STAT solveWithCore 1.97
BRUNCH_STAT solveWithCore_minSuffix 0.35
BRUNCH_STAT solverAddClause 0.01
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 13 core size: 5
UNSAT from BMC at frame: 12
itp             : pi =  1951  po =    13  and =      11  lev =   5
itp             : pi =  1951  po =    13  and =      11  lev =   4
FINDING NEEDED CONSTRAINTS: CoNum: 13 EquivNum: 13
............. Done
Building PDR trace
14: 0 12 11 8 8 8 7 5 5 5 5 5 2 0 
14: 0 12 11 8 8 8 7 5 5 5 5 5 2 0 
14: 0 12 11 8 8 8 7 5 5 5 5 5 5 2 
15: 0 12 11 8 8 8 7 5 5 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 12
BRUNCH_STAT Frame 13
BRUNCH_STAT OrigItp 11
BRUNCH_STAT SimpItp 11
BRUNCH_STAT Aig_ManSimplifyComb 0.04
BRUNCH_STAT Glucose_solve 1.00
BRUNCH_STAT Pdr_solve 0.08
BRUNCH_STAT addCoverCubes 3.92
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT computeNextTr 1.32
BRUNCH_STAT doBmc 2.60
BRUNCH_STAT doPdrTrace 5.90
BRUNCH_STAT doPdrTrace.last 0.35
BRUNCH_STAT doPdrTrace_part1 0.74
BRUNCH_STAT doPdrTrace_part2 4.61
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 4.04
BRUNCH_STAT findItpConstraints 2.76
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.40
BRUNCH_STAT getInterpolant 0.04
BRUNCH_STAT pushClauses 0.09
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.09
BRUNCH_STAT run.loop 11.34
BRUNCH_STAT solveWithCore 2.60
BRUNCH_STAT solveWithCore_minSuffix 0.71
BRUNCH_STAT solverAddClause 0.01
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 14 core size: 7
UNSAT from BMC at frame: 13
itp             : pi =  1951  po =    14  and =      47  lev =   9
itp             : pi =  1951  po =    14  and =      16  lev =   4
FINDING NEEDED CONSTRAINTS: CoNum: 14 EquivNum: 14
.............. Done
Building PDR trace
15: 0 12 11 8 8 8 7 5 5 5 5 5 5 2 0 
15: 0 12 11 8 8 8 7 5 5 5 5 5 5 2 0 
15: 0 12 11 8 8 8 7 5 5 5 5 5 5 2 0 
15: 0 12 11 8 8 8 7 5 5 5 5 5 5 2 0 
15: 0 12 11 8 8 8 7 5 5 5 5 5 5 5 2 
16: 0 12 11 8 8 8 7 5 5 5 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 13
BRUNCH_STAT Frame 14
BRUNCH_STAT OrigItp 47
BRUNCH_STAT SimpItp 16
BRUNCH_STAT Aig_ManSimplifyComb 0.05
BRUNCH_STAT Glucose_solve 1.56
BRUNCH_STAT Pdr_solve 0.09
BRUNCH_STAT addCoverCubes 4.25
BRUNCH_STAT blockCube 0.01
BRUNCH_STAT computeNextTr 1.50
BRUNCH_STAT doBmc 3.44
BRUNCH_STAT doPdrTrace 6.40
BRUNCH_STAT doPdrTrace.last 0.50
BRUNCH_STAT doPdrTrace_part1 0.80
BRUNCH_STAT doPdrTrace_part2 5.01
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 4.38
BRUNCH_STAT findItpConstraints 3.23
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.46
BRUNCH_STAT getInterpolant 0.06
BRUNCH_STAT pushClauses 0.10
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.10
BRUNCH_STAT run.loop 13.18
BRUNCH_STAT solveWithCore 3.44
BRUNCH_STAT solveWithCore_minSuffix 1.24
BRUNCH_STAT solverAddClause 0.01
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 15 core size: 9
UNSAT from BMC at frame: 14
itp             : pi =  1951  po =    15  and =     159  lev =  16
itp             : pi =  1951  po =    15  and =      40  lev =   7
FINDING NEEDED CONSTRAINTS: CoNum: 15 EquivNum: 15
............... Done
Building PDR trace
16: 0 12 11 8 8 8 7 5 5 5 5 5 5 5 2 0 
16: 0 12 11 8 8 8 7 5 5 5 5 5 5 5 2 0 
16: 0 12 11 8 8 8 7 5 5 5 5 5 5 5 2 0 
16: 0 12 11 8 8 8 7 5 5 5 5 5 5 5 2 0 
16: 0 12 11 8 8 8 7 5 5 5 5 5 5 5 2 0 
16: 0 12 11 8 8 8 7 5 5 5 5 5 5 5 2 0 
16: 0 12 11 8 8 8 7 5 5 5 5 5 5 5 5 2 
17: 0 12 11 8 8 8 7 5 5 5 5 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 14
BRUNCH_STAT Frame 15
BRUNCH_STAT OrigItp 159
BRUNCH_STAT SimpItp 40
BRUNCH_STAT Aig_ManSimplifyComb 0.05
BRUNCH_STAT Glucose_solve 2.33
BRUNCH_STAT Pdr_solve 0.09
BRUNCH_STAT addCoverCubes 4.68
BRUNCH_STAT blockCube 0.01
BRUNCH_STAT computeNextTr 1.67
BRUNCH_STAT doBmc 4.47
BRUNCH_STAT doPdrTrace 7.04
BRUNCH_STAT doPdrTrace.last 0.64
BRUNCH_STAT doPdrTrace_part1 0.88
BRUNCH_STAT doPdrTrace_part2 5.51
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 4.81
BRUNCH_STAT findItpConstraints 3.69
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.51
BRUNCH_STAT getInterpolant 0.12
BRUNCH_STAT pushClauses 0.11
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.11
BRUNCH_STAT run.loop 15.38
BRUNCH_STAT solveWithCore 4.47
BRUNCH_STAT solveWithCore_minSuffix 1.96
BRUNCH_STAT solverAddClause 0.01
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 16 core size: 11
UNSAT from BMC at frame: 15
itp             : pi =  1951  po =    16  and =     112  lev =  15
itp             : pi =  1951  po =    16  and =      31  lev =   4
FINDING NEEDED CONSTRAINTS: CoNum: 16 EquivNum: 16
................ Done
Building PDR trace
17: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 2 0 
17: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 2 0 
17: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 2 0 
17: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 2 0 
17: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 2 0 
17: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 2 0 
17: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 2 0 
17: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 2 0 
17: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 2 
18: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 15
BRUNCH_STAT Frame 16
BRUNCH_STAT OrigItp 112
BRUNCH_STAT SimpItp 31
BRUNCH_STAT Aig_ManSimplifyComb 0.06
BRUNCH_STAT Glucose_solve 3.29
BRUNCH_STAT Pdr_solve 0.11
BRUNCH_STAT addCoverCubes 5.25
BRUNCH_STAT blockCube 0.01
BRUNCH_STAT computeNextTr 1.85
BRUNCH_STAT doBmc 5.69
BRUNCH_STAT doPdrTrace 7.91
BRUNCH_STAT doPdrTrace.last 0.87
BRUNCH_STAT doPdrTrace_part1 0.99
BRUNCH_STAT doPdrTrace_part2 6.18
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 5.39
BRUNCH_STAT findItpConstraints 4.19
BRUNCH_STAT generalize 0.01
BRUNCH_STAT getCnfTr 0.57
BRUNCH_STAT getInterpolant 0.17
BRUNCH_STAT pushClauses 0.13
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.13
BRUNCH_STAT run.loop 18.04
BRUNCH_STAT solveWithCore 5.69
BRUNCH_STAT solveWithCore_minSuffix 2.85
BRUNCH_STAT solverAddClause 0.01
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 17 core size: 13
UNSAT from BMC at frame: 16
itp             : pi =  1951  po =    17  and =      66  lev =  10
itp             : pi =  1951  po =    17  and =      27  lev =   3
FINDING NEEDED CONSTRAINTS: CoNum: 17 EquivNum: 17
................. Done
Building PDR trace
18: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 2 0 
18: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 2 0 
18: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 2 0 
18: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 2 0 
18: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 2 0 
18: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 2 0 
18: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 2 0 
18: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 2 0 
18: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 2 0 
18: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 2 0 
18: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 4 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 4 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 16
BRUNCH_STAT Frame 17
BRUNCH_STAT OrigItp 66
BRUNCH_STAT SimpItp 27
BRUNCH_STAT Aig_ManSimplifyComb 0.07
BRUNCH_STAT Glucose_solve 4.66
BRUNCH_STAT Pdr_solve 0.13
BRUNCH_STAT addCoverCubes 5.97
BRUNCH_STAT blockCube 0.01
BRUNCH_STAT computeNextTr 2.02
BRUNCH_STAT doBmc 7.27
BRUNCH_STAT doPdrTrace 9.00
BRUNCH_STAT doPdrTrace.last 1.08
BRUNCH_STAT doPdrTrace_part1 1.13
BRUNCH_STAT doPdrTrace_part2 7.01
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 6.11
BRUNCH_STAT findItpConstraints 4.83
BRUNCH_STAT generalize 0.01
BRUNCH_STAT getCnfTr 0.62
BRUNCH_STAT getInterpolant 0.23
BRUNCH_STAT pushClauses 0.15
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.15
BRUNCH_STAT run.loop 21.41
BRUNCH_STAT solveWithCore 7.27
BRUNCH_STAT solveWithCore_minSuffix 4.09
BRUNCH_STAT solverAddClause 0.02
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 18 core size: 15
UNSAT from BMC at frame: 17
itp             : pi =  1951  po =    18  and =     182  lev =  16
itp             : pi =  1951  po =    18  and =      47  lev =   4
FINDING NEEDED CONSTRAINTS: CoNum: 18 EquivNum: 18
.................. Done
Building PDR trace
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 4 2 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 4 2 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 4 2 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 4 2 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 4 2 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 4 2 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 4 2 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 4 2 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 4 2 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 4 2 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 6 2 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 6 2 0 
19: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 6 4 2 
20: 0 12 11 8 8 8 7 7 5 5 5 5 5 5 5 5 6 4 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 17
BRUNCH_STAT Frame 18
BRUNCH_STAT OrigItp 182
BRUNCH_STAT SimpItp 47
BRUNCH_STAT Aig_ManSimplifyComb 0.07
BRUNCH_STAT Glucose_solve 7.25
BRUNCH_STAT Pdr_solve 0.15
BRUNCH_STAT addCoverCubes 6.76
BRUNCH_STAT blockCube 0.02
BRUNCH_STAT computeNextTr 2.19
BRUNCH_STAT doBmc 10.12
BRUNCH_STAT doPdrTrace 10.20
BRUNCH_STAT doPdrTrace.last 1.20
BRUNCH_STAT doPdrTrace_part1 1.28
BRUNCH_STAT doPdrTrace_part2 7.93
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 6.92
BRUNCH_STAT findItpConstraints 5.47
BRUNCH_STAT generalize 0.01
BRUNCH_STAT getCnfTr 0.68
BRUNCH_STAT getInterpolant 0.34
BRUNCH_STAT pushClauses 0.18
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.17
BRUNCH_STAT run.loop 26.22
BRUNCH_STAT solveWithCore 10.12
BRUNCH_STAT solveWithCore_minSuffix 6.55
BRUNCH_STAT solverAddClause 0.02
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 19 core size: 17
UNSAT from BMC at frame: 18
itp             : pi =  1951  po =    19  and =     516  lev =  24
itp             : pi =  1951  po =    19  and =      83  lev =   6
FINDING NEEDED CONSTRAINTS: CoNum: 19 EquivNum: 19
..............YESS
.YESS
.YESS
.YESS
.YESS
.YESS
 Done
Building PDR trace
20: 0 108 101 73 8 8 7 7 5 5 5 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 8 8 7 7 5 5 5 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 8 8 7 7 5 5 5 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 9 8 8 7 5 5 5 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 9 8 8 7 5 5 5 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 9 8 8 7 7 5 5 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 9 8 8 7 7 5 5 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 9 8 8 7 7 7 5 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 9 8 8 7 7 7 5 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 9 8 8 7 7 7 7 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 9 8 8 7 7 7 7 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 9 8 8 7 7 7 7 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 9 8 8 7 7 7 7 5 5 5 5 5 6 4 2 0 
20: 0 108 109 75 9 8 8 7 7 7 7 5 5 5 5 5 5 6 2 0 
20: 0 108 109 75 9 8 8 7 7 7 7 5 5 5 5 5 5 6 2 0 
20: 0 108 109 75 9 8 8 7 7 7 7 5 5 5 5 5 5 5 2 0 
20: 0 108 109 75 9 8 8 7 7 7 7 5 5 5 5 5 5 5 2 0 
20: 0 108 109 75 9 8 8 7 7 7 7 5 5 5 5 5 5 5 5 2 
21: 0 108 109 75 9 8 8 7 7 7 7 5 5 5 5 5 5 5 5 2 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 18
BRUNCH_STAT Frame 19
BRUNCH_STAT OrigItp 516
BRUNCH_STAT SimpItp 83
BRUNCH_STAT Aig_ManSimplifyComb 0.09
BRUNCH_STAT Glucose_solve 10.00
BRUNCH_STAT Pdr_solve 0.20
BRUNCH_STAT addCoverCubes 7.82
BRUNCH_STAT blockCube 0.02
BRUNCH_STAT computeNextTr 2.37
BRUNCH_STAT doBmc 13.09
BRUNCH_STAT doPdrTrace 11.97
BRUNCH_STAT doPdrTrace.last 1.76
BRUNCH_STAT doPdrTrace_part1 1.50
BRUNCH_STAT doPdrTrace_part2 9.18
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 7.97
BRUNCH_STAT findItpConstraints 6.16
BRUNCH_STAT generalize 0.02
BRUNCH_STAT getCnfTr 0.74
BRUNCH_STAT getInterpolant 0.55
BRUNCH_STAT pushClauses 0.33
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.32
BRUNCH_STAT run.loop 31.86
BRUNCH_STAT solveWithCore 13.09
BRUNCH_STAT solveWithCore_minSuffix 9.02
BRUNCH_STAT solverAddClause 0.03
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 20 core size: 8
UNSAT from BMC at frame: 19
itp             : pi =  1951  po =    20  and =     260  lev =  28
itp             : pi =  1951  po =    20  and =      66  lev =   7
FINDING NEEDED CONSTRAINTS: CoNum: 20 EquivNum: 20
........YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
.YESS
 Done
Building PDR trace
21: 0 140 125 116 115 112 114 8 7 7 7 5 5 5 5 5 5 5 5 2 0 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 2 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 4 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 6 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 8 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 10 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 18 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 18 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 18 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 18 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 18 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 18 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 18 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 22 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 22 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 26 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 26 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 30 
21: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 30 
0
b0
.
22: 0 140 125 116 115 112 114 38 7 7 7 5 5 5 5 5 5 5 5 2 0 32 
Verification of invariant with 32 clauses was successful.

************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 19
BRUNCH_STAT Frame 20
BRUNCH_STAT Invar 32
BRUNCH_STAT OrigItp 260
BRUNCH_STAT SimpItp 66
BRUNCH_STAT Aig_ManSimplifyComb 0.09
BRUNCH_STAT Glucose_solve 13.41
BRUNCH_STAT Pdr_solve 0.31
BRUNCH_STAT addCoverCubes 9.01
BRUNCH_STAT blockCube 0.05
BRUNCH_STAT computeNextTr 2.53
BRUNCH_STAT doBmc 16.60
BRUNCH_STAT doPdrTrace 14.53
BRUNCH_STAT doPdrTrace.last 2.56
BRUNCH_STAT doPdrTrace_part1 1.72
BRUNCH_STAT doPdrTrace_part2 10.54
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 9.14
BRUNCH_STAT findItpConstraints 7.00
BRUNCH_STAT generalize 0.03
BRUNCH_STAT getCnfTr 0.80
BRUNCH_STAT getInterpolant 0.67
BRUNCH_STAT pushClauses 1.08
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 1.05
BRUNCH_STAT run.loop 38.93
BRUNCH_STAT solveWithCore 16.60
BRUNCH_STAT solveWithCore_minSuffix 11.97
BRUNCH_STAT solverAddClause 0.06
BRUNCH_STAT Result UNSAT
************** BRUNCH STATS END ***************** 
[pavy] Witness begin
0
b0
.
[pavy] Witness end
WINNER:  navy
BRUNCH_STAT config 0
BRUNCH_STAT config_name navy
BRUNCH_STAT Result UNSAT
[launch.sh] stop:  Sun Sep 20 20:15:29 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 20:15:32 CEST 2015
[launch.sh] done: Sun Sep 20 20:15:32 CEST 2015
