[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/all/selection/random/eijks1423.aig
[launch.sh] host:  atom18 (atom18)
[launch.sh] start: Fri Sep 18 22:53:19 CEST 2015
[launch.sh] jobid: 7194501
[launch.sh] name:  eijks1423avy
[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/7194501.1.queue/avy-A4Z4lh
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/all/selection/random/eijks1423.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/all/selection/random/eijks1423.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/all/selection/random/eijks1423.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7194501.1.queue/avy-A4Z4lh/eijks1423.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/all/selection/random/eijks1423.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7194501.1.queue/avy-A4Z4lh/eijks1423.pp.aig".

[pavy] finished pp, output=/tmp/7194501.1.queue/avy-A4Z4lh/eijks1423.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/7194501.1.queue/avy-A4Z4lh/navy_avy0.cex /tmp/7194501.1.queue/avy-A4Z4lh/eijks1423.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7194501.1.queue/avy-A4Z4lh/abcpdr_avy1.cex /tmp/7194501.1.queue/avy-A4Z4lh/eijks1423.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/7194501.1.queue/avy-A4Z4lh/avyabsmus_avy2.cex /tmp/7194501.1.queue/avy-A4Z4lh/eijks1423.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7194501.1.queue/avy-A4Z4lh/fib_avy3.cex /tmp/7194501.1.queue/avy-A4Z4lh/eijks1423.pp.aig
[pavy] running: [2062, 2063, 2064, 2065]
[pavy] finished pid 2062 with code 0 and signal 0
[pavy] trying to kill  2063
[pavy] waiting for  2063
[pavy] trying to kill  2064
[pavy] waiting for  2064
[pavy] trying to kill  2065
[pavy] waiting for  2065
AVY PARAMETERS
	fName = /tmp/7194501.1.queue/avy-A4Z4lh/eijks1423.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/7194501.1.queue/avy-A4Z4lh/eijks1423.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 =   147  po =     1  and =      52  lev =  31
itp             : pi =   147  po =     1  and =      23  lev =   6
FINDING NEEDED CONSTRAINTS: CoNum: 1 EquivNum: 1
. Done
Building PDR trace
3: 0 18 1 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 0
BRUNCH_STAT Frame 1
BRUNCH_STAT OrigItp 52
BRUNCH_STAT SimpItp 23
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.00
BRUNCH_STAT doPdrTrace 0.02
BRUNCH_STAT doPdrTrace.last 0.02
BRUNCH_STAT doPdrTrace_part1 0.00
BRUNCH_STAT doPdrTrace_part2 0.01
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.01
BRUNCH_STAT findItpConstraints 0.00
BRUNCH_STAT generalize 0.00
BRUNCH_STAT getCnfTr 0.00
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.00
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.00
BRUNCH_STAT run.loop 0.03
BRUNCH_STAT solveWithCore 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: 2 core size: 3
UNSAT from BMC at frame: 1
itp             : pi =   147  po =     2  and =     214  lev =  73
itp             : pi =   147  po =     2  and =     100  lev =  18
FINDING NEEDED CONSTRAINTS: CoNum: 2 EquivNum: 2
.YESS
.YESS
 Done
Building PDR trace
3: 0 55 79 
4: 0 55 53 38 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 1
BRUNCH_STAT Frame 2
BRUNCH_STAT OrigItp 214
BRUNCH_STAT SimpItp 100
BRUNCH_STAT Aig_ManSimplifyComb 0.01
BRUNCH_STAT Glucose_solve 0.00
BRUNCH_STAT Pdr_solve 0.02
BRUNCH_STAT addCoverCubes 0.01
BRUNCH_STAT blockCube 0.01
BRUNCH_STAT computeNextTr 0.01
BRUNCH_STAT doBmc 0.01
BRUNCH_STAT doPdrTrace 0.08
BRUNCH_STAT doPdrTrace.last 0.06
BRUNCH_STAT doPdrTrace_part1 0.00
BRUNCH_STAT doPdrTrace_part2 0.04
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.01
BRUNCH_STAT findItpConstraints 0.00
BRUNCH_STAT generalize 0.01
BRUNCH_STAT getCnfTr 0.00
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT pushClauses 0.02
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.01
BRUNCH_STAT run.loop 0.11
BRUNCH_STAT solveWithCore 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: 3 core size: 4
UNSAT from BMC at frame: 2
itp             : pi =   147  po =     3  and =     373  lev =  33
itp             : pi =   147  po =     3  and =     236  lev =  14
FINDING NEEDED CONSTRAINTS: CoNum: 3 EquivNum: 3
.YESS
.YESS
.YESS
 Done
Building PDR trace
4: 0 60 73 54 
4: 0 60 120 87 
5: 0 60 120 68 39 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 2
BRUNCH_STAT Frame 3
BRUNCH_STAT OrigItp 373
BRUNCH_STAT SimpItp 236
BRUNCH_STAT Aig_ManSimplifyComb 0.03
BRUNCH_STAT Glucose_solve 0.01
BRUNCH_STAT Pdr_solve 0.06
BRUNCH_STAT addCoverCubes 0.02
BRUNCH_STAT blockCube 0.03
BRUNCH_STAT computeNextTr 0.01
BRUNCH_STAT doBmc 0.02
BRUNCH_STAT doPdrTrace 0.20
BRUNCH_STAT doPdrTrace.last 0.12
BRUNCH_STAT doPdrTrace_part1 0.00
BRUNCH_STAT doPdrTrace_part2 0.07
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.03
BRUNCH_STAT findItpConstraints 0.02
BRUNCH_STAT generalize 0.02
BRUNCH_STAT getCnfTr 0.00
BRUNCH_STAT getInterpolant 0.01
BRUNCH_STAT pushClauses 0.05
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.05
BRUNCH_STAT run.loop 0.27
BRUNCH_STAT solveWithCore 0.02
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 =   147  po =     4  and =     962  lev =  68
itp             : pi =   147  po =     4  and =     534  lev =  18
FINDING NEEDED CONSTRAINTS: CoNum: 4 EquivNum: 4
.YESS
.YESS
.YESS
.YESS
 Done
Building PDR trace
5: 0 56 110 64 51 
5: 0 56 135 89 61 
5: 0 56 135 162 94 
6: 0 56 135 162 58 52 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 3
BRUNCH_STAT Frame 4
BRUNCH_STAT OrigItp 962
BRUNCH_STAT SimpItp 534
BRUNCH_STAT Aig_ManSimplifyComb 0.07
BRUNCH_STAT Glucose_solve 0.03
BRUNCH_STAT Pdr_solve 0.15
BRUNCH_STAT addCoverCubes 0.04
BRUNCH_STAT blockCube 0.09
BRUNCH_STAT computeNextTr 0.02
BRUNCH_STAT doBmc 0.03
BRUNCH_STAT doPdrTrace 0.45
BRUNCH_STAT doPdrTrace.last 0.25
BRUNCH_STAT doPdrTrace_part1 0.01
BRUNCH_STAT doPdrTrace_part2 0.12
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.05
BRUNCH_STAT findItpConstraints 0.04
BRUNCH_STAT generalize 0.08
BRUNCH_STAT getCnfTr 0.00
BRUNCH_STAT getInterpolant 0.02
BRUNCH_STAT pushClauses 0.14
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.13
BRUNCH_STAT run.loop 0.60
BRUNCH_STAT solveWithCore 0.03
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.01
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 =   147  po =     5  and =    3332  lev = 157
itp             : pi =   147  po =     5  and =    1838  lev =  51
FINDING NEEDED CONSTRAINTS: CoNum: 5 EquivNum: 5
..YESS
.YESS
.YESS
.YESS
 Done
Building PDR trace
6: 0 56 145 162 55 60 
6: 0 56 142 161 55 60 
6: 0 56 142 186 80 63 
6: 0 56 142 186 131 98 
7: 0 56 142 186 131 57 49 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 4
BRUNCH_STAT Frame 5
BRUNCH_STAT OrigItp 3332
BRUNCH_STAT SimpItp 1838
BRUNCH_STAT Aig_ManSimplifyComb 0.20
BRUNCH_STAT Glucose_solve 0.09
BRUNCH_STAT Pdr_solve 0.30
BRUNCH_STAT addCoverCubes 0.08
BRUNCH_STAT blockCube 0.18
BRUNCH_STAT computeNextTr 0.02
BRUNCH_STAT doBmc 0.06
BRUNCH_STAT doPdrTrace 0.85
BRUNCH_STAT doPdrTrace.last 0.40
BRUNCH_STAT doPdrTrace_part1 0.01
BRUNCH_STAT doPdrTrace_part2 0.20
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.08
BRUNCH_STAT findItpConstraints 0.12
BRUNCH_STAT generalize 0.16
BRUNCH_STAT getCnfTr 0.00
BRUNCH_STAT getInterpolant 0.06
BRUNCH_STAT pushClauses 0.29
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.28
BRUNCH_STAT run.loop 1.30
BRUNCH_STAT solveWithCore 0.06
BRUNCH_STAT solveWithCore_minSuffix 0.00
BRUNCH_STAT solverAddClause 0.01
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 6 core size: 7
UNSAT from BMC at frame: 5
itp             : pi =   147  po =     6  and =    8332  lev = 490
itp             : pi =   147  po =     6  and =    4408  lev = 115
FINDING NEEDED CONSTRAINTS: CoNum: 6 EquivNum: 6
..YESS
.YESS
.YESS
.YESS
.YESS
 Done
Building PDR trace
7: 0 60 155 193 133 58 52 
7: 0 60 154 198 139 58 53 
7: 0 60 154 214 146 61 57 
7: 0 60 154 214 250 88 94 
7: 0 60 154 214 250 194 111 
8: 0 60 154 214 250 194 68 62 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 5
BRUNCH_STAT Frame 6
BRUNCH_STAT OrigItp 8332
BRUNCH_STAT SimpItp 4408
BRUNCH_STAT Aig_ManSimplifyComb 0.53
BRUNCH_STAT Glucose_solve 0.32
BRUNCH_STAT Pdr_solve 0.90
BRUNCH_STAT addCoverCubes 0.14
BRUNCH_STAT blockCube 0.49
BRUNCH_STAT computeNextTr 0.03
BRUNCH_STAT doBmc 0.12
BRUNCH_STAT doPdrTrace 1.89
BRUNCH_STAT doPdrTrace.last 1.04
BRUNCH_STAT doPdrTrace_part1 0.02
BRUNCH_STAT doPdrTrace_part2 0.30
BRUNCH_STAT doStrengthenVC 0.00
BRUNCH_STAT ensureFrames 0.13
BRUNCH_STAT findItpConstraints 0.41
BRUNCH_STAT generalize 0.43
BRUNCH_STAT getCnfTr 0.00
BRUNCH_STAT getInterpolant 0.22
BRUNCH_STAT pushClauses 0.59
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.57
BRUNCH_STAT run.loop 3.17
BRUNCH_STAT solveWithCore 0.12
BRUNCH_STAT solveWithCore_minSuffix 0.01
BRUNCH_STAT solverAddClause 0.03
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 7 core size: 8
UNSAT from BMC at frame: 6
itp             : pi =   147  po =     7  and =    8971  lev = 337
itp             : pi =   147  po =     7  and =    4749  lev =  93
FINDING NEEDED CONSTRAINTS: CoNum: 7 EquivNum: 7
..YESS
.YESS
.YESS
.YESS
.YESS
. Done
Building PDR trace
8: 0 60 149 232 255 184 76 64 
8: 0 60 149 240 260 184 76 65 
8: 0 60 149 240 293 175 94 86 
8: 0 60 149 240 293 204 162 99 
8: 0 60 149 240 293 204 173 146 
9: 0 60 149 240 293 204 173 61 90 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 6
BRUNCH_STAT Frame 7
BRUNCH_STAT OrigItp 8971
BRUNCH_STAT SimpItp 4749
BRUNCH_STAT Aig_ManSimplifyComb 0.90
BRUNCH_STAT Glucose_solve 0.65
BRUNCH_STAT Pdr_solve 1.35
BRUNCH_STAT addCoverCubes 0.22
BRUNCH_STAT blockCube 0.72
BRUNCH_STAT computeNextTr 0.03
BRUNCH_STAT doBmc 0.20
BRUNCH_STAT doPdrTrace 2.92
BRUNCH_STAT doPdrTrace.last 1.03
BRUNCH_STAT doPdrTrace_part1 0.04
BRUNCH_STAT doPdrTrace_part2 0.42
BRUNCH_STAT doStrengthenVC 0.01
BRUNCH_STAT ensureFrames 0.19
BRUNCH_STAT findItpConstraints 0.79
BRUNCH_STAT generalize 0.63
BRUNCH_STAT getCnfTr 0.01
BRUNCH_STAT getInterpolant 0.46
BRUNCH_STAT pushClauses 1.01
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 0.97
BRUNCH_STAT run.loop 5.28
BRUNCH_STAT solveWithCore 0.20
BRUNCH_STAT solveWithCore_minSuffix 0.02
BRUNCH_STAT solverAddClause 0.05
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 8 core size: 8
UNSAT from BMC at frame: 7
itp             : pi =   147  po =     8  and =    5399  lev = 209
itp             : pi =   147  po =     8  and =    2977  lev =  38
FINDING NEEDED CONSTRAINTS: CoNum: 8 EquivNum: 8
...YESS
.YESS
.... Done
Building PDR trace
9: 0 60 149 240 295 206 172 61 91 
9: 0 60 149 240 295 220 179 61 92 
9: 0 60 149 240 295 220 172 79 155 
9: 0 60 149 240 295 220 172 93 169 
10: 0 60 149 240 295 220 172 93 63 120 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 7
BRUNCH_STAT Frame 8
BRUNCH_STAT OrigItp 5399
BRUNCH_STAT SimpItp 2977
BRUNCH_STAT Aig_ManSimplifyComb 1.11
BRUNCH_STAT Glucose_solve 0.86
BRUNCH_STAT Pdr_solve 1.61
BRUNCH_STAT addCoverCubes 0.28
BRUNCH_STAT blockCube 0.85
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 0.29
BRUNCH_STAT doPdrTrace 3.61
BRUNCH_STAT doPdrTrace.last 0.69
BRUNCH_STAT doPdrTrace_part1 0.05
BRUNCH_STAT doPdrTrace_part2 0.51
BRUNCH_STAT doStrengthenVC 0.01
BRUNCH_STAT ensureFrames 0.24
BRUNCH_STAT findItpConstraints 1.00
BRUNCH_STAT generalize 0.75
BRUNCH_STAT getCnfTr 0.01
BRUNCH_STAT getInterpolant 0.66
BRUNCH_STAT pushClauses 1.31
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 1.26
BRUNCH_STAT run.loop 6.68
BRUNCH_STAT solveWithCore 0.29
BRUNCH_STAT solveWithCore_minSuffix 0.03
BRUNCH_STAT solverAddClause 0.06
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 9 core size: 7
UNSAT from BMC at frame: 8
itp             : pi =   147  po =     9  and =    4054  lev = 329
itp             : pi =   147  po =     9  and =    2057  lev =  89
FINDING NEEDED CONSTRAINTS: CoNum: 9 EquivNum: 9
......... Done
Building PDR trace
10: 0 60 149 240 295 219 174 94 63 120 
10: 0 60 149 240 295 219 181 91 68 121 
10: 0 60 149 240 295 219 181 89 92 133 
10: 0 60 149 240 295 219 181 89 82 175 
11: 0 60 149 240 295 219 181 89 82 49 133 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 8
BRUNCH_STAT Frame 9
BRUNCH_STAT OrigItp 4054
BRUNCH_STAT SimpItp 2057
BRUNCH_STAT Aig_ManSimplifyComb 1.25
BRUNCH_STAT Glucose_solve 1.01
BRUNCH_STAT Pdr_solve 1.72
BRUNCH_STAT addCoverCubes 0.34
BRUNCH_STAT blockCube 0.91
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 0.37
BRUNCH_STAT doPdrTrace 4.14
BRUNCH_STAT doPdrTrace.last 0.53
BRUNCH_STAT doPdrTrace_part1 0.06
BRUNCH_STAT doPdrTrace_part2 0.60
BRUNCH_STAT doStrengthenVC 0.01
BRUNCH_STAT ensureFrames 0.28
BRUNCH_STAT findItpConstraints 1.13
BRUNCH_STAT generalize 0.81
BRUNCH_STAT getCnfTr 0.01
BRUNCH_STAT getInterpolant 0.73
BRUNCH_STAT pushClauses 1.61
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 1.55
BRUNCH_STAT run.loop 7.63
BRUNCH_STAT solveWithCore 0.37
BRUNCH_STAT solveWithCore_minSuffix 0.04
BRUNCH_STAT solverAddClause 0.08
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 10 core size: 8
UNSAT from BMC at frame: 9
itp             : pi =   147  po =    10  and =    5318  lev = 388
itp             : pi =   147  po =    10  and =    2530  lev = 127
FINDING NEEDED CONSTRAINTS: CoNum: 10 EquivNum: 10
.......... Done
Building PDR trace
11: 0 60 149 240 298 231 182 90 83 49 133 
11: 0 60 149 240 298 234 185 90 83 49 133 
11: 0 60 149 240 298 234 191 90 83 49 133 
11: 0 60 149 240 298 234 191 94 74 60 133 
11: 0 60 149 240 298 234 191 94 50 82 157 
11: 0 60 149 240 298 234 191 94 50 80 184 
12: 0 60 149 240 298 234 191 94 50 80 56 136 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 9
BRUNCH_STAT Frame 10
BRUNCH_STAT OrigItp 5318
BRUNCH_STAT SimpItp 2530
BRUNCH_STAT Aig_ManSimplifyComb 1.46
BRUNCH_STAT Glucose_solve 1.16
BRUNCH_STAT Pdr_solve 1.84
BRUNCH_STAT addCoverCubes 0.42
BRUNCH_STAT blockCube 0.97
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 0.48
BRUNCH_STAT doPdrTrace 4.94
BRUNCH_STAT doPdrTrace.last 0.80
BRUNCH_STAT doPdrTrace_part1 0.07
BRUNCH_STAT doPdrTrace_part2 0.73
BRUNCH_STAT doStrengthenVC 0.01
BRUNCH_STAT ensureFrames 0.35
BRUNCH_STAT findItpConstraints 1.24
BRUNCH_STAT generalize 0.86
BRUNCH_STAT getCnfTr 0.01
BRUNCH_STAT getInterpolant 0.83
BRUNCH_STAT pushClauses 2.11
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 2.02
BRUNCH_STAT run.loop 8.97
BRUNCH_STAT solveWithCore 0.48
BRUNCH_STAT solveWithCore_minSuffix 0.06
BRUNCH_STAT solverAddClause 0.10
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 11 core size: 9
UNSAT from BMC at frame: 10
itp             : pi =   147  po =    11  and =    9348  lev = 378
itp             : pi =   147  po =    11  and =    4122  lev = 116
FINDING NEEDED CONSTRAINTS: CoNum: 11 EquivNum: 11
......YESS
.YESS
.... Done
Building PDR trace
12: 0 60 149 240 298 236 192 94 50 80 56 136 
12: 0 60 149 240 298 235 190 92 48 79 57 140 
12: 0 60 149 240 298 235 195 93 48 79 57 140 
12: 0 60 149 240 298 235 195 104 51 81 57 140 
12: 0 60 149 240 298 235 195 104 74 56 78 151 
12: 0 60 149 240 298 235 195 104 74 57 84 171 
12: 0 60 149 240 298 235 195 104 74 57 85 185 
13: 0 60 149 240 298 235 195 104 74 57 85 54 136 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 10
BRUNCH_STAT Frame 11
BRUNCH_STAT OrigItp 9348
BRUNCH_STAT SimpItp 4122
BRUNCH_STAT Aig_ManSimplifyComb 1.81
BRUNCH_STAT Glucose_solve 1.35
BRUNCH_STAT Pdr_solve 2.00
BRUNCH_STAT addCoverCubes 0.54
BRUNCH_STAT blockCube 1.05
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 0.64
BRUNCH_STAT doPdrTrace 5.90
BRUNCH_STAT doPdrTrace.last 0.96
BRUNCH_STAT doPdrTrace_part1 0.09
BRUNCH_STAT doPdrTrace_part2 0.88
BRUNCH_STAT doStrengthenVC 0.02
BRUNCH_STAT ensureFrames 0.43
BRUNCH_STAT findItpConstraints 1.41
BRUNCH_STAT generalize 0.93
BRUNCH_STAT getCnfTr 0.01
BRUNCH_STAT getInterpolant 1.00
BRUNCH_STAT pushClauses 2.68
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 2.58
BRUNCH_STAT run.loop 10.77
BRUNCH_STAT solveWithCore 0.64
BRUNCH_STAT solveWithCore_minSuffix 0.09
BRUNCH_STAT solverAddClause 0.14
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 12 core size: 11
UNSAT from BMC at frame: 11
itp             : pi =   147  po =    12  and =    7567  lev = 327
itp             : pi =   147  po =    12  and =    3416  lev =  96
FINDING NEEDED CONSTRAINTS: CoNum: 12 EquivNum: 12
............ Done
Building PDR trace
13: 0 60 149 234 317 234 195 104 74 57 85 54 136 
13: 0 60 149 234 324 235 195 104 74 57 85 54 136 
13: 0 60 149 234 324 247 194 104 74 57 85 54 136 
13: 0 60 149 234 324 247 203 103 73 54 79 53 145 
13: 0 60 149 234 324 247 203 112 74 56 80 53 145 
13: 0 60 149 234 324 247 203 112 83 56 80 53 145 
13: 0 60 149 234 324 247 203 112 83 64 76 57 146 
13: 0 60 149 234 324 247 203 112 83 64 49 58 183 
13: 0 60 149 234 324 247 203 112 83 64 49 45 209 
14: 0 60 149 234 324 247 203 112 83 64 49 45 62 153 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 11
BRUNCH_STAT Frame 12
BRUNCH_STAT OrigItp 7567
BRUNCH_STAT SimpItp 3416
BRUNCH_STAT Aig_ManSimplifyComb 2.07
BRUNCH_STAT Glucose_solve 1.53
BRUNCH_STAT Pdr_solve 2.16
BRUNCH_STAT addCoverCubes 0.67
BRUNCH_STAT blockCube 1.12
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 0.82
BRUNCH_STAT doPdrTrace 7.24
BRUNCH_STAT doPdrTrace.last 1.34
BRUNCH_STAT doPdrTrace_part1 0.11
BRUNCH_STAT doPdrTrace_part2 1.07
BRUNCH_STAT doStrengthenVC 0.03
BRUNCH_STAT ensureFrames 0.53
BRUNCH_STAT findItpConstraints 1.51
BRUNCH_STAT generalize 1.00
BRUNCH_STAT getCnfTr 0.02
BRUNCH_STAT getInterpolant 1.18
BRUNCH_STAT pushClauses 3.60
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 3.44
BRUNCH_STAT run.loop 12.85
BRUNCH_STAT solveWithCore 0.82
BRUNCH_STAT solveWithCore_minSuffix 0.12
BRUNCH_STAT solverAddClause 0.18
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 13 core size: 10
UNSAT from BMC at frame: 12
itp             : pi =   147  po =    13  and =    2087  lev =  72
itp             : pi =   147  po =    13  and =    1075  lev =  27
FINDING NEEDED CONSTRAINTS: CoNum: 13 EquivNum: 13
............. Done
Building PDR trace
14: 0 60 149 234 324 247 206 111 83 64 49 45 62 153 
14: 0 60 149 234 324 247 206 112 84 64 49 45 62 153 
14: 0 60 149 234 324 247 206 112 88 64 50 45 62 153 
14: 0 60 149 234 324 247 206 112 88 64 50 45 62 153 
14: 0 60 149 234 324 247 206 112 88 68 50 45 62 153 
14: 0 60 149 234 324 247 206 112 88 68 51 40 66 153 
14: 0 60 149 234 324 247 206 112 88 68 51 35 88 156 
14: 0 60 149 234 324 247 206 112 88 68 51 35 48 217 
15: 0 60 149 234 324 247 206 112 88 68 51 35 48 66 156 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 12
BRUNCH_STAT Frame 13
BRUNCH_STAT OrigItp 2087
BRUNCH_STAT SimpItp 1075
BRUNCH_STAT Aig_ManSimplifyComb 2.13
BRUNCH_STAT Glucose_solve 1.68
BRUNCH_STAT Pdr_solve 2.23
BRUNCH_STAT addCoverCubes 0.77
BRUNCH_STAT blockCube 1.16
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 0.97
BRUNCH_STAT doPdrTrace 8.20
BRUNCH_STAT doPdrTrace.last 0.95
BRUNCH_STAT doPdrTrace_part1 0.12
BRUNCH_STAT doPdrTrace_part2 1.23
BRUNCH_STAT doStrengthenVC 0.03
BRUNCH_STAT ensureFrames 0.60
BRUNCH_STAT findItpConstraints 1.55
BRUNCH_STAT generalize 1.04
BRUNCH_STAT getCnfTr 0.02
BRUNCH_STAT getInterpolant 1.24
BRUNCH_STAT pushClauses 4.26
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 4.07
BRUNCH_STAT run.loop 14.14
BRUNCH_STAT solveWithCore 0.97
BRUNCH_STAT solveWithCore_minSuffix 0.15
BRUNCH_STAT solverAddClause 0.21
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 14 core size: 10
UNSAT from BMC at frame: 13
itp             : pi =   147  po =    14  and =    2298  lev = 152
itp             : pi =   147  po =    14  and =    1181  lev =  50
FINDING NEEDED CONSTRAINTS: CoNum: 14 EquivNum: 14
.............. Done
Building PDR trace
15: 0 60 149 234 324 247 206 113 86 68 51 35 48 66 156 
15: 0 60 149 234 324 247 206 113 88 69 51 35 48 66 156 
15: 0 60 149 234 324 247 206 113 88 69 52 35 48 66 156 
15: 0 60 149 234 324 247 206 113 88 69 52 35 48 66 156 
15: 0 60 149 234 324 247 206 113 88 69 52 35 48 66 156 
15: 0 60 149 234 324 247 206 113 88 69 52 32 39 75 158 
15: 0 60 149 234 324 247 206 113 88 69 52 32 18 77 181 
15: 0 60 149 234 324 247 206 113 88 69 52 32 18 45 214 
16: 0 60 149 234 324 247 206 113 88 69 52 32 18 45 67 154 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 13
BRUNCH_STAT Frame 14
BRUNCH_STAT OrigItp 2298
BRUNCH_STAT SimpItp 1181
BRUNCH_STAT Aig_ManSimplifyComb 2.20
BRUNCH_STAT Glucose_solve 1.87
BRUNCH_STAT Pdr_solve 2.27
BRUNCH_STAT addCoverCubes 0.87
BRUNCH_STAT blockCube 1.18
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 1.17
BRUNCH_STAT doPdrTrace 9.06
BRUNCH_STAT doPdrTrace.last 0.86
BRUNCH_STAT doPdrTrace_part1 0.13
BRUNCH_STAT doPdrTrace_part2 1.39
BRUNCH_STAT doStrengthenVC 0.04
BRUNCH_STAT ensureFrames 0.67
BRUNCH_STAT findItpConstraints 1.60
BRUNCH_STAT generalize 1.05
BRUNCH_STAT getCnfTr 0.02
BRUNCH_STAT getInterpolant 1.32
BRUNCH_STAT pushClauses 4.88
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 4.66
BRUNCH_STAT run.loop 15.39
BRUNCH_STAT solveWithCore 1.17
BRUNCH_STAT solveWithCore_minSuffix 0.22
BRUNCH_STAT solverAddClause 0.23
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 15 core size: 12
UNSAT from BMC at frame: 14
itp             : pi =   147  po =    15  and =    3077  lev = 228
itp             : pi =   147  po =    15  and =    1479  lev =  69
FINDING NEEDED CONSTRAINTS: CoNum: 15 EquivNum: 15
............... Done
Building PDR trace
16: 0 60 149 234 324 247 207 113 88 69 52 32 18 45 67 154 
16: 0 60 149 234 324 247 207 115 89 69 52 32 18 45 67 154 
16: 0 60 149 234 324 247 207 115 89 70 52 32 18 45 67 154 
16: 0 60 149 234 324 247 207 115 89 72 52 32 18 45 67 154 
16: 0 60 149 234 324 247 207 115 89 72 52 32 18 45 67 154 
16: 0 60 149 234 324 247 207 115 89 72 52 33 18 45 66 156 
16: 0 60 149 234 324 247 207 115 89 72 52 32 16 34 77 158 
16: 0 60 149 234 324 247 207 115 89 72 52 32 16 31 81 158 
16: 0 60 149 234 324 247 207 115 89 72 52 32 16 14 88 172 
16: 0 60 149 234 324 247 207 115 89 72 52 32 16 14 55 213 
17: 0 60 149 234 324 247 207 115 89 72 52 32 16 14 55 62 158 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 14
BRUNCH_STAT Frame 15
BRUNCH_STAT OrigItp 3077
BRUNCH_STAT SimpItp 1479
BRUNCH_STAT Aig_ManSimplifyComb 2.29
BRUNCH_STAT Glucose_solve 2.12
BRUNCH_STAT Pdr_solve 2.33
BRUNCH_STAT addCoverCubes 1.03
BRUNCH_STAT blockCube 1.20
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 1.43
BRUNCH_STAT doPdrTrace 10.30
BRUNCH_STAT doPdrTrace.last 1.24
BRUNCH_STAT doPdrTrace_part1 0.15
BRUNCH_STAT doPdrTrace_part2 1.59
BRUNCH_STAT doStrengthenVC 0.05
BRUNCH_STAT ensureFrames 0.77
BRUNCH_STAT findItpConstraints 1.65
BRUNCH_STAT generalize 1.08
BRUNCH_STAT getCnfTr 0.02
BRUNCH_STAT getInterpolant 1.40
BRUNCH_STAT pushClauses 5.75
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 5.48
BRUNCH_STAT run.loop 17.12
BRUNCH_STAT solveWithCore 1.43
BRUNCH_STAT solveWithCore_minSuffix 0.30
BRUNCH_STAT solverAddClause 0.29
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 16 core size: 15
UNSAT from BMC at frame: 15
itp             : pi =   147  po =    16  and =    3610  lev = 149
itp             : pi =   147  po =    16  and =    1510  lev =  28
FINDING NEEDED CONSTRAINTS: CoNum: 16 EquivNum: 16
................ Done
Building PDR trace
17: 0 60 149 234 337 249 208 115 89 72 52 32 16 14 55 62 158 
17: 0 60 149 234 345 251 208 115 89 72 52 32 16 14 55 62 158 
17: 0 60 149 234 345 266 209 115 89 72 52 32 16 14 55 62 158 
17: 0 60 149 234 345 266 225 115 89 72 52 32 16 15 55 62 158 
17: 0 60 149 234 345 266 225 131 90 72 52 32 16 15 55 62 158 
17: 0 60 149 234 345 266 225 131 98 69 52 31 15 14 53 62 163 
17: 0 60 149 234 345 266 225 131 98 83 50 33 16 14 53 62 163 
17: 0 60 149 234 345 266 225 131 98 83 60 33 18 14 53 62 164 
17: 0 60 149 234 345 266 225 131 98 83 60 49 18 14 53 62 164 
17: 0 60 149 234 345 266 225 131 98 83 60 49 29 13 45 69 166 
17: 0 60 149 234 345 266 225 131 98 83 60 49 29 26 46 69 166 
17: 0 60 149 234 345 266 225 131 98 83 60 49 29 26 40 89 176 
17: 0 60 149 234 345 266 225 131 98 83 60 49 29 26 40 54 229 
18: 0 60 149 234 345 266 225 131 98 83 60 49 29 26 40 54 66 168 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 15
BRUNCH_STAT Frame 16
BRUNCH_STAT OrigItp 3610
BRUNCH_STAT SimpItp 1510
BRUNCH_STAT Aig_ManSimplifyComb 2.39
BRUNCH_STAT Glucose_solve 2.47
BRUNCH_STAT Pdr_solve 2.54
BRUNCH_STAT addCoverCubes 1.24
BRUNCH_STAT blockCube 1.31
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 1.78
BRUNCH_STAT doPdrTrace 12.33
BRUNCH_STAT doPdrTrace.last 2.03
BRUNCH_STAT doPdrTrace_part1 0.17
BRUNCH_STAT doPdrTrace_part2 1.87
BRUNCH_STAT doStrengthenVC 0.06
BRUNCH_STAT ensureFrames 0.91
BRUNCH_STAT findItpConstraints 1.71
BRUNCH_STAT generalize 1.18
BRUNCH_STAT getCnfTr 0.02
BRUNCH_STAT getInterpolant 1.54
BRUNCH_STAT pushClauses 7.16
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 6.80
BRUNCH_STAT run.loop 19.82
BRUNCH_STAT solveWithCore 1.78
BRUNCH_STAT solveWithCore_minSuffix 0.38
BRUNCH_STAT solverAddClause 0.37
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 17 core size: 16
UNSAT from BMC at frame: 16
itp             : pi =   147  po =    17  and =   10534  lev = 316
itp             : pi =   147  po =    17  and =    4838  lev =  84
FINDING NEEDED CONSTRAINTS: CoNum: 17 EquivNum: 17
............YESS
.YESS
.... Done
Building PDR trace
18: 0 60 149 231 346 268 225 131 98 83 60 49 29 26 40 54 66 168 
18: 0 60 149 231 355 266 225 137 98 83 61 49 29 26 40 54 66 169 
18: 0 60 149 231 355 285 234 137 98 83 61 49 29 26 40 54 66 169 
18: 0 60 149 231 355 285 259 138 98 83 61 49 29 26 40 54 66 169 
18: 0 60 149 231 355 285 259 159 107 83 61 49 29 26 40 54 66 169 
18: 0 60 149 231 355 285 259 159 124 86 61 49 29 26 40 54 66 170 
18: 0 60 149 231 355 285 259 159 124 157 68 49 29 26 40 54 66 171 
18: 0 60 149 231 355 285 259 159 124 157 151 51 29 26 40 54 66 174 
18: 0 60 149 231 355 285 259 159 124 157 151 138 30 27 40 54 66 174 
18: 0 60 149 231 355 285 259 159 124 157 151 138 122 28 40 54 66 174 
18: 0 60 149 231 355 285 259 159 124 157 151 138 122 122 41 54 66 174 
18: 0 60 149 231 355 285 259 159 124 157 151 138 122 122 384 38 81 176 
18: 0 60 149 231 355 285 259 159 124 157 151 138 122 122 384 48 89 185 
18: 0 60 149 231 355 285 259 159 124 157 151 138 122 122 384 48 58 226 
19: 0 60 149 231 355 285 259 159 124 157 151 138 122 122 384 48 58 54 177 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 16
BRUNCH_STAT Frame 17
BRUNCH_STAT OrigItp 10534
BRUNCH_STAT SimpItp 4838
BRUNCH_STAT Aig_ManSimplifyComb 2.76
BRUNCH_STAT Glucose_solve 3.03
BRUNCH_STAT Pdr_solve 4.02
BRUNCH_STAT addCoverCubes 1.49
BRUNCH_STAT blockCube 2.28
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 2.31
BRUNCH_STAT doPdrTrace 16.11
BRUNCH_STAT doPdrTrace.last 3.77
BRUNCH_STAT doPdrTrace_part1 0.21
BRUNCH_STAT doPdrTrace_part2 2.19
BRUNCH_STAT doStrengthenVC 0.07
BRUNCH_STAT ensureFrames 1.08
BRUNCH_STAT findItpConstraints 1.94
BRUNCH_STAT generalize 2.12
BRUNCH_STAT getCnfTr 0.02
BRUNCH_STAT getInterpolant 1.90
BRUNCH_STAT pushClauses 8.98
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 8.51
BRUNCH_STAT run.loop 25.10
BRUNCH_STAT solveWithCore 2.31
BRUNCH_STAT solveWithCore_minSuffix 0.51
BRUNCH_STAT solverAddClause 0.46
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 18 core size: 17
UNSAT from BMC at frame: 17
itp             : pi =   147  po =    18  and =   19405  lev = 348
itp             : pi =   147  po =    18  and =    8684  lev =  84
FINDING NEEDED CONSTRAINTS: CoNum: 18 EquivNum: 18
.............YESS
..YESS
... Done
Building PDR trace
19: 0 60 149 231 367 289 259 159 124 147 151 134 118 121 384 47 58 54 178 
19: 0 60 149 231 372 294 257 159 125 147 151 134 118 121 384 48 58 54 178 
19: 0 60 149 231 372 302 258 157 119 131 122 132 103 106 263 44 58 64 178 
19: 0 60 149 231 372 302 272 156 120 131 122 132 103 106 263 44 58 64 178 
19: 0 60 149 231 372 302 272 170 128 131 122 132 103 106 263 44 58 64 178 
19: 0 60 149 231 372 302 272 170 134 134 118 132 103 106 263 44 58 64 178 
19: 0 60 149 231 372 302 272 170 134 157 129 132 103 106 263 44 58 64 178 
19: 0 60 149 231 372 302 272 170 134 157 146 121 87 97 226 38 58 68 178 
19: 0 60 149 231 372 302 272 170 134 157 146 139 97 97 226 38 58 68 178 
19: 0 60 149 231 372 302 272 170 134 157 146 139 116 101 226 38 58 68 178 
19: 0 60 149 231 372 302 272 170 134 157 146 139 116 117 221 38 58 68 178 
19: 0 60 149 231 372 302 272 170 134 157 146 139 116 117 243 38 58 68 178 
19: 0 60 149 231 372 302 272 170 134 157 146 139 116 117 243 62 56 68 178 
19: 0 60 149 231 372 302 272 170 134 157 146 139 116 117 243 62 45 90 205 
19: 0 60 149 231 372 302 272 170 134 157 146 139 116 117 243 62 45 53 270 
20: 0 60 149 231 372 302 272 170 134 157 146 139 116 117 243 62 45 53 90 184 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 17
BRUNCH_STAT Frame 18
BRUNCH_STAT OrigItp 19405
BRUNCH_STAT SimpItp 8684
BRUNCH_STAT Aig_ManSimplifyComb 3.52
BRUNCH_STAT Glucose_solve 3.71
BRUNCH_STAT Pdr_solve 4.66
BRUNCH_STAT addCoverCubes 1.86
BRUNCH_STAT blockCube 2.63
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 2.87
BRUNCH_STAT doPdrTrace 20.20
BRUNCH_STAT doPdrTrace.last 4.09
BRUNCH_STAT doPdrTrace_part1 0.28
BRUNCH_STAT doPdrTrace_part2 2.62
BRUNCH_STAT doStrengthenVC 0.09
BRUNCH_STAT ensureFrames 1.33
BRUNCH_STAT findItpConstraints 2.42
BRUNCH_STAT generalize 2.44
BRUNCH_STAT getCnfTr 0.03
BRUNCH_STAT getInterpolant 2.67
BRUNCH_STAT pushClauses 11.77
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 11.11
BRUNCH_STAT run.loop 31.77
BRUNCH_STAT solveWithCore 2.87
BRUNCH_STAT solveWithCore_minSuffix 0.64
BRUNCH_STAT solverAddClause 0.58
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 19 core size: 11
UNSAT from BMC at frame: 18
itp             : pi =   147  po =    19  and =    2817  lev = 188
itp             : pi =   147  po =    19  and =    1356  lev =  50
FINDING NEEDED CONSTRAINTS: CoNum: 19 EquivNum: 19
.......... Done
Building PDR trace
20: 0 60 149 231 365 301 272 170 134 157 146 157 111 117 242 62 47 53 90 184 
20: 0 60 149 231 365 301 272 170 134 157 146 157 121 117 242 62 47 53 90 184 
20: 0 60 149 231 365 301 272 170 134 157 146 157 121 118 242 62 47 53 90 184 
20: 0 60 149 231 365 301 272 170 134 157 146 157 121 118 235 62 47 53 90 184 
20: 0 60 149 231 365 301 272 170 134 157 146 157 121 118 235 62 46 53 90 184 
20: 0 60 149 231 365 301 272 170 134 157 146 157 121 118 235 62 48 53 90 184 
20: 0 60 149 231 365 301 272 170 134 157 146 157 121 118 235 62 48 53 90 184 
20: 0 60 149 231 365 301 272 170 134 157 146 157 121 118 235 62 48 32 67 233 
20: 0 60 149 231 365 301 272 170 134 157 146 157 121 118 235 62 48 32 29 273 
21: 0 60 149 231 365 301 272 170 134 157 146 157 121 118 235 62 48 32 29 91 186 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 18
BRUNCH_STAT Frame 19
BRUNCH_STAT OrigItp 2817
BRUNCH_STAT SimpItp 1356
BRUNCH_STAT Aig_ManSimplifyComb 3.62
BRUNCH_STAT Glucose_solve 4.13
BRUNCH_STAT Pdr_solve 4.71
BRUNCH_STAT addCoverCubes 2.00
BRUNCH_STAT blockCube 2.65
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 3.30
BRUNCH_STAT doPdrTrace 21.56
BRUNCH_STAT doPdrTrace.last 1.36
BRUNCH_STAT doPdrTrace_part1 0.30
BRUNCH_STAT doPdrTrace_part2 2.82
BRUNCH_STAT doStrengthenVC 0.10
BRUNCH_STAT ensureFrames 1.44
BRUNCH_STAT findItpConstraints 2.44
BRUNCH_STAT generalize 2.46
BRUNCH_STAT getCnfTr 0.03
BRUNCH_STAT getInterpolant 2.77
BRUNCH_STAT pushClauses 12.80
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 12.08
BRUNCH_STAT run.loop 33.79
BRUNCH_STAT solveWithCore 3.30
BRUNCH_STAT solveWithCore_minSuffix 0.78
BRUNCH_STAT solverAddClause 0.63
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 20 core size: 14
UNSAT from BMC at frame: 19
itp             : pi =   147  po =    20  and =    3463  lev = 216
itp             : pi =   147  po =    20  and =    1411  lev =  62
FINDING NEEDED CONSTRAINTS: CoNum: 20 EquivNum: 20
.................... Done
Building PDR trace
21: 0 60 149 231 365 301 272 170 134 157 148 157 119 118 235 62 48 32 29 91 186 
21: 0 60 149 231 365 301 272 170 134 156 153 157 119 118 235 62 48 32 29 91 186 
21: 0 60 149 231 365 301 272 170 134 156 153 158 119 118 235 62 48 32 29 91 186 
21: 0 60 149 231 365 301 272 170 134 156 153 158 121 118 235 62 48 32 29 91 186 
21: 0 60 149 231 365 301 272 170 134 156 153 158 121 111 235 62 48 32 29 91 186 
21: 0 60 149 231 365 301 272 170 134 156 153 158 121 111 228 62 48 32 29 91 186 
21: 0 60 149 231 365 301 272 170 134 156 153 158 121 111 228 63 48 32 29 91 186 
21: 0 60 149 231 365 301 272 170 134 156 153 158 121 111 228 63 49 32 29 91 186 
21: 0 60 149 231 365 301 272 170 134 156 153 158 121 111 228 63 49 32 29 91 186 
21: 0 60 149 231 365 301 272 170 134 156 153 158 121 111 228 63 49 32 29 91 186 
21: 0 60 149 231 365 301 272 170 134 156 153 158 121 111 228 63 49 32 12 84 215 
21: 0 60 149 231 365 301 272 170 134 156 153 158 121 111 228 63 49 32 12 33 270 
22: 0 60 149 231 365 301 272 170 134 156 153 158 121 111 228 63 49 32 12 33 91 182 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 19
BRUNCH_STAT Frame 20
BRUNCH_STAT OrigItp 3463
BRUNCH_STAT SimpItp 1411
BRUNCH_STAT Aig_ManSimplifyComb 3.71
BRUNCH_STAT Glucose_solve 4.69
BRUNCH_STAT Pdr_solve 4.77
BRUNCH_STAT addCoverCubes 2.23
BRUNCH_STAT blockCube 2.68
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 3.87
BRUNCH_STAT doPdrTrace 23.71
BRUNCH_STAT doPdrTrace.last 2.15
BRUNCH_STAT doPdrTrace_part1 0.32
BRUNCH_STAT doPdrTrace_part2 3.09
BRUNCH_STAT doStrengthenVC 0.12
BRUNCH_STAT ensureFrames 1.58
BRUNCH_STAT findItpConstraints 2.50
BRUNCH_STAT generalize 2.48
BRUNCH_STAT getCnfTr 0.03
BRUNCH_STAT getInterpolant 2.88
BRUNCH_STAT pushClauses 14.48
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 13.65
BRUNCH_STAT run.loop 36.80
BRUNCH_STAT solveWithCore 3.87
BRUNCH_STAT solveWithCore_minSuffix 0.96
BRUNCH_STAT solverAddClause 0.72
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 21 core size: 16
UNSAT from BMC at frame: 20
itp             : pi =   147  po =    21  and =    4053  lev = 206
itp             : pi =   147  po =    21  and =    1836  lev =  56
FINDING NEEDED CONSTRAINTS: CoNum: 21 EquivNum: 21
..................... Done
Building PDR trace
22: 0 60 149 231 365 301 272 170 139 157 153 158 119 112 229 63 49 32 12 33 91 182 
22: 0 60 149 231 365 301 272 170 139 158 153 158 119 112 229 63 49 32 12 33 91 182 
22: 0 60 149 231 365 301 272 170 139 158 153 158 119 112 229 63 49 32 12 33 91 182 
22: 0 60 149 231 365 301 272 170 139 158 153 159 119 112 229 63 49 32 12 33 91 182 
22: 0 60 149 231 365 301 272 170 139 158 153 159 123 112 229 63 49 32 12 33 91 182 
22: 0 60 149 231 365 301 272 170 139 158 153 159 123 112 229 63 50 32 12 33 91 182 
22: 0 60 149 231 365 301 272 170 139 158 153 159 123 112 229 63 50 32 12 33 91 182 
22: 0 60 149 231 365 301 272 170 139 158 153 159 123 112 229 63 50 32 12 33 91 182 
22: 0 60 149 231 365 301 272 170 139 158 153 159 123 112 229 63 50 32 12 33 91 182 
22: 0 60 149 231 365 301 272 170 139 158 153 159 123 112 229 63 50 32 12 33 91 182 
22: 0 60 149 231 365 301 272 170 139 158 153 159 123 112 229 63 50 32 11 33 92 182 
22: 0 60 149 231 365 301 272 170 139 158 153 159 123 112 229 63 50 32 11 33 92 182 
22: 0 60 149 231 365 301 272 170 139 158 153 159 123 112 229 63 50 32 11 11 36 265 
22: 0 60 149 231 365 301 272 170 139 158 153 159 123 112 229 63 50 32 11 11 31 279 
23: 0 60 149 231 365 301 272 170 139 158 153 159 123 112 229 63 50 32 11 11 31 95 188 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 20
BRUNCH_STAT Frame 21
BRUNCH_STAT OrigItp 4053
BRUNCH_STAT SimpItp 1836
BRUNCH_STAT Aig_ManSimplifyComb 3.82
BRUNCH_STAT Glucose_solve 5.48
BRUNCH_STAT Pdr_solve 4.85
BRUNCH_STAT addCoverCubes 2.52
BRUNCH_STAT blockCube 2.72
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 4.67
BRUNCH_STAT doPdrTrace 26.40
BRUNCH_STAT doPdrTrace.last 2.69
BRUNCH_STAT doPdrTrace_part1 0.35
BRUNCH_STAT doPdrTrace_part2 3.41
BRUNCH_STAT doStrengthenVC 0.15
BRUNCH_STAT ensureFrames 1.74
BRUNCH_STAT findItpConstraints 2.58
BRUNCH_STAT generalize 2.52
BRUNCH_STAT getCnfTr 0.03
BRUNCH_STAT getInterpolant 3.06
BRUNCH_STAT pushClauses 16.59
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 15.61
BRUNCH_STAT run.loop 40.68
BRUNCH_STAT solveWithCore 4.67
BRUNCH_STAT solveWithCore_minSuffix 1.17
BRUNCH_STAT solverAddClause 0.83
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 22 core size: 22
UNSAT from BMC at frame: 21
itp             : pi =   147  po =    22  and =   16541  lev = 252
itp             : pi =   147  po =    22  and =    5661  lev =  67
FINDING NEEDED CONSTRAINTS: CoNum: 22 EquivNum: 22
.................YESS
.YESS
.YESS
.YESS
.YESS
. Done
Building PDR trace
23: 0 60 149 275 378 301 272 170 138 158 153 159 120 112 229 63 50 32 11 11 31 95 188 
23: 0 60 149 261 391 309 272 170 138 158 153 160 120 112 229 63 50 32 11 11 31 95 188 
23: 0 60 149 261 403 310 272 170 139 158 153 160 120 112 229 63 50 32 11 11 31 95 188 
23: 0 60 149 261 403 331 274 170 139 158 153 160 120 112 229 63 50 32 11 11 31 95 188 
23: 0 60 149 261 403 331 291 173 138 158 152 157 118 113 229 63 50 32 11 11 31 101 188 
23: 0 60 149 261 403 331 291 193 145 158 152 157 118 113 229 63 51 32 11 11 31 105 188 
23: 0 60 149 261 403 331 291 193 164 158 152 157 118 113 229 63 51 32 11 11 31 105 188 
23: 0 60 149 261 403 331 291 193 164 262 152 157 118 113 229 63 51 32 11 11 31 105 188 
23: 0 60 149 261 403 331 291 193 164 262 259 157 118 113 229 64 51 32 11 11 31 105 188 
23: 0 60 149 261 403 331 291 193 164 262 259 188 121 113 229 64 51 32 12 11 31 105 188 
23: 0 60 149 261 403 331 291 193 164 262 259 188 148 113 229 64 51 32 12 11 31 105 188 
23: 0 60 149 261 403 331 291 193 164 262 259 188 148 140 229 64 51 32 12 11 31 105 188 
23: 0 60 149 261 403 331 291 193 164 262 259 188 148 140 265 64 51 32 12 11 31 105 188 
23: 0 60 149 261 403 331 291 193 164 262 259 188 148 140 265 99 51 32 12 11 31 107 188 
23: 0 60 149 261 403 331 291 193 164 262 259 188 148 140 265 99 69 32 12 11 31 107 188 
23: 0 60 149 261 403 331 291 193 164 262 259 188 148 140 265 99 69 60 12 11 31 107 188 
23: 0 60 149 261 403 331 291 193 164 262 259 188 148 140 265 99 69 60 29 11 31 107 188 
23: 0 60 149 261 403 331 291 193 164 262 259 188 148 140 265 99 69 60 29 20 30 108 188 
23: 0 60 149 261 403 331 291 193 164 262 259 188 148 140 265 99 69 60 29 20 16 76 242 
23: 0 60 149 261 403 331 291 193 164 262 259 188 148 140 265 99 69 60 29 20 16 41 281 
24: 0 60 149 261 403 331 291 193 164 262 259 188 148 140 265 99 69 60 29 20 16 41 111 172 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 21
BRUNCH_STAT Frame 22
BRUNCH_STAT OrigItp 16541
BRUNCH_STAT SimpItp 5661
BRUNCH_STAT Aig_ManSimplifyComb 4.31
BRUNCH_STAT Glucose_solve 7.25
BRUNCH_STAT Pdr_solve 6.16
BRUNCH_STAT addCoverCubes 2.99
BRUNCH_STAT blockCube 3.49
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 6.43
BRUNCH_STAT doPdrTrace 32.85
BRUNCH_STAT doPdrTrace.last 6.46
BRUNCH_STAT doPdrTrace_part1 0.42
BRUNCH_STAT doPdrTrace_part2 3.97
BRUNCH_STAT doStrengthenVC 0.17
BRUNCH_STAT ensureFrames 2.07
BRUNCH_STAT findItpConstraints 2.88
BRUNCH_STAT generalize 3.23
BRUNCH_STAT getCnfTr 0.03
BRUNCH_STAT getInterpolant 3.96
BRUNCH_STAT pushClauses 20.89
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 19.61
BRUNCH_STAT run.loop 50.61
BRUNCH_STAT solveWithCore 6.43
BRUNCH_STAT solveWithCore_minSuffix 1.39
BRUNCH_STAT solverAddClause 1.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 23 core size: 10
UNSAT from BMC at frame: 22
itp             : pi =   147  po =    23  and =    2843  lev = 134
itp             : pi =   147  po =    23  and =    1406  lev =  36
FINDING NEEDED CONSTRAINTS: CoNum: 23 EquivNum: 23
......... Done
Building PDR trace
24: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 99 70 60 29 20 16 41 111 172 
24: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 99 70 61 29 20 16 41 111 172 
24: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 99 70 60 30 20 16 41 111 172 
24: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 99 70 60 30 20 16 41 111 172 
24: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 99 70 60 30 20 16 41 111 172 
24: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 99 70 60 30 20 16 41 111 172 
24: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 99 70 60 30 20 16 16 43 270 
24: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 99 70 60 30 20 16 16 43 271 
25: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 99 70 60 30 20 16 16 43 101 183 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 22
BRUNCH_STAT Frame 23
BRUNCH_STAT OrigItp 2843
BRUNCH_STAT SimpItp 1406
BRUNCH_STAT Aig_ManSimplifyComb 4.40
BRUNCH_STAT Glucose_solve 7.79
BRUNCH_STAT Pdr_solve 6.20
BRUNCH_STAT addCoverCubes 3.11
BRUNCH_STAT blockCube 3.50
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 6.99
BRUNCH_STAT doPdrTrace 33.98
BRUNCH_STAT doPdrTrace.last 1.13
BRUNCH_STAT doPdrTrace_part1 0.44
BRUNCH_STAT doPdrTrace_part2 4.12
BRUNCH_STAT doStrengthenVC 0.20
BRUNCH_STAT ensureFrames 2.14
BRUNCH_STAT findItpConstraints 2.90
BRUNCH_STAT generalize 3.24
BRUNCH_STAT getCnfTr 0.03
BRUNCH_STAT getInterpolant 4.10
BRUNCH_STAT pushClauses 21.74
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 20.41
BRUNCH_STAT run.loop 52.58
BRUNCH_STAT solveWithCore 6.99
BRUNCH_STAT solveWithCore_minSuffix 1.75
BRUNCH_STAT solverAddClause 1.05
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 24 core size: 12
UNSAT from BMC at frame: 23
itp             : pi =   147  po =    24  and =    2779  lev = 109
itp             : pi =   147  po =    24  and =    1183  lev =  42
FINDING NEEDED CONSTRAINTS: CoNum: 24 EquivNum: 24
........... Done
Building PDR trace
25: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 70 60 30 20 16 16 43 101 183 
25: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 60 30 20 16 16 43 101 183 
25: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 16 43 101 183 
25: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 16 43 101 183 
25: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 16 43 101 183 
25: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 16 43 101 183 
25: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 43 101 183 
25: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 43 101 183 
25: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 18 12 305 
25: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 18 12 305 
26: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 18 12 4 303 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 23
BRUNCH_STAT Frame 24
BRUNCH_STAT OrigItp 2779
BRUNCH_STAT SimpItp 1183
BRUNCH_STAT Aig_ManSimplifyComb 4.48
BRUNCH_STAT Glucose_solve 8.35
BRUNCH_STAT Pdr_solve 6.24
BRUNCH_STAT addCoverCubes 3.26
BRUNCH_STAT blockCube 3.52
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 7.57
BRUNCH_STAT doPdrTrace 35.40
BRUNCH_STAT doPdrTrace.last 1.42
BRUNCH_STAT doPdrTrace_part1 0.45
BRUNCH_STAT doPdrTrace_part2 4.32
BRUNCH_STAT doStrengthenVC 0.23
BRUNCH_STAT ensureFrames 2.24
BRUNCH_STAT findItpConstraints 2.92
BRUNCH_STAT generalize 3.26
BRUNCH_STAT getCnfTr 0.04
BRUNCH_STAT getInterpolant 4.24
BRUNCH_STAT pushClauses 22.83
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 21.44
BRUNCH_STAT run.loop 54.84
BRUNCH_STAT solveWithCore 7.57
BRUNCH_STAT solveWithCore_minSuffix 2.01
BRUNCH_STAT solverAddClause 1.10
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 25 core size: 10
UNSAT from BMC at frame: 24
itp             : pi =   147  po =    25  and =      89  lev =  14
itp             : pi =   147  po =    25  and =      41  lev =   6
FINDING NEEDED CONSTRAINTS: CoNum: 25 EquivNum: 25
......... Done
Building PDR trace
26: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 18 12 4 303 
26: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 18 12 4 303 
26: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 18 12 4 303 
26: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 18 12 4 303 
26: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 16 19 12 4 303 
26: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 16 19 12 4 303 
26: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 16 19 12 4 303 
26: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 16 19 12 4 304 
27: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 16 19 12 4 4 302 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 24
BRUNCH_STAT Frame 25
BRUNCH_STAT OrigItp 89
BRUNCH_STAT SimpItp 41
BRUNCH_STAT Aig_ManSimplifyComb 4.49
BRUNCH_STAT Glucose_solve 8.82
BRUNCH_STAT Pdr_solve 6.26
BRUNCH_STAT addCoverCubes 3.36
BRUNCH_STAT blockCube 3.53
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 8.06
BRUNCH_STAT doPdrTrace 36.31
BRUNCH_STAT doPdrTrace.last 0.91
BRUNCH_STAT doPdrTrace_part1 0.46
BRUNCH_STAT doPdrTrace_part2 4.46
BRUNCH_STAT doStrengthenVC 0.25
BRUNCH_STAT ensureFrames 2.30
BRUNCH_STAT findItpConstraints 2.92
BRUNCH_STAT generalize 3.27
BRUNCH_STAT getCnfTr 0.04
BRUNCH_STAT getInterpolant 4.27
BRUNCH_STAT pushClauses 23.52
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 22.08
BRUNCH_STAT run.loop 56.30
BRUNCH_STAT solveWithCore 8.06
BRUNCH_STAT solveWithCore_minSuffix 2.27
BRUNCH_STAT solverAddClause 1.14
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 26 core size: 10
UNSAT from BMC at frame: 25
itp             : pi =   147  po =    26  and =     113  lev =  16
itp             : pi =   147  po =    26  and =      44  lev =   6
FINDING NEEDED CONSTRAINTS: CoNum: 26 EquivNum: 26
......... Done
Building PDR trace
27: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 16 19 12 4 4 302 
27: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 16 19 12 4 4 302 
27: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 19 11 4 4 302 
27: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 19 11 4 4 302 
27: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 18 12 4 4 302 
27: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 18 12 4 4 302 
27: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 18 12 4 4 302 
27: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 18 12 4 4 302 
28: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 16 17 18 12 4 4 2 302 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 25
BRUNCH_STAT Frame 26
BRUNCH_STAT OrigItp 113
BRUNCH_STAT SimpItp 44
BRUNCH_STAT Aig_ManSimplifyComb 4.49
BRUNCH_STAT Glucose_solve 9.25
BRUNCH_STAT Pdr_solve 6.28
BRUNCH_STAT addCoverCubes 3.45
BRUNCH_STAT blockCube 3.54
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 8.50
BRUNCH_STAT doPdrTrace 37.22
BRUNCH_STAT doPdrTrace.last 0.91
BRUNCH_STAT doPdrTrace_part1 0.47
BRUNCH_STAT doPdrTrace_part2 4.60
BRUNCH_STAT doStrengthenVC 0.28
BRUNCH_STAT ensureFrames 2.35
BRUNCH_STAT findItpConstraints 2.92
BRUNCH_STAT generalize 3.28
BRUNCH_STAT getCnfTr 0.04
BRUNCH_STAT getInterpolant 4.30
BRUNCH_STAT pushClauses 24.20
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 22.72
BRUNCH_STAT run.loop 57.72
BRUNCH_STAT solveWithCore 8.50
BRUNCH_STAT solveWithCore_minSuffix 2.54
BRUNCH_STAT solverAddClause 1.19
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 27 core size: 12
UNSAT from BMC at frame: 26
itp             : pi =   147  po =    27  and =      84  lev =  14
itp             : pi =   147  po =    27  and =      52  lev =   6
FINDING NEEDED CONSTRAINTS: CoNum: 27 EquivNum: 27
........... Done
Building PDR trace
28: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 17 18 12 4 4 2 302 
28: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 17 18 12 4 4 2 302 
28: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 17 18 12 4 4 2 302 
28: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 17 18 12 4 4 2 302 
28: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 16 19 13 4 4 2 302 
28: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 16 19 13 4 4 2 302 
28: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 16 19 13 4 4 2 302 
28: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 16 19 13 4 4 2 302 
28: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 16 19 13 4 4 2 302 
28: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 16 19 13 4 4 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 73 61 29 20 17 16 19 13 4 4 2 2 302 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 26
BRUNCH_STAT Frame 27
BRUNCH_STAT OrigItp 84
BRUNCH_STAT SimpItp 52
BRUNCH_STAT Aig_ManSimplifyComb 4.49
BRUNCH_STAT Glucose_solve 9.81
BRUNCH_STAT Pdr_solve 6.30
BRUNCH_STAT addCoverCubes 3.59
BRUNCH_STAT blockCube 3.55
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 9.09
BRUNCH_STAT doPdrTrace 38.44
BRUNCH_STAT doPdrTrace.last 1.22
BRUNCH_STAT doPdrTrace_part1 0.48
BRUNCH_STAT doPdrTrace_part2 4.78
BRUNCH_STAT doStrengthenVC 0.32
BRUNCH_STAT ensureFrames 2.43
BRUNCH_STAT findItpConstraints 2.92
BRUNCH_STAT generalize 3.29
BRUNCH_STAT getCnfTr 0.04
BRUNCH_STAT getInterpolant 4.33
BRUNCH_STAT pushClauses 25.11
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 23.57
BRUNCH_STAT run.loop 59.60
BRUNCH_STAT solveWithCore 9.09
BRUNCH_STAT solveWithCore_minSuffix 2.89
BRUNCH_STAT solverAddClause 1.25
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 28 core size: 16
UNSAT from BMC at frame: 27
itp             : pi =   147  po =    28  and =     165  lev =  15
itp             : pi =   147  po =    28  and =      74  lev =   7
FINDING NEEDED CONSTRAINTS: CoNum: 28 EquivNum: 28
............... Done
Building PDR trace
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 100 74 61 29 20 17 16 19 13 4 4 2 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 75 61 29 20 17 16 19 13 4 4 2 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 19 13 4 4 2 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 19 13 4 4 2 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 19 13 4 4 2 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 19 13 4 4 2 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 19 13 4 4 2 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 19 13 4 4 2 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 18 14 4 4 2 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 18 14 4 4 2 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 18 14 4 4 2 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 18 14 4 4 2 2 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 18 14 4 4 3 3 302 
29: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 18 14 4 4 3 3 302 
30: 0 60 149 261 403 331 291 193 163 262 259 188 145 140 265 101 74 63 29 20 17 16 18 14 4 4 3 3 3 303 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 27
BRUNCH_STAT Frame 28
BRUNCH_STAT OrigItp 165
BRUNCH_STAT SimpItp 74
BRUNCH_STAT Aig_ManSimplifyComb 4.50
BRUNCH_STAT Glucose_solve 10.71
BRUNCH_STAT Pdr_solve 6.33
BRUNCH_STAT addCoverCubes 3.79
BRUNCH_STAT blockCube 3.56
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 10.01
BRUNCH_STAT doPdrTrace 40.34
BRUNCH_STAT doPdrTrace.last 1.90
BRUNCH_STAT doPdrTrace_part1 0.49
BRUNCH_STAT doPdrTrace_part2 5.04
BRUNCH_STAT doStrengthenVC 0.35
BRUNCH_STAT ensureFrames 2.56
BRUNCH_STAT findItpConstraints 2.92
BRUNCH_STAT generalize 3.30
BRUNCH_STAT getCnfTr 0.04
BRUNCH_STAT getInterpolant 4.38
BRUNCH_STAT pushClauses 26.60
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 24.93
BRUNCH_STAT run.loop 62.52
BRUNCH_STAT solveWithCore 10.01
BRUNCH_STAT solveWithCore_minSuffix 3.55
BRUNCH_STAT solverAddClause 1.33
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 29 core size: 26
UNSAT from BMC at frame: 28
itp             : pi =   147  po =    29  and =     150  lev =  10
itp             : pi =   147  po =    29  and =      60  lev =   5
FINDING NEEDED CONSTRAINTS: CoNum: 29 EquivNum: 29
............................. Done
Building PDR trace
30: 0 60 149 261 403 328 286 197 163 262 259 188 146 140 265 101 74 63 29 20 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 163 262 259 188 146 140 265 101 74 63 29 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 263 259 188 147 140 265 101 74 63 29 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 261 188 147 140 265 101 74 64 29 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 140 265 101 74 64 29 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 140 265 101 74 64 29 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 140 265 101 74 64 29 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 144 265 102 74 64 29 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 29 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 29 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 29 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 65 29 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 303 
30: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 303 
31: 0 60 149 261 403 328 286 200 180 262 263 188 147 142 250 102 74 64 30 21 17 16 18 14 4 4 3 3 3 3 302 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 28
BRUNCH_STAT Frame 29
BRUNCH_STAT OrigItp 150
BRUNCH_STAT SimpItp 60
BRUNCH_STAT Aig_ManSimplifyComb 4.50
BRUNCH_STAT Glucose_solve 11.62
BRUNCH_STAT Pdr_solve 6.38
BRUNCH_STAT addCoverCubes 4.30
BRUNCH_STAT blockCube 3.57
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 10.94
BRUNCH_STAT doPdrTrace 46.13
BRUNCH_STAT doPdrTrace.last 5.78
BRUNCH_STAT doPdrTrace_part1 0.54
BRUNCH_STAT doPdrTrace_part2 5.60
BRUNCH_STAT doStrengthenVC 0.39
BRUNCH_STAT ensureFrames 2.86
BRUNCH_STAT findItpConstraints 2.95
BRUNCH_STAT generalize 3.31
BRUNCH_STAT getCnfTr 0.05
BRUNCH_STAT getInterpolant 4.44
BRUNCH_STAT pushClauses 31.45
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 29.38
BRUNCH_STAT run.loop 69.35
BRUNCH_STAT solveWithCore 10.94
BRUNCH_STAT solveWithCore_minSuffix 3.96
BRUNCH_STAT solverAddClause 1.56
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 30 core size: 25
UNSAT from BMC at frame: 29
itp             : pi =   147  po =    30  and =     463  lev =  21
itp             : pi =   147  po =    30  and =     167  lev =   7
FINDING NEEDED CONSTRAINTS: CoNum: 30 EquivNum: 30
.............................. Done
Building PDR trace
31: 0 60 149 261 403 328 286 200 180 264 264 188 147 142 249 101 74 64 30 21 17 16 18 16 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 147 142 249 101 74 64 30 21 17 16 18 16 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 147 142 249 101 74 64 30 21 17 16 18 16 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 147 142 249 101 74 64 30 21 17 16 18 16 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 249 101 74 64 30 21 17 16 18 16 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 249 101 74 64 30 21 17 16 18 16 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 244 101 74 64 30 21 17 16 18 16 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 64 30 21 17 16 18 16 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 4 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 10 4 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 10 10 3 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 10 10 11 3 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 10 10 11 9 3 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 10 10 11 9 11 3 302 
31: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 10 10 11 9 11 11 302 
32: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 18 10 10 11 9 11 11 18 294 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 29
BRUNCH_STAT Frame 30
BRUNCH_STAT OrigItp 463
BRUNCH_STAT SimpItp 167
BRUNCH_STAT Aig_ManSimplifyComb 4.51
BRUNCH_STAT Glucose_solve 12.63
BRUNCH_STAT Pdr_solve 6.47
BRUNCH_STAT addCoverCubes 4.79
BRUNCH_STAT blockCube 3.61
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 11.98
BRUNCH_STAT doPdrTrace 51.28
BRUNCH_STAT doPdrTrace.last 5.15
BRUNCH_STAT doPdrTrace_part1 0.58
BRUNCH_STAT doPdrTrace_part2 6.13
BRUNCH_STAT doStrengthenVC 0.43
BRUNCH_STAT ensureFrames 3.14
BRUNCH_STAT findItpConstraints 2.98
BRUNCH_STAT generalize 3.35
BRUNCH_STAT getCnfTr 0.05
BRUNCH_STAT getInterpolant 4.51
BRUNCH_STAT pushClauses 35.67
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 33.24
BRUNCH_STAT run.loop 75.69
BRUNCH_STAT solveWithCore 11.98
BRUNCH_STAT solveWithCore_minSuffix 4.45
BRUNCH_STAT solverAddClause 1.78
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 31 core size: 10
UNSAT from BMC at frame: 30
itp             : pi =   147  po =    31  and =    1311  lev =  49
itp             : pi =   147  po =    31  and =     436  lev =  14
FINDING NEEDED CONSTRAINTS: CoNum: 31 EquivNum: 31
......... Done
Building PDR trace
32: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 304 
32: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 304 
32: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 304 
32: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 304 
32: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 304 
32: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 304 
32: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 304 
32: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 304 
33: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 8 298 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 30
BRUNCH_STAT Frame 31
BRUNCH_STAT OrigItp 1311
BRUNCH_STAT SimpItp 436
BRUNCH_STAT Aig_ManSimplifyComb 4.55
BRUNCH_STAT Glucose_solve 13.91
BRUNCH_STAT Pdr_solve 6.48
BRUNCH_STAT addCoverCubes 4.91
BRUNCH_STAT blockCube 3.62
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 13.28
BRUNCH_STAT doPdrTrace 52.22
BRUNCH_STAT doPdrTrace.last 0.94
BRUNCH_STAT doPdrTrace_part1 0.59
BRUNCH_STAT doPdrTrace_part2 6.28
BRUNCH_STAT doStrengthenVC 0.46
BRUNCH_STAT ensureFrames 3.20
BRUNCH_STAT findItpConstraints 2.99
BRUNCH_STAT generalize 3.36
BRUNCH_STAT getCnfTr 0.05
BRUNCH_STAT getInterpolant 4.61
BRUNCH_STAT pushClauses 36.36
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 33.89
BRUNCH_STAT run.loop 78.11
BRUNCH_STAT solveWithCore 13.28
BRUNCH_STAT solveWithCore_minSuffix 5.16
BRUNCH_STAT solverAddClause 1.83
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 32 core size: 3
UNSAT from BMC at frame: 31
itp             : pi =   147  po =    32  and =      73  lev =  24
itp             : pi =   147  po =    32  and =      20  lev =   5
FINDING NEEDED CONSTRAINTS: CoNum: 32 EquivNum: 32
.. Done
Building PDR trace
33: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 4 304 
34: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 4 12 294 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 31
BRUNCH_STAT Frame 32
BRUNCH_STAT OrigItp 73
BRUNCH_STAT SimpItp 20
BRUNCH_STAT Aig_ManSimplifyComb 4.55
BRUNCH_STAT Glucose_solve 15.23
BRUNCH_STAT Pdr_solve 6.49
BRUNCH_STAT addCoverCubes 4.94
BRUNCH_STAT blockCube 3.62
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 14.61
BRUNCH_STAT doPdrTrace 52.60
BRUNCH_STAT doPdrTrace.last 0.39
BRUNCH_STAT doPdrTrace_part1 0.59
BRUNCH_STAT doPdrTrace_part2 6.31
BRUNCH_STAT doStrengthenVC 0.50
BRUNCH_STAT ensureFrames 3.21
BRUNCH_STAT findItpConstraints 2.99
BRUNCH_STAT generalize 3.36
BRUNCH_STAT getCnfTr 0.05
BRUNCH_STAT getInterpolant 4.66
BRUNCH_STAT pushClauses 36.68
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 34.21
BRUNCH_STAT run.loop 79.92
BRUNCH_STAT solveWithCore 14.61
BRUNCH_STAT solveWithCore_minSuffix 5.87
BRUNCH_STAT solverAddClause 1.85
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 33 core size: 4
UNSAT from BMC at frame: 32
itp             : pi =   147  po =    33  and =      79  lev =  31
itp             : pi =   147  po =    33  and =      34  lev =   7
FINDING NEEDED CONSTRAINTS: CoNum: 33 EquivNum: 33
... Done
Building PDR trace
34: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 4 12 295 
34: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 4 12 296 
35: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 4 12 126 170 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 32
BRUNCH_STAT Frame 33
BRUNCH_STAT OrigItp 79
BRUNCH_STAT SimpItp 34
BRUNCH_STAT Aig_ManSimplifyComb 4.55
BRUNCH_STAT Glucose_solve 16.53
BRUNCH_STAT Pdr_solve 6.49
BRUNCH_STAT addCoverCubes 4.98
BRUNCH_STAT blockCube 3.62
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 15.94
BRUNCH_STAT doPdrTrace 53.07
BRUNCH_STAT doPdrTrace.last 0.46
BRUNCH_STAT doPdrTrace_part1 0.60
BRUNCH_STAT doPdrTrace_part2 6.36
BRUNCH_STAT doStrengthenVC 0.54
BRUNCH_STAT ensureFrames 3.23
BRUNCH_STAT findItpConstraints 2.99
BRUNCH_STAT generalize 3.36
BRUNCH_STAT getCnfTr 0.05
BRUNCH_STAT getInterpolant 4.72
BRUNCH_STAT pushClauses 37.06
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 34.58
BRUNCH_STAT run.loop 81.80
BRUNCH_STAT solveWithCore 15.94
BRUNCH_STAT solveWithCore_minSuffix 6.48
BRUNCH_STAT solverAddClause 1.87
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 34 core size: 6
UNSAT from BMC at frame: 33
itp             : pi =   147  po =    34  and =    2547  lev = 103
itp             : pi =   147  po =    34  and =    1210  lev =  34
FINDING NEEDED CONSTRAINTS: CoNum: 34 EquivNum: 34
.... Done
Building PDR trace
35: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 6 12 125 175 
35: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 6 12 28 274 
35: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 6 12 72 311 
36: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 6 12 72 129 184 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 33
BRUNCH_STAT Frame 34
BRUNCH_STAT OrigItp 2547
BRUNCH_STAT SimpItp 1210
BRUNCH_STAT Aig_ManSimplifyComb 4.63
BRUNCH_STAT Glucose_solve 18.06
BRUNCH_STAT Pdr_solve 6.59
BRUNCH_STAT addCoverCubes 5.04
BRUNCH_STAT blockCube 3.67
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 17.49
BRUNCH_STAT doPdrTrace 53.72
BRUNCH_STAT doPdrTrace.last 0.65
BRUNCH_STAT doPdrTrace_part1 0.60
BRUNCH_STAT doPdrTrace_part2 6.43
BRUNCH_STAT doStrengthenVC 0.58
BRUNCH_STAT ensureFrames 3.27
BRUNCH_STAT findItpConstraints 3.00
BRUNCH_STAT generalize 3.41
BRUNCH_STAT getCnfTr 0.05
BRUNCH_STAT getInterpolant 4.93
BRUNCH_STAT pushClauses 37.50
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 35.00
BRUNCH_STAT run.loop 84.35
BRUNCH_STAT solveWithCore 17.49
BRUNCH_STAT solveWithCore_minSuffix 7.38
BRUNCH_STAT solverAddClause 1.89
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 35 core size: 6
UNSAT from BMC at frame: 34
itp             : pi =   147  po =    35  and =    3033  lev = 185
itp             : pi =   147  po =    35  and =    1273  lev =  28
FINDING NEEDED CONSTRAINTS: CoNum: 35 EquivNum: 35
..... Done
Building PDR trace
36: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 5 6 12 130 185 
36: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 5 6 12 130 185 
36: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 5 6 11 23 294 
36: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 5 6 11 35 295 
37: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 5 6 11 35 179 126 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 34
BRUNCH_STAT Frame 35
BRUNCH_STAT OrigItp 3033
BRUNCH_STAT SimpItp 1273
BRUNCH_STAT Aig_ManSimplifyComb 4.73
BRUNCH_STAT Glucose_solve 19.32
BRUNCH_STAT Pdr_solve 6.63
BRUNCH_STAT addCoverCubes 5.13
BRUNCH_STAT blockCube 3.70
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 18.77
BRUNCH_STAT doPdrTrace 54.40
BRUNCH_STAT doPdrTrace.last 0.69
BRUNCH_STAT doPdrTrace_part1 0.61
BRUNCH_STAT doPdrTrace_part2 6.51
BRUNCH_STAT doStrengthenVC 0.62
BRUNCH_STAT ensureFrames 3.31
BRUNCH_STAT findItpConstraints 3.01
BRUNCH_STAT generalize 3.43
BRUNCH_STAT getCnfTr 0.06
BRUNCH_STAT getInterpolant 5.19
BRUNCH_STAT pushClauses 37.99
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 35.48
BRUNCH_STAT run.loop 86.73
BRUNCH_STAT solveWithCore 18.77
BRUNCH_STAT solveWithCore_minSuffix 8.11
BRUNCH_STAT solverAddClause 1.93
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 1 of prefix
Assumption size: 36 core size: 7
UNSAT from BMC at frame: 35
itp             : pi =   147  po =    36  and =    7870  lev = 231
itp             : pi =   147  po =    36  and =    3947  lev =  70
FINDING NEEDED CONSTRAINTS: CoNum: 36 EquivNum: 36
...... Done
Building PDR trace
37: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 3 2 4 1 1 317 
37: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 3 2 4 1 1 317 
37: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 3 2 4 1 1 317 
37: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 3 2 4 1 1 317 
37: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 3 2 4 1 1 317 
38: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 3 2 4 1 1 1 316 


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 35
BRUNCH_STAT Frame 36
BRUNCH_STAT OrigItp 7870
BRUNCH_STAT SimpItp 3947
BRUNCH_STAT Aig_ManSimplifyComb 4.99
BRUNCH_STAT Glucose_solve 22.32
BRUNCH_STAT Pdr_solve 6.66
BRUNCH_STAT addCoverCubes 5.23
BRUNCH_STAT blockCube 3.70
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 21.80
BRUNCH_STAT doPdrTrace 55.11
BRUNCH_STAT doPdrTrace.last 0.70
BRUNCH_STAT doPdrTrace_part1 0.62
BRUNCH_STAT doPdrTrace_part2 6.62
BRUNCH_STAT doStrengthenVC 0.65
BRUNCH_STAT ensureFrames 3.37
BRUNCH_STAT findItpConstraints 3.05
BRUNCH_STAT generalize 3.43
BRUNCH_STAT getCnfTr 0.06
BRUNCH_STAT getInterpolant 5.64
BRUNCH_STAT pushClauses 38.48
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 35.95
BRUNCH_STAT run.loop 91.24
BRUNCH_STAT solveWithCore 21.80
BRUNCH_STAT solveWithCore_minSuffix 8.88
BRUNCH_STAT solverAddClause 1.97
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Killed 37 of prefix
Assumption size: 37 core size: 2
UNSAT from BMC at frame: 36
itp             : pi =   147  po =    37  and =      12  lev =  10
itp             : pi =   147  po =    37  and =       6  lev =   3
FINDING NEEDED CONSTRAINTS: CoNum: 37 EquivNum: 37
. Done
Building PDR trace
0
b0
.
39: 0 60 149 261 403 328 286 200 180 264 264 188 149 143 243 101 74 65 30 21 17 16 18 11 5 5 4 3 3 3 8 3 2 4 1 1 1 0 316 
Verification of invariant with 316 clauses was successful.

************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 36
BRUNCH_STAT Frame 37
BRUNCH_STAT Invar 316
BRUNCH_STAT OrigItp 12
BRUNCH_STAT SimpItp 6
BRUNCH_STAT Aig_ManSimplifyComb 4.99
BRUNCH_STAT Glucose_solve 22.97
BRUNCH_STAT Pdr_solve 6.66
BRUNCH_STAT addCoverCubes 5.24
BRUNCH_STAT blockCube 3.70
BRUNCH_STAT computeNextTr 0.04
BRUNCH_STAT doBmc 22.47
BRUNCH_STAT doPdrTrace 55.14
BRUNCH_STAT doPdrTrace.last 0.03
BRUNCH_STAT doPdrTrace_part1 0.62
BRUNCH_STAT doPdrTrace_part2 6.64
BRUNCH_STAT doStrengthenVC 0.65
BRUNCH_STAT ensureFrames 3.37
BRUNCH_STAT findItpConstraints 3.05
BRUNCH_STAT generalize 3.43
BRUNCH_STAT getCnfTr 0.06
BRUNCH_STAT getInterpolant 5.69
BRUNCH_STAT pushClauses 38.49
BRUNCH_STAT pushClauses.Pdr_ManCheckCube 35.96
BRUNCH_STAT run.loop 92.04
BRUNCH_STAT solveWithCore 22.47
BRUNCH_STAT solveWithCore_minSuffix 8.88
BRUNCH_STAT solverAddClause 1.97
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:  Fri Sep 18 22:55:03 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 22:55:07 CEST 2015
[launch.sh] done: Fri Sep 18 22:55:07 CEST 2015
