[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b12s.aig
[launch.sh] host:  atom19 (atom19)
[launch.sh] start: Thu Sep 17 07:19:11 CEST 2015
[launch.sh] jobid: 7191397
[launch.sh] name:  oski15a14b12savy
[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/7191397.1.queue/avy-21gQi2
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b12s.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b12s.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b12s.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7191397.1.queue/avy-21gQi2/oski15a14b12s.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b12s.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7191397.1.queue/avy-21gQi2/oski15a14b12s.pp.aig".

[pavy] finished pp, output=/tmp/7191397.1.queue/avy-21gQi2/oski15a14b12s.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/7191397.1.queue/avy-21gQi2/navy_avy0.cex /tmp/7191397.1.queue/avy-21gQi2/oski15a14b12s.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7191397.1.queue/avy-21gQi2/abcpdr_avy1.cex /tmp/7191397.1.queue/avy-21gQi2/oski15a14b12s.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/7191397.1.queue/avy-21gQi2/avyabsmus_avy2.cex /tmp/7191397.1.queue/avy-21gQi2/oski15a14b12s.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7191397.1.queue/avy-21gQi2/fib_avy3.cex /tmp/7191397.1.queue/avy-21gQi2/oski15a14b12s.pp.aig
[pavy] running: [31688, 31689, 31690, 31691]
[pavy] finished pid 31689 with code 0 and signal 0
[pavy] trying to kill  31688
[pavy] waiting for  31688
[pavy] trying to kill  31690
[pavy] waiting for  31690
[pavy] trying to kill  31691
[pavy] waiting for  31691


************** BRUNCH STATS ***************** 
BRUNCH_STAT run 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
	Reading AIG from '/tmp/7191397.1.queue/avy-21gQi2/oski15a14b12s.pp.aig'
VarMax = 300. FrameMax = 10000. QueMax = 0. TimeMax = 0. MonoCNF = no. SkipGen = no. SolveAll = no.
  1 : 0 0                                                                  0      0.06 sec
  1 : 0 1                                                                  1      0.07 sec
  1 : 0 1                                                                  1      0.07 sec
  2 : 0 1 0                                                                0      0.07 sec
  2 : 0 1 1                                                                2      0.08 sec
  2 : 0 1 2                                                                2      0.08 sec
  2 : 0 2 4                                                                4      0.11 sec
  2 : 0 2 4                                                                4      0.11 sec
  3 : 0 1 1 1                                                              0      0.12 sec
  3 : 0 1 1 7                                                              7      0.17 sec
  3 : 0 1 1 9                                                              8      0.20 sec
  3 : 0 1 1 11                                                            10      0.23 sec
  3 : 0 1 1 13                                                            12      0.26 sec
  3 : 0 1 1 15                                                            14      0.28 sec
  3 : 0 1 1 17                                                            16      0.31 sec
  3 : 0 1 1 19                                                            18      0.33 sec
  3 : 0 1 1 21                                                            20      0.36 sec
  3 : 0 1 1 23                                                            22      0.38 sec
  3 : 0 1 1 25                                                            24      0.41 sec
  3 : 0 1 1 27                                                            26      0.43 sec
  3 : 0 1 1 29                                                            28      0.46 sec
  3 : 0 1 1 31                                                            30      0.50 sec
  3 : 0 1 1 33                                                            32      0.53 sec
  3 : 0 1 1 35                                                            34      0.56 sec
  3 : 0 1 1 37                                                            36      0.60 sec
  3 : 0 1 1 39                                                            38      0.63 sec
  3 : 0 1 1 41                                                            40      0.66 sec
  3 : 0 1 1 43                                                            42      0.69 sec
  3 : 0 1 1 45                                                            44      0.72 sec
  3 : 0 1 1 47                                                            46      0.75 sec
  3 : 0 1 1 49                                                            48      0.78 sec
  3 : 0 1 1 51                                                            50      0.81 sec
  3 : 0 1 1 53                                                            52      0.83 sec
  3 : 0 1 1 55                                                            54      0.86 sec
  3 : 0 1 1 57                                                            56      0.89 sec
  3 : 0 1 1 59                                                            58      0.92 sec
  3 : 0 1 1 61                                                            60      0.94 sec
  3 : 0 1 1 63                                                            62      0.97 sec
  3 : 0 1 1 65                                                            64      1.00 sec
  3 : 0 1 1 67                                                            66      1.03 sec
  3 : 0 1 1 69                                                            68      1.06 sec
  3 : 0 1 1 71                                                            70      1.09 sec
  3 : 0 1 1 73                                                            72      1.11 sec
  3 : 0 1 1 75                                                            74      1.14 sec
  3 : 0 1 1 77                                                            76      1.17 sec
  3 : 0 1 1 79                                                            78      1.19 sec
  3 : 0 1 1 81                                                            80      1.22 sec
  3 : 0 1 1 83                                                            82      1.25 sec
  3 : 0 1 1 85                                                            84      1.27 sec
  3 : 0 1 1 87                                                            86      1.30 sec
  3 : 0 1 1 89                                                            88      1.33 sec
  3 : 0 1 1 91                                                            90      1.36 sec
  3 : 0 1 1 93                                                            92      1.39 sec
  3 : 0 1 1 95                                                            94      1.42 sec
  3 : 0 1 1 97                                                            96      1.45 sec
  3 : 0 1 1 99                                                            98      1.47 sec
  3 : 0 1 1 101                                                          100      1.50 sec
  3 : 0 1 1 103                                                          102      1.53 sec
  3 : 0 1 1 105                                                          104      1.55 sec
  3 : 0 1 1 107                                                          106      1.58 sec
  3 : 0 1 1 109                                                          108      1.61 sec
  3 : 0 1 1 111                                                          110      1.63 sec
  3 : 0 1 1 113                                                          112      1.66 sec
  3 : 0 1 1 115                                                          114      1.68 sec
  3 : 0 1 1 117                                                          116      1.71 sec
  3 : 0 1 1 119                                                          118      1.73 sec
  3 : 0 1 1 121                                                          120      1.76 sec
  3 : 0 1 1 123                                                          122      1.79 sec
  3 : 0 1 1 125                                                          124      1.82 sec
  3 : 0 1 1 127                                                          126      1.84 sec
  3 : 0 1 1 129                                                          128      1.87 sec
  3 : 0 1 1 131                                                          130      1.90 sec
  3 : 0 1 1 133                                                          132      1.92 sec
  3 : 0 1 1 135                                                          134      1.95 sec
  3 : 0 1 1 137                                                          136      1.97 sec
  3 : 0 1 1 139                                                          138      2.00 sec
  3 : 0 1 1 141                                                          140      2.02 sec
  3 : 0 1 1 143                                                          142      2.05 sec
  3 : 0 1 1 145                                                          144      2.07 sec
  3 : 0 1 1 147                                                          146      2.09 sec
  3 : 0 1 1 149                                                          148      2.12 sec
  3 : 0 1 1 149                                                          148      2.12 sec
  4 : 0 1 1 0 78                                                           0      2.14 sec
Invariant F[3] : 78 clauses with 21 flops (out of 3449)
Verification of invariant with 78 clauses was successful.  Time =     0.02 sec
Block =   76  Oblig =   380  Clause =   154  Call =  2418 (sat=66.3%)  Start =   6
SAT solving =     1.53 sec ( 70.53 %)
  unsat     =     0.15 sec (  7.11 %)
  sat       =     1.38 sec ( 63.41 %)
Generalize  =     1.77 sec ( 81.22 %)
Push clause =     0.03 sec (  1.45 %)
Ternary sim =     0.23 sec ( 10.50 %)
Containment =     0.01 sec (  0.58 %)
CNF compute =     0.06 sec (  2.81 %)
TOTAL       =     2.17 sec (100.00 %)
Property proved.  Time =     2.19 sec
Result: false


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 3
BRUNCH_STAT run 2.19
BRUNCH_STAT run.loop 2.17
BRUNCH_STAT Result UNSAT
************** BRUNCH STATS END ***************** 
[pavy] Witness begin
0
b0
.
[pavy] Witness end
WINNER:  abcpdr
BRUNCH_STAT config 1
BRUNCH_STAT config_name abcpdr
BRUNCH_STAT Result UNSAT
[launch.sh] stop:  Thu Sep 17 07:19:20 CEST 2015
[launch.sh] round 1: killall abcpdr avy avybmc navy
[launch.sh] round 2: killall abcpdr avy avybmc navy
[launch.sh] round 3: killall abcpdr avy avybmc navy
[launch.sh] sync: Thu Sep 17 07:19:23 CEST 2015
[launch.sh] done: Thu Sep 17 07:19:23 CEST 2015
