[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b20s.aig
[launch.sh] host:  atom25 (atom25)
[launch.sh] start: Fri Sep 18 03:41:35 CEST 2015
[launch.sh] jobid: 7193061
[launch.sh] name:  oski15a01b20savy
[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/7193061.1.queue/avy-HWDOAi
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b20s.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b20s.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b20s.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7193061.1.queue/avy-HWDOAi/oski15a01b20s.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b20s.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7193061.1.queue/avy-HWDOAi/oski15a01b20s.pp.aig".

Error: The network is combinational.
[pavy] finished pp, output=/tmp/7193061.1.queue/avy-HWDOAi/oski15a01b20s.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/7193061.1.queue/avy-HWDOAi/navy_avy0.cex /tmp/7193061.1.queue/avy-HWDOAi/oski15a01b20s.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7193061.1.queue/avy-HWDOAi/abcpdr_avy1.cex /tmp/7193061.1.queue/avy-HWDOAi/oski15a01b20s.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/7193061.1.queue/avy-HWDOAi/avyabsmus_avy2.cex /tmp/7193061.1.queue/avy-HWDOAi/oski15a01b20s.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7193061.1.queue/avy-HWDOAi/fib_avy3.cex /tmp/7193061.1.queue/avy-HWDOAi/oski15a01b20s.pp.aig
[pavy] running: [3510, 3511, 3512, 3513]
[pavy] finished pid 3510 with code 0 and signal 11
[pavy] running: [3511, 3512, 3513]
[pavy] finished pid 3511 with code 2 and signal 0
[pavy] running: [3512, 3513]
[pavy] finished pid 3512 with code 0 and signal 0
[pavy] trying to kill  3513
[pavy] waiting for  3513
AVY PARAMETERS
	fName = /tmp/7193061.1.queue/avy-HWDOAi/oski15a01b20s.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/7193061.1.queue/avy-HWDOAi/oski15a01b20s.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: 1
Core size: original: 1 mincore: 1
UNSAT from BMC at frame: 0
itp             : pi =     1  po =     1  and =       0  lev =   0
itp             : pi =     1  po =     1  and =       0  lev =   0
Building PDR trace
0
b0
.
3: 0 0 1 
Verification of invariant with 1 clauses was successful.

************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 0
BRUNCH_STAT Frame 1
BRUNCH_STAT Invar 1
BRUNCH_STAT OrigItp 0
BRUNCH_STAT SimpItp 0
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.01
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 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.02
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 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 03:41:40 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 03:41:44 CEST 2015
[launch.sh] done: Fri Sep 18 03:41:44 CEST 2015
