[runlim] version:		1.9
[runlim] time limit:		311040000 seconds
[runlim] real time limit:	3600 seconds
[runlim] space limit:		7000 MB
[runlim] argv[0]:		/home/biere/hwmcc15/solvers/shiftbmc/single.shiftbmc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a08b17s.aig
[runlim] start:			Fri Sep 18 10:20:50 2015
[runlim] main pid:		6647
[shift-bmc] shiftbmc, Norbert Manthey, 2015
[shift-bmc] based on the aigbmc bounded model checker
c nonZeroInitialized: 0 outputs: 1 inputs: 15696
[shift-bmc] simplify with ABC
[shift-bmc] initial MILOA: 841049 15696 16357 1 808996  -- set number of initial latches to 16357 - 
[runlim] sample:		9.1 time, 10.5 real, 272.5 MB
[runlim] sample:		19.1 time, 20.5 real, 285.0 MB
[runlim] sample:		29.0 time, 30.5 real, 341.3 MB
[runlim] sample:		39.0 time, 40.5 real, 408.5 MB
[runlim] sample:		49.0 time, 50.5 real, 270.9 MB
[runlim] sample:		59.0 time, 60.5 real, 348.3 MB
[runlim] sample:		69.0 time, 70.5 real, 301.5 MB
[runlim] sample:		79.0 time, 80.5 real, 281.9 MB
[runlim] sample:		89.0 time, 90.5 real, 331.5 MB
[runlim] sample:		99.0 time, 100.5 real, 309.4 MB
[runlim] sample:		109.0 time, 110.5 real, 337.2 MB
[runlim] sample:		119.0 time, 120.5 real, 332.6 MB
[runlim] sample:		129.0 time, 130.5 real, 332.6 MB
[runlim] sample:		139.0 time, 140.5 real, 320.6 MB
[runlim] sample:		149.0 time, 150.5 real, 347.9 MB
[runlim] sample:		159.0 time, 160.5 real, 366.2 MB
[runlim] sample:		169.0 time, 170.5 real, 371.5 MB
[runlim] sample:		179.0 time, 180.5 real, 343.0 MB
[runlim] sample:		189.0 time, 190.5 real, 343.0 MB
[runlim] sample:		199.0 time, 200.5 real, 343.0 MB
[runlim] sample:		209.0 time, 210.5 real, 343.0 MB
[runlim] sample:		219.0 time, 220.5 real, 343.0 MB
[runlim] sample:		229.0 time, 230.5 real, 343.0 MB
[runlim] sample:		239.0 time, 240.5 real, 343.0 MB
[runlim] sample:		248.9 time, 250.5 real, 343.0 MB
[runlim] sample:		258.9 time, 260.5 real, 343.0 MB
[runlim] sample:		268.9 time, 270.5 real, 343.0 MB
[runlim] sample:		278.9 time, 280.5 real, 343.0 MB
[shift-bmc] aig preprocessing tool 271.413411 seconds
c set initial latches to 16357
[shift-bmc] encode MILOA = 800409 15696 15767 1 768946
[shift-bmc] WARNING using 1 outputs as bad state properties
[shift-bmc] init outer CNF simplification with configuration BMC_FULL:-bve_early:-no-cp3_stats:-cp3_bve_limit=50000000:-all_strength_res=4:-pr-vivi:-cp3_Abva:-3resolve
[runlim] sample:		288.9 time, 290.5 real, 535.3 MB
[runlim] sample:		298.9 time, 300.5 real, 796.8 MB
[runlim] sample:		308.9 time, 310.5 real, 865.4 MB
[runlim] sample:		318.9 time, 320.5 real, 835.7 MB
[runlim] sample:		328.9 time, 330.5 real, 835.7 MB
[runlim] sample:		338.9 time, 340.5 real, 835.9 MB
[runlim] sample:		348.9 time, 350.5 real, 835.9 MB
[runlim] sample:		358.9 time, 360.5 real, 835.9 MB
[runlim] sample:		368.9 time, 370.5 real, 835.9 MB
[runlim] sample:		378.9 time, 380.5 real, 835.9 MB
[runlim] sample:		388.9 time, 390.5 real, 835.9 MB
[runlim] sample:		398.9 time, 400.5 real, 835.9 MB
[runlim] sample:		408.9 time, 410.5 real, 835.9 MB
[runlim] sample:		418.9 time, 420.5 real, 835.9 MB
[runlim] sample:		428.9 time, 430.5 real, 836.0 MB
[runlim] sample:		438.9 time, 440.5 real, 836.4 MB
[runlim] sample:		448.9 time, 450.5 real, 836.4 MB
[runlim] sample:		458.8 time, 460.5 real, 836.4 MB
[runlim] sample:		468.8 time, 470.5 real, 836.4 MB
[runlim] sample:		478.8 time, 480.5 real, 836.4 MB
[runlim] sample:		488.8 time, 490.5 real, 836.4 MB
[runlim] sample:		498.8 time, 500.5 real, 837.0 MB
[runlim] sample:		508.8 time, 510.5 real, 837.6 MB
[runlim] sample:		518.8 time, 520.5 real, 838.4 MB
[runlim] sample:		528.8 time, 530.5 real, 838.4 MB
[runlim] sample:		538.8 time, 540.5 real, 838.4 MB
[runlim] sample:		548.8 time, 550.5 real, 838.4 MB
[runlim] sample:		558.8 time, 560.5 real, 838.4 MB
[runlim] sample:		568.8 time, 570.5 real, 838.4 MB
[runlim] sample:		578.8 time, 580.5 real, 838.4 MB
[runlim] sample:		588.8 time, 590.5 real, 838.4 MB
[runlim] sample:		598.8 time, 600.5 real, 838.4 MB
[runlim] sample:		608.8 time, 610.5 real, 838.4 MB
[runlim] sample:		618.7 time, 620.5 real, 838.4 MB
[runlim] sample:		628.7 time, 630.5 real, 838.4 MB
[runlim] sample:		638.7 time, 640.5 real, 838.4 MB
[runlim] sample:		648.7 time, 650.5 real, 838.4 MB
[runlim] sample:		658.7 time, 660.5 real, 838.4 MB
[runlim] sample:		668.7 time, 670.5 real, 838.4 MB
[runlim] sample:		678.7 time, 680.5 real, 838.4 MB
[runlim] sample:		688.7 time, 690.5 real, 838.4 MB
[runlim] sample:		698.7 time, 700.5 real, 838.4 MB
[runlim] sample:		708.7 time, 710.5 real, 838.4 MB
[runlim] sample:		718.6 time, 720.5 real, 838.4 MB
[runlim] sample:		728.6 time, 730.5 real, 838.4 MB
[runlim] sample:		738.6 time, 740.5 real, 838.4 MB
[runlim] sample:		748.6 time, 750.5 real, 838.4 MB
[runlim] sample:		758.6 time, 760.5 real, 838.4 MB
[runlim] sample:		768.6 time, 770.5 real, 838.4 MB
[runlim] sample:		778.6 time, 780.5 real, 838.4 MB
[shift-bmc] outer CNF preprocessing tool 489.086465 seconds
[shift-bmc] pp time summary: aig: 271.413 inner-cnf: 0 outer-cnf: 489.086
[runlim] sample:		788.6 time, 790.5 real, 1022.5 MB
[runlim] sample:		798.6 time, 800.5 real, 968.4 MB
found a bad state around bound 6
c print witness with initial latches 16357
c model size before: 800419 with formula variables: 800411 and shrink: 8
c model size afterwards: 800411
c model size before: 800419 with formula variables: 800411 and shrink: 8
c model size afterwards: 800411
[shift-bmc] use original latch variables
c model size before: 800419 with formula variables: 800411 and shrink: 8
c model size afterwards: 800411
c model size before: 800419 with formula variables: 800411 and shrink: 8
c model size afterwards: 800411
c model size before: 800419 with formula variables: 800411 and shrink: 8
c model size afterwards: 800411
c model size before: 800419 with formula variables: 800411 and shrink: 8
c model size afterwards: 800411
c model size before: 800419 with formula variables: 800411 and shrink: 8
c model size afterwards: 800411
c model size before: 800419 with formula variables: 800411 and shrink: 8
c model size afterwards: 800411
c model size before: 800419 with formula variables: 800411 and shrink: 8
c model size afterwards: 800411
[runlim] end:			Fri Sep 18 10:34:14 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		8038
[runlim] real:			804.29 seconds
[runlim] time:			802.26 seconds
[runlim] space:			1133.9 MB
[runlim] samples:		8038
