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

[pavy] finished pp, output=/tmp/7197829.1.queue/avy-tT_pct/6s309b046.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/7197829.1.queue/avy-tT_pct/navy_avy0.cex /tmp/7197829.1.queue/avy-tT_pct/6s309b046.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/abcpdr --verbose=2 --cex=/tmp/7197829.1.queue/avy-tT_pct/abcpdr_avy1.cex /tmp/7197829.1.queue/avy-tT_pct/6s309b046.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/7197829.1.queue/avy-tT_pct/avyabsmus_avy2.cex /tmp/7197829.1.queue/avy-tT_pct/6s309b046.pp.aig
[pavy] kicking off  /home/biere/hwmcc15/solvers/avy/extracted/avybmc --opt-bmc --glucose --depth=1000 --verbose=2 --cex=/tmp/7197829.1.queue/avy-tT_pct/fib_avy3.cex /tmp/7197829.1.queue/avy-tT_pct/6s309b046.pp.aig
[pavy] running: [15826, 15827, 15828, 15829]
[pavy] finished pid 15829 with code 1 and signal 0
[pavy] trying to kill  15826
[pavy] waiting for  15826
[pavy] trying to kill  15827
[pavy] waiting for  15827
[pavy] trying to kill  15828
[pavy] waiting for  15828
AVY PARAMETERS
	fName = /tmp/7197829.1.queue/avy-tT_pct/6s309b046.pp.aig
	ipt = 0
	avy = 0
	stutter = 0
	reset-cover = 0
	shallow_push = 0
	min-core = 0
	abstraction = 0
	tr0 = 0
	pdr = 0
	min-suffix = 0
	sat1 = 0
	minisat = 0
	glucose = 1
	minisat_itp = 0
	glucose_itp = 0
	sat_simp = 0
	itp_simp = 0
	proof_reorder = 0
	gen-conf-limit = 0
	kstep = 0
	stick-error = 0
	itp-simplify = 1
	max-frame = 1000
END
Starting ABC
	Reading AIG from '/tmp/7197829.1.queue/avy-tT_pct/6s309b046.pp.aig'


************** BRUNCH STATS ***************** 
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Assumption is: 19086
Solving 0 ...
Result: false
Assumption is: 57252
Solving 1 ...
Result: false
Assumption is: 95418
Solving 2 ...
Result: false
Assumption is: 133608
Solving 3 ...
Result: false
Assumption is: 171792
Solving 4 ...
Result: false
Assumption is: 209976
Solving 5 ...
Result: false
Assumption is: 248160
Solving 6 ...
Result: false
Assumption is: 286344
Solving 7 ...
Result: false
Assumption is: 324528
Solving 8 ...
Result: false
Assumption is: 362712
Solving 9 ...
Result: false
Assumption is: 400896
Solving 10 ...
Result: false
Assumption is: 439080
Solving 11 ...
Result: false
Assumption is: 477264
Solving 12 ...
Result: false
Assumption is: 515448
Solving 13 ...
Result: false
Assumption is: 554474
Solving 14 ...
Result: false
Assumption is: 593106
Solving 15 ...
Result: false
Assumption is: 631796
Solving 16 ...
Result: false
Assumption is: 673662
Solving 17 ...
Result: false
Assumption is: 713352
Solving 18 ...
Result: false
Assumption is: 766842
Solving 19 ...
Result: false
Assumption is: 809512
Solving 20 ...
Result: false
Assumption is: 852484
Solving 21 ...
Result: false
Assumption is: 895632
Solving 22 ...
Result: false
Assumption is: 938634
Solving 23 ...
Result: false
Assumption is: 981824
Solving 24 ...
Result: false
Assumption is: 1025224
Solving 25 ...
Result: false
Assumption is: 1068850
Solving 26 ...
Result: false
Assumption is: 1112468
Solving 27 ...
Result: false
Assumption is: 1156100
Solving 28 ...
Result: false
Assumption is: 1199732
Solving 29 ...
Result: false
Assumption is: 1243366
Solving 30 ...
Result: false
Assumption is: 1287000
Solving 31 ...
Result: false
Assumption is: 1330634
Solving 32 ...
Result: false
Assumption is: 1379506
Solving 33 ...
Result: false
Assumption is: 1423432
Solving 34 ...
Result: false
Assumption is: 1468392
Solving 35 ...
Result: false
Assumption is: 1515820
Solving 36 ...
Result: false
Assumption is: 1560298
Solving 37 ...
Result: false
Assumption is: 1604796
Solving 38 ...
Result: false
Assumption is: 1924978
Solving 39 ...
Result: false
Assumption is: 2038942
Solving 40 ...
Result: false
Assumption is: 2139156
Solving 41 ...
Result: false
Assumption is: 2239290
Solving 42 ...
Result: false
Assumption is: 2341114
Solving 43 ...
Result: false
Assumption is: 2442230
Solving 44 ...
Result: false
Assumption is: 2558212
Solving 45 ...
Result: false
Assumption is: 2661372
Solving 46 ...
Result: false
Assumption is: 2781240
Solving 47 ...
Result: false
Assumption is: 2886466
Solving 48 ...
Result: false
Assumption is: 2989964
Solving 49 ...
Result: true
Generating CEX: /tmp/7197829.1.queue/avy-tT_pct/fib_avy3.cex
[pavy] Witness begin
1
b0
[encoded data, 27581 characters]
.
[pavy] Witness end
WINNER:  fib
BRUNCH_STAT config 3
BRUNCH_STAT config_name fib
BRUNCH_STAT Result SAT
[launch.sh] stop:  Sun Sep 20 20:09:24 CEST 2015
[launch.sh] round 1: killall abcpdr avy avybmc navy
[launch.sh] round 2: killall abcpdr avy avybmc navy
[launch.sh] round 3: killall abcpdr avy avybmc navy
[launch.sh] sync: Sun Sep 20 20:09:27 CEST 2015
[launch.sh] done: Sun Sep 20 20:09:27 CEST 2015
