# data * SAT 1345 * UNSAT 0 * TIMEOUT 594 * UNKNOWN 0 * UNSET 61 * ERROR 61 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: smt-sat-bv
Z3 repo: https://github.com/Z3Prover/z3
Z3 commit: b870ed192ada7f98d3a98c8140a2b1899ef09449
Z3 branch: sls
Z3 options: "-T:20 -v:2 smt.sls.enable=false sat.smt=true -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify smt)" model_validate=true"
Z3 inputs: inputs/QF_BV_SAT
Z3 commit message: include disequality expansion for non-unit case.

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |bench_6998.smt2 | 0.005s | 18.504MiB| sat | 0 | | | |bench_8073.smt2 | 0.005s | 18.256MiB| sat | 0 | | | |try5_small_true_functions_dwp_yes.close_stdout_set_file_name.il.dwp.smt2 | 0.005s | 18.252MiB| sat | 0 | | | |bench_3707.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_3750.smt2 | 0.006s | 18.76MiB| sat | 0 | | | |bench_868.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_6954.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_302.smt2 | 0.006s | 18.384MiB| sat | 0 | | | |bench_3964.smt2 | 0.006s | 18.744MiB| sat | 0 | | | |bench_4642.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_4968.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_8116.smt2 | 0.006s | 18.248MiB| sat | 0 | | | |bench_1957.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_8103.smt2 | 0.006s | 18.48MiB| sat | 0 | | | |bench_4219.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_1187.smt2 | 0.006s | 18.76MiB| sat | 0 | | | |bench_7758.smt2 | 0.006s | 18.248MiB| sat | 0 | | | |bench_3416.smt2 | 0.006s | 18.424MiB| sat | 0 | | | |bench_7495.smt2 | 0.006s | 18.588MiB| sat | 0 | | | |bench_3048.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_6906.smt2 | 0.006s | 18.26MiB| sat | 0 | | | |bench_7083.smt2 | 0.006s | 18.76MiB| sat | 0 | | | |bench_4644.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_5645.smt2 | 0.006s | 18.508MiB| sat | 0 | | | |bench_3539.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_3358.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_7872.smt2 | 0.006s | 18.516MiB| sat | 0 | | | |bench_4706.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_7834.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_8296.smt2 | 0.006s | 18.648MiB| sat | 0 | | | |bench_5408.smt2 | 0.006s | 18.76MiB| sat | 0 | | | |bench_883.smt2 | 0.006s | 18.76MiB| sat | 0 | | | |bench_165.smt2 | 0.006s | 18.416MiB| sat | 0 | | | |bench_7565.smt2 | 0.006s | 18.76MiB| sat | 0 | | | |bench_7573.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_6756.smt2 | 0.006s | 18.512MiB| sat | 0 | | | |a97test0001.smt2 | 0.006s | 18.248MiB| sat | 0 | | | |bench_7663.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_7696.smt2 | 0.006s | 18.216MiB| sat | 0 | | | |bench_8054.smt2 | 0.006s | 18.48MiB| sat | 0 | | | |bench_3894.smt2 | 0.006s | 18.268MiB| sat | 0 | | | |bench_7823.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_3623.smt2 | 0.006s | 18.328MiB| sat | 0 | | | |bench_295.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_2432.smt2 | 0.006s | 18.264MiB| sat | 0 | | | |bench_4971.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_4662.smt2 | 0.006s | 18.76MiB| sat | 0 | | | |bench_5674.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_4834.smt2 | 0.006s | 18.76MiB| sat | 0 | | | |bench_4319.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_3719.smt2 | 0.006s | 18.76MiB| sat | 0 | | | |bench_5187.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_1629.smt2 | 0.006s | 18.248MiB| sat | 0 | | | |bench_7765.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_6886.smt2 | 0.006s | 18.512MiB| sat | 0 | | | |bvsdiv.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_4387.smt2 | 0.006s | 18.512MiB| sat | 0 | | | |bench_15.smt2 | 0.006s | 18.476MiB| sat | 0 | | | |bench_497.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_168.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_4321.smt2 | 0.006s | 18.508MiB| sat | 0 | | | |bench_1055.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_5238.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_1863.smt2 | 0.006s | 18.76MiB| sat | 0 | | | |bench_3335.smt2 | 0.006s | 18.516MiB| sat | 0 | | | |bench_789.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_2308.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_3578.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_4820.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_6867.smt2 | 0.006s | 18.76MiB| sat | 0 | | | |bench_92.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_5210.smt2 | 0.006s | 18.256MiB| sat | 0 | | | |bench_7811.smt2 | 0.006s | 18.76MiB| sat | 0 | | | |bench_2551.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_8088.smt2 | 0.006s | 18.164MiB| sat | 0 | | | |adpcm.smt2 | 0.006s | 18.508MiB| sat | 0 | | | |bench_7319.smt2 | 0.006s | 18.512MiB| sat | 0 | | | |bench_1453.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_179.smt2 | 0.006s | 18.504MiB| sat | 0 | | | |bench_7454.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_2188.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_7274.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_5309.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_4568.smt2 | 0.007s | 18.48MiB| sat | 0 | | | |bench_3475.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_1059.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_2558.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_4273.smt2 | 0.007s | 18.256MiB| sat | 0 | | | |bench_3421.smt2 | 0.007s | 18.508MiB| sat | 0 | | | |bench_3881.smt2 | 0.007s | 18.256MiB| sat | 0 | | | |a407test0024.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |a213test0012.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_7517.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_4628.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_1869.smt2 | 0.007s | 18.764MiB| sat | 0 | | | |bench_120.smt2 | 0.007s | 18.52MiB| sat | 0 | | | |bench_8379.smt2 | 0.007s | 18.42MiB| sat | 0 | | | |bench_4576.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_6830.smt2 | 0.007s | 18.736MiB| sat | 0 | | | |bench_6713.smt2 | 0.007s | 19.016MiB| sat | 0 | | | |bench_4526.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_565.smt2 | 0.007s | 18.48MiB| sat | 0 | | | |bench_7219.smt2 | 0.007s | 18.804MiB| sat | 0 | | | |bench_5649.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_3963.smt2 | 0.007s | 18.256MiB| sat | 0 | | | |bench_3352.smt2 | 0.007s | 18.284MiB| sat | 0 | | | |a333test0009.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_2524.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_4635.smt2 | 0.007s | 18.736MiB| sat | 0 | | | |bench_3329.smt2 | 0.007s | 18.608MiB| sat | 0 | | | |a58test0007.smt2 | 0.007s | 18.764MiB| sat | 0 | | | |bench_965.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_5613.smt2 | 0.007s | 18.736MiB| sat | 0 | | | |bench_3308.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_301.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_7655.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_348.smt2 | 0.007s | 19.016MiB| sat | 0 | | | |bench_7415.smt2 | 0.007s | 18.824MiB| sat | 0 | | | |bench_1963.smt2 | 0.007s | 18.544MiB| sat | 0 | | | |bench_5666.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |a397test0029.smt2 | 0.007s | 18.728MiB| sat | 0 | | | |bench_7532.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_3636.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_7138.smt2 | 0.007s | 18.616MiB| sat | 0 | | | |a128test0016.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_7489.smt2 | 0.007s | 18.348MiB| sat | 0 | | | |a614test0091.smt2 | 0.007s | 18.26MiB| sat | 0 | | | |bench_5123.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_2727.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_919.smt2 | 0.007s | 19.016MiB| sat | 0 | | | |bench_3834.smt2 | 0.007s | 18.772MiB| sat | 0 | | | |bench_5155.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_5432.smt2 | 0.007s | 18.464MiB| sat | 0 | | | |bench_3765.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_7671.smt2 | 0.007s | 18.952MiB| sat | 0 | | | |bench_5360.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_1442.smt2 | 0.007s | 18.736MiB| sat | 0 | | | |bench_7673.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_1283.smt2 | 0.007s | 18.508MiB| sat | 0 | | | |bench_2521.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_wc.quoting_options_from_style.il.flanagansaxe.smt2 | 0.007s | 19.028MiB| sat | 0 | | | |a640test0019.smt2 | 0.007s | 18.52MiB| sat | 0 | | | |bench_7270.smt2 | 0.007s | 18.744MiB| sat | 0 | | | |a689test0069.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_2676.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_288.smt2 | 0.007s | 18.448MiB| sat | 0 | | | |bench_8228.smt2 | 0.007s | 18.52MiB| sat | 0 | | | |bench_2517.smt2 | 0.007s | 18.26MiB| sat | 0 | | | |bench_8049.smt2 | 0.007s | 18.34MiB| sat | 0 | | | |bench_5183.smt2 | 0.007s | 18.232MiB| sat | 0 | | | |bench_5440.smt2 | 0.007s | 18.524MiB| sat | 0 | | | |bench_5218.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_6828.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_78.smt2 | 0.007s | 18.896MiB| sat | 0 | | | |bench_113.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_4965.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_7828.smt2 | 0.007s | 18.408MiB| sat | 0 | | | |bench_7800.smt2 | 0.007s | 18.736MiB| sat | 0 | | | |bench_306.smt2 | 0.007s | 19.016MiB| sat | 0 | | | |bench_7867.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_456.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_7139.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_7166.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_2779.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_4522.smt2 | 0.007s | 18.536MiB| sat | 0 | | | |bench_1630.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_375.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_720.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_3431.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_2983.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_7575.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_7182.smt2 | 0.007s | 18.78MiB| sat | 0 | | | |bench_926.smt2 | 0.007s | 18.648MiB| sat | 0 | | | |bench_4581.smt2 | 0.007s | 18.784MiB| sat | 0 | | | |bench_8082.smt2 | 0.007s | 18.468MiB| sat | 0 | | | |bench_988.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_7310.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_1627.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_7670.smt2 | 0.007s | 19.016MiB| sat | 0 | | | |bench_7819.smt2 | 0.007s | 18.736MiB| sat | 0 | | | |bench_7749.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_7833.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_1720.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |unconstrained10.smt2 | 0.007s | 18.764MiB| sat | 0 | | | |a631test0073.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_1759.smt2 | 0.007s | 18.256MiB| sat | 0 | | | |bench_2070.smt2 | 0.007s | 18.26MiB| sat | 0 | | | |bench_6734.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_3755.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_4650.smt2 | 0.007s | 18.256MiB| sat | 0 | | | |bench_4160.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_5765.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_2811.smt2 | 0.007s | 18.256MiB| sat | 0 | | | |a218test0003.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_7627.smt2 | 0.007s | 18.516MiB| sat | 0 | | | |bench_2358.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_2075.smt2 | 0.007s | 18.524MiB| sat | 0 | | | |bench_2671.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_8084.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_7943.smt2 | 0.007s | 18.252MiB| sat | 0 | | | |bench_3882.smt2 | 0.007s | 18.324MiB| sat | 0 | | | |bench_4520.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_8110.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_8282.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_3558.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_2384.smt2 | 0.007s | 18.764MiB| sat | 0 | | | |bench_7863.smt2 | 0.007s | 18.464MiB| sat | 0 | | | |bench_1864.smt2 | 0.007s | 18.632MiB| sat | 0 | | | |bench_8019.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |a695test0015.smt2 | 0.007s | 18.78MiB| sat | 0 | | | |bench_4627.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_5543.smt2 | 0.007s | 18.788MiB| sat | 0 | | | |bench_5190.smt2 | 0.007s | 18.476MiB| sat | 0 | | | |bench_2264.smt2 | 0.007s | 18.252MiB| sat | 0 | | | |bench_4990.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_160.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_4985.smt2 | 0.007s | 18.256MiB| sat | 0 | | | |bench_685.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |try5_small_true_functions_flanagansaxe_vdir.unsigned_file_size.il.flanagansaxe.smt2 | 0.007s | 18.624MiB| sat | 0 | | | |bench_303.smt2 | 0.007s | 18.324MiB| sat | 0 | | | |bench_8289.smt2 | 0.007s | 18.288MiB| sat | 0 | | | |bench_4157.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_3469.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bitops7.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_5.smt2 | 0.007s | 18.268MiB| sat | 0 | | | |a657test0107.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_5222.smt2 | 0.007s | 18.456MiB| sat | 0 | | | |bench_317.smt2 | 0.007s | 18.608MiB| sat | 0 | | | |bench_7033.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_3997.smt2 | 0.007s | 18.48MiB| sat | 0 | | | |bench_7534.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_1888.smt2 | 0.007s | 18.492MiB| sat | 0 | | | |bench_3394.smt2 | 0.007s | 18.244MiB| sat | 0 | | | |bench_2755.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_8200.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_838.smt2 | 0.007s | 18.476MiB| sat | 0 | | | |bench_7412.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_8093.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_91.smt2 | 0.007s | 18.572MiB| sat | 0 | | | |bench_7024.smt2 | 0.007s | 18.66MiB| sat | 0 | | | |a663test0096.smt2 | 0.007s | 18.256MiB| sat | 0 | | | |bench_3062.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_5154.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_1495.smt2 | 0.007s | 18.78MiB| sat | 0 | | | |bench_163.smt2 | 0.007s | 18.488MiB| sat | 0 | | | |bench_748.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_8393.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_3879.smt2 | 0.007s | 18.204MiB| sat | 0 | | | |bench_204.smt2 | 0.007s | 18.304MiB| sat | 0 | | | |bench_3103.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_2149.smt2 | 0.007s | 18.256MiB| sat | 0 | | | |bench_5005.smt2 | 0.007s | 18.648MiB| sat | 0 | | | |bench_2148.smt2 | 0.007s | 18.68MiB| sat | 0 | | | |bench_8170.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_4508.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |a185test0001.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_8507.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_5636.smt2 | 0.007s | 18.256MiB| sat | 0 | | | |bench_7304.smt2 | 0.007s | 18.276MiB| sat | 0 | | | |bench_4112.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_6731.smt2 | 0.007s | 18.736MiB| sat | 0 | | | |bench_2548.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_5209.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_8306.smt2 | 0.007s | 18.596MiB| sat | 0 | | | |bench_1478.smt2 | 0.007s | 19.0MiB| sat | 0 | | | |bench_1900.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_6923.smt2 | 0.007s | 18.472MiB| sat | 0 | | | |bench_8309.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_7465.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_4580.smt2 | 0.007s | 18.764MiB| sat | 0 | | | |bench_2431.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_4555.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_7842.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_7142.smt2 | 0.007s | 18.52MiB| sat | 0 | | | |bench_4375.smt2 | 0.007s | 18.792MiB| sat | 0 | | | |bench_7088.smt2 | 0.007s | 18.508MiB| sat | 0 | | | |bench_1748.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_957.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_7641.smt2 | 0.007s | 19.012MiB| sat | 0 | | | |bench_8315.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_7086.smt2 | 0.007s | 18.752MiB| sat | 0 | | | |bench_2309.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_535.smt2 | 0.007s | 18.576MiB| sat | 0 | | | |bench_3757.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_7835.smt2 | 0.007s | 18.992MiB| sat | 0 | | | |bench_2175.smt2 | 0.007s | 18.804MiB| sat | 0 | | | |bench_7375.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_2750.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_3548.smt2 | 0.007s | 19.016MiB| sat | 0 | | | |bench_4279.smt2 | 0.007s | 18.836MiB| sat | 0 | | | |bench_5192.smt2 | 0.007s | 18.356MiB| sat | 0 | | | |bench_5159.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_6953.smt2 | 0.007s | 18.212MiB| sat | 0 | | | |bench_1946.smt2 | 0.007s | 18.484MiB| sat | 0 | | | |bench_6966.smt2 | 0.007s | 18.508MiB| sat | 0 | | | |bench_4818.smt2 | 0.007s | 18.248MiB| sat | 0 | | | |bench_3936.smt2 | 0.007s | 18.256MiB| sat | 0 | | | |bench_3476.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_7329.smt2 | 0.007s | 18.58MiB| sat | 0 | | | |bench_4920.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_4175.smt2 | 0.007s | 18.508MiB| sat | 0 | | | |bench_2072.smt2 | 0.007s | 18.416MiB| sat | 0 | | | |bench_4654.smt2 | 0.007s | 18.508MiB| sat | 0 | | | |a664test0013.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |a409test0002.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_864.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_7881.smt2 | 0.007s | 18.42MiB| sat | 0 | | | |bench_296.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_6986.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_3866.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |b265test0001.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_6861.smt2 | 0.007s | 18.432MiB| sat | 0 | | | |bench_3206.smt2 | 0.007s | 18.256MiB| sat | 0 | | | |bench_4137.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_2729.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_4156.smt2 | 0.007s | 18.512MiB| sat | 0 | | | |bench_8512.smt2 | 0.007s | 18.756MiB| sat | 0 | | | |bench_2312.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_2552.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_4768.smt2 | 0.007s | 18.516MiB| sat | 0 | | | |a222test0008.smt2 | 0.007s | 18.768MiB| sat | 0 | | | |bench_2642.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_3087.smt2 | 0.007s | 18.592MiB| sat | 0 | | | |bench_3671.smt2 | 0.007s | 18.76MiB| sat | 0 | | | |bench_5165.smt2 | 0.007s | 18.508MiB| sat | 0 | | | |bench_4019.smt2 | 0.007s | 18.504MiB| sat | 0 | | | |bench_457.smt2 | 0.007s | 18.828MiB| sat | 0 | | | |bench_4397.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_4007.smt2 | 0.008s | 19.028MiB| sat | 0 | | | |run_03230.trace.cond_000028_0x40201f_00.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_3268.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |bench_5153.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |a503test0089.smt2 | 0.008s | 19.024MiB| sat | 0 | | | |bench_1873.smt2 | 0.008s | 19.024MiB| sat | 0 | | | |bench_1697.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_1338.smt2 | 0.008s | 18.532MiB| sat | 0 | | | |bench_8271.smt2 | 0.008s | 18.48MiB| sat | 0 | | | |bench_7552.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |a665test0064.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_4350.smt2 | 0.008s | 18.452MiB| sat | 0 | | | |bench_2291.smt2 | 0.008s | 18.576MiB| sat | 0 | | | |bench_941.smt2 | 0.008s | 18.728MiB| sat | 0 | | | |bench_7539.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_3018.smt2 | 0.008s | 18.308MiB| sat | 0 | | | |bench_1455.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_7556.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_7388.smt2 | 0.008s | 18.524MiB| sat | 0 | | | |bench_6973.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_2839.smt2 | 0.008s | 18.768MiB| sat | 0 | | | |bench_4164.smt2 | 0.008s | 18.996MiB| sat | 0 | | | |bench_709.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |try5_small_noof_functions_dwp_expr.nomoreargs.il.dwp.smt2 | 0.008s | 18.84MiB| sat | 0 | | | |a668test0098.smt2 | 0.008s | 18.768MiB| sat | 0 | | | |bench_7021.smt2 | 0.008s | 18.668MiB| sat | 0 | | | |bench_8394.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_527.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_1476.smt2 | 0.008s | 19.528MiB| sat | 0 | | | |bench_200.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_2386.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_7242.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_4046.smt2 | 0.008s | 19.248MiB| sat | 0 | | | |bench_881.smt2 | 0.008s | 19.168MiB| sat | 0 | | | |bench_3333.smt2 | 0.008s | 18.256MiB| sat | 0 | | | |bench_706.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_4312.smt2 | 0.008s | 18.256MiB| sat | 0 | | | |bench_8344.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |a430test0028.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_7736.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_2129.smt2 | 0.008s | 18.26MiB| sat | 0 | | | |bench_7550.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |a601test0056.smt2 | 0.008s | 19.528MiB| sat | 0 | | | |bench_4021.smt2 | 0.008s | 18.596MiB| sat | 0 | | | |bench_1233.smt2 | 0.008s | 18.256MiB| sat | 0 | | | |bench_8165.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_4023.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_7278.smt2 | 0.008s | 18.992MiB| sat | 0 | | | |bench_28.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |bench_1905.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_7496.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_7146.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_2704.smt2 | 0.008s | 18.92MiB| sat | 0 | | | |bench_7498.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_7973.smt2 | 0.008s | 18.256MiB| sat | 0 | | | |bench_2108.smt2 | 0.008s | 18.84MiB| sat | 0 | | | |bench_3094.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |bench_5658.smt2 | 0.008s | 18.508MiB| sat | 0 | | | |bench_7807.smt2 | 0.008s | 18.248MiB| sat | 0 | | | |bench_2876.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_1761.smt2 | 0.008s | 18.516MiB| sat | 0 | | | |bench_1123.smt2 | 0.008s | 18.676MiB| sat | 0 | | | |bench_3509.smt2 | 0.008s | 18.736MiB| sat | 0 | | | |bench_8117.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_6699.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_7633.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_5188.smt2 | 0.008s | 18.656MiB| sat | 0 | | | |bench_900.smt2 | 0.008s | 18.248MiB| sat | 0 | | | |bench_1739.smt2 | 0.008s | 19.248MiB| sat | 0 | | | |bench_234.smt2 | 0.008s | 18.532MiB| sat | 0 | | | |bench_7119.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_4954.smt2 | 0.008s | 18.768MiB| sat | 0 | | | |a616test0001.smt2 | 0.008s | 18.576MiB| sat | 0 | | | |bench_1253.smt2 | 0.008s | 19.272MiB| sat | 0 | | | |bench_2701.smt2 | 0.008s | 18.46MiB| sat | 0 | | | |a55test0003.smt2 | 0.008s | 19.036MiB| sat | 0 | | | |bench_7705.smt2 | 0.008s | 18.416MiB| sat | 0 | | | |bench_4626.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_6938.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_4518.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |try3_noof_functions_dwp_touch.yyerror.il.dwp.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |a217test0011.smt2 | 0.008s | 18.248MiB| sat | 0 | | | |bench_7537.smt2 | 0.008s | 18.584MiB| sat | 0 | | | |bench_5131.smt2 | 0.008s | 18.828MiB| sat | 0 | | | |bench_1111.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |bench_6837.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_259.smt2 | 0.008s | 18.764MiB| sat | 0 | | | |run_03230.trace.cond_000032_0x40248d_00.smt2 | 0.008s | 18.768MiB| sat | 0 | | | |run_00000.trace.Alloc_zero__011273.smt2 | 0.008s | 18.78MiB| sat | 0 | | | |a683test0094.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |a392test0051.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_238.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |a620test0100.smt2 | 0.008s | 19.248MiB| sat | 0 | | | |bench_1386.smt2 | 0.008s | 18.516MiB| sat | 0 | | | |bench_1405.smt2 | 0.008s | 18.768MiB| sat | 0 | | | |bench_4494.smt2 | 0.008s | 18.428MiB| sat | 0 | | | |bench_964.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |bench_991.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_975.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_76.smt2 | 0.008s | 18.768MiB| sat | 0 | | | |bench_7528.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_4788.smt2 | 0.008s | 18.572MiB| sat | 0 | | | |bench_2612.smt2 | 0.008s | 19.02MiB| sat | 0 | | | |bench_7563.smt2 | 0.008s | 18.828MiB| sat | 0 | | | |bench_8320.smt2 | 0.008s | 18.488MiB| sat | 0 | | | |bench_5303.smt2 | 0.008s | 18.768MiB| sat | 0 | | | |bench_1082.smt2 | 0.008s | 18.768MiB| sat | 0 | | | |bench_1583.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_979.smt2 | 0.008s | 18.928MiB| sat | 0 | | | |bench_7229.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_4617.smt2 | 0.008s | 18.344MiB| sat | 0 | | | |bench_248.smt2 | 0.008s | 18.608MiB| sat | 0 | | | |bench_3275.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_5077.smt2 | 0.008s | 18.58MiB| sat | 0 | | | |bench_4906.smt2 | 0.008s | 18.82MiB| sat | 0 | | | |bench_6857.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_214.smt2 | 0.008s | 18.992MiB| sat | 0 | | | |bench_2550.smt2 | 0.008s | 18.216MiB| sat | 0 | | | |bench_2435.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_5170.smt2 | 0.008s | 18.592MiB| sat | 0 | | | |bench_2044.smt2 | 0.008s | 18.488MiB| sat | 0 | | | |bench_7188.smt2 | 0.008s | 18.524MiB| sat | 0 | | | |bench_7832.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_2150.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_8234.smt2 | 0.008s | 18.488MiB| sat | 0 | | | |bench_4689.smt2 | 0.008s | 18.524MiB| sat | 0 | | | |bench_285.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |bench_7140.smt2 | 0.008s | 18.532MiB| sat | 0 | | | |try5_small_true_functions_flanagansaxe_join.initseq.il.flanagansaxe.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_7438.smt2 | 0.008s | 19.272MiB| sat | 0 | | | |bench_3338.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_4065.smt2 | 0.008s | 18.516MiB| sat | 0 | | | |bench_7714.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_1770.smt2 | 0.008s | 18.568MiB| sat | 0 | | | |bench_4921.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_3307.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |bench_3915.smt2 | 0.008s | 18.992MiB| sat | 0 | | | |bench_5127.smt2 | 0.008s | 18.248MiB| sat | 0 | | | |bench_8294.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_6843.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |a393test0014.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_4692.smt2 | 0.008s | 18.496MiB| sat | 0 | | | |bench_7095.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_7878.smt2 | 0.008s | 18.776MiB| sat | 0 | | | |bench_3489.smt2 | 0.008s | 18.632MiB| sat | 0 | | | |bench_243.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_6924.smt2 | 0.008s | 18.736MiB| sat | 0 | | | |bench_1665.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_4908.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_2493.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_4696.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_7729.smt2 | 0.008s | 18.852MiB| sat | 0 | | | |bench_5139.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_639.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_1017.smt2 | 0.008s | 18.744MiB| sat | 0 | | | |try5_small_true_functions_flanagansaxe_md5sum.md5_init_ctx.il.flanagansaxe.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_6826.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_3688.smt2 | 0.008s | 18.256MiB| sat | 0 | | | |bench_5417.smt2 | 0.008s | 18.236MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_seq.quoting_options_from_style.il.flanagansaxe.smt2 | 0.008s | 19.276MiB| sat | 0 | | | |bench_4516.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_4839.smt2 | 0.008s | 18.548MiB| sat | 0 | | | |bench_5752.smt2 | 0.008s | 18.256MiB| sat | 0 | | | |bench_6917.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_unexpand.quoting_options_from_style.il.flanagansaxe.smt2 | 0.008s | 19.272MiB| sat | 0 | | | |a685test0080.smt2 | 0.008s | 18.768MiB| sat | 0 | | | |bench_4010.smt2 | 0.008s | 18.992MiB| sat | 0 | | | |bench_3754.smt2 | 0.008s | 18.82MiB| sat | 0 | | | |QF_BV_counter_v_cc_ref_max.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |b188test0002.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_1280.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |a448test0003.smt2 | 0.008s | 19.032MiB| sat | 0 | | | |bench_938.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |a164test0005.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |bench_7523.smt2 | 0.008s | 18.516MiB| sat | 0 | | | |try5_small_true_functions_flanagansaxe_chgrp.i_ring_init.il.flanagansaxe.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_4058.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_954.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |bench_8298.smt2 | 0.008s | 18.248MiB| sat | 0 | | | |bench_7070.smt2 | 0.008s | 18.764MiB| sat | 0 | | | |bench_4840.smt2 | 0.008s | 18.26MiB| sat | 0 | | | |a676test0004.smt2 | 0.008s | 18.992MiB| sat | 0 | | | |bench_1143.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_500.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_1976.smt2 | 0.008s | 18.456MiB| sat | 0 | | | |bench_119.smt2 | 0.008s | 18.764MiB| sat | 0 | | | |bench_1757.smt2 | 0.008s | 18.788MiB| sat | 0 | | | |a623test0035.smt2 | 0.008s | 18.256MiB| sat | 0 | | | |bench_2866.smt2 | 0.008s | 18.568MiB| sat | 0 | | | |bench_4313.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_8487.smt2 | 0.008s | 18.248MiB| sat | 0 | | | |bench_372.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_5662.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |try5_small_true_functions_flanagansaxe_tac.rpl_re_set_syntax.il.flanagansaxe.smt2 | 0.008s | 18.744MiB| sat | 0 | | | |bench_3799.smt2 | 0.008s | 19.272MiB| sat | 0 | | | |bench_5449.smt2 | 0.008s | 18.736MiB| sat | 0 | | | |bench_7082.smt2 | 0.008s | 18.516MiB| sat | 0 | | | |bench_981.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_5084.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_7636.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |a653test0023.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_7233.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_1763.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_3295.smt2 | 0.008s | 19.248MiB| sat | 0 | | | |bench_2327.smt2 | 0.008s | 18.828MiB| sat | 0 | | | |a208test0005.smt2 | 0.008s | 18.508MiB| sat | 0 | | | |try5_small_true_functions_flanagansaxe_vdir.hash_get_n_entries.il.flanagansaxe.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_8245.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |a167test0001.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |a60test0004.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |bench_7601.smt2 | 0.008s | 18.736MiB| sat | 0 | | | |a434test0027.smt2 | 0.008s | 18.568MiB| sat | 0 | | | |bench_4115.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_2717.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_4964.smt2 | 0.008s | 18.256MiB| sat | 0 | | | |bench_4505.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_8042.smt2 | 0.008s | 18.78MiB| sat | 0 | | | |bench_961.smt2 | 0.008s | 18.572MiB| sat | 0 | | | |bench_5623.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_2710.smt2 | 0.008s | 18.508MiB| sat | 0 | | | |bench_1391.smt2 | 0.008s | 18.252MiB| sat | 0 | | | |bench_3689.smt2 | 0.008s | 18.512MiB| sat | 0 | | | |bench_831.smt2 | 0.008s | 18.736MiB| sat | 0 | | | |predicate_2801.smt2 | 0.008s | 18.788MiB| sat | 0 | | | |bench_8342.smt2 | 0.008s | 18.76MiB| sat | 0 | | | |bench_8030.smt2 | 0.008s | 18.256MiB| sat | 0 | | | |a402test0032.smt2 | 0.008s | 19.016MiB| sat | 0 | | | |bench_4583.smt2 | 0.008s | 18.716MiB| sat | 0 | | | |bench_3484.smt2 | 0.008s | 18.532MiB| sat | 0 | | | |bench_3339.smt2 | 0.008s | 18.504MiB| sat | 0 | | | |bench_5301.smt2 | 0.009s | 19.016MiB| sat | 0 | | | |bench_6765.smt2 | 0.009s | 19.064MiB| sat | 0 | | | |a497test0020.smt2 | 0.009s | 19.28MiB| sat | 0 | | | |bench_2400.smt2 | 0.009s | 18.744MiB| sat | 0 | | | |bench_6929.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |a214test0017.smt2 | 0.009s | 18.504MiB| sat | 0 | | | |bench_808.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |bench_4069.smt2 | 0.009s | 18.508MiB| sat | 0 | | | |bench_4141.smt2 | 0.009s | 19.016MiB| sat | 0 | | | |bench_98.smt2 | 0.009s | 19.016MiB| sat | 0 | | | |bench_5261.smt2 | 0.009s | 18.844MiB| sat | 0 | | | |a600test0040.smt2 | 0.009s | 18.768MiB| sat | 0 | | | |a423test0008.smt2 | 0.009s | 18.516MiB| sat | 0 | | | |bv-term-small-rw_36.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |bench_3926.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |bench_2261.smt2 | 0.009s | 19.012MiB| sat | 0 | | | |bench_2117.smt2 | 0.009s | 18.488MiB| sat | 0 | | | |bench_5332.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |a331test0008.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |a669test0063.smt2 | 0.009s | 19.024MiB| sat | 0 | | | |bench_1858.smt2 | 0.009s | 19.024MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_test.quoting_options_from_style.il.flanagansaxe.smt2 | 0.009s | 19.024MiB| sat | 0 | | | |bench_2650.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |bench_1446.smt2 | 0.009s | 19.248MiB| sat | 0 | | | |bench_4390.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |bench_3263.smt2 | 0.009s | 19.276MiB| sat | 0 | | | |bench_4710.smt2 | 0.009s | 19.016MiB| sat | 0 | | | |bench_4170.smt2 | 0.009s | 18.268MiB| sat | 0 | | | |bench_5086.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |bench_4275.smt2 | 0.009s | 19.016MiB| sat | 0 | | | |bench_4477.smt2 | 0.009s | 19.528MiB| sat | 0 | | | |bench_5019.smt2 | 0.009s | 18.832MiB| sat | 0 | | | |bench_1942.smt2 | 0.009s | 19.016MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_link.quoting_options_from_style.il.flanagansaxe.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_cut.hash_int.il.flanagansaxe.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |bench_2099.smt2 | 0.009s | 18.672MiB| sat | 0 | | | |bench_1201.smt2 | 0.009s | 18.992MiB| sat | 0 | | | |bench_2688.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |bench_5234.smt2 | 0.009s | 18.412MiB| sat | 0 | | | |bench_281.smt2 | 0.009s | 20.04MiB| sat | 0 | | | |bench_7494.smt2 | 0.009s | 18.6MiB| sat | 0 | | | |a330test0007.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |bench_1106.smt2 | 0.009s | 19.016MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_nl.quoting_options_from_style.il.flanagansaxe.smt2 | 0.009s | 19.256MiB| sat | 0 | | | |bench_4399.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |bench_5392.smt2 | 0.009s | 19.016MiB| sat | 0 | | | |a324test0010.smt2 | 0.009s | 18.692MiB| sat | 0 | | | |try5_small_true_functions_fse-bfs_stty.visible.il.fse-bfs.smt2 | 0.009s | 19.092MiB| sat | 0 | | | |run_03230.trace.cond_011955_0x4182de_00.smt2 | 0.009s | 19.016MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_cat.quoting_options_from_style.il.flanagansaxe.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |QF_BV_bv8_bv_swap_three_cc_ref_max.smt2 | 0.009s | 18.528MiB| sat | 0 | | | |bench_945.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |bench_7686.smt2 | 0.009s | 18.992MiB| sat | 0 | | | |bench_2067.smt2 | 0.009s | 18.504MiB| sat | 0 | | | |bench_3721.smt2 | 0.009s | 18.768MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_touch.quoting_options_from_style.il.flanagansaxe.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |bench_1465.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_true.quoting_options_from_style.il.flanagansaxe.smt2 | 0.009s | 19.024MiB| sat | 0 | | | |a603test0055.smt2 | 0.009s | 19.028MiB| sat | 0 | | | |try5_small_noof_functions_dwp_cut.hash_int.il.dwp.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |bench_4775.smt2 | 0.009s | 18.992MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_users.quoting_options_from_style.il.flanagansaxe.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |bench_4919.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |a674test0008.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |bench_4447.smt2 | 0.009s | 18.516MiB| sat | 0 | | | |try5_small_noof_functions_fse-bfs_shuf.input_numbers_option_used.il.fse-bfs.smt2 | 0.009s | 19.036MiB| sat | 0 | | | |bench_4340.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |bench_3223.smt2 | 0.009s | 19.172MiB| sat | 0 | | | |bench_3715.smt2 | 0.009s | 18.448MiB| sat | 0 | | | |bench_3434.smt2 | 0.009s | 18.8MiB| sat | 0 | | | |bench_5236.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |bench_702.smt2 | 0.009s | 18.5MiB| sat | 0 | | | |bench_129.smt2 | 0.009s | 19.016MiB| sat | 0 | | | |bench_2021.smt2 | 0.009s | 18.812MiB| sat | 0 | | | |a625test0095.smt2 | 0.009s | 18.988MiB| sat | 0 | | | |bench_8070.smt2 | 0.009s | 18.256MiB| sat | 0 | | | |a658test0026.smt2 | 0.009s | 18.504MiB| sat | 0 | | | |bench_183.smt2 | 0.009s | 18.692MiB| sat | 0 | | | |bench_743.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |a335test0041.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |bench_1136.smt2 | 0.009s | 18.772MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_kill.quoting_options_from_style.il.flanagansaxe.smt2 | 0.009s | 19.024MiB| sat | 0 | | | |bench_7754.smt2 | 0.009s | 18.256MiB| sat | 0 | | | |bench_5326.smt2 | 0.009s | 19.532MiB| sat | 0 | | | |bench_2077.smt2 | 0.009s | 18.904MiB| sat | 0 | | | |bench_1477.smt2 | 0.009s | 19.128MiB| sat | 0 | | | |bench_4352.smt2 | 0.009s | 18.768MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_vdir.quoting_options_from_style.il.flanagansaxe.smt2 | 0.009s | 19.08MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_fold.quoting_options_from_style.il.flanagansaxe.smt2 | 0.009s | 19.304MiB| sat | 0 | | | |bench_6901.smt2 | 0.009s | 19.192MiB| sat | 0 | | | |try5_small_true_functions_flanagansaxe_stty.visible.il.flanagansaxe.smt2 | 0.009s | 19.288MiB| sat | 0 | | | |bench_1802.smt2 | 0.009s | 18.836MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_env.quoting_options_from_style.il.flanagansaxe.smt2 | 0.009s | 19.028MiB| sat | 0 | | | |bench_3951.smt2 | 0.009s | 18.488MiB| sat | 0 | | | |bench_5257.smt2 | 0.009s | 19.016MiB| sat | 0 | | | |bench_8492.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_nice.quoting_options_from_style.il.flanagansaxe.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |bench_6560.smt2 | 0.009s | 19.752MiB| sat | 0 | | | |bench_7612.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |bench_5034.smt2 | 0.009s | 18.768MiB| sat | 0 | | | |bench_2192.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |run_03230.trace.cond_011951_0x4182b4_00.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |bench_7826.smt2 | 0.009s | 18.532MiB| sat | 0 | | | |bench_1882.smt2 | 0.009s | 18.632MiB| sat | 0 | | | |a421test0007.smt2 | 0.009s | 18.676MiB| sat | 0 | | | |a611test0014.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |bench_571.smt2 | 0.009s | 19.336MiB| sat | 0 | | | |bench_746.smt2 | 0.009s | 19.076MiB| sat | 0 | | | |bench_944.smt2 | 0.009s | 18.552MiB| sat | 0 | | | |bench_6902.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |bench_1361.smt2 | 0.009s | 19.024MiB| sat | 0 | | | |bench_7642.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |run_03230.trace.cond_011742_0x4066e2_00.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |bench_5030.smt2 | 0.009s | 19.76MiB| sat | 0 | | | |bench_7076.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |bench_5150.smt2 | 0.009s | 18.504MiB| sat | 0 | | | |bench_4472.smt2 | 0.009s | 19.528MiB| sat | 0 | | | |bench_3058.smt2 | 0.009s | 19.0MiB| sat | 0 | | | |bench_875.smt2 | 0.009s | 18.76MiB| sat | 0 | | | |bench_7331.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |bench_1332.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |bench_6908.smt2 | 0.009s | 18.248MiB| sat | 0 | | | |bench_7081.smt2 | 0.009s | 18.536MiB| sat | 0 | | | |a628test0066.smt2 | 0.009s | 19.272MiB| sat | 0 | | | |bench_983.smt2 | 0.009s | 19.504MiB| sat | 0 | | | |bench_2635.smt2 | 0.009s | 18.56MiB| sat | 0 | | | |a406test0030.smt2 | 0.009s | 18.824MiB| sat | 0 | | | |bench_2864.smt2 | 0.009s | 18.512MiB| sat | 0 | | | |bv-term-small-rw_314.smt2 | 0.010s | 20.296MiB| sat | 0 | | | |bench_1278.smt2 | 0.010s | 19.272MiB| sat | 0 | | | |a613test0087.smt2 | 0.010s | 19.024MiB| sat | 0 | | | |bench_791.smt2 | 0.010s | 19.628MiB| sat | 0 | | | |a479test0010.smt2 | 0.010s | 19.192MiB| sat | 0 | | | |bench_1996.smt2 | 0.010s | 18.576MiB| sat | 0 | | | |bv-term-small-rw_47.smt2 | 0.010s | 19.792MiB| sat | 0 | | | |bench_7127.smt2 | 0.010s | 19.792MiB| sat | 0 | | | |bench_270.smt2 | 0.010s | 19.528MiB| sat | 0 | | | |a605test0062.smt2 | 0.010s | 19.54MiB| sat | 0 | | | |bench_3813.smt2 | 0.010s | 19.28MiB| sat | 0 | | | |bench_8462.smt2 | 0.010s | 20.296MiB| sat | 0 | | | |bench_1445.smt2 | 0.010s | 19.016MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_hostid.quoting_options_from_style.il.flanagansaxe.smt2 | 0.010s | 19.02MiB| sat | 0 | | | |bench_7185.smt2 | 0.010s | 18.76MiB| sat | 0 | | | |bench_3995.smt2 | 0.010s | 19.464MiB| sat | 0 | | | |bench_1707.smt2 | 0.010s | 19.068MiB| sat | 0 | | | |bench_299.smt2 | 0.010s | 19.528MiB| sat | 0 | | | |bench_3739.smt2 | 0.010s | 18.768MiB| unset | 1 | | | |bench_4728.smt2 | 0.010s | 19.536MiB| sat | 0 | | | |bench_436.smt2 | 0.010s | 19.036MiB| sat | 0 | | | |bench_4879.smt2 | 0.010s | 19.248MiB| sat | 0 | | | |bench_8051.smt2 | 0.010s | 18.256MiB| sat | 0 | | | |bench_3818.smt2 | 0.010s | 19.02MiB| sat | 0 | | | |QF_BV_bv_bv_swap_two_cc_ref_max.smt2 | 0.010s | 18.256MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_pinky.quoting_options_from_style.il.flanagansaxe.smt2 | 0.010s | 19.016MiB| sat | 0 | | | |bench_4759.smt2 | 0.010s | 18.76MiB| unset | 1 | | | |try5_small_noof_functions_flanagansaxe_sum.quoting_options_from_style.il.flanagansaxe.smt2 | 0.010s | 19.272MiB| sat | 0 | | | |bv-term-small-rw_166.smt2 | 0.010s | 20.296MiB| sat | 0 | | | |QF_BV_protocols.1.prop1_cc_ref_max.smt2 | 0.010s | 18.512MiB| sat | 0 | | | |bench_1335.smt2 | 0.010s | 19.472MiB| sat | 0 | | | |bench_4607.smt2 | 0.010s | 19.76MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_echo.quoting_options_from_style.il.flanagansaxe.smt2 | 0.010s | 19.272MiB| sat | 0 | | | |bench_2735.smt2 | 0.010s | 18.772MiB| sat | 0 | | | |bench_710.smt2 | 0.010s | 18.808MiB| sat | 0 | | | |bench_8053.smt2 | 0.010s | 18.504MiB| sat | 0 | | | |bench_2499.smt2 | 0.010s | 18.532MiB| sat | 0 | | | |bench_290.smt2 | 0.010s | 18.936MiB| sat | 0 | | | |a494test0007.smt2 | 0.010s | 19.504MiB| sat | 0 | | | |bench_4368.smt2 | 0.010s | 19.784MiB| sat | 0 | | | |try5_small_true_functions_dwp_stty.visible.il.dwp.smt2 | 0.010s | 19.504MiB| sat | 0 | | | |bench_749.smt2 | 0.010s | 19.3MiB| sat | 0 | | | |bench_8283.smt2 | 0.010s | 18.256MiB| sat | 0 | | | |bench_2514.smt2 | 0.010s | 19.292MiB| sat | 0 | | | |bench_2645.smt2 | 0.010s | 19.016MiB| sat | 0 | | | |bench_528.smt2 | 0.010s | 19.516MiB| sat | 0 | | | |QF_BV_bv_bv_resistance.2.prop1_cc_ref_max.smt2 | 0.010s | 19.016MiB| sat | 0 | | | |bench_225.smt2 | 0.010s | 19.784MiB| sat | 0 | | | |bench_894.smt2 | 0.010s | 19.272MiB| sat | 0 | | | |run_03230.trace.cond_012011_0x4182de_00.smt2 | 0.010s | 19.136MiB| sat | 0 | | | |bench_3239.smt2 | 0.010s | 20.296MiB| sat | 0 | | | |bench_1953.smt2 | 0.010s | 18.764MiB| sat | 0 | | | |bench_6848.smt2 | 0.010s | 18.416MiB| sat | 0 | | | |QF_BV_bv_bv_synabs_cc_ref_max.smt2 | 0.010s | 18.58MiB| sat | 0 | | | |a649test0047.smt2 | 0.010s | 20.04MiB| sat | 0 | | | |b26test0001.smt2 | 0.010s | 19.016MiB| sat | 0 | | | |bench_3788.smt2 | 0.010s | 19.28MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_tsort.quoting_options_from_style.il.flanagansaxe.smt2 | 0.010s | 19.056MiB| sat | 0 | | | |bench_3522.smt2 | 0.011s | 19.792MiB| sat | 0 | | | |bv-term-small-rw_720.smt2 | 0.011s | 20.376MiB| sat | 0 | | | |bench_7421.smt2 | 0.011s | 19.596MiB| sat | 0 | | | |bench_1228.smt2 | 0.011s | 20.156MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_sleep.quoting_options_from_style.il.flanagansaxe.smt2 | 0.011s | 19.024MiB| sat | 0 | | | |bv-term-small-rw_904.smt2 | 0.011s | 20.56MiB| sat | 0 | | | |bench_1235.smt2 | 0.011s | 19.28MiB| sat | 0 | | | |bench_2269.smt2 | 0.011s | 19.548MiB| sat | 0 | | | |bv-term-small-rw_45.smt2 | 0.011s | 20.3MiB| sat | 0 | | | |bench_3787.smt2 | 0.011s | 19.4MiB| sat | 0 | | | |bench_325.smt2 | 0.011s | 19.712MiB| sat | 0 | | | |a681test0048.smt2 | 0.011s | 19.832MiB| sat | 0 | | | |QF_BV_bv8_bv_schedule_world.1.prop1_cc_ref_max.smt2 | 0.011s | 19.112MiB| sat | 0 | | | |bench_4435.smt2 | 0.011s | 20.04MiB| sat | 0 | | | |run_03230.trace.cond_011969_0x4182de_00.smt2 | 0.011s | 19.272MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_chgrp.quoting_options_from_style.il.flanagansaxe.smt2 | 0.011s | 19.016MiB| sat | 0 | | | |bench_796.smt2 | 0.011s | 18.76MiB| sat | 0 | | | |bench_815.smt2 | 0.011s | 20.304MiB| sat | 0 | | | |bench_1379.smt2 | 0.011s | 19.248MiB| sat | 0 | | | |bench_8357.smt2 | 0.011s | 18.256MiB| sat | 0 | | | |bv-term-small-rw_250.smt2 | 0.011s | 19.784MiB| sat | 0 | | | |bench_793.smt2 | 0.011s | 19.024MiB| sat | 0 | | | |bench_2639.smt2 | 0.011s | 19.536MiB| sat | 0 | | | |bench_4220.smt2 | 0.011s | 19.568MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_tty.quoting_options_from_style.il.flanagansaxe.smt2 | 0.011s | 19.024MiB| sat | 0 | | | |run_03230.trace.cond_011923_0x4182b4_00.smt2 | 0.011s | 18.768MiB| sat | 0 | | | |bench_631.smt2 | 0.011s | 18.856MiB| sat | 0 | | | |bench_1229.smt2 | 0.011s | 20.04MiB| sat | 0 | | | |bench_4570.smt2 | 0.011s | 19.732MiB| sat | 0 | | | |bv-term-small-rw_521.smt2 | 0.011s | 20.56MiB| sat | 0 | | | |bench_930.smt2 | 0.011s | 19.536MiB| sat | 0 | | | |bench_3890.smt2 | 0.011s | 19.784MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_tac.quoting_options_from_style.il.flanagansaxe.smt2 | 0.011s | 19.272MiB| sat | 0 | | | |bv-term-small-rw_356.smt2 | 0.011s | 20.62MiB| sat | 0 | | | |bench_1686.smt2 | 0.011s | 19.016MiB| sat | 0 | | | |bench_3697.smt2 | 0.011s | 19.28MiB| sat | 0 | | | |bench_414.smt2 | 0.011s | 20.296MiB| sat | 0 | | | |bench_1285.smt2 | 0.011s | 18.992MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_mkfifo.quoting_options_from_style.il.flanagansaxe.smt2 | 0.011s | 18.84MiB| sat | 0 | | | |bench_4813.smt2 | 0.011s | 19.784MiB| sat | 0 | | | |bench_2420.smt2 | 0.011s | 18.256MiB| sat | 0 | | | |bench_4669.smt2 | 0.011s | 18.512MiB| sat | 0 | | | |bench_4192.smt2 | 0.011s | 19.784MiB| sat | 0 | | | |bench_1041.smt2 | 0.011s | 20.052MiB| sat | 0 | | | |inf1.smt2 | 0.011s | 19.6MiB| sat | 0 | | | |run_03230.trace.cond_012053_0x4182de_00.smt2 | 0.012s | 19.532MiB| sat | 0 | | | |bench_1012.smt2 | 0.012s | 18.768MiB| sat | 0 | | | |bv-term-small-rw_318.smt2 | 0.012s | 19.792MiB| sat | 0 | | | |bench_4755.smt2 | 0.012s | 20.888MiB| sat | 0 | | | |bench_820.smt2 | 0.012s | 19.528MiB| sat | 0 | | | |run_03230.trace.cond_012161_0x4182b4_00.smt2 | 0.012s | 19.784MiB| sat | 0 | | | |bench_4231.smt2 | 0.012s | 21.32MiB| sat | 0 | | | |bench_4100.smt2 | 0.012s | 20.816MiB| sat | 0 | | | |bv-term-small-rw_207.smt2 | 0.012s | 20.3MiB| sat | 0 | | | |run_03230.trace.cond_012035_0x4182b4_00.smt2 | 0.012s | 19.284MiB| sat | 0 | | | |bench_5037.smt2 | 0.012s | 21.32MiB| sat | 0 | | | |bench_2503.smt2 | 0.012s | 19.536MiB| sat | 0 | | | |QF_BV_bv_bv_cyclic_scheduler.2.prop1_cc_ref_max.smt2 | 0.012s | 19.34MiB| sat | 0 | | | |bench_4154.smt2 | 0.012s | 20.816MiB| sat | 0 | | | |bench_1249.smt2 | 0.012s | 20.208MiB| sat | 0 | | | |bench_824.smt2 | 0.012s | 20.048MiB| sat | 0 | | | |bench_3681.smt2 | 0.013s | 18.512MiB| sat | 0 | | | |bench_4740.smt2 | 0.013s | 21.064MiB| sat | 0 | | | |bench_3699.smt2 | 0.013s | 19.468MiB| sat | 0 | | | |bench_1336.smt2 | 0.013s | 21.068MiB| sat | 0 | | | |bench_4040.smt2 | 0.013s | 21.324MiB| sat | 0 | | | |try5_small_true_functions_flanagansaxe_sha1sum.sha1_read_ctx.il.flanagansaxe.smt2 | 0.013s | 19.28MiB| sat | 0 | | | |bench_4753.smt2 | 0.013s | 21.32MiB| sat | 0 | | | |bench_4356.smt2 | 0.013s | 20.892MiB| sat | 0 | | | |run_03230.trace.cond_025570_0x41821d_00.smt2 | 0.013s | 19.344MiB| sat | 0 | | | |run_03230.trace.cond_012175_0x4182b4_00.smt2 | 0.013s | 19.504MiB| sat | 0 | | | |bench_1481.smt2 | 0.013s | 20.56MiB| sat | 0 | | | |QF_BV_bv8_bv_cyclic_scheduler.2.prop1_cc_ref_max.smt2 | 0.013s | 19.272MiB| sat | 0 | | | |bench_1880.smt2 | 0.013s | 19.808MiB| sat | 0 | | | |bench_6987.smt2 | 0.013s | 20.552MiB| sat | 0 | | | |bench_3819.smt2 | 0.013s | 21.32MiB| sat | 0 | | | |run_03230.trace.cond_025597_0x418209_00.smt2 | 0.013s | 19.62MiB| sat | 0 | | | |bench_2265.smt2 | 0.013s | 20.028MiB| sat | 0 | | | |bench_7314.smt2 | 0.013s | 20.024MiB| sat | 0 | | | |bench_4143.smt2 | 0.013s | 21.072MiB| sat | 0 | | | |bench_4051.smt2 | 0.013s | 20.808MiB| sat | 0 | | | |bench_3675.smt2 | 0.013s | 19.612MiB| sat | 0 | | | |bench_4481.smt2 | 0.013s | 20.272MiB| sat | 0 | | | |bench_4594.smt2 | 0.013s | 20.62MiB| sat | 0 | | | |run_03230.trace.cond_025314_0x41821d_00.smt2 | 0.013s | 19.968MiB| sat | 0 | | | |bench_1414.smt2 | 0.013s | 20.56MiB| sat | 0 | | | |bench_3538.smt2 | 0.013s | 20.048MiB| sat | 0 | | | |bench_2579.smt2 | 0.013s | 20.808MiB| sat | 0 | | | |bench_3637.smt2 | 0.013s | 21.576MiB| sat | 0 | | | |bench_3885.smt2 | 0.013s | 20.372MiB| sat | 0 | | | |bench_3320.smt2 | 0.013s | 20.784MiB| sat | 0 | | | |bench_4233.smt2 | 0.013s | 20.816MiB| sat | 0 | | | |run_03230.trace.cond_025439_0x418209_00.smt2 | 0.013s | 19.62MiB| sat | 0 | | | |bench_3937.smt2 | 0.013s | 21.072MiB| sat | 0 | | | |try5_small_noof_functions_flanagansaxe_ptx.quoting_options_from_style.il.flanagansaxe.smt2 | 0.013s | 19.024MiB| sat | 0 | | | |bench_2189.smt2 | 0.013s | 18.772MiB| sat | 0 | | | |run_03230.trace.cond_012133_0x4182b4_00.smt2 | 0.013s | 19.684MiB| sat | 0 | | | |bench_3191.smt2 | 0.013s | 19.912MiB| sat | 0 | | | |bench_4031.smt2 | 0.013s | 19.272MiB| sat | 0 | | | |bench_3317.smt2 | 0.013s | 20.788MiB| sat | 0 | | | |bench_581.smt2 | 0.013s | 21.136MiB| sat | 0 | | | |bench_6813.smt2 | 0.013s | 20.188MiB| sat | 0 | | | |run_03230.trace.cond_025442_0x41821d_00.smt2 | 0.014s | 19.876MiB| sat | 0 | | | |run_03230.trace.cond_025600_0x41821d_00.smt2 | 0.014s | 19.62MiB| sat | 0 | | | |run_03230.trace.cond_025469_0x418209_00.smt2 | 0.014s | 19.624MiB| sat | 0 | | | |bench_1179.smt2 | 0.014s | 20.584MiB| sat | 0 | | | |bench_1359.smt2 | 0.014s | 20.908MiB| sat | 0 | | | |run_03230.trace.cond_025616_0x41820e_00.smt2 | 0.014s | 19.62MiB| sat | 0 | | | |bench_2580.smt2 | 0.014s | 20.732MiB| sat | 0 | | | |bench_1270.smt2 | 0.014s | 19.76MiB| sat | 0 | | | |bench_4444.smt2 | 0.014s | 18.256MiB| sat | 0 | | | |run_03230.trace.cond_025582_0x418209_00.smt2 | 0.014s | 19.436MiB| sat | 0 | | | |bench_4890.smt2 | 0.014s | 21.024MiB| sat | 0 | | | |bench_4346.smt2 | 0.014s | 18.512MiB| sat | 0 | | | |bench_7357.smt2 | 0.014s | 21.184MiB| sat | 0 | | | |bench_3838.smt2 | 0.015s | 20.82MiB| sat | 0 | | | |bench_3832.smt2 | 0.015s | 21.348MiB| sat | 0 | | | |bench_7339.smt2 | 0.015s | 20.768MiB| sat | 0 | | | |try5_small_noof_functions_dwp_stty.visible.il.dwp.smt2 | 0.015s | 20.772MiB| sat | 0 | | | |bench_5744.smt2 | 0.015s | 20.508MiB| sat | 0 | | | |run_03230.trace.cond_025454_0x418209_00.smt2 | 0.015s | 19.612MiB| sat | 0 | | | |bench_6911.smt2 | 0.015s | 18.172MiB| sat | 0 | | | |bench_3465.smt2 | 0.015s | 20.876MiB| sat | 0 | | | |try3_noof_functions_dwp_stty.visible.il.dwp.smt2 | 0.015s | 20.368MiB| sat | 0 | | | |bench_7056.smt2 | 0.015s | 18.672MiB| sat | 0 | | | |bench_8055.smt2 | 0.015s | 18.16MiB| sat | 0 | | | |bench_4900.smt2 | 0.015s | 20.836MiB| sat | 0 | | | |bench_7708.smt2 | 0.015s | 18.256MiB| sat | 0 | | | |bench_1063.smt2 | 0.015s | 21.328MiB| sat | 0 | | | |bench_2573.smt2 | 0.015s | 20.56MiB| sat | 0 | | | |bench_2880.smt2 | 0.015s | 22.0MiB| sat | 0 | | | |bench_2931.smt2 | 0.015s | 22.088MiB| sat | 0 | | | |QF_BV_eq_sdp_v5_cc_ref_max.smt2 | 0.016s | 20.296MiB| sat | 0 | | | |bench_4099.smt2 | 0.016s | 20.492MiB| sat | 0 | | | |run_03230.trace.cond_025552_0x41820e_00.smt2 | 0.016s | 19.512MiB| sat | 0 | | | |bench_1053.smt2 | 0.016s | 18.508MiB| sat | 0 | | | |bench_7383.smt2 | 0.016s | 20.564MiB| sat | 0 | | | |bench_4467.smt2 | 0.016s | 20.756MiB| sat | 0 | | | |bench_3461.smt2 | 0.016s | 22.456MiB| sat | 0 | | | |bench_825.smt2 | 0.016s | 21.32MiB| sat | 0 | | | |bench_4738.smt2 | 0.016s | 21.072MiB| sat | 0 | | | |bench_2574.smt2 | 0.016s | 21.332MiB| sat | 0 | | | |bench_5041.smt2 | 0.016s | 22.888MiB| sat | 0 | | | |run_03230.trace.cond_025506_0x41821d_00.smt2 | 0.017s | 19.62MiB| sat | 0 | | | |bench_2917.smt2 | 0.017s | 22.108MiB| sat | 0 | | | |bench_3311.smt2 | 0.017s | 23.032MiB| sat | 0 | | | |bench_797.smt2 | 0.017s | 21.572MiB| sat | 0 | | | |QF_BV_bv_bv_eq_sdp_v4_cc_ref_max.smt2 | 0.017s | 20.388MiB| sat | 0 | | | |bench_5536.smt2 | 0.017s | 20.792MiB| sat | 0 | | | |bench_112.smt2 | 0.017s | 21.584MiB| sat | 0 | | | |bench_8260.smt2 | 0.017s | 18.996MiB| sat | 0 | | | |bench_3068.smt2 | 0.017s | 20.988MiB| sat | 0 | | | |bench_3846.smt2 | 0.017s | 20.732MiB| sat | 0 | | | |bench_559.smt2 | 0.017s | 22.32MiB| sat | 0 | | | |bench_2897.smt2 | 0.017s | 21.3MiB| sat | 0 | | | |bench_1467.smt2 | 0.017s | 18.98MiB| sat | 0 | | | |bench_972.smt2 | 0.017s | 22.408MiB| sat | 0 | | | |run_03230.trace.cond_025638_0x41821d_00.smt2 | 0.017s | 19.396MiB| sat | 0 | | | |bench_1670.smt2 | 0.017s | 20.308MiB| sat | 0 | | | |run_03230.trace.cond_025405_0x418209_00.smt2 | 0.017s | 19.6MiB| sat | 0 | | | |bv-term-small-rw_1391.smt2 | 0.018s | 20.572MiB| sat | 0 | | | |bench_437.smt2 | 0.018s | 22.856MiB| sat | 0 | | | |bench_1680.smt2 | 0.018s | 22.64MiB| sat | 0 | | | |bench_5459.smt2 | 0.018s | 21.452MiB| sat | 0 | | | |bench_2202.smt2 | 0.018s | 22.116MiB| sat | 0 | | | |bench_3446.smt2 | 0.018s | 19.456MiB| sat | 0 | | | |bench_2566.smt2 | 0.018s | 22.608MiB| sat | 0 | | | |bench_3551.smt2 | 0.018s | 22.736MiB| sat | 0 | | | |bench_1441.smt2 | 0.018s | 22.172MiB| sat | 0 | | | |bv-term-small-rw_337.smt2 | 0.018s | 19.272MiB| sat | 0 | | | |bench_2789.smt2 | 0.018s | 22.268MiB| sat | 0 | | | |bench_993.smt2 | 0.019s | 22.092MiB| sat | 0 | | | |bench_778.smt2 | 0.019s | 21.584MiB| sat | 0 | | | |bench_1769.smt2 | 0.019s | 21.124MiB| sat | 0 | | | |bench_6866.smt2 | 0.019s | 20.664MiB| sat | 0 | | | |bench_1318.smt2 | 0.019s | 21.84MiB| sat | 0 | | | |bench_3114.smt2 | 0.019s | 19.86MiB| sat | 0 | | | |bench_3886.smt2 | 0.019s | 22.576MiB| sat | 0 | | | |bench_2567.smt2 | 0.019s | 22.9MiB| sat | 0 | | | |bench_3524.smt2 | 0.019s | 22.088MiB| sat | 0 | | | |bench_4359.smt2 | 0.020s | 20.552MiB| sat | 0 | | | |bench_1440.smt2 | 0.020s | 22.72MiB| sat | 0 | | | |bench_525.smt2 | 0.020s | 22.648MiB| sat | 0 | | | |bench_4565.smt2 | 0.020s | 24.392MiB| sat | 0 | | | |bench_6898.smt2 | 0.020s | 22.6MiB| sat | 0 | | | |bench_2737.smt2 | 0.020s | 22.696MiB| sat | 0 | | | |bench_360.smt2 | 0.020s | 24.74MiB| sat | 0 | | | |bench_1088.smt2 | 0.020s | 20.828MiB| sat | 0 | | | |bench_379.smt2 | 0.020s | 21.808MiB| sat | 0 | | | |bench_997.smt2 | 0.020s | 21.832MiB| sat | 0 | | | |bench_3642.smt2 | 0.020s | 21.628MiB| sat | 0 | | | |bench_556.smt2 | 0.021s | 21.668MiB| sat | 0 | | | |bench_1266.smt2 | 0.021s | 20.54MiB| sat | 0 | | | |bench_609.smt2 | 0.021s | 24.648MiB| sat | 0 | | | |bench_2855.smt2 | 0.021s | 23.124MiB| sat | 0 | | | |bench_3415.smt2 | 0.021s | 23.724MiB| sat | 0 | | | |run_00000.trace.cond_017116_0x950130a_00.smt2 | 0.022s | 23.336MiB| sat | 0 | | | |bench_2798.smt2 | 0.022s | 23.376MiB| sat | 0 | | | |bench_6943.smt2 | 0.022s | 20.808MiB| sat | 0 | | | |bench_3367.smt2 | 0.022s | 21.84MiB| sat | 0 | | | |bench_4605.smt2 | 0.022s | 20.356MiB| sat | 0 | | | |bench_2646.smt2 | 0.022s | 21.968MiB| sat | 0 | | | |bench_3794.smt2 | 0.022s | 23.12MiB| sat | 0 | | | |bench_2169.smt2 | 0.022s | 24.216MiB| sat | 0 | | | |bench_856.smt2 | 0.022s | 21.424MiB| sat | 0 | | | |bench_531.smt2 | 0.022s | 23.664MiB| sat | 0 | | | |bench_5593.smt2 | 0.023s | 24.484MiB| sat | 0 | | | |bench_2406.smt2 | 0.023s | 21.468MiB| sat | 0 | | | |bench_2724.smt2 | 0.024s | 22.652MiB| sat | 0 | | | |bench_2211.smt2 | 0.024s | 24.964MiB| sat | 0 | | | |bench_2141.smt2 | 0.024s | 24.868MiB| sat | 0 | | | |bench_1159.smt2 | 0.024s | 22.864MiB| sat | 0 | | | |bv-term-small-rw_1516.smt2 | 0.024s | 20.312MiB| sat | 0 | | | |bench_3032.smt2 | 0.024s | 24.272MiB| sat | 0 | | | |bench_4725.smt2 | 0.024s | 22.6MiB| sat | 0 | | | |bench_658.smt2 | 0.024s | 23.556MiB| sat | 0 | | | |bench_3815.smt2 | 0.024s | 23.508MiB| sat | 0 | | | |bench_7382.smt2 | 0.024s | 21.508MiB| sat | 0 | | | |bench_2846.smt2 | 0.024s | 24.676MiB| sat | 0 | | | |bench_3411.smt2 | 0.024s | 22.136MiB| sat | 0 | | | |bench_2257.smt2 | 0.025s | 24.8MiB| sat | 0 | | | |bench_36.smt2 | 0.025s | 24.904MiB| sat | 0 | | | |bench_974.smt2 | 0.026s | 24.46MiB| sat | 0 | | | |bench_440.smt2 | 0.026s | 28.224MiB| sat | 0 | | | |bench_4560.smt2 | 0.026s | 23.328MiB| sat | 0 | | | |bench_2221.smt2 | 0.026s | 24.656MiB| sat | 0 | | | |bench_29.smt2 | 0.026s | 24.628MiB| sat | 0 | | | |simple_bit8_na1_nr1_twocond.smt2 | 0.027s | 24.916MiB| sat | 0 | | | |sort.smt2 | 0.027s | 22.304MiB| sat | 0 | | | |bench_1674.smt2 | 0.027s | 25.3MiB| sat | 0 | | | |run_00000.trace.cond_017924_0x950130a_00.smt2 | 0.028s | 23.392MiB| sat | 0 | | | |run_00000.trace.cond_285172_0xe7af40_00.smt2 | 0.028s | 21.32MiB| sat | 0 | | | |QF_BV_bv8_bv_cyclic_scheduler.4.prop1_cc_ref_max.smt2 | 0.028s | 20.8MiB| sat | 0 | | | |bv-term-small-rw_327.smt2 | 0.029s | 24.276MiB| sat | 0 | | | |bench_1878.smt2 | 0.029s | 23.112MiB| sat | 0 | | | |bench_1307.smt2 | 0.029s | 24.304MiB| sat | 0 | | | |bench_2225.smt2 | 0.030s | 27.348MiB| sat | 0 | | | |run_00012.trace.cond_057573_0x16388_00.smt2 | 0.030s | 35.324MiB| sat | 0 | | | |bench_2351.smt2 | 0.030s | 23.408MiB| sat | 0 | | | |bench_4553.smt2 | 0.030s | 25.416MiB| sat | 0 | | | |bench_2659.smt2 | 0.030s | 21.836MiB| sat | 0 | | | |run_00000.trace.cond_016653_0x95026e6_00.smt2 | 0.031s | 23.368MiB| sat | 0 | | | |bench_2841.smt2 | 0.032s | 25.672MiB| sat | 0 | | | |bench_2102.smt2 | 0.032s | 26.532MiB| sat | 0 | | | |bench_5525.smt2 | 0.032s | 26.232MiB| sat | 0 | | | |bench_7406.smt2 | 0.032s | 23.312MiB| sat | 0 | | | |bench_1610.smt2 | 0.033s | 25.228MiB| sat | 0 | | | |bench_2272.smt2 | 0.034s | 24.828MiB| sat | 0 | | | |bench_1434.smt2 | 0.034s | 24.108MiB| sat | 0 | | | |run_00000.trace.cond_285198_0xe7af87_00.smt2 | 0.034s | 22.06MiB| sat | 0 | | | |bench_2349.smt2 | 0.034s | 19.6MiB| unset | 1 | | | |bench_2183.smt2 | 0.035s | 24.756MiB| sat | 0 | | | |bv-term-small-rw_260.smt2 | 0.035s | 22.784MiB| sat | 0 | | | |bench_924.smt2 | 0.038s | 27.524MiB| sat | 0 | | | |bench_5492.smt2 | 0.039s | 26.772MiB| sat | 0 | | | |bench_4412.smt2 | 0.040s | 30.632MiB| sat | 0 | | | |bench_1652.smt2 | 0.040s | 26.056MiB| sat | 0 | | | |bench_3789.smt2 | 0.041s | 23.66MiB| sat | 0 | | | |bench_2326.smt2 | 0.042s | 24.648MiB| sat | 0 | | | |bench_5503.smt2 | 0.043s | 26.62MiB| sat | 0 | | | |run_00000.trace.cond_018783_0x950130a_00.smt2 | 0.043s | 24.984MiB| sat | 0 | | | |run_00000.trace.cond_019659_0x950130a_00.smt2 | 0.043s | 25.248MiB| sat | 0 | | | |run_00000.trace.Alloc_zero__018344.smt2 | 0.043s | 24.888MiB| sat | 0 | | | |bench_5509.smt2 | 0.044s | 26.58MiB| sat | 0 | | | |bench_712.smt2 | 0.045s | 26.228MiB| sat | 0 | | | |bench_2304.smt2 | 0.045s | 25.028MiB| sat | 0 | | | |bench_2207.smt2 | 0.046s | 27.22MiB| sat | 0 | | | |bench_2229.smt2 | 0.048s | 26.824MiB| sat | 0 | | | |bench_1993.smt2 | 0.048s | 27.512MiB| sat | 0 | | | |run_00000.trace.cond_019196_0x95026e6_00.smt2 | 0.048s | 25.044MiB| sat | 0 | | | |bench_2122.smt2 | 0.049s | 25.884MiB| sat | 0 | | | |bench_2233.smt2 | 0.050s | 27.244MiB| sat | 0 | | | |bench_1389.smt2 | 0.050s | 22.744MiB| sat | 0 | | | |run_00000.trace.Alloc_zero__020079.smt2 | 0.051s | 26.28MiB| sat | 0 | | | |bench_3460.smt2 | 0.051s | 22.844MiB| sat | 0 | | | |bv-term-small-rw_465.smt2 | 0.052s | 28.66MiB| sat | 0 | | | |QF_BV_v_Unidec_cc_ref_max.smt2 | 0.052s | 23.408MiB| sat | 0 | | | |bench_2295.smt2 | 0.054s | 25.452MiB| sat | 0 | | | |bench_5499.smt2 | 0.054s | 29.3MiB| sat | 0 | | | |bench_2293.smt2 | 0.057s | 25.848MiB| sat | 0 | | | |bench_2436.smt2 | 0.058s | 21.96MiB| sat | 0 | | | |run_00000.trace.cond_455476_0xe7af69_00.smt2 | 0.058s | 25.124MiB| sat | 0 | | | |predicate_1245.smt2 | 0.063s | 34.112MiB| sat | 0 | | | |bench_1549.smt2 | 0.063s | 30.464MiB| sat | 0 | | | |bench_787.smt2 | 0.065s | 24.744MiB| sat | 0 | | | |bench_7851.smt2 | 0.067s | 26.3MiB| sat | 0 | | | |predicate_1246.smt2 | 0.069s | 34.34MiB| sat | 0 | | | |run_00000.trace.Alloc_zero__019220.smt2 | 0.071s | 26.056MiB| sat | 0 | | | |bench_2613.smt2 | 0.074s | 25.692MiB| sat | 0 | | | |bench_335.smt2 | 0.076s | 36.58MiB| sat | 0 | | | |bench_1904.smt2 | 0.082s | 25.268MiB| sat | 0 | | | |bench_1374.smt2 | 0.086s | 25.968MiB| sat | 0 | | | |bv-term-small-rw_230.smt2 | 0.086s | 23.968MiB| sat | 0 | | | |bench_1778.smt2 | 0.087s | 28.88MiB| sat | 0 | | | |bench_4304.smt2 | 0.093s | 35.18MiB| sat | 0 | | | |bench_2747.smt2 | 0.096s | 21.928MiB| sat | 0 | | | |bench_1043.smt2 | 0.097s | 28.948MiB| sat | 0 | | | |bench_2832.smt2 | 0.111s | 29.896MiB| sat | 0 | | | |bench_1545.smt2 | 0.112s | 31.688MiB| sat | 0 | | | |bench_1424.smt2 | 0.113s | 31.36MiB| sat | 0 | | | |bench_4838.smt2 | 0.114s | 30.212MiB| sat | 0 | | | |bench_1811.smt2 | 0.117s | 27.292MiB| sat | 0 | | | |bench_1532.smt2 | 0.117s | 36.36MiB| sat | 0 | | | |bench_1.smt2 | 0.117s | 24.176MiB| sat | 0 | | | |bench_1417.smt2 | 0.125s | 35.084MiB| sat | 0 | | | |bgpd_bgpd_vc76752.smt2 | 0.129s | 49.032MiB| sat | 0 | | | |bench_607.smt2 | 0.132s | 73.268MiB| sat | 0 | | | |bench_3169.smt2 | 0.144s | 24.584MiB| unset | 1 | | | |bench_2469.smt2 | 0.156s | 23.652MiB| unset | 1 | | | |bench_2097.smt2 | 0.156s | 35.148MiB| sat | 0 | | | |bench_2620.smt2 | 0.158s | 25.78MiB| sat | 0 | | | |bench_7171.smt2 | 0.167s | 24.424MiB| unset | 1 | | | |bench_16382.smt2 | 0.169s | 34.704MiB| sat | 0 | | | |bench_1412.smt2 | 0.171s | 43.196MiB| sat | 0 | | | |bench_690.smt2 | 0.172s | 48.832MiB| sat | 0 | | | |bench_640.smt2 | 0.176s | 51.12MiB| sat | 0 | | | |bin_eventlogadm_vc331002.smt2 | 0.218s | 107.0MiB| sat | 0 | | | |bench_1367.smt2 | 0.219s | 25.808MiB| sat | 0 | | | |bench_2433.smt2 | 0.223s | 25.764MiB| unset | 1 | | | |bench_2428.smt2 | 0.232s | 25.912MiB| unset | 1 | | | |bench_760.smt2 | 0.236s | 70.916MiB| sat | 0 | | | |bin_eventlogadm_vc331001.smt2 | 0.237s | 76.544MiB| sat | 0 | | | |bench_1961.smt2 | 0.252s | 58.456MiB| sat | 0 | | | |bench_4208.smt2 | 0.259s | 41.084MiB| sat | 0 | | | |bin_libmsrpc_vc1225601.smt2 | 0.263s | 78.356MiB| sat | 0 | | | |bench_2407.smt2 | 0.299s | 26.9MiB| unset | 1 | | | |bin_libsmbsharemodes_vc5735.smt2 | 0.310s | 106.0MiB| sat | 0 | | | |bench_1094.smt2 | 0.341s | 27.156MiB| sat | 0 | | | |predicate_496.smt2 | 0.342s | 138.0MiB| sat | 0 | | | |bgpd_bgpd_vc76751.smt2 | 0.343s | 54.92MiB| sat | 0 | | | |bin_libmsrpc_vc1225139.smt2 | 0.349s | 109.0MiB| sat | 0 | | | |run_00000.trace.cond_020055_0x95026e6_00.smt2 | 0.351s | 26.672MiB| unset | 1 | | | |bin_libsmbsharemodes_vc5771.smt2 | 0.385s | 85.176MiB| sat | 0 | | | |bench_4097.smt2 | 0.399s | 60.708MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7285.smt2 | 0.406s | 116.0MiB| sat | 0 | | | |predicate_484.smt2 | 0.417s | 33.3MiB| unset | 1 | | | |matrixsqrt.smt2 | 0.423s | 56.172MiB| sat | 0 | | | |bench_753.smt2 | 0.429s | 27.044MiB| sat | 0 | | | |problem_1.smt2 | 0.449s | 31.056MiB| unset | 1 | | | |predicate_493.smt2 | 0.456s | 33.3MiB| unset | 1 | | | |bench_3888.smt2 | 0.458s | 83.528MiB| sat | 0 | | | |bench_1400.smt2 | 0.460s | 58.756MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5689.smt2 | 0.463s | 57.544MiB| sat | 0 | | | |predicate_490.smt2 | 0.469s | 33.464MiB| unset | 1 | | | |bin_libsmbsharemodes_vc7281.smt2 | 0.472s | 120.0MiB| sat | 0 | | | |bin_eventlogadm_vc352293.smt2 | 0.551s | 84.464MiB| sat | 0 | | | |e2_2.c.smt2 | 0.551s | 34.94MiB| unset | 1 | | | |e1_1.c.smt2 | 0.555s | 39.292MiB| unset | 1 | | | |bin_eventlogadm_vc352302.smt2 | 0.564s | 86.332MiB| sat | 0 | | | |send-more-money.smt2 | 0.585s | 51.684MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7060.smt2 | 0.590s | 81.976MiB| sat | 0 | | | |bin_eventlogadm_vc330978.smt2 | 0.627s | 124.0MiB| sat | 0 | | | |problem_9.smt2 | 0.630s | 23.936MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6845.smt2 | 0.638s | 82.516MiB| sat | 0 | | | |bench_888.smt2 | 0.669s | 125.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7064.smt2 | 0.679s | 103.0MiB| sat | 0 | | | |bin_eventlogadm_vc351344.smt2 | 0.686s | 93.9MiB| sat | 0 | | | |bench_6854.smt2 | 0.692s | 28.204MiB| sat | 0 | | | |src_wget_vc17453.smt2 | 0.703s | 451.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6139.smt2 | 0.709s | 194.0MiB| sat | 0 | | | |bench_1199.smt2 | 0.743s | 116.0MiB| sat | 0 | | | |bench_1401.smt2 | 0.746s | 55.184MiB| sat | 0 | | | |bin_eventlogadm_vc330950.smt2 | 0.768s | 91.72MiB| sat | 0 | | | |bin_libmsrpc_vc1225628.smt2 | 0.777s | 88.948MiB| sat | 0 | | | |bin_libsmbclient_vc1225164.smt2 | 0.923s | 304.0MiB| sat | 0 | | | |bin_eventlogadm_vc331088.smt2 | 0.961s | 210.0MiB| sat | 0 | | | |bench_3672.smt2 | 0.969s | 144.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6049.smt2 | 0.976s | 147.0MiB| sat | 0 | | | |bench_650.smt2 | 0.994s | 150.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc4289.smt2 | 1.037s | 97.224MiB| sat | 0 | | | |bench_705.smt2 | 1.055s | 144.0MiB| sat | 0 | | | |bench_3156.smt2 | 1.062s | 184.0MiB| sat | 0 | | | |bench_700.smt2 | 1.064s | 143.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5840.smt2 | 1.190s | 123.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5327.smt2 | 1.207s | 227.0MiB| sat | 0 | | | |bin_eventlogadm_vc331003.smt2 | 1.212s | 130.0MiB| sat | 0 | | | |bench_424.smt2 | 1.214s | 190.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6150.smt2 | 1.220s | 133.0MiB| sat | 0 | | | |predicate_2077.smt2 | 1.235s | 59.416MiB| sat | 0 | | | |innfeed_imapfeed_vc24623.smt2 | 1.261s | 183.0MiB| sat | 0 | | | |bench_3992.smt2 | 1.268s | 70.468MiB| sat | 0 | | | |bench_3587.smt2 | 1.274s | 181.0MiB| sat | 0 | | | |bench_5532.smt2 | 1.275s | 159.0MiB| sat | 0 | | | |bin_libmsrpc_vc1225626.smt2 | 1.279s | 126.0MiB| sat | 0 | | | |bin_eventlogadm_vc330976.smt2 | 1.296s | 132.0MiB| sat | 0 | | | |bench_3360.smt2 | 1.300s | 70.38MiB| sat | 0 | | | |bin_libmsrpc_vc1225745.smt2 | 1.320s | 200.0MiB| sat | 0 | | | |bin_eventlogadm_vc351348.smt2 | 1.323s | 130.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6074.smt2 | 1.328s | 154.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6271.smt2 | 1.335s | 213.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6272.smt2 | 1.361s | 152.0MiB| sat | 0 | | | |bench_826.smt2 | 1.380s | 135.0MiB| sat | 0 | | | |bench_630.smt2 | 1.382s | 172.0MiB| sat | 0 | | | |bin_eventlogadm_vc331007.smt2 | 1.442s | 324.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5848.smt2 | 1.462s | 218.0MiB| sat | 0 | | | |bench_390.smt2 | 1.469s | 186.0MiB| sat | 0 | | | |bench_3091.smt2 | 1.489s | 164.0MiB| sat | 0 | | | |bench_402.smt2 | 1.499s | 190.0MiB| sat | 0 | | | |bin_eventlogadm_vc331089.smt2 | 1.507s | 145.0MiB| sat | 0 | | | |rand_65_500_1235857888_0_k-6_sat.gph.smt2 | 1.515s | 85.22MiB| unset | 1 | | | |bench_502.smt2 | 1.530s | 195.0MiB| sat | 0 | | | |bench_451.smt2 | 1.570s | 214.0MiB| sat | 0 | | | |bench_663.smt2 | 1.609s | 136.0MiB| sat | 0 | | | |bench_369.smt2 | 1.610s | 204.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7652.smt2 | 1.616s | 313.0MiB| sat | 0 | | | |bench_3093.smt2 | 1.622s | 68.332MiB| sat | 0 | | | |bench_10127.smt2 | 1.644s | 68.98MiB| sat | 0 | | | |bench_97.smt2 | 1.646s | 146.0MiB| sat | 0 | | | |bench_613.smt2 | 1.652s | 182.0MiB| sat | 0 | | | |bench_659.smt2 | 1.660s | 180.0MiB| sat | 0 | | | |bench_15783.smt2 | 1.676s | 48.84MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5680.smt2 | 1.687s | 266.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7296.smt2 | 1.697s | 145.0MiB| sat | 0 | | | |bin_eventlogadm_vc351277.smt2 | 1.755s | 55.964MiB| unset | 1 | | | |bench_5723.smt2 | 1.761s | 158.0MiB| sat | 0 | | | |bench_142.smt2 | 1.772s | 156.0MiB| sat | 0 | | | |cvs_vc105458.smt2 | 1.804s | 173.0MiB| sat | 0 | | | |bench_5722.smt2 | 1.855s | 170.0MiB| sat | 0 | | | |bench_5590.smt2 | 1.859s | 150.0MiB| sat | 0 | | | |bench_3031.smt2 | 1.873s | 225.0MiB| sat | 0 | | | |bench_542.smt2 | 1.877s | 201.0MiB| sat | 0 | | | |cvs_vc105323.smt2 | 1.901s | 149.0MiB| sat | 0 | | | |cvs_vc105369.smt2 | 1.966s | 157.0MiB| sat | 0 | | | |bench_143.smt2 | 2.075s | 144.0MiB| sat | 0 | | | |bench_385.smt2 | 2.083s | 209.0MiB| sat | 0 | | | |servers_slapd_a_vc149572.smt2 | 2.093s | 76.064MiB| sat | 0 | | | |bin_libsmbsharemodes_vc4243.smt2 | 2.101s | 82.112MiB| unset | 1 | | | |rand_80_500_1235848939_0_k-9_sat.gph.smt2 | 2.105s | 87.324MiB| unset | 1 | | | |bench_1588.smt2 | 2.111s | 174.0MiB| sat | 0 | | | |bench_668.smt2 | 2.130s | 181.0MiB| sat | 0 | | | |bench_3099.smt2 | 2.135s | 215.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc4773.smt2 | 2.139s | 68.704MiB| unset | 1 | | | |cvs_vc105421.smt2 | 2.161s | 142.0MiB| sat | 0 | | | |bench_2507.smt2 | 2.165s | 167.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc4232.smt2 | 2.166s | 90.016MiB| sat | 0 | | | |bench_366.smt2 | 2.167s | 213.0MiB| sat | 0 | | | |bench_3279.smt2 | 2.225s | 205.0MiB| sat | 0 | | | |bench_6215.smt2 | 2.234s | 72.548MiB| unset | 1 | | | |cvs_vc105422.smt2 | 2.285s | 140.0MiB| sat | 0 | | | |bench_5779.smt2 | 2.297s | 185.0MiB| sat | 0 | | | |bench_247.smt2 | 2.303s | 242.0MiB| sat | 0 | | | |bin_eventlogadm_vc331054.smt2 | 2.307s | 198.0MiB| sat | 0 | | | |bin_libsmbclient_vc1225668.smt2 | 2.317s | 154.0MiB| sat | 0 | | | |bench_5401.smt2 | 2.339s | 152.0MiB| sat | 0 | | | |bench_717.smt2 | 2.357s | 140.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5285.smt2 | 2.380s | 161.0MiB| sat | 0 | | | |bench_230.smt2 | 2.389s | 262.0MiB| sat | 0 | | | |bench_5377.smt2 | 2.412s | 171.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7072.smt2 | 2.413s | 376.0MiB| sat | 0 | | | |bench_5718.smt2 | 2.422s | 175.0MiB| sat | 0 | | | |bench_1568.smt2 | 2.435s | 161.0MiB| sat | 0 | | | |bench_267.smt2 | 2.440s | 235.0MiB| sat | 0 | | | |bench_637.smt2 | 2.452s | 114.0MiB| sat | 0 | | | |bench_86.smt2 | 2.527s | 164.0MiB| sat | 0 | | | |cvs_vc105319.smt2 | 2.560s | 129.0MiB| sat | 0 | | | |bench_1573.smt2 | 2.563s | 173.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc4297.smt2 | 2.571s | 97.732MiB| unset | 1 | | | |cvs_vc105322.smt2 | 2.575s | 130.0MiB| sat | 0 | | | |bench_365.smt2 | 2.575s | 207.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5748.smt2 | 2.588s | 237.0MiB| sat | 0 | | | |bench_66.smt2 | 2.596s | 171.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc5712.smt2 | 2.603s | 175.0MiB| sat | 0 | | | |bench_823.smt2 | 2.657s | 130.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc6343.smt2 | 2.715s | 309.0MiB| sat | 0 | | | |bench_388.smt2 | 2.720s | 223.0MiB| sat | 0 | | | |bin_libsmbclient_vc1225689.smt2 | 2.739s | 687.0MiB| sat | 0 | | | |bench_141.smt2 | 2.773s | 144.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6289.smt2 | 2.787s | 187.0MiB| sat | 0 | | | |bench_1470.smt2 | 2.845s | 130.0MiB| sat | 0 | | | |bench_2161.smt2 | 2.872s | 60.16MiB| sat | 0 | | | |bench_3121.smt2 | 2.889s | 200.0MiB| unset | 1 | | | |bench_494.smt2 | 2.940s | 196.0MiB| sat | 0 | | | |bench_657.smt2 | 2.989s | 178.0MiB| unset | 1 | | | |bench_5733.smt2 | 3.042s | 182.0MiB| sat | 0 | | | |bench_50.smt2 | 3.135s | 177.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5817.smt2 | 3.142s | 139.0MiB| sat | 0 | | | |bench_17324.smt2 | 3.186s | 74.188MiB| sat | 0 | | | |bench_2957.smt2 | 3.190s | 329.0MiB| sat | 0 | | | |bench_5373.smt2 | 3.216s | 191.0MiB| sat | 0 | | | |bench_480.smt2 | 3.216s | 195.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc4296.smt2 | 3.233s | 118.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc4791.smt2 | 3.304s | 101.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc5793.smt2 | 3.346s | 275.0MiB| sat | 0 | | | |bench_2113.smt2 | 3.372s | 126.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7086.smt2 | 3.457s | 408.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5782.smt2 | 3.463s | 392.0MiB| sat | 0 | | | |bench_905.smt2 | 3.484s | 175.0MiB| unset | 1 | | | |bin_libmsrpc_vc1232013.smt2 | 3.496s | 363.0MiB| sat | 0 | | | |bench_52.smt2 | 3.557s | 180.0MiB| sat | 0 | | | |bench_1603.smt2 | 3.570s | 165.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5751.smt2 | 3.597s | 837.0MiB| sat | 0 | | | |bin_libsmbclient_vc1225748.smt2 | 3.642s | 296.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6181.smt2 | 3.650s | 290.0MiB| sat | 0 | | | |bin_eventlogadm_vc331126.smt2 | 3.695s | 194.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7225.smt2 | 3.745s | 118.0MiB| sat | 0 | | | |bench_208.smt2 | 3.757s | 287.0MiB| sat | 0 | | | |cvs_vc105357.smt2 | 3.801s | 140.0MiB| sat | 0 | | | |bin_libsmbclient_vc1225676.smt2 | 3.826s | 221.0MiB| sat | 0 | | | |bench_3541.smt2 | 3.893s | 193.0MiB| sat | 0 | | | |innd_innd_vc32478.smt2 | 3.901s | 540.0MiB| sat | 0 | | | |bench_2965.smt2 | 3.933s | 293.0MiB| sat | 0 | | | |bench_704.smt2 | 3.972s | 147.0MiB| sat | 0 | | | |bench_3795.smt2 | 4.059s | 84.712MiB| unset | 1 | | | |bin_libsmbsharemodes_vc6291.smt2 | 4.176s | 256.0MiB| sat | 0 | | | |bin_eventlogadm_vc331044.smt2 | 4.244s | 169.0MiB| sat | 0 | | | |bench_5445.smt2 | 4.257s | 157.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6315.smt2 | 4.263s | 309.0MiB| sat | 0 | | | |bench_472.smt2 | 4.290s | 182.0MiB| sat | 0 | | | |bench_5457.smt2 | 4.291s | 180.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6117.smt2 | 4.293s | 177.0MiB| sat | 0 | | | |bench_3011.smt2 | 4.309s | 245.0MiB| unset | 1 | | | |bench_404.smt2 | 4.326s | 190.0MiB| sat | 0 | | | |bench_1816.smt2 | 4.362s | 92.672MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7068.smt2 | 4.401s | 412.0MiB| sat | 0 | | | |bench_11971.smt2 | 4.413s | 112.0MiB| sat | 0 | | | |bench_3196.smt2 | 4.430s | 184.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5729.smt2 | 4.588s | 222.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc6280.smt2 | 4.590s | 275.0MiB| sat | 0 | | | |bench_3598.smt2 | 4.593s | 191.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6346.smt2 | 4.662s | 304.0MiB| sat | 0 | | | |bench_387.smt2 | 4.684s | 218.0MiB| sat | 0 | | | |bench_2994.smt2 | 4.766s | 270.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc6309.smt2 | 4.769s | 332.0MiB| sat | 0 | | | |bench_830.smt2 | 4.815s | 125.0MiB| sat | 0 | | | |bench_171.smt2 | 4.996s | 142.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6308.smt2 | 5.102s | 299.0MiB| sat | 0 | | | |bench_498.smt2 | 5.117s | 195.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6295.smt2 | 5.131s | 363.0MiB| sat | 0 | | | |113.smt2 | 5.175s | 88.264MiB| unset | 1 | | | |bin_libsmbsharemodes_vc6266.smt2 | 5.323s | 301.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6120.smt2 | 5.331s | 549.0MiB| sat | 0 | | | |fig5.phx.smt2 | 5.541s | 214.0MiB| sat | 0 | | | |bin_eventlogadm_vc331052.smt2 | 5.547s | 308.0MiB| sat | 0 | | | |bench_4894.smt2 | 5.699s | 46.036MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5806.smt2 | 5.761s | 332.0MiB| unset | 1 | | | |bench_3209.smt2 | 5.873s | 51.788MiB| sat | 0 | | | |bench_5371.smt2 | 5.887s | 204.0MiB| sat | 0 | | | |bin_libmsrpc_vc1225324.smt2 | 5.963s | 728.0MiB| sat | 0 | | | |bench_3716.smt2 | 6.037s | 48.14MiB| sat | 0 | | | |bench_619.smt2 | 6.043s | 165.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5711.smt2 | 6.043s | 247.0MiB| unset | 1 | | | |bench_2155.smt2 | 6.133s | 210.0MiB| sat | 0 | | | |bench_46.smt2 | 6.162s | 189.0MiB| sat | 0 | | | |bench_51.smt2 | 6.178s | 184.0MiB| sat | 0 | | | |bin_libmsrpc_vc1228478.smt2 | 6.216s | 385.0MiB| sat | 0 | | | |bench_368.smt2 | 6.284s | 190.0MiB| sat | 0 | | | |bench_135.smt2 | 6.311s | 153.0MiB| sat | 0 | | | |bench_1636.smt2 | 6.456s | 150.0MiB| sat | 0 | | | |bin_libmsrpc_vc1225779.smt2 | 6.547s | 216.0MiB| unset | 1 | | | |bench_561.smt2 | 6.600s | 113.0MiB| sat | 0 | | | |bench_166.smt2 | 6.695s | 132.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6287.smt2 | 6.775s | 349.0MiB| sat | 0 | | | |bin_eventlogadm_vc352355.smt2 | 6.850s | 114.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6199.smt2 | 6.987s | 345.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5733.smt2 | 7.058s | 477.0MiB| sat | 0 | | | |bench_629.smt2 | 7.106s | 151.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5794.smt2 | 7.129s | 462.0MiB| unset | 1 | | | |bench_5545.smt2 | 7.175s | 211.0MiB| sat | 0 | | | |bench_347.smt2 | 7.208s | 113.0MiB| sat | 0 | | | |bin_libmsrpc_vc1228492.smt2 | 7.282s | 531.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7104.smt2 | 7.309s | 331.0MiB| sat | 0 | | | |innd_innd_vc32473.smt2 | 7.438s | 1797.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6297.smt2 | 7.517s | 321.0MiB| sat | 0 | | | |predicate_1898.smt2 | 7.694s | 41.284MiB| sat | 0 | | | |bench_187.smt2 | 7.697s | 127.0MiB| sat | 0 | | | |bin_eventlogadm_vc331092.smt2 | 7.698s | 750.0MiB| sat | 0 | | | |bench_6696.smt2 | 7.714s | 237.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc6161.smt2 | 7.799s | 680.0MiB| sat | 0 | | | |bench_15833.smt2 | 7.833s | 213.0MiB| unset | 1 | | | |bin_eventlogadm_vc331114.smt2 | 7.835s | 402.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5331.smt2 | 7.935s | 274.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5742.smt2 | 7.968s | 467.0MiB| sat | 0 | | | |Sz512_15128_3.smt2 | 8.036s | 70.904MiB| sat | 0 | | | |bin_libmsrpc_vc1225280.smt2 | 8.155s | 543.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6328.smt2 | 8.162s | 366.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6270.smt2 | 8.219s | 426.0MiB| sat | 0 | | | |bin_libmsrpc_vc1232007.smt2 | 8.221s | 429.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6339.smt2 | 8.265s | 238.0MiB| unset | 1 | | | |bench_9846.smt2 | 8.364s | 254.0MiB| unset | 1 | | | |bin_libmsrpc_vc1225824.smt2 | 8.628s | 553.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6178.smt2 | 8.684s | 329.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7105.smt2 | 8.710s | 692.0MiB| sat | 0 | | | |bin_eventlogadm_vc331082.smt2 | 8.714s | 227.0MiB| unset | 1 | | | |src_wget_vc18169.smt2 | 8.770s | 182.0MiB| sat | 0 | | | |bin_libmsrpc_vc1225756.smt2 | 8.835s | 516.0MiB| sat | 0 | | | |innd_innd_vc33564.smt2 | 8.898s | 1897.0MiB| sat | 0 | | | |bench_9280.smt2 | 9.334s | 52.368MiB| sat | 0 | | | |bench_5365.smt2 | 9.349s | 189.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6105.smt2 | 9.417s | 443.0MiB| sat | 0 | | | |bin_libmsrpc_vc1225312.smt2 | 9.636s | 481.0MiB| sat | 0 | | | |ndist.b.21996.smt2 | 9.704s | 460.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7116.smt2 | 9.740s | 404.0MiB| sat | 0 | | | |bin_libmsrpc_vc1228463.smt2 | 10.027s | 411.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5769.smt2 | 10.069s | 727.0MiB| sat | 0 | | | |bench_3906.smt2 | 10.116s | 98.0MiB| sat | 0 | | | |bench_14875.smt2 | 10.136s | 271.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc6182.smt2 | 10.233s | 292.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6255.smt2 | 10.447s | 348.0MiB| sat | 0 | | | |innfeed_innfeed_vc36459.smt2 | 10.707s | 1275.0MiB| sat | 0 | | | |innd_innd_vc33342.smt2 | 10.796s | 420.0MiB| sat | 0 | | | |nnrpd_nnrpd_vc21435.smt2 | 10.835s | 835.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc5749.smt2 | 10.859s | 339.0MiB| unset | 1 | | | |bench_8579.smt2 | 10.905s | 289.0MiB| unset | 1 | | | |innd_innd_vc33528.smt2 | 10.922s | 336.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6288.smt2 | 11.344s | 369.0MiB| sat | 0 | | | |bench_2961.smt2 | 11.366s | 322.0MiB| sat | 0 | | | |bench_1985.smt2 | 12.122s | 52.856MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7120.smt2 | 12.154s | 574.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc7119.smt2 | 12.157s | 793.0MiB| sat | 0 | | | |bench_2995.smt2 | 12.194s | 261.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7130.smt2 | 12.321s | 646.0MiB| sat | 0 | | | |bin_libsmbclient_vc1225736.smt2 | 12.331s | 666.0MiB| sat | 0 | | | |Example_16.txt.smt2 | 12.404s | 123.0MiB| unset | 1 | | | |bench_279.smt2 | 12.423s | 120.0MiB| sat | 0 | | | |bench_10841.smt2 | 12.436s | 226.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc6336.smt2 | 12.506s | 244.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7666.smt2 | 13.141s | 717.0MiB| sat | 0 | | | |nnrpd_nnrpd_vc21648.smt2 | 13.214s | 506.0MiB| sat | 0 | | | |bin_libmsrpc_vc1225299.smt2 | 13.372s | 1700.0MiB| sat | 0 | | | |bench_13284.smt2 | 13.387s | 631.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7087.smt2 | 13.637s | 877.0MiB| unset | 1 | | | |bench_11232.smt2 | 13.840s | 235.0MiB| unset | 1 | | | |bin_libmsrpc_vc1232036.smt2 | 14.263s | 815.0MiB| sat | 0 | | | |bin_libmsrpc_vc1225786.smt2 | 14.275s | 485.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6241.smt2 | 14.301s | 353.0MiB| sat | 0 | | | |bin_libsmbclient_vc1225211.smt2 | 14.350s | 973.0MiB| sat | 0 | | | |bench_721.smt2 | 14.588s | 140.0MiB| sat | 0 | | | |bench_5358.smt2 | 14.594s | 50.304MiB| sat | 0 | | | |bin_libsmbclient_vc1225692.smt2 | 14.782s | 1115.0MiB| sat | 0 | | | |bench_15105.smt2 | 14.804s | 305.0MiB| unset | 1 | | | |Example_9.txt.smt2 | 14.889s | 228.0MiB| unset | 1 | | | |bench_16640.smt2 | 15.214s | 364.0MiB| sat | 0 | | | |bench_14486.smt2 | 15.358s | 258.0MiB| unset | 1 | | | |bench_4256.smt2 | 15.395s | 77.152MiB| sat | 0 | | | |bin_libsmbclient_vc1225238.smt2 | 15.646s | 576.0MiB| sat | 0 | | | |bench_3065.smt2 | 15.709s | 62.312MiB| sat | 0 | | | |bench_5136.smt2 | 15.770s | 49.924MiB| sat | 0 | | | |nnrpd_nnrpd_vc21666.smt2 | 16.181s | 1857.0MiB| sat | 0 | | | |bin_libmsrpc_vc1232002.smt2 | 16.267s | 1012.0MiB| sat | 0 | | | |bin_eventlogadm_vc331086.smt2 | 16.339s | 322.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6205.smt2 | 16.349s | 322.0MiB| sat | 0 | | | |innfeed_imapfeed_vc24627.smt2 | 16.513s | 1186.0MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7124.smt2 | 16.550s | 896.0MiB| sat | 0 | | | |bench_14817.smt2 | 16.581s | 257.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc7094.smt2 | 16.699s | 797.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc7637.smt2 | 16.885s | 989.0MiB| sat | 0 | | | |test_v3_r3_vr10_c1_s24300.smt2 | 17.110s | 217.0MiB| unset | 1 | | | |bench_2974.smt2 | 17.142s | 294.0MiB| unset | 1 | | | |bench_445.smt2 | 17.360s | 190.0MiB| sat | 0 | | | |bench_4588.smt2 | 17.592s | 95.664MiB| sat | 0 | | | |bin_libsmbsharemodes_vc7636.smt2 | 17.767s | 888.0MiB| sat | 0 | | | |innd_innd_vc33162.smt2 | 17.975s | 958.0MiB| unset | 1 | | | |bin_libsmbsharemodes_vc7133.smt2 | 17.995s | 786.0MiB| sat | 0 | | | |ndist.b.27984.smt2 | 18.069s | 687.0MiB| sat | 0 | | | |bench_15365.smt2 | 18.135s | 281.0MiB| unset | 1 | | | |bench_16467.smt2 | 18.322s | 165.0MiB| sat | 0 | | | |bench_2167.smt2 | 18.449s | 63.576MiB| sat | 0 | | | |bench_5081.smt2 | 18.581s | 53.016MiB| timeout | 0 | | | |bin_libsmbclient_vc1228442.smt2 | 18.609s | 735.0MiB| timeout | 0 | | | |bench_10228.smt2 | 18.663s | 150.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225207.smt2 | 18.670s | 692.0MiB| timeout | 0 | | | |bench_2395.smt2 | 18.682s | 57.068MiB| sat | 0 | | | |bench_2868.smt2 | 18.687s | 56.616MiB| timeout | 0 | | | |bench_11826.smt2 | 18.841s | 38.956MiB| timeout | 0 | | | |bin_libmsrpc_vc1228577.smt2 | 18.862s | 738.0MiB| timeout | 0 | | | |bench_1909.smt2 | 18.864s | 58.424MiB| timeout | 0 | | | |bin_libsmbclient_vc1225779.smt2 | 18.866s | 1492.0MiB| timeout | 0 | | | |bench_2152.smt2 | 18.891s | 56.804MiB| timeout | 0 | | | |innfeed_innfeed_vc37255.smt2 | 18.899s | 1732.0MiB| timeout | 0 | | | |bin_eventlogadm_vc331106.smt2 | 18.923s | 747.0MiB| timeout | 0 | | | |bench_6458.smt2 | 18.925s | 54.336MiB| timeout | 0 | | | |bench_3500.smt2 | 18.942s | 53.74MiB| timeout | 0 | | | |bench_5424.smt2 | 18.953s | 58.608MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc6305.smt2 | 18.953s | 249.0MiB| timeout | 0 | | | |20.smt2 | 18.958s | 186.0MiB| timeout | 0 | | | |bench_2621.smt2 | 18.963s | 61.852MiB| timeout | 0 | | | |bench_5575.smt2 | 18.969s | 55.232MiB| timeout | 0 | | | |bench_1717.smt2 | 18.974s | 76.952MiB| timeout | 0 | | | |bench_10111.smt2 | 18.978s | 49.036MiB| sat | 0 | | | |bin_libsmbsharemodes_vc6299.smt2 | 18.990s | 266.0MiB| timeout | 0 | | | |bench_2875.smt2 | 18.992s | 64.504MiB| timeout | 0 | | | |bin_eventlogadm_vc331137.smt2 | 18.994s | 1224.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1228524.smt2 | 18.995s | 1922.0MiB| timeout | 0 | | | |bench_4261.smt2 | 19.005s | 75.46MiB| timeout | 0 | | | |bench_5581.smt2 | 19.011s | 88.288MiB| timeout | 0 | | | |bench_3221.smt2 | 19.019s | 72.064MiB| timeout | 0 | | | |gryzzles.8.lp.smt2 | 19.019s | 87.672MiB| sat | 0 | | | |innd_innd_vc33738.smt2 | 19.022s | 344.0MiB| timeout | 0 | | | |bench_102.smt2 | 19.028s | 459.0MiB| timeout | 0 | | | |bench_2682.smt2 | 19.031s | 61.272MiB| timeout | 0 | | | |bin_libmsrpc_vc1232137.smt2 | 19.038s | 663.0MiB| timeout | 0 | | | |bench_3266.smt2 | 19.039s | 59.356MiB| timeout | 0 | | | |bench_10940.smt2 | 19.040s | 198.0MiB| timeout | 0 | | | |bin_eventlogadm_vc331148.smt2 | 19.042s | 702.0MiB| timeout | 0 | | | |bench_1839.smt2 | 19.045s | 55.268MiB| timeout | 0 | | | |bench_1710.smt2 | 19.046s | 63.008MiB| timeout | 0 | | | |bench_2675.smt2 | 19.048s | 59.636MiB| timeout | 0 | | | |bench_1663.smt2 | 19.053s | 55.612MiB| timeout | 0 | | | |bin_libsmbclient_vc1225745.smt2 | 19.057s | 585.0MiB| timeout | 0 | | | |bench_12625.smt2 | 19.059s | 151.0MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21434.smt2 | 19.061s | 502.0MiB| timeout | 0 | | | |bench_2022.smt2 | 19.068s | 65.416MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc6217.smt2 | 19.069s | 321.0MiB| timeout | 0 | | | |bench_2867.smt2 | 19.074s | 67.144MiB| timeout | 0 | | | |innfeed_imapfeed_vc25456.smt2 | 19.075s | 1120.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225263.smt2 | 19.077s | 769.0MiB| timeout | 0 | | | |bench_9343.smt2 | 19.088s | 61.548MiB| timeout | 0 | | | |bench_6097.smt2 | 19.089s | 152.0MiB| timeout | 0 | | | |innd_innd_vc32648.smt2 | 19.099s | 1242.0MiB| timeout | 0 | | | |bench_2258.smt2 | 19.102s | 54.184MiB| timeout | 0 | | | |bench_5944.smt2 | 19.108s | 318.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225237.smt2 | 19.110s | 526.0MiB| sat | 0 | | | |bench_12655.smt2 | 19.112s | 62.876MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc7117.smt2 | 19.123s | 515.0MiB| timeout | 0 | | | |bench_13147.smt2 | 19.124s | 421.0MiB| timeout | 0 | | | |bench_2767.smt2 | 19.124s | 64.024MiB| timeout | 0 | | | |bench_2858.smt2 | 19.126s | 65.004MiB| timeout | 0 | | | |15.smt2 | 19.132s | 135.0MiB| timeout | 0 | | | |bench_3041.smt2 | 19.134s | 60.756MiB| timeout | 0 | | | |bench_1851.smt2 | 19.142s | 61.648MiB| timeout | 0 | | | |bench_1113.smt2 | 19.144s | 56.372MiB| timeout | 0 | | | |bench_3437.smt2 | 19.148s | 58.032MiB| timeout | 0 | | | |bench_10815.smt2 | 19.148s | 207.0MiB| timeout | 0 | | | |bench_3111.smt2 | 19.148s | 60.368MiB| timeout | 0 | | | |bin_libmsrpc_vc1228479.smt2 | 19.151s | 530.0MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc7644.smt2 | 19.175s | 514.0MiB| timeout | 0 | | | |bench_9653.smt2 | 19.178s | 212.0MiB| timeout | 0 | | | |bench_5036.smt2 | 19.186s | 64.128MiB| timeout | 0 | | | |bin_eventlogadm_vc331167.smt2 | 19.188s | 861.0MiB| timeout | 0 | | | |bench_10579.smt2 | 19.188s | 223.0MiB| timeout | 0 | | | |bench_1523.smt2 | 19.191s | 54.276MiB| timeout | 0 | | | |bench_3218.smt2 | 19.199s | 55.332MiB| timeout | 0 | | | |bench_4888.smt2 | 19.199s | 171.0MiB| timeout | 0 | | | |bench_2844.smt2 | 19.200s | 51.556MiB| timeout | 0 | | | |bench_3502.smt2 | 19.207s | 59.34MiB| timeout | 0 | | | |rand_200_800_1159728969_10.lp.smt2 | 19.207s | 152.0MiB| timeout | 0 | | | |innd_innd_vc33741.smt2 | 19.207s | 1031.0MiB| timeout | 0 | | | |bench_2197.smt2 | 19.213s | 54.28MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21427.smt2 | 19.214s | 1213.0MiB| timeout | 0 | | | |41.smt2 | 19.214s | 127.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225820.smt2 | 19.218s | 885.0MiB| timeout | 0 | | | |innd_innd_vc33561.smt2 | 19.223s | 586.0MiB| timeout | 0 | | | |bench_3105.smt2 | 19.225s | 57.5MiB| timeout | 0 | | | |bench_3351.smt2 | 19.238s | 57.18MiB| timeout | 0 | | | |bench_2644.smt2 | 19.238s | 59.46MiB| timeout | 0 | | | |bench_858.smt2 | 19.238s | 87.904MiB| timeout | 0 | | | |bench_353.smt2 | 19.243s | 134.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225758.smt2 | 19.250s | 648.0MiB| timeout | 0 | | | |bench_5284.smt2 | 19.251s | 50.388MiB| timeout | 0 | | | |bench_8478.smt2 | 19.253s | 151.0MiB| timeout | 0 | | | |rand_100_400_1159666138_9.lp.smt2 | 19.254s | 96.632MiB| timeout | 0 | | | |VS3-benchmark-S1.smt2 | 19.264s | 1652.0MiB| timeout | 0 | | | |bench_3145.smt2 | 19.267s | 53.796MiB| timeout | 0 | | | |bin_libmsrpc_vc1225816.smt2 | 19.273s | 1877.0MiB| timeout | 0 | | | |bench_16707.smt2 | 19.274s | 369.0MiB| timeout | 0 | | | |bench_13129.smt2 | 19.276s | 245.0MiB| timeout | 0 | | | |bench_9009.smt2 | 19.276s | 370.0MiB| timeout | 0 | | | |bench_7862.smt2 | 19.279s | 715.0MiB| timeout | 0 | | | |bench_276.smt2 | 19.280s | 71.616MiB| timeout | 0 | | | |bench_2653.smt2 | 19.282s | 54.3MiB| timeout | 0 | | | |bench_1643.smt2 | 19.284s | 59.24MiB| timeout | 0 | | | |bench_3847.smt2 | 19.286s | 76.348MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21422.smt2 | 19.290s | 322.0MiB| timeout | 0 | | | |bench_9337.smt2 | 19.292s | 210.0MiB| timeout | 0 | | | |bench_4963.smt2 | 19.295s | 56.104MiB| timeout | 0 | | | |bench_7030.smt2 | 19.300s | 319.0MiB| timeout | 0 | | | |innfeed_imapfeed_vc24827.smt2 | 19.303s | 2362.0MiB| timeout | 0 | | | |bench_3207.smt2 | 19.304s | 63.42MiB| timeout | 0 | | | |bench_1252.smt2 | 19.310s | 66.708MiB| timeout | 0 | | | |bench_3561.smt2 | 19.314s | 63.02MiB| timeout | 0 | | | |bench_11357.smt2 | 19.315s | 3295.0MiB| timeout | 0 | | | |src_wget_vc17913.smt2 | 19.315s | 2005.0MiB| timeout | 0 | | | |bench_2475.smt2 | 19.324s | 53.748MiB| timeout | 0 | | | |bench_7669.smt2 | 19.325s | 359.0MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc7643.smt2 | 19.326s | 656.0MiB| timeout | 0 | | | |bench_5157.smt2 | 19.329s | 50.18MiB| timeout | 0 | | | |bench_2360.smt2 | 19.331s | 56.508MiB| timeout | 0 | | | |bench_489.smt2 | 19.333s | 372.0MiB| timeout | 0 | | | |bench_11696.smt2 | 19.335s | 356.0MiB| timeout | 0 | | | |bench_10832.smt2 | 19.338s | 355.0MiB| timeout | 0 | | | |bench_1180.smt2 | 19.344s | 63.264MiB| timeout | 0 | | | |bench_5292.smt2 | 19.345s | 48.88MiB| timeout | 0 | | | |predicate_602.smt2 | 19.347s | 2147.0MiB| timeout | 0 | | | |bench_536.smt2 | 19.347s | 235.0MiB| timeout | 0 | | | |rand_150_600_1159731678_14.lp.smt2 | 19.350s | 133.0MiB| timeout | 0 | | | |bench_1323.smt2 | 19.351s | 103.0MiB| timeout | 0 | | | |bench_2325.smt2 | 19.359s | 52.544MiB| timeout | 0 | | | |bench_2582.smt2 | 19.360s | 210.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1228472.smt2 | 19.362s | 591.0MiB| timeout | 0 | | | |94.smt2 | 19.363s | 214.0MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21211.smt2 | 19.364s | 596.0MiB| timeout | 0 | | | |bench_1829.smt2 | 19.369s | 59.084MiB| timeout | 0 | | | |bench_6791.smt2 | 19.378s | 61.832MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21221.smt2 | 19.388s | 1191.0MiB| timeout | 0 | | | |bench_1202.smt2 | 19.388s | 190.0MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc6325.smt2 | 19.388s | 235.0MiB| timeout | 0 | | | |bench_1250.smt2 | 19.389s | 67.3MiB| timeout | 0 | | | |bench_6614.smt2 | 19.393s | 107.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225771.smt2 | 19.393s | 627.0MiB| timeout | 0 | | | |bench_8178.smt2 | 19.397s | 189.0MiB| timeout | 0 | | | |bench_5517.smt2 | 19.399s | 62.116MiB| timeout | 0 | | | |bench_1937.smt2 | 19.401s | 64.3MiB| timeout | 0 | | | |26.smt2 | 19.406s | 154.0MiB| timeout | 0 | | | |bench_11408.smt2 | 19.407s | 456.0MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc6195.smt2 | 19.411s | 434.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225332.smt2 | 19.411s | 2174.0MiB| timeout | 0 | | | |bench_14941.smt2 | 19.412s | 407.0MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc6298.smt2 | 19.418s | 315.0MiB| timeout | 0 | | | |bench_11736.smt2 | 19.420s | 96.508MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc6229.smt2 | 19.421s | 312.0MiB| timeout | 0 | | | |src_wget_vc17906.smt2 | 19.421s | 2575.0MiB| timeout | 0 | | | |innfeed_innfeed_vc36634.smt2 | 19.424s | 1339.0MiB| timeout | 0 | | | |bin_eventlogadm_vc331097.smt2 | 19.427s | 443.0MiB| timeout | 0 | | | |bench_14595.smt2 | 19.428s | 75.872MiB| timeout | 0 | | | |bin_libsmbclient_vc1225835.smt2 | 19.429s | 1597.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225783.smt2 | 19.430s | 629.0MiB| timeout | 0 | | | |innfeed_innfeed_vc36443.smt2 | 19.433s | 1133.0MiB| timeout | 0 | | | |bench_12422.smt2 | 19.434s | 1698.0MiB| timeout | 0 | | | |170.smt2 | 19.438s | 238.0MiB| timeout | 0 | | | |unconstrained04.smt2 | 19.438s | 6382.0MiB| timeout | 0 | | | |bench_334.smt2 | 19.439s | 391.0MiB| timeout | 0 | | | |innfeed_innfeed_vc36615.smt2 | 19.439s | 1223.0MiB| timeout | 0 | | | |bench_3953.smt2 | 19.443s | 70.8MiB| timeout | 0 | | | |bin_libsmbclient_vc1225887.smt2 | 19.445s | 1877.0MiB| timeout | 0 | | | |bench_1844.smt2 | 19.446s | 60.628MiB| timeout | 0 | | | |bench_5191.smt2 | 19.447s | 53.98MiB| timeout | 0 | | | |innfeed_innfeed_vc36461.smt2 | 19.453s | 1460.0MiB| timeout | 0 | | | |bench_1166.smt2 | 19.457s | 63.124MiB| timeout | 0 | | | |bench_5270.smt2 | 19.459s | 290.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225764.smt2 | 19.459s | 1131.0MiB| timeout | 0 | | | |bench_1081.smt2 | 19.467s | 73.152MiB| timeout | 0 | | | |bench_1712.smt2 | 19.467s | 92.82MiB| timeout | 0 | | | |bench_17759.smt2 | 19.470s | 289.0MiB| timeout | 0 | | | |bench_15719.smt2 | 19.471s | 394.0MiB| timeout | 0 | | | |bench_1560.smt2 | 19.471s | 74.572MiB| timeout | 0 | | | |bench_6462.smt2 | 19.473s | 55.276MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21428.smt2 | 19.477s | 705.0MiB| timeout | 0 | | | |mobiledevice_bit8_na6_nr3_twocond.smt2 | 19.480s | 913.0MiB| timeout | 0 | | | |bench_5898.smt2 | 19.483s | 276.0MiB| timeout | 0 | | | |bench_3575.smt2 | 19.486s | 73.04MiB| timeout | 0 | | | |bench_14358.smt2 | 19.487s | 99.0MiB| timeout | 0 | | | |bench_1350.smt2 | 19.488s | 54.048MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc6314.smt2 | 19.488s | 249.0MiB| timeout | 0 | | | |src_wget_vc17912.smt2 | 19.490s | 1490.0MiB| timeout | 0 | | | |predicate_735.smt2 | 19.492s | 2247.0MiB| timeout | 0 | | | |bench_7152.smt2 | 19.492s | 378.0MiB| timeout | 0 | | | |64.smt2 | 19.496s | 229.0MiB| timeout | 0 | | | |bench_15711.smt2 | 19.500s | 253.0MiB| timeout | 0 | | | |29.smt2 | 19.500s | 158.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225762.smt2 | 19.502s | 560.0MiB| timeout | 0 | | | |innfeed_imapfeed_vc24829.smt2 | 19.504s | 830.0MiB| timeout | 0 | | | |bench_4893.smt2 | 19.504s | 57.112MiB| timeout | 0 | | | |bin_libmsrpc_vc1225320.smt2 | 19.505s | 965.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225318.smt2 | 19.510s | 854.0MiB| timeout | 0 | | | |bench_17082.smt2 | 19.516s | 764.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225305.smt2 | 19.518s | 975.0MiB| timeout | 0 | | | |src_wget_vc17891.smt2 | 19.523s | 1041.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1232117.smt2 | 19.524s | 757.0MiB| timeout | 0 | | | |bench_1822.smt2 | 19.526s | 54.316MiB| timeout | 0 | | | |bench_11708.smt2 | 19.528s | 1351.0MiB| timeout | 0 | | | |ndist.b.28982.smt2 | 19.528s | 643.0MiB| timeout | 0 | | | |bench_2831.smt2 | 19.529s | 61.18MiB| timeout | 0 | | | |bench_11341.smt2 | 19.530s | 379.0MiB| timeout | 0 | | | |bench_10714.smt2 | 19.531s | 130.0MiB| timeout | 0 | | | |div.c.20.smt2 | 19.531s | 1980.0MiB| timeout | 0 | | | |bench_6606.smt2 | 19.534s | 328.0MiB| timeout | 0 | | | |90.smt2 | 19.539s | 241.0MiB| timeout | 0 | | | |bench_14861.smt2 | 19.539s | 165.0MiB| timeout | 0 | | | |bench_1760.smt2 | 19.540s | 54.86MiB| timeout | 0 | | | |bench_3015.smt2 | 19.540s | 60.344MiB| timeout | 0 | | | |bin_libmsrpc_vc1225394.smt2 | 19.547s | 847.0MiB| timeout | 0 | | | |bench_9360.smt2 | 19.547s | 90.36MiB| timeout | 0 | | | |bench_5466.smt2 | 19.552s | 61.188MiB| timeout | 0 | | | |innd_innd_vc33343.smt2 | 19.555s | 834.0MiB| timeout | 0 | | | |98.smt2 | 19.558s | 179.0MiB| timeout | 0 | | | |bench_4037.smt2 | 19.559s | 303.0MiB| timeout | 0 | | | |innd_innd_vc32642.smt2 | 19.563s | 632.0MiB| timeout | 0 | | | |bench_4822.smt2 | 19.564s | 92.524MiB| timeout | 0 | | | |bench_3181.smt2 | 19.568s | 53.604MiB| timeout | 0 | | | |bench_10784.smt2 | 19.570s | 102.0MiB| timeout | 0 | | | |bench_4933.smt2 | 19.570s | 216.0MiB| timeout | 0 | | | |bench_1810.smt2 | 19.573s | 62.22MiB| timeout | 0 | | | |innd_innd_vc33728.smt2 | 19.573s | 981.0MiB| timeout | 0 | | | |bench_5296.smt2 | 19.575s | 61.964MiB| timeout | 0 | | | |innfeed_imapfeed_vc25433.smt2 | 19.580s | 891.0MiB| timeout | 0 | | | |bench_16245.smt2 | 19.581s | 217.0MiB| timeout | 0 | | | |bench_4289.smt2 | 19.582s | 271.0MiB| timeout | 0 | | | |bench_15255.smt2 | 19.583s | 330.0MiB| timeout | 0 | | | |bench_3968.smt2 | 19.586s | 206.0MiB| timeout | 0 | | | |bench_261.smt2 | 19.587s | 141.0MiB| sat | 0 | | | |bench_2628.smt2 | 19.589s | 60.268MiB| timeout | 0 | | | |bench_1555.smt2 | 19.590s | 62.764MiB| timeout | 0 | | | |bench_4724.smt2 | 19.594s | 3291.0MiB| timeout | 0 | | | |unconstrained08.smt2 | 19.600s | 3198.0MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21209.smt2 | 19.600s | 1893.0MiB| timeout | 0 | | | |bench_2842.smt2 | 19.601s | 58.992MiB| timeout | 0 | | | |bench_2425.smt2 | 19.601s | 52.36MiB| timeout | 0 | | | |nnrpd_nnrpd_vc20411.smt2 | 19.601s | 955.0MiB| timeout | 0 | | | |bench_12246.smt2 | 19.603s | 293.0MiB| timeout | 0 | | | |src_wget_vc17911.smt2 | 19.605s | 2753.0MiB| timeout | 0 | | | |bench_1608.smt2 | 19.605s | 58.9MiB| timeout | 0 | | | |bin_libmsrpc_vc1225395.smt2 | 19.606s | 798.0MiB| timeout | 0 | | | |bench_2915.smt2 | 19.607s | 52.56MiB| timeout | 0 | | | |bench_3521.smt2 | 19.607s | 59.972MiB| timeout | 0 | | | |bench_1657.smt2 | 19.608s | 52.464MiB| timeout | 0 | | | |bench_5223.smt2 | 19.609s | 58.508MiB| timeout | 0 | | | |bench_11473.smt2 | 19.609s | 679.0MiB| timeout | 0 | | | |Sz512_15128_2.smt2 | 19.611s | 70.696MiB| timeout | 0 | | | |innd_innd_vc33732.smt2 | 19.612s | 743.0MiB| timeout | 0 | | | |bench_2547.smt2 | 19.613s | 63.26MiB| timeout | 0 | | | |predicate_169_0.smt2 | 19.618s | 1535.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1232030.smt2 | 19.632s | 813.0MiB| timeout | 0 | | | |bench_2962.smt2 | 19.633s | 148.0MiB| timeout | 0 | | | |bench_1837.smt2 | 19.638s | 70.512MiB| timeout | 0 | | | |bench_4015.smt2 | 19.641s | 252.0MiB| timeout | 0 | | | |6moves_mti_7-Atd_00004_bmc.smt2 | 19.646s | 55.964MiB| timeout | 0 | | | |bin_eventlogadm_vc331161.smt2 | 19.654s | 965.0MiB| timeout | 0 | | | |bench_2817.smt2 | 19.663s | 66.58MiB| timeout | 0 | | | |bin_libsmbclient_vc1225826.smt2 | 19.663s | 980.0MiB| timeout | 0 | | | |bench_1621.smt2 | 19.670s | 56.384MiB| timeout | 0 | | | |bench_14284.smt2 | 19.673s | 367.0MiB| timeout | 0 | | | |bench_8562.smt2 | 19.676s | 152.0MiB| timeout | 0 | | | |bench_1013.smt2 | 19.677s | 62.492MiB| timeout | 0 | | | |bin_libmsrpc_vc1232128.smt2 | 19.685s | 884.0MiB| timeout | 0 | | | |bench_253.smt2 | 19.690s | 148.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1228571.smt2 | 19.691s | 848.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225271.smt2 | 19.692s | 783.0MiB| timeout | 0 | | | |innfeed_imapfeed_vc24797.smt2 | 19.693s | 1473.0MiB| timeout | 0 | | | |bench_620.smt2 | 19.693s | 174.0MiB| timeout | 0 | | | |bench_3174.smt2 | 19.694s | 63.064MiB| timeout | 0 | | | |bench_1504.smt2 | 19.696s | 288.0MiB| timeout | 0 | | | |bench_11811.smt2 | 19.698s | 306.0MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc7131.smt2 | 19.703s | 456.0MiB| timeout | 0 | | | |innfeed_innfeed_vc37058.smt2 | 19.717s | 729.0MiB| timeout | 0 | | | |bench_3557.smt2 | 19.718s | 81.376MiB| timeout | 0 | | | |innd_innd_vc32492.smt2 | 19.722s | 1201.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225336.smt2 | 19.728s | 1585.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225246.smt2 | 19.729s | 1425.0MiB| timeout | 0 | | | |bench_4405.smt2 | 19.735s | 79.968MiB| timeout | 0 | | | |bin_libmsrpc_vc1225380.smt2 | 19.736s | 622.0MiB| timeout | 0 | | | |bench_1872.smt2 | 19.737s | 59.156MiB| timeout | 0 | | | |bench_2248.smt2 | 19.739s | 56.596MiB| timeout | 0 | | | |bench_10144.smt2 | 19.742s | 494.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1228491.smt2 | 19.742s | 815.0MiB| timeout | 0 | | | |bench_1388.smt2 | 19.747s | 59.028MiB| timeout | 0 | | | |bench_8495.smt2 | 19.750s | 2008.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1228474.smt2 | 19.755s | 1630.0MiB| timeout | 0 | | | |bench_4385.smt2 | 19.763s | 386.0MiB| timeout | 0 | | | |bench_17033.smt2 | 19.766s | 141.0MiB| timeout | 0 | | | |innd_innd_vc33743.smt2 | 19.769s | 1374.0MiB| timeout | 0 | | | |bench_6408.smt2 | 19.771s | 183.0MiB| timeout | 0 | | | |bench_14984.smt2 | 19.772s | 559.0MiB| timeout | 0 | | | |bench_4173.smt2 | 19.776s | 3301.0MiB| timeout | 0 | | | |bin_eventlogadm_vc331169.smt2 | 19.781s | 1244.0MiB| timeout | 0 | | | |bench_1586.smt2 | 19.785s | 61.404MiB| timeout | 0 | | | |bench_2397.smt2 | 19.788s | 55.248MiB| timeout | 0 | | | |bench_2443.smt2 | 19.794s | 57.08MiB| timeout | 0 | | | |bench_3173.smt2 | 19.794s | 64.2MiB| timeout | 0 | | | |bench_3159.smt2 | 19.795s | 55.148MiB| timeout | 0 | | | |bench_2278.smt2 | 19.796s | 59.612MiB| timeout | 0 | | | |bench_2849.smt2 | 19.798s | 64.12MiB| timeout | 0 | | | |bench_14932.smt2 | 19.804s | 65.88MiB| timeout | 0 | | | |bin_libsmbclient_vc1228531.smt2 | 19.804s | 2048.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1232066.smt2 | 19.805s | 637.0MiB| timeout | 0 | | | |bench_1355.smt2 | 19.816s | 54.236MiB| timeout | 0 | | | |bench_985.smt2 | 19.826s | 221.0MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21244.smt2 | 19.829s | 1524.0MiB| timeout | 0 | | | |bench_994.smt2 | 19.831s | 223.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225806.smt2 | 19.835s | 821.0MiB| timeout | 0 | | | |10.smt2 | 19.841s | 127.0MiB| timeout | 0 | | | |bench_2162.smt2 | 19.850s | 60.328MiB| timeout | 0 | | | |smulov4bw1024.smt2 | 19.850s | 3876.0MiB| timeout | 0 | | | |bench_1218.smt2 | 19.853s | 62.252MiB| timeout | 0 | | | |bench_10033.smt2 | 19.855s | 61.044MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc7750.smt2 | 19.862s | 538.0MiB| timeout | 0 | | | |bench_232.smt2 | 19.863s | 75.976MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc7727.smt2 | 19.870s | 663.0MiB| timeout | 0 | | | |bench_10306.smt2 | 19.873s | 119.0MiB| timeout | 0 | | | |bench_1365.smt2 | 19.883s | 60.656MiB| timeout | 0 | | | |bench_11033.smt2 | 19.883s | 274.0MiB| timeout | 0 | | | |bench_2268.smt2 | 19.886s | 55.176MiB| timeout | 0 | | | |bin_libmsrpc_vc1225912.smt2 | 19.887s | 1644.0MiB| timeout | 0 | | | |bench_1145.smt2 | 19.887s | 70.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225213.smt2 | 19.896s | 483.0MiB| timeout | 0 | | | |bench_3943.smt2 | 19.902s | 218.0MiB| timeout | 0 | | | |bench_3177.smt2 | 19.903s | 62.072MiB| timeout | 0 | | | |Example_17.txt.smt2 | 19.904s | 131.0MiB| timeout | 0 | | | |bench_154.smt2 | 19.905s | 55.9MiB| timeout | 0 | | | |115.smt2 | 19.906s | 186.0MiB| timeout | 0 | | | |bench_2034.smt2 | 19.909s | 64.036MiB| timeout | 0 | | | |innd_innd_vc33153.smt2 | 19.912s | 930.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225279.smt2 | 19.914s | 2591.0MiB| timeout | 0 | | | |bench_5974.smt2 | 19.915s | 446.0MiB| timeout | 0 | | | |bench_996.smt2 | 19.920s | 190.0MiB| timeout | 0 | | | |bench_10800.smt2 | 19.922s | 84.16MiB| timeout | 0 | | | |bench_3113.smt2 | 19.924s | 59.66MiB| timeout | 0 | | | |bench_12158.smt2 | 19.927s | 98.608MiB| timeout | 0 | | | |bench_6012.smt2 | 19.927s | 281.0MiB| timeout | 0 | | | |innfeed_innfeed_vc37055.smt2 | 19.928s | 2008.0MiB| timeout | 0 | | | |bench_2757.smt2 | 19.929s | 78.084MiB| timeout | 0 | | | |bench_4957.smt2 | 19.930s | 55.284MiB| timeout | 0 | | | |bench_9299.smt2 | 19.930s | 66.772MiB| timeout | 0 | | | |bench_1841.smt2 | 19.931s | 78.576MiB| timeout | 0 | | | |bench_5421.smt2 | 19.932s | 73.8MiB| timeout | 0 | | | |bin_libmsrpc_vc1225939.smt2 | 19.933s | 495.0MiB| timeout | 0 | | | |bench_2330.smt2 | 19.939s | 65.636MiB| timeout | 0 | | | |bench_3182.smt2 | 19.940s | 305.0MiB| timeout | 0 | | | |bench_1306.smt2 | 19.941s | 67.964MiB| timeout | 0 | | | |bench_1567.smt2 | 19.941s | 63.332MiB| timeout | 0 | | | |bench_674.smt2 | 19.953s | 213.0MiB| timeout | 0 | | | |bench_17335.smt2 | 19.953s | 377.0MiB| timeout | 0 | | | |bench_9535.smt2 | 19.954s | 78.664MiB| timeout | 0 | | | |bench_1050.smt2 | 19.962s | 64.504MiB| timeout | 0 | | | |bench_5435.smt2 | 19.962s | 53.152MiB| timeout | 0 | | | |bench_2121.smt2 | 19.964s | 59.224MiB| timeout | 0 | | | |bench_3603.smt2 | 19.965s | 76.8MiB| timeout | 0 | | | |bench_2144.smt2 | 19.965s | 54.748MiB| timeout | 0 | | | |bench_1256.smt2 | 19.965s | 55.86MiB| timeout | 0 | | | |bench_1721.smt2 | 19.966s | 59.476MiB| timeout | 0 | | | |bench_3240.smt2 | 19.966s | 60.44MiB| timeout | 0 | | | |bench_12059.smt2 | 19.967s | 73.156MiB| timeout | 0 | | | |bench_12821.smt2 | 19.968s | 130.0MiB| timeout | 0 | | | |bench_3451.smt2 | 19.968s | 59.624MiB| timeout | 0 | | | |bench_3246.smt2 | 19.968s | 219.0MiB| timeout | 0 | | | |bench_1992.smt2 | 19.969s | 69.532MiB| timeout | 0 | | | |bin_libmsrpc_vc1228527.smt2 | 19.969s | 620.0MiB| timeout | 0 | | | |bench_2826.smt2 | 19.971s | 55.496MiB| timeout | 0 | | | |bench_3326.smt2 | 19.972s | 56.428MiB| timeout | 0 | | | |bench_1496.smt2 | 19.972s | 60.88MiB| timeout | 0 | | | |bench_1578.smt2 | 19.973s | 59.012MiB| timeout | 0 | | | |bin_libmsrpc_vc1228487.smt2 | 19.974s | 922.0MiB| timeout | 0 | | | |bench_3080.smt2 | 19.974s | 62.648MiB| timeout | 0 | | | |unconstrained07.smt2 | 19.974s | 6382.0MiB| timeout | 0 | | | |bench_16594.smt2 | 19.975s | 275.0MiB| timeout | 0 | | | |bench_6691.smt2 | 19.976s | 54.788MiB| timeout | 0 | | | |bench_7116.smt2 | 19.976s | 169.0MiB| timeout | 0 | | | |bench_1958.smt2 | 19.977s | 59.244MiB| timeout | 0 | | | |bench_2629.smt2 | 19.977s | 61.876MiB| timeout | 0 | | | |rand_20_100_1235851242_0_k-3_v-15_e-25_sat.gph.smt2 | 19.977s | 97.0MiB| timeout | 0 | | | |bench_11014.smt2 | 19.979s | 238.0MiB| timeout | 0 | | | |bench_1756.smt2 | 19.979s | 526.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1232071.smt2 | 19.980s | 1417.0MiB| timeout | 0 | | | |bench_5395.smt2 | 19.981s | 53.332MiB| timeout | 0 | | | |bench_3297.smt2 | 19.981s | 58.076MiB| timeout | 0 | | | |bench_6665.smt2 | 19.982s | 61.252MiB| timeout | 0 | | | |bench_2594.smt2 | 19.983s | 58.472MiB| timeout | 0 | | | |bench_2263.smt2 | 19.984s | 55.212MiB| timeout | 0 | | | |bench_1498.smt2 | 19.984s | 62.76MiB| timeout | 0 | | | |bench_3499.smt2 | 19.984s | 53.576MiB| timeout | 0 | | | |bench_10737.smt2 | 19.985s | 338.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1228448.smt2 | 19.985s | 778.0MiB| timeout | 0 | | | |bench_3485.smt2 | 19.986s | 54.992MiB| timeout | 0 | | | |bench_15547.smt2 | 19.986s | 121.0MiB| timeout | 0 | | | |bench_2059.smt2 | 19.987s | 59.336MiB| timeout | 0 | | | |bench_3588.smt2 | 19.987s | 75.152MiB| timeout | 0 | | | |bench_1099.smt2 | 19.987s | 59.892MiB| timeout | 0 | | | |bench_1897.smt2 | 19.988s | 58.76MiB| timeout | 0 | | | |bench_3194.smt2 | 19.988s | 114.0MiB| timeout | 0 | | | |bench_3379.smt2 | 19.988s | 60.364MiB| timeout | 0 | | | |bench_5349.smt2 | 19.988s | 53.348MiB| timeout | 0 | | | |bench_13773.smt2 | 19.988s | 68.728MiB| timeout | 0 | | | |bench_14461.smt2 | 19.989s | 98.0MiB| timeout | 0 | | | |bench_1559.smt2 | 19.989s | 174.0MiB| timeout | 0 | | | |bin_eventlogadm_vc331154.smt2 | 19.989s | 393.0MiB| timeout | 0 | | | |innd_innd_vc33538.smt2 | 19.989s | 180.0MiB| timeout | 0 | | | |Sz512_15128_0.smt2 | 19.989s | 90.888MiB| timeout | 0 | | | |bench_1329.smt2 | 19.990s | 261.0MiB| timeout | 0 | | | |bench_3010.smt2 | 19.991s | 50.472MiB| timeout | 0 | | | |bench_2115.smt2 | 19.991s | 52.952MiB| timeout | 0 | | | |bench_1286.smt2 | 19.991s | 63.448MiB| timeout | 0 | | | |bench_145.smt2 | 19.991s | 69.916MiB| timeout | 0 | | | |bench_16064.smt2 | 19.991s | 218.0MiB| timeout | 0 | | | |bench_10791.smt2 | 19.991s | 421.0MiB| timeout | 0 | | | |111.smt2 | 19.991s | 518.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1232034.smt2 | 19.992s | 646.0MiB| timeout | 0 | | | |bench_1222.smt2 | 19.992s | 61.84MiB| timeout | 0 | | | |problem_8.smt2 | 19.992s | 135.0MiB| timeout | 0 | | | |bench_1093.smt2 | 19.992s | 64.34MiB| timeout | 0 | | | |bench_14885.smt2 | 19.993s | 125.0MiB| timeout | 0 | | | |bench_3019.smt2 | 19.993s | 57.268MiB| timeout | 0 | | | |bench_12006.smt2 | 19.993s | 267.0MiB| timeout | 0 | | | |102.smt2 | 19.993s | 245.0MiB| timeout | 0 | | | |bench_3171.smt2 | 19.993s | 58.336MiB| timeout | 0 | | | |100.smt2 | 19.993s | 186.0MiB| timeout | 0 | | | |Sz512_15128_1.smt2 | 19.993s | 98.0MiB| timeout | 0 | | | |bench_14165.smt2 | 19.994s | 235.0MiB| timeout | 0 | | | |bench_5526.smt2 | 19.994s | 67.948MiB| timeout | 0 | | | |bench_2174.smt2 | 19.994s | 56.184MiB| timeout | 0 | | | |bench_2050.smt2 | 19.994s | 57.656MiB| timeout | 0 | | | |bench_1724.smt2 | 19.994s | 60.576MiB| timeout | 0 | | | |bench_5302.smt2 | 19.994s | 57.072MiB| timeout | 0 | | | |bench_2076.smt2 | 19.994s | 60.584MiB| timeout | 0 | | | |bench_2602.smt2 | 19.995s | 245.0MiB| timeout | 0 | | | |bench_2380.smt2 | 19.995s | 241.0MiB| timeout | 0 | | | |bench_323.smt2 | 19.995s | 92.384MiB| timeout | 0 | | | |bench_7005.smt2 | 19.996s | 195.0MiB| timeout | 0 | | | |bench_12473.smt2 | 19.996s | 198.0MiB| timeout | 0 | | | |bench_1981.smt2 | 19.996s | 66.516MiB| timeout | 0 | | | |bench_2586.smt2 | 19.996s | 213.0MiB| timeout | 0 | | | |bench_1585.smt2 | 19.997s | 75.248MiB| timeout | 0 | | | |bench_1977.smt2 | 19.997s | 55.648MiB| timeout | 0 | | | |bench_2606.smt2 | 19.997s | 63.536MiB| timeout | 0 | | | |bench_14209.smt2 | 19.997s | 70.38MiB| timeout | 0 | | | |bench_10451.smt2 | 19.997s | 3310.0MiB| timeout | 0 | | | |bench_11027.smt2 | 19.997s | 150.0MiB| timeout | 0 | | | |bench_2170.smt2 | 19.998s | 57.768MiB| timeout | 0 | | | |bench_1349.smt2 | 19.998s | 54.896MiB| timeout | 0 | | | |bench_9301.smt2 | 19.998s | 312.0MiB| timeout | 0 | | | |bench_2992.smt2 | 19.998s | 68.084MiB| timeout | 0 | | | |bench_2083.smt2 | 19.998s | 57.852MiB| timeout | 0 | | | |162.smt2 | 19.998s | 230.0MiB| timeout | 0 | | | |bench_9173.smt2 | 19.998s | 58.524MiB| timeout | 0 | | | |bench_16862.smt2 | 19.998s | 136.0MiB| timeout | 0 | | | |rand_150_600_1159731678_15.lp.smt2 | 19.998s | 133.0MiB| timeout | 0 | | | |bench_5340.smt2 | 19.999s | 56.512MiB| timeout | 0 | | | |bench_2463.smt2 | 19.999s | 57.04MiB| timeout | 0 | | | |bench_5096.smt2 | 19.999s | 56.168MiB| timeout | 0 | | | |bench_479.smt2 | 19.999s | 215.0MiB| timeout | 0 | | | |bench_4873.smt2 | 19.999s | 55.46MiB| timeout | 0 | | | |bench_1447.smt2 | 19.999s | 58.428MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc6242.smt2 | 19.999s | 251.0MiB| timeout | 0 | | | |bench_2599.smt2 | 20.000s | 58.604MiB| timeout | 0 | | | |bench_1204.smt2 | 20.000s | 57.336MiB| timeout | 0 | | | |bench_6882.smt2 | 20.000s | 118.0MiB| timeout | 0 | | | |bench_1522.smt2 | 20.000s | 55.48MiB| timeout | 0 | | | |bench_14156.smt2 | 20.000s | 359.0MiB| timeout | 0 | | | |bench_1196.smt2 | 20.001s | 59.24MiB| timeout | 0 | | | |bench_6742.smt2 | 20.001s | 74.632MiB| timeout | 0 | | | |bench_3516.smt2 | 20.001s | 104.0MiB| timeout | 0 | | | |bench_14161.smt2 | 20.001s | 234.0MiB| timeout | 0 | | | |bench_1184.smt2 | 20.002s | 63.74MiB| timeout | 0 | | | |33.smt2 | 20.002s | 132.0MiB| timeout | 0 | | | |bench_1907.smt2 | 20.002s | 66.136MiB| timeout | 0 | | | |bench_3420.smt2 | 20.002s | 63.62MiB| timeout | 0 | | | |problem_7.smt2 | 20.002s | 104.0MiB| timeout | 0 | | | |bench_2773.smt2 | 20.003s | 328.0MiB| timeout | 0 | | | |mult2.c.10.smt2 | 20.003s | 214.0MiB| timeout | 0 | | | |bench_9946.smt2 | 20.004s | 53.388MiB| timeout | 0 | | | |bench_2284.smt2 | 20.004s | 53.668MiB| timeout | 0 | | | |bench_992.smt2 | 20.004s | 237.0MiB| timeout | 0 | | | |bench_1614.smt2 | 20.004s | 60.064MiB| timeout | 0 | | | |bench_8147.smt2 | 20.004s | 143.0MiB| timeout | 0 | | | |gryzzles.22.lp.smt2 | 20.004s | 97.852MiB| timeout | 0 | | | |knightTour.in01.smt2 | 20.004s | 100.0MiB| timeout | 0 | | | |bench_1236.smt2 | 20.004s | 75.74MiB| timeout | 0 | | | |f23.smt2 | 20.005s | 203.0MiB| timeout | 0 | | | |bench_1168.smt2 | 20.005s | 194.0MiB| timeout | 0 | | | |bench_6016.smt2 | 20.005s | 445.0MiB| timeout | 0 | | | |bench_5137.smt2 | 20.005s | 54.44MiB| timeout | 0 | | | |bin_libmsrpc_vc1225405.smt2 | 20.005s | 1035.0MiB| timeout | 0 | | | |bench_4937.smt2 | 20.005s | 212.0MiB| timeout | 0 | | | |bench_13744.smt2 | 20.006s | 200.0MiB| timeout | 0 | | | |bench_228.smt2 | 20.006s | 235.0MiB| timeout | 0 | | | |bench_10096.smt2 | 20.006s | 218.0MiB| timeout | 0 | | | |80.smt2 | 20.007s | 258.0MiB| timeout | 0 | | | |bench_5329.smt2 | 20.007s | 178.0MiB| timeout | 0 | | | |bench_7306.smt2 | 20.007s | 73.292MiB| timeout | 0 | | | |bench_4461.smt2 | 20.008s | 146.0MiB| timeout | 0 | | | |bench_914.smt2 | 20.010s | 227.0MiB| timeout | 0 | | | |bench_3168.smt2 | 20.010s | 178.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225800.smt2 | 20.010s | 862.0MiB| timeout | 0 | | | |bench_449.smt2 | 20.013s | 194.0MiB| timeout | 0 | | | |innd_innd_vc33347.smt2 | 20.014s | 403.0MiB| timeout | 0 | | | |bench_4253.smt2 | 20.014s | 415.0MiB| timeout | 0 | | | |bench_313.smt2 | 20.016s | 311.0MiB| timeout | 0 | | | |bench_452.smt2 | 20.016s | 172.0MiB| timeout | 0 | | | |bench_13790.smt2 | 20.017s | 280.0MiB| timeout | 0 | | | |bench_13336.smt2 | 20.018s | 385.0MiB| timeout | 0 | | | |bin_libsmbsharemodes_vc6250.smt2 | 20.020s | 276.0MiB| timeout | 0 | | | |bench_8461.smt2 | 20.020s | 382.0MiB| timeout | 0 | | | |bench_12224.smt2 | 20.023s | 615.0MiB| timeout | 0 | | | |bench_11032.smt2 | 20.023s | 364.0MiB| timeout | 0 | | | |bench_4614.smt2 | 20.024s | 461.0MiB| timeout | 0 | | | |bench_11151.smt2 | 20.027s | 462.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225895.smt2 | 20.028s | 712.0MiB| timeout | 0 | | | |bench_224.smt2 | 20.028s | 614.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225236.smt2 | 20.029s | 698.0MiB| timeout | 0 | | | |bench_7085.smt2 | 20.030s | 361.0MiB| timeout | 0 | | | |bench_11110.smt2 | 20.030s | 290.0MiB| timeout | 0 | | | |bench_14720.smt2 | 20.031s | 413.0MiB| timeout | 0 | | | |innd_innd_vc33349.smt2 | 20.031s | 782.0MiB| timeout | 0 | | | |bin_eventlogadm_vc331156.smt2 | 20.032s | 1613.0MiB| timeout | 0 | | | |bench_3082.smt2 | 20.032s | 382.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225860.smt2 | 20.035s | 606.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225303.smt2 | 20.036s | 602.0MiB| timeout | 0 | | | |innfeed_imapfeed_vc24830.smt2 | 20.038s | 1056.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225733.smt2 | 20.038s | 524.0MiB| timeout | 0 | | | |108.smt2 | 20.038s | 537.0MiB| timeout | 0 | | | |mult1.c.20.smt2 | 20.039s | 392.0MiB| timeout | 0 | | | |innd_innd_vc33544.smt2 | 20.040s | 829.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225843.smt2 | 20.042s | 1200.0MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21451.smt2 | 20.044s | 622.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225841.smt2 | 20.044s | 520.0MiB| timeout | 0 | | | |bench_16409.smt2 | 20.044s | 633.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225330.smt2 | 20.044s | 868.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1228610.smt2 | 20.044s | 685.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1228446.smt2 | 20.045s | 710.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225454.smt2 | 20.046s | 1120.0MiB| timeout | 0 | | | |innd_innd_vc32659.smt2 | 20.046s | 1024.0MiB| timeout | 0 | | | |bench_10696.smt2 | 20.047s | 545.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225412.smt2 | 20.048s | 862.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1228491.smt2 | 20.050s | 649.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1228514.smt2 | 20.051s | 1210.0MiB| timeout | 0 | | | |innfeed_imapfeed_vc25444.smt2 | 20.052s | 898.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225316.smt2 | 20.053s | 689.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1228508.smt2 | 20.053s | 758.0MiB| timeout | 0 | | | |bench_13483.smt2 | 20.055s | 1246.0MiB| timeout | 0 | | | |div3.c.20.smt2 | 20.057s | 984.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225399.smt2 | 20.058s | 749.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225731.smt2 | 20.059s | 918.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1228509.smt2 | 20.060s | 821.0MiB| timeout | 0 | | | |innd_innd_vc33158.smt2 | 20.061s | 747.0MiB| timeout | 0 | | | |bin_eventlogadm_vc331146.smt2 | 20.062s | 836.0MiB| timeout | 0 | | | |innfeed_innfeed_vc37224.smt2 | 20.063s | 848.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225256.smt2 | 20.065s | 1121.0MiB| timeout | 0 | | | |bench_14598.smt2 | 20.066s | 368.0MiB| timeout | 0 | | | |innd_innd_vc32740.smt2 | 20.067s | 706.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225392.smt2 | 20.067s | 1054.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225275.smt2 | 20.071s | 902.0MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21229.smt2 | 20.072s | 534.0MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21446.smt2 | 20.072s | 826.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225264.smt2 | 20.078s | 1726.0MiB| timeout | 0 | | | |bench_10726.smt2 | 20.079s | 1365.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1232138.smt2 | 20.079s | 1004.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225257.smt2 | 20.079s | 1029.0MiB| timeout | 0 | | | |bench_3945.smt2 | 20.082s | 3555.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225910.smt2 | 20.083s | 1198.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1228430.smt2 | 20.088s | 1092.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1228496.smt2 | 20.090s | 1396.0MiB| timeout | 0 | | | |bench_15128.smt2 | 20.095s | 1062.0MiB| timeout | 0 | | | |src_wget_vc18506.smt2 | 20.096s | 1417.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1228512.smt2 | 20.099s | 1413.0MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21034.smt2 | 20.100s | 1239.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225815.smt2 | 20.100s | 1420.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225346.smt2 | 20.103s | 1840.0MiB| timeout | 0 | | | |bench_12204.smt2 | 20.103s | 3035.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1228452.smt2 | 20.109s | 1385.0MiB| timeout | 0 | | | |rfunit_flat-64.smt2 | 20.110s | 3793.0MiB| timeout | 0 | | | |innfeed_imapfeed_vc24828.smt2 | 20.116s | 2429.0MiB| timeout | 0 | | | |bench_11931.smt2 | 20.117s | 3308.0MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21232.smt2 | 20.118s | 884.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225858.smt2 | 20.124s | 1658.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225773.smt2 | 20.127s | 1228.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1228479.smt2 | 20.131s | 2109.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225761.smt2 | 20.137s | 1157.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225900.smt2 | 20.139s | 2293.0MiB| timeout | 0 | | | |bench_7150.smt2 | 20.142s | 3817.0MiB| timeout | 0 | | | |bin_eventlogadm_vc331166.smt2 | 20.142s | 1771.0MiB| timeout | 0 | | | |bin_libsmbclient_vc1225231.smt2 | 20.144s | 1056.0MiB| timeout | 0 | | | |innfeed_innfeed_vc37260.smt2 | 20.147s | 1644.0MiB| timeout | 0 | | | |bin_libmsrpc_vc1225408.smt2 | 20.150s | 2091.0MiB| timeout | 0 | | | |innfeed_imapfeed_vc25420.smt2 | 20.159s | 1916.0MiB| timeout | 0 | | | |predicate_275.smt2 | 20.187s | 2126.0MiB| timeout | 0 | | | |nnrpd_nnrpd_vc21636.smt2 | 20.208s | 2191.0MiB| timeout | 0 | | | |servers_slapd_a_vc149789.smt2 | 20.244s | 5214.0MiB| timeout | 0 | | | |bench_8564.smt2 | 20.246s | 3226.0MiB| timeout | 0 | | |