[launch.sh] args:  /home/biere/hwmcc15/solvers/avy/single.avy /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b21s.aig
[launch.sh] host:  atom28 (atom28)
[launch.sh] start: Fri Sep 18 02:23:39 CEST 2015
[launch.sh] jobid: 7192741
[launch.sh] name:  oski15a01b21savy
[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/7192741.1.queue/avy-wQhZu4
[pavy] starting run with fname=/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b21s.aig
BRUNCH_STAT Result UNKNOWN
[pavy] running pp
[pavy] in_name =  /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b21s.aig
[pavy] /home/biere/hwmcc15/solvers/avy/extracted/abc -c &r /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b21s.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7192741.1.queue/avy-wQhZu4/oski15a01b21s.pp.aig
ABC command line: "&r /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a01b21s.aig ; &lcorr ; &dc2; &scorr; &dc2; &fraig ; &w /tmp/7192741.1.queue/avy-wQhZu4/oski15a01b21s.pp.aig".

[pavy] finished pp, output=/tmp/7192741.1.queue/avy-wQhZu4/oski15a01b21s.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/7192741.1.queue/avy-wQhZu4/navy_avy0.cex /tmp/7192741.1.queue/avy-wQhZu4/oski15a01b21s.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7192741.1.queue/avy-wQhZu4/abcpdr_avy1.cex /tmp/7192741.1.queue/avy-wQhZu4/oski15a01b21s.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/7192741.1.queue/avy-wQhZu4/avyabsmus_avy2.cex /tmp/7192741.1.queue/avy-wQhZu4/oski15a01b21s.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7192741.1.queue/avy-wQhZu4/fib_avy3.cex /tmp/7192741.1.queue/avy-wQhZu4/oski15a01b21s.pp.aig
[pavy] running: [7724, 7725, 7726, 7727]
[pavy] finished pid 7725 with code 1 and signal 0
[pavy] trying to kill  7724
[pavy] waiting for  7724
[pavy] trying to kill  7726
[pavy] waiting for  7726
[pavy] trying to kill  7727
[pavy] waiting for  7727


************** BRUNCH STATS ***************** 
BRUNCH_STAT run 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
	Reading AIG from '/tmp/7192741.1.queue/avy-wQhZu4/oski15a01b21s.pp.aig'
VarMax = 300. FrameMax = 10000. QueMax = 0. TimeMax = 0. MonoCNF = no. SkipGen = no. SolveAll = no.
  1 : 0 0                                                                  0      0.74 sec
  1 : 0 1                                                                  1      0.85 sec
  1 : 0 2                                                                  2      0.87 sec
  1 : 0 3                                                                  3      0.89 sec
  1 : 0 4                                                                  4      0.91 sec
  1 : 0 5                                                                  5      0.93 sec
  1 : 0 6                                                                  6      0.95 sec
  1 : 0 7                                                                  7      0.97 sec
  1 : 0 8                                                                  8      0.99 sec
  1 : 0 9                                                                  9      1.00 sec
  1 : 0 10                                                                10      1.02 sec
  1 : 0 11                                                                11      1.04 sec
  1 : 0 12                                                                12      1.06 sec
  1 : 0 13                                                                13      1.07 sec
  1 : 0 14                                                                14      1.08 sec
  1 : 0 15                                                                15      1.09 sec
  1 : 0 15                                                                17      1.16 sec
Block =   16  Oblig =    33  Clause =    15  Call =    33 (sat=51.5%)  Start =   0
SAT solving =     0.05 sec (  4.31 %)
  unsat     =     0.00 sec (  0.01 %)
  sat       =     0.05 sec (  4.30 %)
Generalize  =     0.15 sec ( 12.58 %)
Push clause =     0.00 sec (  0.00 %)
Ternary sim =     0.21 sec ( 16.85 %)
Containment =     0.00 sec (  0.01 %)
CNF compute =     0.09 sec (  7.65 %)
TOTAL       =     1.22 sec (100.00 %)
Output 0 of miter "/tmp/7192741.1.queue/avy-wQhZu4/oski15a01b21s.pp" was asserted in frame 1.  Time =     1.58 sec
Result: true
Generating counterexample: /tmp/7192741.1.queue/avy-wQhZu4/abcpdr_avy1.cex


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 0
BRUNCH_STAT run 1.92
BRUNCH_STAT run.loop 1.49
BRUNCH_STAT Result SAT
************** BRUNCH STATS END ***************** 
[pavy] Witness begin
1
b0
[encoded data, 55969 characters]
.
[pavy] Witness end
WINNER:  abcpdr
BRUNCH_STAT config 1
BRUNCH_STAT config_name abcpdr
BRUNCH_STAT Result SAT
[launch.sh] stop:  Fri Sep 18 02:25:00 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 02:25:03 CEST 2015
[launch.sh] done: Fri Sep 18 02:25:03 CEST 2015
