[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b04s.aig
[launch.sh] host:  atom06 (atom06)
[launch.sh] start: Thu Sep 17 22:31:19 CEST 2015
[launch.sh] jobid: 7192565
[launch.sh] name:  oski15a01b04savy
[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/7192565.1.queue/avy-Iqg4ES
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b04s.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b04s.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b04s.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7192565.1.queue/avy-Iqg4ES/oski15a01b04s.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b04s.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7192565.1.queue/avy-Iqg4ES/oski15a01b04s.pp.aig".

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


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


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 0
BRUNCH_STAT Frame 1
BRUNCH_STAT OrigItp 1
BRUNCH_STAT SimpItp 1
BRUNCH_STAT Aig_ManSimplifyComb 0.04
BRUNCH_STAT Glucose_solve 0.58
BRUNCH_STAT Pdr_solve 0.00
BRUNCH_STAT addCoverCubes 0.62
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT doBmc 1.18
BRUNCH_STAT doPdrTrace 1.56
BRUNCH_STAT doPdrTrace.last 1.56
BRUNCH_STAT doPdrTrace_part1 0.27
BRUNCH_STAT doPdrTrace_part2 0.64
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 1.25
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getInterpolant 0.10
BRUNCH_STAT pushClauses 0.01
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.01
BRUNCH_STAT run.loop 2.88
BRUNCH_STAT solveWithCore 0.88
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: 74220 core size: 6
Core size: original: 6 mincore: 6
UNSAT from BMC at frame: 2
itp             : pi = 24740  po =     3  and =       3  lev =   1
itp             : pi = 24740  po =     3  and =       3  lev =   1
Building PDR trace
3: 0 1 3 
4: 0 1 1 2 
5: 0 1 1 1 1 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 2
BRUNCH_STAT Frame 2
BRUNCH_STAT OrigItp 3
BRUNCH_STAT SimpItp 3
BRUNCH_STAT Aig_ManSimplifyComb 0.06
BRUNCH_STAT Glucose_solve 5.31
BRUNCH_STAT Pdr_solve 0.00
BRUNCH_STAT addCoverCubes 2.32
BRUNCH_STAT blockCube 0.00
BRUNCH_STAT doBmc 7.73
BRUNCH_STAT doPdrTrace 4.06
BRUNCH_STAT doPdrTrace.last 2.50
BRUNCH_STAT doPdrTrace_part1 0.91
BRUNCH_STAT doPdrTrace_part2 2.42
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 2.98
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getInterpolant 0.33
BRUNCH_STAT pushClauses 0.02
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.02
BRUNCH_STAT run.loop 12.18
BRUNCH_STAT solveWithCore 6.48
BRUNCH_STAT solveWithCore_minCore 0.19
BRUNCH_STAT solveWithCore_minSuffix 0.13
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 123700 core size: 27
Core size: original: 27 mincore: 27
UNSAT from BMC at frame: 4
itp             : pi = 24740  po =     5  and =      22  lev =   9
itp             : pi = 24740  po =     5  and =      22  lev =   5
Building PDR trace
5: 0 19 2 1 1 
5: 0 19 2 2 1 
5: 0 19 2 2 2 
6: 0 19 2 2 1 2 
7: 0 19 2 2 1 1 1 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 4
BRUNCH_STAT Frame 3
BRUNCH_STAT OrigItp 22
BRUNCH_STAT SimpItp 22
BRUNCH_STAT Aig_ManSimplifyComb 0.10
BRUNCH_STAT Glucose_solve 20.54
BRUNCH_STAT Pdr_solve 0.02
BRUNCH_STAT addCoverCubes 5.13
BRUNCH_STAT blockCube 0.01
BRUNCH_STAT doBmc 26.31
BRUNCH_STAT doPdrTrace 8.36
BRUNCH_STAT doPdrTrace.last 4.30
BRUNCH_STAT doPdrTrace_part1 1.98
BRUNCH_STAT doPdrTrace_part2 5.36
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 5.80
BRUNCH_STAT generalize 0.01
BRUNCH_STAT getInterpolant 0.93
BRUNCH_STAT pushClauses 0.19
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.19
BRUNCH_STAT run.loop 35.69
BRUNCH_STAT solveWithCore 23.35
BRUNCH_STAT solveWithCore_minCore 3.21
BRUNCH_STAT solveWithCore_minSuffix 2.30
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 4 of prefix
Assumption size: 173180 core size: 9
Core size: original: 9 mincore: 9
UNSAT from BMC at frame: 6
itp             : pi = 24740  po =     7  and =       6  lev =   2
itp             : pi = 24740  po =     7  and =       5  lev =   2
Building PDR trace
7: 0 18 1 1 1 1 3 
7: 0 18 1 1 1 1 4 
8: 0 18 1 1 1 1 1 4 
0
b0
.
9: 0 18 1 1 1 1 1 0 5 
Verification of invariant with 5 clauses was successful.

************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 6
BRUNCH_STAT Frame 4
BRUNCH_STAT Invar 5
BRUNCH_STAT OrigItp 6
BRUNCH_STAT SimpItp 5
BRUNCH_STAT Aig_ManSimplifyComb 0.13
BRUNCH_STAT Glucose_solve 41.90
BRUNCH_STAT Pdr_solve 0.03
BRUNCH_STAT addCoverCubes 7.37
BRUNCH_STAT blockCube 0.01
BRUNCH_STAT doBmc 52.89
BRUNCH_STAT doPdrTrace 11.69
BRUNCH_STAT doPdrTrace.last 3.33
BRUNCH_STAT doPdrTrace_part1 2.85
BRUNCH_STAT doPdrTrace_part2 7.71
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 8.08
BRUNCH_STAT generalize 0.01
BRUNCH_STAT getInterpolant 1.68
BRUNCH_STAT pushClauses 0.20
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.20
BRUNCH_STAT run.loop 66.45
BRUNCH_STAT solveWithCore 47.09
BRUNCH_STAT solveWithCore_minCore 6.46
BRUNCH_STAT solveWithCore_minSuffix 5.90
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 22:33:50 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 22:33:53 CEST 2015
[launch.sh] done: Thu Sep 17 22:33:53 CEST 2015
