[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b08s.aig
[launch.sh] host:  atom21 (atom21)
[launch.sh] start: Thu Sep 17 09:49:03 CEST 2015
[launch.sh] jobid: 7191509
[launch.sh] name:  oski15a14b08savy
[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/7191509.1.queue/avy-ZQRMmH
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b08s.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b08s.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b08s.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7191509.1.queue/avy-ZQRMmH/oski15a14b08s.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b08s.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7191509.1.queue/avy-ZQRMmH/oski15a14b08s.pp.aig".

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


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


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 0
BRUNCH_STAT Frame 1
BRUNCH_STAT OrigItp 4
BRUNCH_STAT SimpItp 4
BRUNCH_STAT Aig_ManSimplifyComb 0.00
BRUNCH_STAT Glucose_solve 0.05
BRUNCH_STAT Pdr_solve 0.00
BRUNCH_STAT addCoverCubes 0.05
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT doBmc 0.10
BRUNCH_STAT doPdrTrace 0.13
BRUNCH_STAT doPdrTrace.last 0.13
BRUNCH_STAT doPdrTrace_part1 0.01
BRUNCH_STAT doPdrTrace_part2 0.05
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.11
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.25
BRUNCH_STAT solveWithCore 0.08
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 2 of prefix
Assumption size: 10353 core size: 15
Core size: original: 15 mincore: 14
UNSAT from BMC at frame: 2
itp             : pi =  3451  po =     3  and =      25  lev =  12
itp             : pi =  3451  po =     3  and =       9  lev =   4
Building PDR trace
4: 0 1 1 4 
5: 0 1 1 2 3 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 2
BRUNCH_STAT Frame 2
BRUNCH_STAT OrigItp 25
BRUNCH_STAT SimpItp 9
BRUNCH_STAT Aig_ManSimplifyComb 0.01
BRUNCH_STAT Glucose_solve 0.60
BRUNCH_STAT Pdr_solve 0.01
BRUNCH_STAT addCoverCubes 0.16
BRUNCH_STAT blockCube 0.01
BRUNCH_STAT doBmc 0.88
BRUNCH_STAT doPdrTrace 0.29
BRUNCH_STAT doPdrTrace.last 0.15
BRUNCH_STAT doPdrTrace_part1 0.03
BRUNCH_STAT doPdrTrace_part2 0.17
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.22
BRUNCH_STAT generalize 0.01
BRUNCH_STAT getInterpolant 0.05
BRUNCH_STAT pushClauses 0.01
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.01
BRUNCH_STAT run.loop 1.22
BRUNCH_STAT solveWithCore 0.74
BRUNCH_STAT solveWithCore_minCore 0.07
BRUNCH_STAT solveWithCore_minSuffix 0.01
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 3 of prefix
Assumption size: 17255 core size: 22
Core size: original: 22 mincore: 16
UNSAT from BMC at frame: 4
itp             : pi =  3451  po =     5  and =      46  lev =  27
itp             : pi =  3451  po =     5  and =      11  lev =   4
Building PDR trace
5: 0 1 1 1 5 
6: 0 1 1 1 2 3 
7: 0 1 1 1 2 4 1 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 4
BRUNCH_STAT Frame 3
BRUNCH_STAT OrigItp 46
BRUNCH_STAT SimpItp 11
BRUNCH_STAT Aig_ManSimplifyComb 0.01
BRUNCH_STAT Glucose_solve 2.00
BRUNCH_STAT Pdr_solve 0.02
BRUNCH_STAT addCoverCubes 0.35
BRUNCH_STAT blockCube 0.01
BRUNCH_STAT doBmc 2.67
BRUNCH_STAT doPdrTrace 0.57
BRUNCH_STAT doPdrTrace.last 0.29
BRUNCH_STAT doPdrTrace_part1 0.07
BRUNCH_STAT doPdrTrace_part2 0.37
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.43
BRUNCH_STAT generalize 0.01
BRUNCH_STAT getInterpolant 0.11
BRUNCH_STAT pushClauses 0.02
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.02
BRUNCH_STAT run.loop 3.37
BRUNCH_STAT solveWithCore 2.31
BRUNCH_STAT solveWithCore_minCore 0.39
BRUNCH_STAT solveWithCore_minSuffix 0.07
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 4 of prefix
Assumption size: 24157 core size: 35
Core size: original: 35 mincore: 29
UNSAT from BMC at frame: 6
itp             : pi =  3451  po =     7  and =     184  lev =  39
itp             : pi =  3451  po =     7  and =      31  lev =   6
Building PDR trace
7: 0 1 1 1 1 4 2 
7: 0 1 1 1 1 1 7 
8: 0 1 1 1 1 1 2 5 
9: 0 1 1 1 1 1 2 4 2 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 6
BRUNCH_STAT Frame 4
BRUNCH_STAT OrigItp 184
BRUNCH_STAT SimpItp 31
BRUNCH_STAT Aig_ManSimplifyComb 0.02
BRUNCH_STAT Glucose_solve 4.84
BRUNCH_STAT Pdr_solve 0.04
BRUNCH_STAT addCoverCubes 0.60
BRUNCH_STAT blockCube 0.02
BRUNCH_STAT doBmc 6.22
BRUNCH_STAT doPdrTrace 0.96
BRUNCH_STAT doPdrTrace.last 0.39
BRUNCH_STAT doPdrTrace_part1 0.12
BRUNCH_STAT doPdrTrace_part2 0.64
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.69
BRUNCH_STAT generalize 0.02
BRUNCH_STAT getInterpolant 0.22
BRUNCH_STAT pushClauses 0.03
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.03
BRUNCH_STAT run.loop 7.42
BRUNCH_STAT solveWithCore 5.46
BRUNCH_STAT solveWithCore_minCore 1.45
BRUNCH_STAT solveWithCore_minSuffix 0.22
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 7 of prefix
Assumption size: 31059 core size: 26
Core size: original: 26 mincore: 19
UNSAT from BMC at frame: 8
itp             : pi =  3451  po =     9  and =      58  lev =  21
itp             : pi =  3451  po =     9  and =      11  lev =   5
Building PDR trace
9: 0 1 1 1 1 1 2 3 4 
10: 0 1 1 1 1 1 2 3 3 2 
11: 0 1 1 1 1 1 2 3 3 4 1 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 8
BRUNCH_STAT Frame 5
BRUNCH_STAT OrigItp 58
BRUNCH_STAT SimpItp 11
BRUNCH_STAT Aig_ManSimplifyComb 0.03
BRUNCH_STAT Glucose_solve 8.08
BRUNCH_STAT Pdr_solve 0.05
BRUNCH_STAT addCoverCubes 0.78
BRUNCH_STAT blockCube 0.03
BRUNCH_STAT doBmc 10.29
BRUNCH_STAT doPdrTrace 1.23
BRUNCH_STAT doPdrTrace.last 0.27
BRUNCH_STAT doPdrTrace_part1 0.15
BRUNCH_STAT doPdrTrace_part2 0.83
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.88
BRUNCH_STAT generalize 0.03
BRUNCH_STAT getInterpolant 0.35
BRUNCH_STAT pushClauses 0.05
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.05
BRUNCH_STAT run.loop 11.90
BRUNCH_STAT solveWithCore 9.08
BRUNCH_STAT solveWithCore_minCore 2.31
BRUNCH_STAT solveWithCore_minSuffix 0.61
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 6 of prefix
Assumption size: 37961 core size: 54
Core size: original: 54 mincore: 43
UNSAT from BMC at frame: 10
itp             : pi =  3451  po =    11  and =     493  lev =  63
itp             : pi =  3451  po =    11  and =      88  lev =  10
Building PDR trace
11: 0 1 1 1 1 1 1 3 4 4 1 
11: 0 1 1 1 1 1 1 2 3 5 1 
11: 0 1 1 1 1 1 1 2 3 5 1 
11: 0 1 1 1 1 1 1 2 3 3 4 
12: 0 1 1 1 1 1 1 2 3 3 3 2 
13: 0 1 1 1 1 1 1 2 3 3 3 4 1 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 10
BRUNCH_STAT Frame 6
BRUNCH_STAT OrigItp 493
BRUNCH_STAT SimpItp 88
BRUNCH_STAT Aig_ManSimplifyComb 0.04
BRUNCH_STAT Glucose_solve 14.27
BRUNCH_STAT Pdr_solve 0.08
BRUNCH_STAT addCoverCubes 1.15
BRUNCH_STAT blockCube 0.05
BRUNCH_STAT doBmc 17.62
BRUNCH_STAT doPdrTrace 1.80
BRUNCH_STAT doPdrTrace.last 0.57
BRUNCH_STAT doPdrTrace_part1 0.22
BRUNCH_STAT doPdrTrace_part2 1.21
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 1.26
BRUNCH_STAT generalize 0.05
BRUNCH_STAT getInterpolant 0.58
BRUNCH_STAT pushClauses 0.09
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.09
BRUNCH_STAT run.loop 20.03
BRUNCH_STAT solveWithCore 15.75
BRUNCH_STAT solveWithCore_minCore 5.44
BRUNCH_STAT solveWithCore_minSuffix 1.04
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 7 of prefix
Assumption size: 44863 core size: 62
Core size: original: 62 mincore: 47
UNSAT from BMC at frame: 12
itp             : pi =  3451  po =    13  and =     982  lev =  84
itp             : pi =  3451  po =    13  and =      82  lev =   9
Building PDR trace
13: 0 1 1 1 1 1 1 1 2 3 4 4 1 
13: 0 1 1 1 1 1 1 1 2 3 4 4 1 
13: 0 1 1 1 1 1 1 1 2 3 2 5 1 
13: 0 1 1 1 1 1 1 1 2 3 2 5 1 
13: 0 1 1 1 1 1 1 1 2 3 2 3 4 
14: 0 1 1 1 1 1 1 1 2 3 2 3 3 2 
15: 0 1 1 1 1 1 1 1 2 3 2 3 3 4 1 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 12
BRUNCH_STAT Frame 7
BRUNCH_STAT OrigItp 982
BRUNCH_STAT SimpItp 82
BRUNCH_STAT Aig_ManSimplifyComb 0.06
BRUNCH_STAT Glucose_solve 23.43
BRUNCH_STAT Pdr_solve 0.10
BRUNCH_STAT addCoverCubes 1.58
BRUNCH_STAT blockCube 0.07
BRUNCH_STAT doBmc 28.23
BRUNCH_STAT doPdrTrace 2.45
BRUNCH_STAT doPdrTrace.last 0.66
BRUNCH_STAT doPdrTrace_part1 0.31
BRUNCH_STAT doPdrTrace_part2 1.66
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 1.70
BRUNCH_STAT generalize 0.07
BRUNCH_STAT getInterpolant 0.90
BRUNCH_STAT pushClauses 0.15
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.15
BRUNCH_STAT run.loop 31.64
BRUNCH_STAT solveWithCore 25.48
BRUNCH_STAT solveWithCore_minCore 9.90
BRUNCH_STAT solveWithCore_minSuffix 2.15
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 8 of prefix
Assumption size: 51765 core size: 72
Core size: original: 72 mincore: 59
UNSAT from BMC at frame: 14
itp             : pi =  3451  po =    15  and =    1110  lev =  76
itp             : pi =  3451  po =    15  and =     119  lev =  10
Building PDR trace
15: 0 1 1 1 1 1 1 1 1 1 4 2 4 4 1 
0
b0
.
15: 0 1 1 1 1 1 1 1 1 0 0 0 0 0 12 
Verification of invariant with 12 clauses was successful.

************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 14
BRUNCH_STAT Frame 8
BRUNCH_STAT Invar 12
BRUNCH_STAT OrigItp 1110
BRUNCH_STAT SimpItp 119
BRUNCH_STAT Aig_ManSimplifyComb 0.09
BRUNCH_STAT Glucose_solve 35.17
BRUNCH_STAT Pdr_solve 0.11
BRUNCH_STAT addCoverCubes 1.70
BRUNCH_STAT blockCube 0.08
BRUNCH_STAT doBmc 41.55
BRUNCH_STAT doPdrTrace 2.64
BRUNCH_STAT doPdrTrace.last 0.19
BRUNCH_STAT doPdrTrace_part1 0.33
BRUNCH_STAT doPdrTrace_part2 1.79
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 1.82
BRUNCH_STAT generalize 0.08
BRUNCH_STAT getInterpolant 1.31
BRUNCH_STAT pushClauses 0.16
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.16
BRUNCH_STAT run.loop 45.61
BRUNCH_STAT solveWithCore 37.85
BRUNCH_STAT solveWithCore_minCore 16.27
BRUNCH_STAT solveWithCore_minSuffix 3.53
BRUNCH_STAT solverAddClause 0.00
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:  Thu Sep 17 09:49:57 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: Thu Sep 17 09:50:00 CEST 2015
[launch.sh] done: Thu Sep 17 09:50:00 CEST 2015
