[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/all/selection/random/pdtvisns3p02.aig
[launch.sh] host:  atom31 (atom31)
[launch.sh] start: Sat Sep 19 18:42:07 CEST 2015
[launch.sh] jobid: 7196133
[launch.sh] name:  pdtvisns3p02avy
[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/7196133.1.queue/avy-fOYjjq
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/all/selection/random/pdtvisns3p02.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/all/selection/random/pdtvisns3p02.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/all/selection/random/pdtvisns3p02.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7196133.1.queue/avy-fOYjjq/pdtvisns3p02.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/all/selection/random/pdtvisns3p02.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7196133.1.queue/avy-fOYjjq/pdtvisns3p02.pp.aig".

[pavy] finished pp, output=/tmp/7196133.1.queue/avy-fOYjjq/pdtvisns3p02.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/7196133.1.queue/avy-fOYjjq/navy_avy0.cex /tmp/7196133.1.queue/avy-fOYjjq/pdtvisns3p02.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7196133.1.queue/avy-fOYjjq/abcpdr_avy1.cex /tmp/7196133.1.queue/avy-fOYjjq/pdtvisns3p02.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/7196133.1.queue/avy-fOYjjq/avyabsmus_avy2.cex /tmp/7196133.1.queue/avy-fOYjjq/pdtvisns3p02.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7196133.1.queue/avy-fOYjjq/fib_avy3.cex /tmp/7196133.1.queue/avy-fOYjjq/pdtvisns3p02.pp.aig
[pavy] running: [10804, 10805, 10806, 10807]
[pavy] finished pid 10805 with code 0 and signal 0
[pavy] trying to kill  10804
[pavy] waiting for  10804
[pavy] trying to kill  10806
[pavy] waiting for  10806
[pavy] trying to kill  10807
[pavy] waiting for  10807


************** BRUNCH STATS ***************** 
BRUNCH_STAT run 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
	Reading AIG from '/tmp/7196133.1.queue/avy-fOYjjq/pdtvisns3p02.pp.aig'
VarMax = 300. FrameMax = 10000. QueMax = 0. TimeMax = 0. MonoCNF = no. SkipGen = no. SolveAll = no.
  1 : 0 0                                                                  0      0.00 sec
  1 : 0 1                                                                  1      0.00 sec
  1 : 0 1                                                                  1      0.00 sec
  2 : 0 1 0                                                                0      0.00 sec
  2 : 0 8 9                                                               10      0.01 sec
  2 : 0 8 9                                                               10      0.01 sec
  3 : 0 7 9 0                                                              0      0.01 sec
  3 : 0 16 26 24                                                          31      0.04 sec
  3 : 0 16 27 26                                                          31      0.04 sec
  3 : 0 16 28 28                                                          31      0.05 sec
  3 : 0 16 29 30                                                          31      0.05 sec
  3 : 0 16 29 31                                                          31      0.05 sec
  3 : 0 16 29 31                                                          31      0.05 sec
  4 : 0 12 29 25 7                                                         0      0.06 sec
  4 : 0 14 39 55 56                                                       52      0.13 sec
  4 : 0 14 39 55 56                                                       52      0.13 sec
  5 : 0 13 31 33 31 23                                                     0      0.14 sec
  5 : 0 13 32 39 69 80                                                    57      0.24 sec
  5 : 0 13 32 39 69 81                                                    58      0.24 sec
  5 : 0 13 32 39 69 82                                                    59      0.24 sec
  5 : 0 13 32 39 69 82                                                    59      0.24 sec
  6 : 0 13 32 38 48 28 52                                                  0      0.26 sec
  6 : 0 13 32 38 48 28 52                                                  0      0.26 sec
  7 : 0 13 32 38 47 27 16 36                                               0      0.28 sec
  7 : 0 13 32 40 57 65 44 71                                              70      0.43 sec
  7 : 0 13 32 40 57 65 44 72                                              70      0.43 sec
  7 : 0 13 32 40 57 65 44 73                                              70      0.43 sec
  7 : 0 13 32 40 57 65 44 73                                              70      0.43 sec
  8 : 0 13 32 40 50 36 21 6 72                                             0      0.46 sec
  8 : 0 13 32 40 50 36 21 6 82                                            38      0.47 sec
  8 : 0 13 32 40 50 36 21 6 82                                            38      0.47 sec
  9 : 0 13 32 40 50 36 20 2 6 79                                           0      0.50 sec
  9 : 0 13 32 40 50 36 20 2 6 79                                           0      0.50 sec
 10 : 0 13 32 40 50 36 20 2 6 4 75                                         0      0.52 sec
 10 : 0 13 32 40 50 36 20 2 6 4 75                                         0      0.52 sec
 11 : 0 13 32 40 50 36 20 2 6 4 6 69                                       0      0.55 sec
 11 : 0 13 32 40 50 36 20 2 6 4 6 69                                       0      0.55 sec
 12 : 0 13 32 40 50 36 20 2 6 4 6 11 58                                    0      0.57 sec
 12 : 0 13 32 40 50 36 20 2 7 5 14 15 70                                  12      0.60 sec
 12 : 0 13 32 40 50 36 20 2 7 5 14 15 72                                  14      0.61 sec
 12 : 0 13 32 40 50 36 20 2 7 5 14 15 74                                  16      0.61 sec
 12 : 0 13 32 40 50 36 20 2 7 5 14 15 76                                  18      0.61 sec
 12 : 0 13 32 40 50 36 20 2 7 5 14 15 76                                  18      0.61 sec
 13 : 0 13 32 40 50 36 20 1 0 0 0 0 0 90                                   0      0.64 sec
Invariant F[8] : 90 clauses with 70 flops (out of 100)
Verification of invariant with 90 clauses was successful.  Time =     0.01 sec
Block =   19  Oblig =   842  Clause =   429  Call =  6620 (sat=71.1%)  Start =  16
SAT solving =     0.54 sec ( 82.26 %)
  unsat     =     0.07 sec ( 10.91 %)
  sat       =     0.46 sec ( 71.35 %)
Generalize  =     0.33 sec ( 50.81 %)
Push clause =     0.21 sec ( 32.76 %)
Ternary sim =     0.01 sec (  1.93 %)
Containment =     0.00 sec (  0.10 %)
CNF compute =     0.02 sec (  2.46 %)
TOTAL       =     0.65 sec (100.00 %)
Property proved.  Time =     0.66 sec
Result: false


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 12
BRUNCH_STAT run 0.64
BRUNCH_STAT run.loop 0.64
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:  Sat Sep 19 18:42:12 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: Sat Sep 19 18:42:15 CEST 2015
[launch.sh] done: Sat Sep 19 18:42:15 CEST 2015
