[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/all/selection/random/6s131.aig
[launch.sh] host:  atom03 (atom03)
[launch.sh] start: Sun Sep 20 13:56:19 CEST 2015
[launch.sh] jobid: 7197381
[launch.sh] name:  h6s131avy
[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/7197381.1.queue/avy-7xwz_B
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/all/selection/random/6s131.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/all/selection/random/6s131.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/all/selection/random/6s131.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7197381.1.queue/avy-7xwz_B/6s131.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/all/selection/random/6s131.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7197381.1.queue/avy-7xwz_B/6s131.pp.aig".

[pavy] finished pp, output=/tmp/7197381.1.queue/avy-7xwz_B/6s131.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/7197381.1.queue/avy-7xwz_B/navy_avy0.cex /tmp/7197381.1.queue/avy-7xwz_B/6s131.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7197381.1.queue/avy-7xwz_B/abcpdr_avy1.cex /tmp/7197381.1.queue/avy-7xwz_B/6s131.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/7197381.1.queue/avy-7xwz_B/avyabsmus_avy2.cex /tmp/7197381.1.queue/avy-7xwz_B/6s131.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7197381.1.queue/avy-7xwz_B/fib_avy3.cex /tmp/7197381.1.queue/avy-7xwz_B/6s131.pp.aig
[pavy] running: [10573, 10574, 10575, 10576]
[pavy] finished pid 10575 with code 0 and signal 0
[pavy] trying to kill  10573
[pavy] waiting for  10573
[pavy] trying to kill  10574
[pavy] waiting for  10574
[pavy] trying to kill  10576
[pavy] waiting for  10576
AVY PARAMETERS
	fName = /tmp/7197381.1.queue/avy-7xwz_B/6s131.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/7197381.1.queue/avy-7xwz_B/6s131.pp.aig'


************** BRUNCH STATS ***************** 
BRUNCH_STAT run.loop 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 608 core size: 23
Core size: original: 23 mincore: 14
UNSAT from BMC at frame: 0
itp             : pi =   608  po =     1  and =     730  lev = 221
itp             : pi =   608  po =     1  and =     260  lev =  51
Building PDR trace
3: 0 13 1 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 0
BRUNCH_STAT Frame 1
BRUNCH_STAT OrigItp 730
BRUNCH_STAT SimpItp 260
BRUNCH_STAT Aig_ManSimplifyComb 0.02
BRUNCH_STAT Glucose_solve 0.03
BRUNCH_STAT Pdr_solve 0.00
BRUNCH_STAT addCoverCubes 0.03
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT doBmc 0.06
BRUNCH_STAT doPdrTrace 0.08
BRUNCH_STAT doPdrTrace.last 0.08
BRUNCH_STAT doPdrTrace_part1 0.01
BRUNCH_STAT doPdrTrace_part2 0.03
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.07
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getInterpolant 0.01
BRUNCH_STAT pushClauses 0.00
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.00
BRUNCH_STAT run.loop 0.17
BRUNCH_STAT solveWithCore 0.04
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: 1824 core size: 129
Core size: original: 129 mincore: 65
UNSAT from BMC at frame: 2
itp             : pi =   608  po =     3  and =   21690  lev = 708
itp             : pi =   608  po =     3  and =    8026  lev = 120
Building PDR trace
3: 0 51 10 
4: 0 51 15 538 
5: 0 51 15 4 537 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 2
BRUNCH_STAT Frame 2
BRUNCH_STAT OrigItp 21690
BRUNCH_STAT SimpItp 8026
BRUNCH_STAT Aig_ManSimplifyComb 0.86
BRUNCH_STAT Glucose_solve 0.52
BRUNCH_STAT Pdr_solve 2.22
BRUNCH_STAT addCoverCubes 0.19
BRUNCH_STAT blockCube 0.98
BRUNCH_STAT doBmc 0.67
BRUNCH_STAT doPdrTrace 2.59
BRUNCH_STAT doPdrTrace.last 2.50
BRUNCH_STAT doPdrTrace_part1 0.03
BRUNCH_STAT doPdrTrace_part2 0.20
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.23
BRUNCH_STAT generalize 0.88
BRUNCH_STAT getInterpolant 0.21
BRUNCH_STAT pushClauses 0.08
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.08
BRUNCH_STAT run.loop 4.33
BRUNCH_STAT solveWithCore 0.57
BRUNCH_STAT solveWithCore_minCore 0.28
BRUNCH_STAT solveWithCore_minSuffix 0.05
BRUNCH_STAT solverAddClause 0.01
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 3040 core size: 473
Core size: original: 473 mincore: 213
UNSAT from BMC at frame: 4
itp             : pi =   608  po =     5  and =   78456  lev = 517
itp             : pi =   608  po =     5  and =   39064  lev = 177
Building PDR trace
5: 0 241 15 4 539 
5: 0 241 66 4 1590 
5: 0 241 66 3 1594 
6: 0 241 66 3 3 1592 
7: 0 241 66 3 3 1 1594 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 4
BRUNCH_STAT Frame 3
BRUNCH_STAT OrigItp 78456
BRUNCH_STAT SimpItp 39064
BRUNCH_STAT Aig_ManSimplifyComb 4.88
BRUNCH_STAT Glucose_solve 7.59
BRUNCH_STAT Pdr_solve 13.47
BRUNCH_STAT addCoverCubes 0.68
BRUNCH_STAT blockCube 6.04
BRUNCH_STAT doBmc 8.58
BRUNCH_STAT doPdrTrace 14.97
BRUNCH_STAT doPdrTrace.last 12.39
BRUNCH_STAT doPdrTrace_part1 0.14
BRUNCH_STAT doPdrTrace_part2 0.67
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.70
BRUNCH_STAT generalize 4.83
BRUNCH_STAT getInterpolant 2.62
BRUNCH_STAT pushClauses 0.56
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.46
BRUNCH_STAT run.loop 31.06
BRUNCH_STAT solveWithCore 7.72
BRUNCH_STAT solveWithCore_minCore 6.45
BRUNCH_STAT solveWithCore_minSuffix 0.11
BRUNCH_STAT solverAddClause 0.04
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 4256 core size: 839
Core size: original: 839 mincore: 343
UNSAT from BMC at frame: 6
itp             : pi =   608  po =     7  and =   51393  lev = 798
itp             : pi =   608  po =     7  and =   20398  lev = 156
Building PDR trace
7: 0 281 20 25 21 1 1596 
7: 0 281 84 527 5 19 1599 
7: 0 281 84 288 312 20 1603 
7: 0 281 84 288 1221 239 1933 
7: 0 281 84 288 1221 43 2376 
8: 0 281 84 288 1221 43 4 2378 
9: 0 281 84 288 1221 43 4 2 2379 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 6
BRUNCH_STAT Frame 4
BRUNCH_STAT OrigItp 51393
BRUNCH_STAT SimpItp 20398
BRUNCH_STAT Aig_ManSimplifyComb 7.21
BRUNCH_STAT Glucose_solve 23.16
BRUNCH_STAT Pdr_solve 46.64
BRUNCH_STAT addCoverCubes 1.33
BRUNCH_STAT blockCube 30.91
BRUNCH_STAT doBmc 24.99
BRUNCH_STAT doPdrTrace 50.88
BRUNCH_STAT doPdrTrace.last 35.91
BRUNCH_STAT doPdrTrace_part1 0.25
BRUNCH_STAT doPdrTrace_part2 1.27
BRUNCH_STAT doStrengthenVC 0.01
BRUNCH_STAT ensureFrames 1.27
BRUNCH_STAT generalize 27.85
BRUNCH_STAT getInterpolant 5.16
BRUNCH_STAT pushClauses 2.45
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 2.10
BRUNCH_STAT run.loop 88.25
BRUNCH_STAT solveWithCore 23.41
BRUNCH_STAT solveWithCore_minCore 18.54
BRUNCH_STAT solveWithCore_minSuffix 1.09
BRUNCH_STAT solverAddClause 0.15
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 5472 core size: 856
Core size: original: 856 mincore: 180
UNSAT from BMC at frame: 8
itp             : pi =   608  po =     9  and =   96347  lev = 496
itp             : pi =   608  po =     9  and =   34475  lev = 190
Building PDR trace
9: 0 280 40 37 33 43 4 2 2379 
9: 0 280 40 37 33 43 4 2 2379 
9: 0 280 40 37 33 43 4 2 2635 
9: 0 280 40 37 33 43 4 2 2635 
9: 0 280 40 37 33 43 4 2 2635 
9: 0 280 40 37 33 43 4 2 2635 
9: 0 280 40 37 33 43 4 1 2639 
0
b0
.
10: 0 280 40 37 33 43 4 1 0 2639 
Verification of invariant with 2639 clauses was successful.

************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 8
BRUNCH_STAT Frame 5
BRUNCH_STAT Invar 2639
BRUNCH_STAT OrigItp 96347
BRUNCH_STAT SimpItp 34475
BRUNCH_STAT Aig_ManSimplifyComb 10.92
BRUNCH_STAT Glucose_solve 36.39
BRUNCH_STAT Pdr_solve 48.67
BRUNCH_STAT addCoverCubes 2.07
BRUNCH_STAT blockCube 31.74
BRUNCH_STAT doBmc 39.01
BRUNCH_STAT doPdrTrace 56.03
BRUNCH_STAT doPdrTrace.last 5.14
BRUNCH_STAT doPdrTrace_part1 0.42
BRUNCH_STAT doPdrTrace_part2 1.96
BRUNCH_STAT doStrengthenVC 0.01
BRUNCH_STAT ensureFrames 1.90
BRUNCH_STAT generalize 28.51
BRUNCH_STAT getInterpolant 8.63
BRUNCH_STAT pushClauses 4.56
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 3.61
BRUNCH_STAT run.loop 114.69
BRUNCH_STAT solveWithCore 36.80
BRUNCH_STAT solveWithCore_minCore 26.69
BRUNCH_STAT solveWithCore_minSuffix 2.54
BRUNCH_STAT solverAddClause 0.28
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:  Sun Sep 20 13:58:25 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 13:58:28 CEST 2015
[launch.sh] done: Sun Sep 20 13:58:28 CEST 2015
