[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/all/selection/random/boblivear.aig
[launch.sh] host:  atom27 (atom27)
[launch.sh] start: Fri Sep 18 17:10:27 CEST 2015
[launch.sh] jobid: 7194005
[launch.sh] name:  boblivearavy
[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/7194005.1.queue/avy-bGNubb
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/all/selection/random/boblivear.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/all/selection/random/boblivear.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/all/selection/random/boblivear.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7194005.1.queue/avy-bGNubb/boblivear.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/all/selection/random/boblivear.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7194005.1.queue/avy-bGNubb/boblivear.pp.aig".

[pavy] finished pp, output=/tmp/7194005.1.queue/avy-bGNubb/boblivear.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/7194005.1.queue/avy-bGNubb/navy_avy0.cex /tmp/7194005.1.queue/avy-bGNubb/boblivear.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7194005.1.queue/avy-bGNubb/abcpdr_avy1.cex /tmp/7194005.1.queue/avy-bGNubb/boblivear.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/7194005.1.queue/avy-bGNubb/avyabsmus_avy2.cex /tmp/7194005.1.queue/avy-bGNubb/boblivear.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7194005.1.queue/avy-bGNubb/fib_avy3.cex /tmp/7194005.1.queue/avy-bGNubb/boblivear.pp.aig
[pavy] running: [1723, 1724, 1725, 1726]
[pavy] finished pid 1725 with code 0 and signal 0
[pavy] trying to kill  1723
[pavy] waiting for  1723
[pavy] trying to kill  1724
[pavy] waiting for  1724
[pavy] trying to kill  1726
[pavy] waiting for  1726
AVY PARAMETERS
	fName = /tmp/7194005.1.queue/avy-bGNubb/boblivear.pp.aig
	ipt = 0
	avy = 1
	stutter = 0
	reset-cover = 1
	shallow_push = 1
	min-core = 1
	abstraction = 1
	tr0 = 1
	pdr = 100000
	min-suffix = 1
	sat1 = 0
	minisat = 0
	glucose = 1
	minisat_itp = 0
	glucose_itp = 1
	sat_simp = 1
	itp_simp = 1
	proof_reorder = 0
	gen-conf-limit = 0
	kstep = 2
	stick-error = 1
	itp-simplify = 1
	max-frame = 100000
END
Starting ABC
	Reading AIG from '/tmp/7194005.1.queue/avy-bGNubb/boblivear.pp.aig'


************** BRUNCH STATS ***************** 
BRUNCH_STAT run.loop 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 78 core size: 4
Core size: original: 4 mincore: 4
UNSAT from BMC at frame: 0
itp             : pi =    78  po =     1  and =       5  lev =   4
itp             : pi =    78  po =     1  and =       3  lev =   3
Building PDR trace
3: 0 2 1 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 0
BRUNCH_STAT Frame 1
BRUNCH_STAT OrigItp 5
BRUNCH_STAT SimpItp 3
BRUNCH_STAT Aig_ManSimplifyComb 0.00
BRUNCH_STAT Glucose_solve 0.00
BRUNCH_STAT Pdr_solve 0.00
BRUNCH_STAT addCoverCubes 0.00
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT doBmc 0.00
BRUNCH_STAT doPdrTrace 0.00
BRUNCH_STAT doPdrTrace.last 0.00
BRUNCH_STAT doPdrTrace_part1 0.00
BRUNCH_STAT doPdrTrace_part2 0.00
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.00
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.00
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.00
BRUNCH_STAT run.loop 0.01
BRUNCH_STAT solveWithCore 0.00
BRUNCH_STAT solveWithCore_minCore 0.00
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 234 core size: 27
Core size: original: 27 mincore: 20
UNSAT from BMC at frame: 2
itp             : pi =    78  po =     3  and =      23  lev =   9
itp             : pi =    78  po =     3  and =      14  lev =   4
Building PDR trace
3: 0 4 6 
4: 0 4 3 7 
5: 0 4 3 2 10 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 2
BRUNCH_STAT Frame 2
BRUNCH_STAT OrigItp 23
BRUNCH_STAT SimpItp 14
BRUNCH_STAT Aig_ManSimplifyComb 0.00
BRUNCH_STAT Glucose_solve 0.01
BRUNCH_STAT Pdr_solve 0.00
BRUNCH_STAT addCoverCubes 0.01
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT doBmc 0.02
BRUNCH_STAT doPdrTrace 0.02
BRUNCH_STAT doPdrTrace.last 0.02
BRUNCH_STAT doPdrTrace_part1 0.00
BRUNCH_STAT doPdrTrace_part2 0.01
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.01
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.00
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.00
BRUNCH_STAT run.loop 0.04
BRUNCH_STAT solveWithCore 0.01
BRUNCH_STAT solveWithCore_minCore 0.00
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 390 core size: 39
Core size: original: 39 mincore: 39
UNSAT from BMC at frame: 4
itp             : pi =    78  po =     5  and =      41  lev =   7
itp             : pi =    78  po =     5  and =      29  lev =   4
Building PDR trace
5: 0 6 3 8 12 
5: 0 6 5 8 13 
5: 0 6 5 8 17 
6: 0 6 5 8 4 19 
7: 0 6 5 8 4 9 22 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 4
BRUNCH_STAT Frame 3
BRUNCH_STAT OrigItp 41
BRUNCH_STAT SimpItp 29
BRUNCH_STAT Aig_ManSimplifyComb 0.01
BRUNCH_STAT Glucose_solve 0.02
BRUNCH_STAT Pdr_solve 0.01
BRUNCH_STAT addCoverCubes 0.02
BRUNCH_STAT blockCube 0.01
BRUNCH_STAT doBmc 0.04
BRUNCH_STAT doPdrTrace 0.06
BRUNCH_STAT doPdrTrace.last 0.04
BRUNCH_STAT doPdrTrace_part1 0.00
BRUNCH_STAT doPdrTrace_part2 0.03
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.02
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.00
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.00
BRUNCH_STAT run.loop 0.10
BRUNCH_STAT solveWithCore 0.03
BRUNCH_STAT solveWithCore_minCore 0.01
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 546 core size: 152
Core size: original: 152 mincore: 106
UNSAT from BMC at frame: 6
itp             : pi =    78  po =     7  and =     792  lev =  63
itp             : pi =    78  po =     7  and =     304  lev =  25
Building PDR trace
7: 0 6 11 8 4 9 23 
7: 0 6 13 8 4 9 27 
7: 0 6 13 17 4 13 42 
7: 0 6 13 17 7 52 43 
7: 0 6 13 17 7 68 54 
8: 0 6 13 17 7 68 11 59 
9: 0 6 13 17 7 68 11 5 61 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 6
BRUNCH_STAT Frame 4
BRUNCH_STAT OrigItp 792
BRUNCH_STAT SimpItp 304
BRUNCH_STAT Aig_ManSimplifyComb 0.03
BRUNCH_STAT Glucose_solve 0.06
BRUNCH_STAT Pdr_solve 0.05
BRUNCH_STAT addCoverCubes 0.04
BRUNCH_STAT blockCube 0.03
BRUNCH_STAT doBmc 0.08
BRUNCH_STAT doPdrTrace 0.17
BRUNCH_STAT doPdrTrace.last 0.11
BRUNCH_STAT doPdrTrace_part1 0.00
BRUNCH_STAT doPdrTrace_part2 0.06
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.05
BRUNCH_STAT generalize 0.02
BRUNCH_STAT getInterpolant 0.01
BRUNCH_STAT pushClauses 0.02
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.02
BRUNCH_STAT run.loop 0.29
BRUNCH_STAT solveWithCore 0.07
BRUNCH_STAT solveWithCore_minCore 0.04
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 702 core size: 370
Core size: original: 370 mincore: 150
UNSAT from BMC at frame: 8
itp             : pi =    78  po =     9  and =    4728  lev = 158
itp             : pi =    78  po =     9  and =    2480  lev =  59
Building PDR trace
9: 0 6 14 17 8 68 11 5 61 
9: 0 6 15 17 8 68 11 5 61 
9: 0 6 15 20 7 34 34 5 62 
9: 0 6 15 20 16 34 34 5 66 
9: 0 6 15 20 16 52 35 6 90 
9: 0 6 15 20 16 52 53 11 93 
9: 0 6 15 20 16 52 53 21 99 
10: 0 6 15 20 16 52 53 21 13 106 
11: 0 6 15 20 16 52 53 21 13 16 108 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 8
BRUNCH_STAT Frame 5
BRUNCH_STAT OrigItp 4728
BRUNCH_STAT SimpItp 2480
BRUNCH_STAT Aig_ManSimplifyComb 0.18
BRUNCH_STAT Glucose_solve 0.20
BRUNCH_STAT Pdr_solve 0.16
BRUNCH_STAT addCoverCubes 0.08
BRUNCH_STAT blockCube 0.09
BRUNCH_STAT doBmc 0.24
BRUNCH_STAT doPdrTrace 0.40
BRUNCH_STAT doPdrTrace.last 0.23
BRUNCH_STAT doPdrTrace_part1 0.01
BRUNCH_STAT doPdrTrace_part2 0.10
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.08
BRUNCH_STAT generalize 0.08
BRUNCH_STAT getInterpolant 0.04
BRUNCH_STAT pushClauses 0.07
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.06
BRUNCH_STAT run.loop 0.86
BRUNCH_STAT solveWithCore 0.21
BRUNCH_STAT solveWithCore_minCore 0.15
BRUNCH_STAT solveWithCore_minSuffix 0.01
BRUNCH_STAT solverAddClause 0.01
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 6 of prefix
Assumption size: 858 core size: 204
Core size: original: 204 mincore: 122
UNSAT from BMC at frame: 10
itp             : pi =    78  po =    11  and =    1312  lev =  86
itp             : pi =    78  po =    11  and =     648  lev =  19
Building PDR trace
11: 0 6 14 20 16 51 53 27 15 16 112 
11: 0 6 14 20 16 51 53 36 16 16 113 
11: 0 6 14 20 16 51 53 36 32 18 124 
11: 0 6 14 20 16 51 53 36 32 41 137 
12: 0 6 14 20 16 51 53 36 32 41 21 151 
13: 0 6 14 20 16 51 53 36 32 41 21 7 149 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 10
BRUNCH_STAT Frame 6
BRUNCH_STAT OrigItp 1312
BRUNCH_STAT SimpItp 648
BRUNCH_STAT Aig_ManSimplifyComb 0.22
BRUNCH_STAT Glucose_solve 0.34
BRUNCH_STAT Pdr_solve 0.29
BRUNCH_STAT addCoverCubes 0.11
BRUNCH_STAT blockCube 0.18
BRUNCH_STAT doBmc 0.40
BRUNCH_STAT doPdrTrace 0.61
BRUNCH_STAT doPdrTrace.last 0.22
BRUNCH_STAT doPdrTrace_part1 0.01
BRUNCH_STAT doPdrTrace_part2 0.13
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.11
BRUNCH_STAT generalize 0.16
BRUNCH_STAT getInterpolant 0.06
BRUNCH_STAT pushClauses 0.10
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.09
BRUNCH_STAT run.loop 1.29
BRUNCH_STAT solveWithCore 0.35
BRUNCH_STAT solveWithCore_minCore 0.27
BRUNCH_STAT solveWithCore_minSuffix 0.02
BRUNCH_STAT solverAddClause 0.02
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 6 of prefix
Assumption size: 1014 core size: 262
Core size: original: 262 mincore: 140
UNSAT from BMC at frame: 12
itp             : pi =    78  po =    13  and =    2743  lev = 184
itp             : pi =    78  po =    13  and =    1167  lev =  32
Building PDR trace
13: 0 6 14 20 16 51 54 50 34 42 21 7 151 
13: 0 6 14 20 16 51 54 56 45 43 22 7 152 
13: 0 6 14 20 16 51 54 56 51 62 25 9 156 
13: 0 6 14 20 16 51 54 56 51 75 29 15 177 
13: 0 6 14 20 16 51 54 56 51 75 32 18 203 
13: 0 6 14 20 16 51 54 56 51 75 32 19 204 
14: 0 6 14 20 16 51 54 56 51 75 32 19 18 195 
15: 0 6 14 20 16 51 54 56 51 75 32 19 18 19 177 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 12
BRUNCH_STAT Frame 7
BRUNCH_STAT OrigItp 2743
BRUNCH_STAT SimpItp 1167
BRUNCH_STAT Aig_ManSimplifyComb 0.28
BRUNCH_STAT Glucose_solve 0.60
BRUNCH_STAT Pdr_solve 0.52
BRUNCH_STAT addCoverCubes 0.17
BRUNCH_STAT blockCube 0.31
BRUNCH_STAT doBmc 0.68
BRUNCH_STAT doPdrTrace 1.05
BRUNCH_STAT doPdrTrace.last 0.43
BRUNCH_STAT doPdrTrace_part1 0.02
BRUNCH_STAT doPdrTrace_part2 0.19
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.15
BRUNCH_STAT generalize 0.29
BRUNCH_STAT getInterpolant 0.11
BRUNCH_STAT pushClauses 0.22
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.19
BRUNCH_STAT run.loop 2.11
BRUNCH_STAT solveWithCore 0.62
BRUNCH_STAT solveWithCore_minCore 0.48
BRUNCH_STAT solveWithCore_minSuffix 0.02
BRUNCH_STAT solverAddClause 0.04
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 8 of prefix
Assumption size: 1170 core size: 252
Core size: original: 252 mincore: 122
UNSAT from BMC at frame: 14
itp             : pi =    78  po =    15  and =    4452  lev =  80
itp             : pi =    78  po =    15  and =    2135  lev =  28
Building PDR trace
15: 0 6 14 20 16 51 54 56 51 83 31 19 18 19 180 
15: 0 6 14 20 16 51 54 56 51 72 51 23 20 20 191 
15: 0 6 14 20 16 51 54 56 51 72 39 33 24 21 219 
15: 0 6 14 20 16 51 54 56 51 72 39 36 38 22 231 
15: 0 6 14 20 16 51 54 56 51 72 39 36 30 26 241 
15: 0 6 14 20 16 51 54 56 51 72 39 36 30 26 241 
16: 0 6 14 20 16 51 54 56 51 72 39 36 30 26 5 244 
17: 0 6 14 20 16 51 54 56 51 72 39 36 30 26 5 9 236 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 14
BRUNCH_STAT Frame 8
BRUNCH_STAT OrigItp 4452
BRUNCH_STAT SimpItp 2135
BRUNCH_STAT Aig_ManSimplifyComb 0.41
BRUNCH_STAT Glucose_solve 0.87
BRUNCH_STAT Pdr_solve 0.85
BRUNCH_STAT addCoverCubes 0.24
BRUNCH_STAT blockCube 0.49
BRUNCH_STAT doBmc 0.99
BRUNCH_STAT doPdrTrace 1.65
BRUNCH_STAT doPdrTrace.last 0.61
BRUNCH_STAT doPdrTrace_part1 0.02
BRUNCH_STAT doPdrTrace_part2 0.25
BRUNCH_STAT doStrengthenVC 0.01
BRUNCH_STAT ensureFrames 0.21
BRUNCH_STAT generalize 0.45
BRUNCH_STAT getInterpolant 0.21
BRUNCH_STAT pushClauses 0.38
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.34
BRUNCH_STAT run.loop 3.27
BRUNCH_STAT solveWithCore 0.90
BRUNCH_STAT solveWithCore_minCore 0.68
BRUNCH_STAT solveWithCore_minSuffix 0.04
BRUNCH_STAT solverAddClause 0.06
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 10 of prefix
Assumption size: 1326 core size: 232
Core size: original: 232 mincore: 117
UNSAT from BMC at frame: 16
itp             : pi =    78  po =    17  and =    2549  lev = 101
itp             : pi =    78  po =    17  and =    1092  lev =  32
Building PDR trace
17: 0 6 14 20 16 51 54 56 51 72 37 30 33 28 7 9 239 
17: 0 6 14 20 16 51 54 56 51 72 37 17 12 25 9 11 277 
17: 0 6 14 20 16 51 54 56 51 72 37 17 9 19 11 17 287 
0
b0
.
17: 0 6 14 20 16 51 54 56 51 72 37 17 9 2 0 0 336 
Verification of invariant with 336 clauses was successful.

************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 16
BRUNCH_STAT Frame 9
BRUNCH_STAT Invar 336
BRUNCH_STAT OrigItp 2549
BRUNCH_STAT SimpItp 1092
BRUNCH_STAT Aig_ManSimplifyComb 0.49
BRUNCH_STAT Glucose_solve 1.12
BRUNCH_STAT Pdr_solve 0.92
BRUNCH_STAT addCoverCubes 0.28
BRUNCH_STAT blockCube 0.52
BRUNCH_STAT doBmc 1.28
BRUNCH_STAT doPdrTrace 1.92
BRUNCH_STAT doPdrTrace.last 0.27
BRUNCH_STAT doPdrTrace_part1 0.03
BRUNCH_STAT doPdrTrace_part2 0.29
BRUNCH_STAT doStrengthenVC 0.01
BRUNCH_STAT ensureFrames 0.23
BRUNCH_STAT generalize 0.48
BRUNCH_STAT getInterpolant 0.27
BRUNCH_STAT pushClauses 0.52
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.45
BRUNCH_STAT run.loop 3.99
BRUNCH_STAT solveWithCore 1.16
BRUNCH_STAT solveWithCore_minCore 0.88
BRUNCH_STAT solveWithCore_minSuffix 0.05
BRUNCH_STAT solverAddClause 0.08
BRUNCH_STAT Result UNSAT
************** BRUNCH STATS END ***************** 
[pavy] Witness begin
0
b0
.
[pavy] Witness end
WINNER:  avyabsmus
BRUNCH_STAT config 2
BRUNCH_STAT config_name avyabsmus
BRUNCH_STAT Result UNSAT
[launch.sh] stop:  Fri Sep 18 17:10:38 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: Fri Sep 18 17:10:41 CEST 2015
[launch.sh] done: Fri Sep 18 17:10:41 CEST 2015
