Commit 9b8d6b41 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

absynth results

parent 4a37c023
This diff is collapsed.
/home/pldiae/pwhile
2drwalk.imp Bound: 2 max(0, 1 - d + n)
bayesian_network.imp Bound: 5 max(0, n)
ber.imp Bound: 2 max(0, n - x)
bin.imp Bound: 0.2 max(0, 9 + n)
C4B_t09.imp Bound: 8.27273 max(0, x)
C4B_t13.imp Bound: 1.25 max(0, x) + max(0, y)
C4B_t15_2.imp C4B_t15.imp Bound: max(0, -1 + x) + max(0, x)
C4B_t19.imp Bound: max(0, 51 + i + k) + 2 max(0, i)
C4B_t30_2.imp C4B_t30.imp Bound: 0.333333 max(0, 2 + x) + 0.166667 max(0, 2 + x) max(0, 2 + y)
C4B_t61.imp Bound: 0.0606061 max(0, -1 + l) + max(0, l)
condand.imp Bound: 2 max(0, m)
cooling.absynth Bound: 0.42 max(0, 5 + t) + max(0, mt - st)
coupon.imp Bound: 15
cowboy_duel_3way.absynth Bound: 2.08333
cowboy_duel.imp Bound: 1.2
fcall.absynth Bound: 2 max(0, n - x)
filling_vol.absynth Bound: 0.333333 max(0, 10 + volToFill) + 0.333333 max(0, 11 + volToFill)
geo.absynth Bound: 5
hyper.absynth Bound: 5 max(0, n - x)
linear01.imp Bound: 0.6 max(0, x)
prdwalk.absynth Bound: 1.14286 max(0, 4 + n - x)
prnes.absynth Bound: 68.4795 max(0, -n) + 0.0526316 max(0, y)
prseq-2.absynth Bound: 0.66 max(0, 1 + x - y) + 1.32 max(0, 2 + x - y) + 0.15 max(0, 9 + y)
prseq.absynth Bound: 1.65 max(0, x - y) + 0.15 max(0, y)
prseq_bin.absynth Bound: 1.65 max(0, 1 + x - y) + 0.15 max(0, y)
prspeed.imp Bound: 2 max(0, m - y) + 0.666667 max(0, n - x)
race.absynth Bound: 0.666667 max(0, 9 - h + t)
rdseql.imp Bound: 2.25 max(0, x) + max(0, y)
rdspeed.absynth Bound: 2 max(0, m - y) + 0.666667 max(0, n - x)
rdwalk.imp Bound: 2 max(0, 1 + n - x)
rejection_sampling.imp Bound: 2 max(0, n)
rfind_lv.imp Bound: 2
rfind_mc.imp Bound: max(0, k)
robot.imp Bound: 0.384615 max(0, 6 + n)
roulette.absynth Bound: 4.93333 max(0, 10010 - n)
sprdwalk.absynth Bound: 2 max(0, n - x)
trapped_miner.imp Bound: 7.5 max(0, n)
complex-2.absynth Bound: 18 max(0, M) max(0, N) + 9 max(0, N) + max(0, w) + 3 max(0, y)
complex.absynth Bound: 6 max(0, m) max(0, n) + 3 max(0, n) + max(0, y)
multirace.absynth Bound: 2 max(0, m) max(0, n) + 4 max(0, n)
pol04.imp Bound: 7.5 max(0, x) + 4.5 max(0, x)²
pol05.absynth Bound: max(0, x) + max(0, x)²
pol06.absynth Bound: 0.5 max(0, -minPrice + sPrice)
pol07.imp Bound: 1.5 max(0, -2 + n) max(0, -1 + n)
rdbub.absynth Bound: 3 max(0, n)²
recursive.absynth Bound: 1.75 max(0, h - l) + 0.25 max(0, h - l)²
simple_game.imp Bound: 2 max(0, 1 + x)
trader.absynth Bound: 9.99991 max(0, -minPrice + sPrice)
Done.
This diff is collapsed.
processing ... examples/oopsla/2drobot.imp
 examples/oopsla/2drobot.imp : 2.821s : [Success] 1/2·<a + -2·(a·b) + a^2 + -b + b^2> + 2·<1 + 2·(a) + -2·(a·b) + a^2 + -2·(b) + b^2> + 1267/18·<6 + a + -b>
processing ... examples/oopsla/absynth/linear/2drwalk.imp
 examples/oopsla/absynth/linear/2drwalk.imp : 0.025s : [Success] 2·<1 + -d + n>
processing ... examples/oopsla/absynth/linear/C4B_t09.imp
 examples/oopsla/absynth/linear/C4B_t09.imp : 0.007s : [Success] 41·<x>
processing ... examples/oopsla/absynth/linear/C4B_t13.imp
 examples/oopsla/absynth/linear/C4B_t13.imp : 0.005s : [Success] [y ≥ 0] · (5/4·<x> + <y>)
processing ... examples/oopsla/absynth/linear/C4B_t15.imp
 examples/oopsla/absynth/linear/C4B_t15.imp : 0.142s : [Failed ]
processing ... examples/oopsla/absynth/linear/C4B_t15_2.imp
 examples/oopsla/absynth/linear/C4B_t15_2.imp : 0.005s : [Success] [y ≥ 0] · 2·<1 + x>
processing ... examples/oopsla/absynth/linear/C4B_t19.imp
 examples/oopsla/absynth/linear/C4B_t19.imp : 0.005s : [Success] 2·<-100 + i> + <51 + i + k>
processing ... examples/oopsla/absynth/linear/C4B_t30.imp
 examples/oopsla/absynth/linear/C4B_t30.imp : 0.011s : [Failed ]
processing ... examples/oopsla/absynth/linear/C4B_t30_2.imp
 examples/oopsla/absynth/linear/C4B_t30_2.imp : 0.001s : [Success] [y ≥ -1] · (<2 + y> + <x>)
processing ... examples/oopsla/absynth/linear/C4B_t61.imp
 examples/oopsla/absynth/linear/C4B_t61.imp : 0.004s : [Success] 160/19·<-7 + l> + 7
processing ... examples/oopsla/absynth/linear/bayesian_network.imp
 examples/oopsla/absynth/linear/bayesian_network.: 0.002s : [Success] 5·<n>
processing ... examples/oopsla/absynth/linear/ber.imp
 examples/oopsla/absynth/linear/ber.imp : 0.001s : [Success] 2·<n + -x>
processing ... examples/oopsla/absynth/linear/bin.imp
 examples/oopsla/absynth/linear/bin.imp : 0.006s : [Success] 1024/1023·<n>
processing ... examples/oopsla/absynth/linear/condand.imp
 examples/oopsla/absynth/linear/condand.imp : 0.002s : [Success] 2·<m>
processing ... examples/oopsla/absynth/linear/cooling.pwhile
 examples/oopsla/absynth/linear/cooling.pwhile : 0.015s : [Success] 21/10·<1 + t> + <mt + -st>
processing ... examples/oopsla/absynth/linear/coupon.imp
 examples/oopsla/absynth/linear/coupon.imp : 0.003s : [Success] 25
processing ... examples/oopsla/absynth/linear/cowboy_duel.imp
 examples/oopsla/absynth/linear/cowboy_duel.imp : 0.001s : [Success] 6/5
processing ... examples/oopsla/absynth/linear/cowboy_duel_3way.pwhile
 examples/oopsla/absynth/linear/cowboy_duel_3way.: 0.005s : [Success] 83/24
processing ... examples/oopsla/absynth/linear/fcall.pwhile
 examples/oopsla/absynth/linear/fcall.pwhile : 0.001s : [Success] 2·<n + -x>
processing ... examples/oopsla/absynth/linear/filling_vol.pwhile
 examples/oopsla/absynth/linear/filling_vol.pwhil: 0.009s : [Success] 3/5·<1 + volToFill> + 3/5·<volToFill>
processing ... examples/oopsla/absynth/linear/geo.pwhile
 examples/oopsla/absynth/linear/geo.pwhile : 0.001s : [Success] <1>
processing ... examples/oopsla/absynth/linear/hyper.pwhile
 examples/oopsla/absynth/linear/hyper.pwhile : 0.001s : [Success] 145/28·<-1 + n + -x>
processing ... examples/oopsla/absynth/linear/linear01.imp
 examples/oopsla/absynth/linear/linear01.imp : 0.001s : [Success] <-1 + x>
processing ... examples/oopsla/absynth/linear/prdwalk.pwhile
 examples/oopsla/absynth/linear/prdwalk.pwhile : 0.003s : [Success] 8/3·<n + -x>
processing ... examples/oopsla/absynth/linear/prnes.pwhile
 examples/oopsla/absynth/linear/prnes.pwhile : 0.146s : [Success] [y ≥ 0] · (50/9·<99·(n) + -n·y> + 250000/81·<n^2>)
processing ... examples/oopsla/absynth/linear/prseq-2.pwhile
 examples/oopsla/absynth/linear/prseq-2.pwhile : 0.011s : [Success] [y ≥ 10] · (3·<x + -y> + 3·<x + -y> + 3/2·<y>)
processing ... examples/oopsla/absynth/linear/prseq.pwhile
 examples/oopsla/absynth/linear/prseq.pwhile : 0.010s : [Success] [y ≥ 10] · (3·<-2 + x + -y> + 3/2·<-9 + y> + 3·<-2 + x + -y>)
processing ... examples/oopsla/absynth/linear/prseq_bin.pwhile
 examples/oopsla/absynth/linear/prseq_bin.pwhile : 0.015s : [Success] [y ≥ 10] · (16/5·<-2 + x + -y> + 3/2·<-9 + y> + 16/5·<-2 + x + -y>)
processing ... examples/oopsla/absynth/linear/prspeed.imp
 examples/oopsla/absynth/linear/prspeed.imp : 0.015s : [Success] 4/3·<-2 + n + -x> + 2·<m + -y>
processing ... examples/oopsla/absynth/linear/race.pwhile
 examples/oopsla/absynth/linear/race.pwhile : 0.012s : [Success] 11/6·<3 + -h + t>
processing ... examples/oopsla/absynth/linear/rdseql.imp
 examples/oopsla/absynth/linear/rdseql.imp : 0.008s : [Success] [y ≥ 0] · (9/4·<x> + <y>)
processing ... examples/oopsla/absynth/linear/rdspeed.pwhile
 examples/oopsla/absynth/linear/rdspeed.pwhile : 0.013s : [Success] 4/3·<-2 + n + -x> + 2·<m + -y>
processing ... examples/oopsla/absynth/linear/rdwalk.imp
 examples/oopsla/absynth/linear/rdwalk.imp : 0.003s : [Success] 2·<1 + n + -x>
processing ... examples/oopsla/absynth/linear/rejection_sampling.imp
 examples/oopsla/absynth/linear/rejection_samplin: 0.003s : [Success] 2·<n>
processing ... examples/oopsla/absynth/linear/rfind_lv.imp
 examples/oopsla/absynth/linear/rfind_lv.imp : 0.001s : [Success] 2
processing ... examples/oopsla/absynth/linear/rfind_mc.imp
 examples/oopsla/absynth/linear/rfind_mc.imp : 0.002s : [Success] <k>
processing ... examples/oopsla/absynth/linear/robot.imp
 examples/oopsla/absynth/linear/robot.imp : 0.006s : [Success] 5/4·<n>
processing ... examples/oopsla/absynth/linear/roulette.pwhile
 examples/oopsla/absynth/linear/roulette.pwhile : 0.028s : [Success] 74/15·<10011 + -n>
processing ... examples/oopsla/absynth/linear/sprdwalk.pwhile
 examples/oopsla/absynth/linear/sprdwalk.pwhile : 0.001s : [Success] 2·<n + -x>
processing ... examples/oopsla/absynth/linear/trapped_miner.imp
 examples/oopsla/absynth/linear/trapped_miner.imp: 0.002s : [Success] 15/2·<n>
processing ... examples/oopsla/absynth/polynomial/complex-2.pwhile
 examples/oopsla/absynth/polynomial/complex-2.pwh: 0.030s : [Success] [M ≥ 0 ∧ y ≥ 0] · (<w> + 18·<M·N + N> + 3·<y>)
processing ... examples/oopsla/absynth/polynomial/complex.pwhile
 examples/oopsla/absynth/polynomial/complex.pwhil: 0.026s : [Success] [m ≥ 0 ∧ y ≥ 0] · (6·<m·n + n> + <y>)
processing ... examples/oopsla/absynth/polynomial/multirace.pwhile
 examples/oopsla/absynth/polynomial/multirace.pwh: 0.012s : [Success] [m ≥ 0] · 4·<m·n + n>
processing ... examples/oopsla/absynth/polynomial/pol04.imp
 examples/oopsla/absynth/polynomial/pol04.imp : 0.012s : [Success] 15/2·<x> + 9/2·<x^2>
processing ... examples/oopsla/absynth/polynomial/pol05.pwhile
 examples/oopsla/absynth/polynomial/pol05.pwhile : 0.011s : [Success] 3/4·<x> + 3/2·<x^2>
processing ... examples/oopsla/absynth/polynomial/pol06.pwhile
 examples/oopsla/absynth/polynomial/pol06.pwhile : 0.039s : [Success] <1 + minPrice + minPrice·sPrice + sPrice> + <-minPrice + -minPrice·sPrice + sPrice + sPrice^2>
processing ... examples/oopsla/absynth/polynomial/pol07.imp
 examples/oopsla/absynth/polynomial/pol07.imp : 0.014s : [Success] 3/2·<1 + -2·(n) + n^2>
processing ... examples/oopsla/absynth/polynomial/rdbub.pwhile
 examples/oopsla/absynth/polynomial/rdbub.pwhile : 0.009s : [Success] 3·<n^2>
processing ... examples/oopsla/absynth/polynomial/simple_game.imp
 examples/oopsla/absynth/polynomial/simple_game.i: 0.005s : [Success] 2·<1 + x>
processing ... examples/oopsla/absynth/polynomial/trader.pwhile
 examples/oopsla/absynth/polynomial/trader.pwhile: 0.048s : [Success] 20·<-minPrice + minPrice·sPrice + -minPrice^2 + sPrice> + 10·<-2·(minPrice·sPrice) + minPrice^2 + sPrice^2>
processing ... examples/oopsla/bridge.imp
 examples/oopsla/bridge.imp : 0.008s : [Success] <-a·b + a·x + b·x + -x^2>
processing ... examples/oopsla/coupons-10.imp
 examples/oopsla/coupons-10.imp : 0.017s : [Success] 110
processing ... examples/oopsla/coupons-100.imp
 examples/oopsla/coupons-100.imp : 1.223s : [Success] 10100
processing ... examples/oopsla/coupons-50.imp
 examples/oopsla/coupons-50.imp : 0.323s : [Success] 2550
processing ... examples/oopsla/coupons-N.pwhile
 examples/oopsla/coupons-N.pwhile : 0.181s : [Success] 1/2 + <N> + 1/2·<N^2>
processing ... examples/oopsla/nest-2.pwhile
 examples/oopsla/nest-2.pwhile : 0.077s : [Success] 4·<1 + 2·(n) + n^2> + <1 + n>
processing ... examples/oopsla/nest-3.pwhile
 examples/oopsla/nest-3.pwhile : 60.00s : [Timeout]
processing ... examples/oopsla/queueing-network.pwhile
 examples/oopsla/queueing-network.pwhile : 29.67s : [Success] 2·<-1 + -n> + 4/125·<1 + n> + 3/250·<1 + 2·(n) + n^2>
processing ... examples/oopsla/trader-10.pwhile
 examples/oopsla/trader-10.pwhile : 0.043s : [Success] 10·<-min + min·price + -min^2 + price> + 5·<-2·(min·price) + min^2 + price^2>
processing ... examples/oopsla/trader-100.pwhile
 examples/oopsla/trader-100.pwhile : 0.049s : [Success] 100·<-min + min·price + -min^2 + price> + 50·<-2·(min·price) + min^2 + price^2>
processing ... examples/oopsla/trader-1000.pwhile
 examples/oopsla/trader-1000.pwhile : 0.070s : [Success] 1000·<-min + min·price + -min^2 + price> + 500·<-2·(min·price) + min^2 + price^2>
processing ... examples/oopsla/trader-10000.pwhile
 examples/oopsla/trader-10000.pwhile : 0.280s : [Success] 10000·<-min + min·price + -min^2 + price> + 5000·<-2·(min·price) + min^2 + price^2>
processing ... examples/oopsla/trader-100000.pwhile
 examples/oopsla/trader-100000.pwhile : 2.707s : [Success] 100000·<-min + min·price + -min^2 + price> + 50000·<-2·(min·price) + min^2 + price^2>
processing ... examples/oopsla/trader-1000000.pwhile
 examples/oopsla/trader-1000000.pwhile : 34.98s : [Success] 1000000·<-min + min·price + -min^2 + price> + 500000·<-2·(min·price) + min^2 + price^2>
processing ... examples/oopsla/trader-50.pwhile
 examples/oopsla/trader-50.pwhile : 0.041s : [Success] 50·<-min + min·price + -min^2 + price> + 25·<-2·(min·price) + min^2 + price^2>
processing ... examples/oopsla/trader-500.pwhile
 examples/oopsla/trader-500.pwhile : 0.052s : [Success] 500·<-min + min·price + -min^2 + price> + 250·<-2·(min·price) + min^2 + price^2>
processing ... examples/oopsla/trader-5000.pwhile
 examples/oopsla/trader-5000.pwhile : 0.139s : [Success] 5000·<-min + min·price + -min^2 + price> + 2500·<-2·(min·price) + min^2 + price^2>
processing ... examples/oopsla/trader-N.pwhile
 examples/oopsla/trader-N.pwhile : 3.080s : [Failed ]
processing ... examples/oopsla/absynthLinear/2drwalk.imp
 examples/oopsla/absynthLinear/2drwalk.imp : 0.031s : [Success] [n ≥ 1 + d]·2·(1 + -d + n)
processing ... examples/oopsla/absynthLinear/C4B_t09.imp
 examples/oopsla/absynthLinear/C4B_t09.imp : 0.007s : [Success] [x ≥ 1]·41·(x)
processing ... examples/oopsla/absynthLinear/C4B_t13.imp
 examples/oopsla/absynthLinear/C4B_t13.imp : 0.008s : [Success] [x ≥ 1 ∧ y ≥ 0]·(5/4·(x) + y)
processing ... examples/oopsla/absynthLinear/C4B_t15.imp
 examples/oopsla/absynthLinear/C4B_t15.imp : 0.171s : [Failed ]
processing ... examples/oopsla/absynthLinear/C4B_t15_2.imp
 examples/oopsla/absynthLinear/C4B_t15_2.imp : 0.004s : [Success] [x ≥ 0 ∧ x ≥ 1 + y ∧ y ≥ 0]·(1 + x)
processing ... examples/oopsla/absynthLinear/C4B_t19.imp
 examples/oopsla/absynthLinear/C4B_t19.imp : 0.012s : [Success] ite(i ≥ 101,2·(-100 + i) + 51 + i + k,[50 + i + k ≥ 0]·(51 + i + k))
processing ... examples/oopsla/absynthLinear/C4B_t30.imp
 examples/oopsla/absynthLinear/C4B_t30.imp : 0.008s : [Failed ]
processing ... examples/oopsla/absynthLinear/C4B_t30_2.imp
 examples/oopsla/absynthLinear/C4B_t30_2.imp : 0.001s : [Success] [x ≥ 1 ∧ y ≥ -1]·(2·(2 + y) + 2·(x))
processing ... examples/oopsla/absynthLinear/C4B_t61.imp
 examples/oopsla/absynthLinear/C4B_t61.imp : 0.011s : [Success] ite(l ≥ 8,10·(-7 + l) + 7,[l ≥ 1]·(l))
processing ... examples/oopsla/absynthLinear/bayesian.imp
 examples/oopsla/absynthLinear/bayesian.imp : 0.002s : [Success] [n ≥ 1]·4·(n)
processing ... examples/oopsla/absynthLinear/ber.imp
 examples/oopsla/absynthLinear/ber.imp : 0.001s : [Success] [n ≥ 1 + x]·(n + -x)
processing ... examples/oopsla/absynthLinear/bin.imp
 examples/oopsla/absynthLinear/bin.imp : 0.001s : [Success] [n ≥ 1 + x]·(n + -x)
processing ... examples/oopsla/absynthLinear/condand.imp
 examples/oopsla/absynthLinear/condand.imp : 0.002s : [Success] [m ≥ 1 ∧ n ≥ 1]·2·(m)
processing ... examples/oopsla/absynthLinear/cooling.imp
 examples/oopsla/absynthLinear/cooling.imp : 0.023s : [Success] [t ≥ 0]·(21/10·(1 + t) + mt + -st)
processing ... examples/oopsla/absynthLinear/filling.imp
 examples/oopsla/absynthLinear/filling.imp : 0.008s : [Success] [volToFill ≥ 0]·3/5·(1 + volToFill) + [volToFill ≥ 1]·3/5·(volToFill)
processing ... examples/oopsla/absynthLinear/linear01.imp
 examples/oopsla/absynthLinear/linear01.imp : 0.001s : [Success] [x ≥ 2]·(-1 + x)
processing ... examples/oopsla/absynthLinear/miner.imp
 examples/oopsla/absynthLinear/miner.imp : 0.002s : [Success] [n ≥ 1]·15/2·(n)
processing ... examples/oopsla/absynthLinear/prdwalk.imp
 examples/oopsla/absynthLinear/prdwalk.imp : 0.002s : [Success] [n ≥ 1 + x]·40/13·(n + -x)
processing ... examples/oopsla/absynthLinear/prnes.imp
 examples/oopsla/absynthLinear/prnes.imp : 0.737s : [Success] [0 ≥ 1 + n ∧ y ≥ 0]·(50/9·(99·(n) + -n·y) + 250000/81·(n^2))
processing ... examples/oopsla/absynthLinear/prseq.imp
 examples/oopsla/absynthLinear/prseq.imp : 0.017s : [Success] [y ≥ 10]·ite(x + -y ≥ 3,3·(-2 + x + -y) + 9/4·(-2 + x + -y) + 3/2·(-9 + y),[y ≥ 10]·3/2·(-9 + y))
processing ... examples/oopsla/absynthLinear/prspeed.imp
 examples/oopsla/absynthLinear/prspeed.imp : 0.019s : [Success] [n ≥ 3 + x]·(4/3·(-2 + n + -x) + 2·(m + -y))
processing ... examples/oopsla/absynthLinear/race.imp
 examples/oopsla/absynthLinear/race.imp : 0.014s : [Success] [t ≥ h]·11/6·(3 + -h + t)
processing ... examples/oopsla/absynthLinear/rdseql.imp
 examples/oopsla/absynthLinear/rdseql.imp : 0.014s : [Success] [x ≥ 1 ∧ y ≥ 0]·(9/4·(x) + y)
processing ... examples/oopsla/absynthLinear/rdspeed.imp
 examples/oopsla/absynthLinear/rdspeed.imp : 0.016s : [Success] [n ≥ 3 + x]·(4/3·(-2 + n + -x) + 2·(m + -y))
processing ... examples/oopsla/absynthLinear/rdwalk.imp
 examples/oopsla/absynthLinear/rdwalk.imp : 0.003s : [Success] [n ≥ 1 + x]·2·(1 + n + -x)
processing ... examples/oopsla/absynthLinear/robot.imp
 examples/oopsla/absynthLinear/robot.imp : 0.006s : [Success] [N ≥ 1]·5/4·(N)
processing ... examples/oopsla/absynthLinear/roulette.imp
 examples/oopsla/absynthLinear/roulette.imp : 0.049s : [Success] [10 ≥ n]·74/15·(21 + -n)
processing ... examples/oopsla/absynthLinear/sampling.imp
 examples/oopsla/absynthLinear/sampling.imp : 0.002s : [Success] [n ≥ 1]·2·(n)
processing ... examples/oopsla/absynthLinear/sprdwalk.imp
 examples/oopsla/absynthLinear/sprdwalk.imp : 0.001s : [Success] [n ≥ 1 + x]·2·(n + -x)
processing ... examples/oopsla/absynthPolynomial/complex.imp
 examples/oopsla/absynthPolynomial/complex.imp : 0.181s : [Success] [M ≥ 0 ∧ y ≥ 0]·ite(N ≥ 1,6·(3·(M·N) + 2·(N)) + w + 3·(y),[y ≥ 1]·(w + 3·(y)))
processing ... examples/oopsla/absynthPolynomial/multirace.imp
 examples/oopsla/absynthPolynomial/multirace.imp : 0.018s : [Success] [m ≥ 0 ∧ n ≥ 1]·4·(m·n + n)
processing ... examples/oopsla/absynthPolynomial/pol04.imp
 examples/oopsla/absynthPolynomial/pol04.imp : 0.017s : [Success] [x ≥ 1]·(15/2·(x) + 9/2·(x^2))
processing ... examples/oopsla/absynthPolynomial/pol05.imp
 examples/oopsla/absynthPolynomial/pol05.imp : 0.019s : [Success] [x ≥ 1]·(5/8·(x) + 5/4·(x^2))
processing ... examples/oopsla/absynthPolynomial/pol06.imp
 examples/oopsla/absynthPolynomial/pol06.imp : 0.019s : [Success] [minPrice ≥ 0 ∧ sPrice ≥ 1 + minPrice]·8/3·(-minPrice + sPrice)
processing ... examples/oopsla/absynthPolynomial/pol07.imp
 examples/oopsla/absynthPolynomial/pol07.imp : 0.022s : [Success] [n ≥ 2]·3/2·(1 + -2·(n) + n^2)
processing ... examples/oopsla/absynthPolynomial/rdbub.imp
 examples/oopsla/absynthPolynomial/rdbub.imp : 0.009s : [Success] [n ≥ 1]·(n + n^2)
processing ... examples/oopsla/absynthPolynomial/trader.imp
 examples/oopsla/absynthPolynomial/trader.imp : 0.057s : [Success] ite(sPrice ≥ 1 + minPrice,3·(-minPrice + -minPrice·sPrice + sPrice + sPrice^2) + z,z)
processing ... examples/oopsla/bridge.imp
 examples/oopsla/bridge.imp : 0.009s : [Success] [b ≥ 1 + x ∧ x ≥ 1 + a]·(-a·b + a·x + b·x + -x^2)
processing ... examples/oopsla/coupons.imp
 examples/oopsla/coupons.imp : 0.195s : [Success] [N ≥ 1]·(1/2 + N + 1/2·(N^2))
processing ... examples/oopsla/geo.imp
 examples/oopsla/geo.imp : 0.001s : [Success] [1 ≥ b ∧ b ≥ 1]·2·(b)
processing ... examples/oopsla/trader.imp
 examples/oopsla/trader.imp : 0.068s : [Success] [min ≥ 0 ∧ price ≥ 1 + min]·9/2·(1 + 2·(price) + price^2)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment