[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/all/selection/random/beemfwt2b2.aig
[launch.sh] host:  atom31 (atom31)
[launch.sh] start: Sun Sep 20 07:40:11 CEST 2015
[launch.sh] jobid: 7196981
[launch.sh] name:  beemfwt2b2avy
[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/7196981.1.queue/avy-ZUBir6
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/all/selection/random/beemfwt2b2.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/all/selection/random/beemfwt2b2.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/all/selection/random/beemfwt2b2.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7196981.1.queue/avy-ZUBir6/beemfwt2b2.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/all/selection/random/beemfwt2b2.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7196981.1.queue/avy-ZUBir6/beemfwt2b2.pp.aig".

[pavy] finished pp, output=/tmp/7196981.1.queue/avy-ZUBir6/beemfwt2b2.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/7196981.1.queue/avy-ZUBir6/navy_avy0.cex /tmp/7196981.1.queue/avy-ZUBir6/beemfwt2b2.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7196981.1.queue/avy-ZUBir6/abcpdr_avy1.cex /tmp/7196981.1.queue/avy-ZUBir6/beemfwt2b2.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/7196981.1.queue/avy-ZUBir6/avyabsmus_avy2.cex /tmp/7196981.1.queue/avy-ZUBir6/beemfwt2b2.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7196981.1.queue/avy-ZUBir6/fib_avy3.cex /tmp/7196981.1.queue/avy-ZUBir6/beemfwt2b2.pp.aig
[pavy] running: [12074, 12075, 12076, 12077]
[pavy] finished pid 12074 with code 0 and signal 0
[pavy] trying to kill  12075
[pavy] waiting for  12075
[pavy] trying to kill  12076
[pavy] waiting for  12076
[pavy] trying to kill  12077
[pavy] waiting for  12077
AVY PARAMETERS
	fName = /tmp/7196981.1.queue/avy-ZUBir6/beemfwt2b2.pp.aig
	ipt = 0
	avy = 1
	stutter = 0
	reset-cover = 1
	shallow_push = 1
	min-core = 0
	abstraction = 0
	tr0 = 0
	pdr = 100000
	min-suffix = 1
	sat1 = 0
	minisat = 0
	glucose = 1
	minisat_itp = 0
	glucose_itp = 1
	sat_simp = 0
	itp_simp = 0
	proof_reorder = 0
	gen-conf-limit = 0
	kstep = 1
	stick-error = 0
	itp-simplify = 1
	max-frame = 100000
END
Starting ABC
	Reading AIG from '/tmp/7196981.1.queue/avy-ZUBir6/beemfwt2b2.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: 2
UNSAT from BMC at frame: 0
itp             : pi =   610  po =     1  and =       1  lev =   1
itp             : pi =   610  po =     1  and =       1  lev =   1
FINDING NEEDED CONSTRAINTS: CoNum: 1 EquivNum: 1
. Done
Building PDR trace
3: 0 1 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 0
BRUNCH_STAT Frame 1
BRUNCH_STAT OrigItp 1
BRUNCH_STAT SimpItp 1
BRUNCH_STAT Aig_ManSimplifyComb 0.00
BRUNCH_STAT Glucose_solve 0.00
BRUNCH_STAT Pdr_solve 0.01
BRUNCH_STAT addCoverCubes 0.02
BRUNCH_STAT blockCube 0.01
BRUNCH_STAT doBmc 0.00
BRUNCH_STAT doPdrTrace 0.07
BRUNCH_STAT doPdrTrace.last 0.07
BRUNCH_STAT doPdrTrace_part1 0.00
BRUNCH_STAT doPdrTrace_part2 0.03
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.04
BRUNCH_STAT findItpConstraints 0.00
BRUNCH_STAT generalize 0.01
BRUNCH_STAT getCnfTr 0.00
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.01
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.01
BRUNCH_STAT run.loop 0.08
BRUNCH_STAT solveWithCore 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: 2 core size: 2
UNSAT from BMC at frame: 1
itp             : pi =   610  po =     2  and =      78  lev =  78
itp             : pi =   610  po =     2  and =      78  lev =   7
FINDING NEEDED CONSTRAINTS: CoNum: 2 EquivNum: 2
. Done
Building PDR trace
4: 0 1 1 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 1
BRUNCH_STAT Frame 2
BRUNCH_STAT OrigItp 78
BRUNCH_STAT SimpItp 78
BRUNCH_STAT Aig_ManSimplifyComb 0.01
BRUNCH_STAT Glucose_solve 0.00
BRUNCH_STAT Pdr_solve 0.04
BRUNCH_STAT addCoverCubes 0.04
BRUNCH_STAT blockCube 0.04
BRUNCH_STAT computeNextTr 0.00
BRUNCH_STAT doBmc 0.04
BRUNCH_STAT doPdrTrace 0.15
BRUNCH_STAT doPdrTrace.last 0.07
BRUNCH_STAT doPdrTrace_part1 0.01
BRUNCH_STAT doPdrTrace_part2 0.06
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.07
BRUNCH_STAT findItpConstraints 0.00
BRUNCH_STAT generalize 0.04
BRUNCH_STAT getCnfTr 0.02
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.01
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.01
BRUNCH_STAT run.loop 0.20
BRUNCH_STAT solveWithCore 0.04
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 3 of prefix
Assumption size: 3 core size: 2
UNSAT from BMC at frame: 2
itp             : pi =   610  po =     3  and =     280  lev = 280
itp             : pi =   610  po =     3  and =     280  lev =   9
FINDING NEEDED CONSTRAINTS: CoNum: 3 EquivNum: 3
. Done
Building PDR trace
5: 0 1 1 1 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 2
BRUNCH_STAT Frame 3
BRUNCH_STAT OrigItp 280
BRUNCH_STAT SimpItp 280
BRUNCH_STAT Aig_ManSimplifyComb 0.02
BRUNCH_STAT Glucose_solve 0.01
BRUNCH_STAT Pdr_solve 0.18
BRUNCH_STAT addCoverCubes 0.07
BRUNCH_STAT blockCube 0.18
BRUNCH_STAT computeNextTr 0.00
BRUNCH_STAT doBmc 0.09
BRUNCH_STAT doPdrTrace 0.35
BRUNCH_STAT doPdrTrace.last 0.20
BRUNCH_STAT doPdrTrace_part1 0.01
BRUNCH_STAT doPdrTrace_part2 0.09
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.09
BRUNCH_STAT findItpConstraints 0.00
BRUNCH_STAT generalize 0.18
BRUNCH_STAT getCnfTr 0.04
BRUNCH_STAT getInterpolant 0.01
BRUNCH_STAT pushClauses 0.02
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.02
BRUNCH_STAT run.loop 0.47
BRUNCH_STAT solveWithCore 0.09
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 4 core size: 5
UNSAT from BMC at frame: 3
itp             : pi =   610  po =     4  and =     397  lev = 273
itp             : pi =   610  po =     4  and =     305  lev =   9
FINDING NEEDED CONSTRAINTS: CoNum: 4 EquivNum: 4
.... Done
Building PDR trace
5: 0 3 1 1 0 
5: 0 3 3 1 0 
5: 0 3 3 2 0 
6: 0 3 3 2 1 0 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 3
BRUNCH_STAT Frame 4
BRUNCH_STAT OrigItp 397
BRUNCH_STAT SimpItp 305
BRUNCH_STAT Aig_ManSimplifyComb 0.04
BRUNCH_STAT Glucose_solve 0.05
BRUNCH_STAT Pdr_solve 0.39
BRUNCH_STAT addCoverCubes 0.16
BRUNCH_STAT blockCube 0.38
BRUNCH_STAT computeNextTr 0.00
BRUNCH_STAT doBmc 0.17
BRUNCH_STAT doPdrTrace 0.73
BRUNCH_STAT doPdrTrace.last 0.38
BRUNCH_STAT doPdrTrace_part1 0.03
BRUNCH_STAT doPdrTrace_part2 0.22
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.19
BRUNCH_STAT findItpConstraints 0.00
BRUNCH_STAT generalize 0.38
BRUNCH_STAT getCnfTr 0.06
BRUNCH_STAT getInterpolant 0.02
BRUNCH_STAT pushClauses 0.04
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.04
BRUNCH_STAT run.loop 0.96
BRUNCH_STAT solveWithCore 0.17
BRUNCH_STAT solveWithCore_minSuffix 0.04
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 5 core size: 6
UNSAT from BMC at frame: 4
itp             : pi =   610  po =     5  and =     606  lev = 299
itp             : pi =   610  po =     5  and =     366  lev =   9
FINDING NEEDED CONSTRAINTS: CoNum: 5 EquivNum: 5
..... Done
Building PDR trace
6: 0 3 3 2 1 1 
6: 0 3 7 2 1 1 
6: 0 3 7 2 1 1 
6: 0 3 7 2 1 1 
7: 0 3 7 2 1 1 1 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 4
BRUNCH_STAT Frame 5
BRUNCH_STAT OrigItp 606
BRUNCH_STAT SimpItp 366
BRUNCH_STAT Aig_ManSimplifyComb 0.06
BRUNCH_STAT Glucose_solve 0.12
BRUNCH_STAT Pdr_solve 0.61
BRUNCH_STAT addCoverCubes 0.27
BRUNCH_STAT blockCube 0.60
BRUNCH_STAT computeNextTr 0.00
BRUNCH_STAT doBmc 0.27
BRUNCH_STAT doPdrTrace 1.19
BRUNCH_STAT doPdrTrace.last 0.46
BRUNCH_STAT doPdrTrace_part1 0.05
BRUNCH_STAT doPdrTrace_part2 0.38
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.31
BRUNCH_STAT findItpConstraints 0.01
BRUNCH_STAT generalize 0.60
BRUNCH_STAT getCnfTr 0.08
BRUNCH_STAT getInterpolant 0.04
BRUNCH_STAT pushClauses 0.08
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.08
BRUNCH_STAT run.loop 1.57
BRUNCH_STAT solveWithCore 0.27
BRUNCH_STAT solveWithCore_minSuffix 0.10
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 6 core size: 3
UNSAT from BMC at frame: 5
itp             : pi =   610  po =     6  and =     585  lev = 316
itp             : pi =   610  po =     6  and =     381  lev =   9
FINDING NEEDED CONSTRAINTS: CoNum: 6 EquivNum: 6
.. Done
Building PDR trace
7: 0 3 7 2 1 8 4 
8: 0 3 7 2 1 8 1 4 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 5
BRUNCH_STAT Frame 6
BRUNCH_STAT OrigItp 585
BRUNCH_STAT SimpItp 381
BRUNCH_STAT Aig_ManSimplifyComb 0.08
BRUNCH_STAT Glucose_solve 0.24
BRUNCH_STAT Pdr_solve 1.84
BRUNCH_STAT addCoverCubes 0.32
BRUNCH_STAT blockCube 1.82
BRUNCH_STAT computeNextTr 0.00
BRUNCH_STAT doBmc 0.44
BRUNCH_STAT doPdrTrace 2.53
BRUNCH_STAT doPdrTrace.last 1.34
BRUNCH_STAT doPdrTrace_part1 0.06
BRUNCH_STAT doPdrTrace_part2 0.45
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.36
BRUNCH_STAT findItpConstraints 0.01
BRUNCH_STAT generalize 1.82
BRUNCH_STAT getCnfTr 0.10
BRUNCH_STAT getInterpolant 0.06
BRUNCH_STAT pushClauses 0.10
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.10
BRUNCH_STAT run.loop 3.12
BRUNCH_STAT solveWithCore 0.44
BRUNCH_STAT solveWithCore_minSuffix 0.20
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 7 core size: 6
UNSAT from BMC at frame: 6
itp             : pi =   610  po =     7  and =     710  lev = 301
itp             : pi =   610  po =     7  and =     379  lev =   9
FINDING NEEDED CONSTRAINTS: CoNum: 7 EquivNum: 7
..... Done
Building PDR trace
8: 0 3 7 7 3 8 1 4 
8: 0 3 7 7 3 1 1 4 
8: 0 3 7 7 3 2 1 4 
8: 0 3 7 7 3 2 3 4 
9: 0 3 7 7 3 2 3 1 4 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 6
BRUNCH_STAT Frame 7
BRUNCH_STAT OrigItp 710
BRUNCH_STAT SimpItp 379
BRUNCH_STAT Aig_ManSimplifyComb 0.11
BRUNCH_STAT Glucose_solve 0.43
BRUNCH_STAT Pdr_solve 2.39
BRUNCH_STAT addCoverCubes 0.45
BRUNCH_STAT blockCube 2.35
BRUNCH_STAT computeNextTr 0.00
BRUNCH_STAT doBmc 0.67
BRUNCH_STAT doPdrTrace 3.35
BRUNCH_STAT doPdrTrace.last 0.82
BRUNCH_STAT doPdrTrace_part1 0.08
BRUNCH_STAT doPdrTrace_part2 0.62
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.49
BRUNCH_STAT findItpConstraints 0.01
BRUNCH_STAT generalize 2.35
BRUNCH_STAT getCnfTr 0.13
BRUNCH_STAT getInterpolant 0.10
BRUNCH_STAT pushClauses 0.16
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.16
BRUNCH_STAT run.loop 4.24
BRUNCH_STAT solveWithCore 0.67
BRUNCH_STAT solveWithCore_minSuffix 0.35
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 8 core size: 6
UNSAT from BMC at frame: 7
itp             : pi =   610  po =     8  and =     620  lev = 294
itp             : pi =   610  po =     8  and =     394  lev =   9
FINDING NEEDED CONSTRAINTS: CoNum: 8 EquivNum: 8
..... Done
Building PDR trace
0
b0
.
9: 0 3 7 7 0 0 0 0 10 
Verification of invariant with 10 clauses was successful.

************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 7
BRUNCH_STAT Frame 8
BRUNCH_STAT Invar 10
BRUNCH_STAT OrigItp 620
BRUNCH_STAT SimpItp 394
BRUNCH_STAT Aig_ManSimplifyComb 0.13
BRUNCH_STAT Glucose_solve 0.80
BRUNCH_STAT Pdr_solve 2.46
BRUNCH_STAT addCoverCubes 0.47
BRUNCH_STAT blockCube 2.42
BRUNCH_STAT computeNextTr 0.00
BRUNCH_STAT doBmc 1.08
BRUNCH_STAT doPdrTrace 3.47
BRUNCH_STAT doPdrTrace.last 0.12
BRUNCH_STAT doPdrTrace_part1 0.08
BRUNCH_STAT doPdrTrace_part2 0.65
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.51
BRUNCH_STAT findItpConstraints 0.02
BRUNCH_STAT generalize 2.42
BRUNCH_STAT getCnfTr 0.15
BRUNCH_STAT getInterpolant 0.14
BRUNCH_STAT pushClauses 0.17
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.17
BRUNCH_STAT run.loop 4.87
BRUNCH_STAT solveWithCore 1.08
BRUNCH_STAT solveWithCore_minSuffix 0.69
BRUNCH_STAT solverAddClause 0.00
BRUNCH_STAT Result UNSAT
************** BRUNCH STATS END ***************** 
[pavy] Witness begin
0
b0
.
[pavy] Witness end
WINNER:  navy
BRUNCH_STAT config 0
BRUNCH_STAT config_name navy
BRUNCH_STAT Result UNSAT
[launch.sh] stop:  Sun Sep 20 07:40:21 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 07:40:24 CEST 2015
[launch.sh] done: Sun Sep 20 07:40:24 CEST 2015
