# . * SAT 477 * UNSAT 600 * TIMEOUT 47 * UNKNOWN 23 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: use has_real_monomial as the gate to bounded nlsat
Job tag: bnsat
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: e62d4e9d50ad91d0ba940dd95d2fb4c377b8c954
Z3 branch: bnsat
Z3 options: "-T:200 "
Z3 inputs: inputs/QF_NRA_small
Z3 commit message: Gate early bounded_nlsat on real monomials, remove parameter

Only call bounded_nlsat before the lemma return when the to-refine
set contains real (non-integer) monomials. Integer NLA problems are
better served by the lemma pipeline; calling nlsat drains the rlimit
budget without benefit. For real NLA (QF_NRA, QF_UFNRA, QF_NIRA with
reals), nlsat via CAD is the right approach when bounds propagation
is not converging.

Remove the arith.nl.nra_before_lemma_return parameter since the
has_real_monomial() gate is precise enough.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |atan-vega-3-weak-chunk-0534.smt2 | 0.024s | 19.148MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0103.smt2 | 0.025s | 20.908MiB| sat | 0 | | | |sin-cos-346-b-chunk-0348.smt2 | 0.025s | 18.836MiB| unsat | 0 | | | |sin-problem-10-2-chunk-0024.smt2 | 0.025s | 18.72MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0135.smt2 | 0.025s | 21.02MiB| unsat | 0 | | | |atan-vega-3-chunk-0350.smt2 | 0.025s | 18.98MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0021.smt2 | 0.025s | 18.696MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0316.smt2 | 0.026s | 19.22MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0079.smt2 | 0.026s | 18.708MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_linear_enc_global_1.smt2 | 0.027s | 18.888MiB| unsat | 0 | | | |ball_count_2d_plain.04.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.027s | 18.972MiB| unsat | 0 | | | |ball_count_1d_plain.04.seq_lazy_global_1.smt2 | 0.027s | 19.06MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0555.smt2 | 0.027s | 20.656MiB| sat | 0 | | | |log-fun-ineq-g-chunk-0036.smt2 | 0.027s | 18.752MiB| unsat | 0 | | | |sin-problem-7-weak2-chunk-0088.smt2 | 0.027s | 18.788MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0224.smt2 | 0.028s | 21.028MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0078.smt2 | 0.028s | 19.04MiB| unsat | 0 | | | |Chua-2-VC2-L-chunk-0029.smt2 | 0.028s | 20.708MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0205.smt2 | 0.028s | 20.856MiB| unsat | 0 | | | |atan-vega-3-chunk-0210.smt2 | 0.028s | 20.748MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0059.smt2 | 0.028s | 20.808MiB| unsat | 0 | | | |atan-vega-3-chunk-0099.smt2 | 0.028s | 20.624MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0171.smt2 | 0.028s | 18.732MiB| unsat | 0 | | | |Chua-2-VC2-L-chunk-0040.smt2 | 0.029s | 20.884MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0067.smt2 | 0.029s | 20.884MiB| sat | 0 | | | |atan-problem-2-chunk-0080.smt2 | 0.029s | 20.756MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0021.smt2 | 0.029s | 20.768MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0020.smt2 | 0.029s | 21.048MiB| sat | 0 | | | |polypaver-bench-exp-3d-chunk-0085.smt2 | 0.029s | 20.76MiB| unsat | 0 | | | |sin-problem-7-chunk-0361.smt2 | 0.029s | 18.94MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0129.smt2 | 0.029s | 18.916MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0076.smt2 | 0.029s | 20.764MiB| unsat | 0 | | | |sin-problem-7-chunk-0091.smt2 | 0.029s | 20.948MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0046.smt2 | 0.029s | 20.84MiB| sat | 0 | | | |sin-cos-346-b-chunk-0102.smt2 | 0.029s | 18.98MiB| unsat | 0 | | | |Chua-1-VC1-U-chunk-0032.smt2 | 0.030s | 21.08MiB| sat | 0 | | | |atan-problem-2-chunk-0037.smt2 | 0.030s | 20.652MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0084.smt2 | 0.030s | 18.952MiB| unsat | 0 | | | |Chua-1-IL-U-chunk-0038.smt2 | 0.030s | 20.6MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_global_7.smt2 | 0.030s | 19.524MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0052.smt2 | 0.030s | 20.676MiB| sat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_linear_enc_global_5.smt2 | 0.030s | 19.568MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0057.smt2 | 0.030s | 20.512MiB| sat | 0 | | | |sin-cos-346-b-chunk-0092.smt2 | 0.030s | 18.912MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0010.smt2 | 0.030s | 20.6MiB| sat | 0 | | | |Chua-1-IL-U-chunk-0025.smt2 | 0.030s | 20.568MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0008.smt2 | 0.030s | 20.596MiB| unsat | 0 | | | |ball_count_1d_plain.05.redlog_global_1.smt2 | 0.030s | 18.98MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0434.smt2 | 0.031s | 20.892MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0218.smt2 | 0.031s | 20.928MiB| unsat | 0 | | | |MulliganEconomicsModel0006a.smt2 | 0.031s | 20.696MiB| sat | 0 | | | |ball_count_2d_hill.10.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.031s | 19.056MiB| unsat | 0 | | | |ball_count_1d_plain.02.redlog_global_3.smt2 | 0.031s | 19.06MiB| unsat | 0 | | | |CMOS-opamp-chunk-0213.smt2 | 0.031s | 20.652MiB| sat | 0 | | | |Chua-1-VC2-L-chunk-0027.smt2 | 0.031s | 18.708MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0671.smt2 | 0.031s | 20.904MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0021.smt2 | 0.031s | 20.636MiB| sat | 0 | | | |sin-cos-346-b-chunk-0494.smt2 | 0.031s | 20.764MiB| sat | 0 | | | |polypaver-bench-exp-3d-chunk-0126.smt2 | 0.031s | 20.964MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0024.smt2 | 0.031s | 20.54MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_lemmas_global_5.smt2 | 0.031s | 19.196MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0043.smt2 | 0.031s | 20.656MiB| sat | 0 | | | |atan-vega-3-chunk-0045.smt2 | 0.031s | 20.708MiB| sat | 0 | | | |CMOS-opamp-chunk-0137.smt2 | 0.031s | 20.708MiB| sat | 0 | | | |atan-problem-1-chunk-0022.smt2 | 0.031s | 20.852MiB| sat | 0 | | | |Chua-1-IL-U-chunk-0049.smt2 | 0.031s | 20.68MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0107.smt2 | 0.031s | 20.608MiB| unsat | 0 | | | |ball_count_2d_hill.10.seq_lazy_global_3.smt2 | 0.031s | 19.228MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.redlog_global_3.smt2 | 0.031s | 19.128MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0183.smt2 | 0.031s | 20.66MiB| sat | 0 | | | |ball_count_2d_hill.01.seq_lazy_global_3.smt2 | 0.031s | 19.284MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0066.smt2 | 0.031s | 20.664MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0277.smt2 | 0.031s | 21.012MiB| unsat | 0 | | | |sqrt-problem-12vars3-chunk-0068.smt2 | 0.031s | 20.792MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0435.smt2 | 0.031s | 20.764MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0115.smt2 | 0.032s | 20.66MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.redlog_global_7.smt2 | 0.032s | 19.504MiB| unsat | 0 | | | |ball_count_1d_plain.03.qfree_global_3.smt2 | 0.032s | 20.976MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0504.smt2 | 0.032s | 21.24MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0301.smt2 | 0.032s | 20.764MiB| sat | 0 | | | |atan-problem-2-chunk-0059.smt2 | 0.032s | 20.676MiB| sat | 0 | | | |CMOS-opamp-chunk-0062.smt2 | 0.032s | 20.796MiB| unsat | 0 | | | |atan-problem-1-weak-chunk-0035.smt2 | 0.032s | 20.612MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0023.smt2 | 0.032s | 20.92MiB| sat | 0 | | | |Chua-1-VC2-L-chunk-0077.smt2 | 0.032s | 20.948MiB| sat | 0 | | | |matrix-1-all-47.smt2 | 0.032s | 20.708MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0510.smt2 | 0.032s | 20.78MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0132.smt2 | 0.032s | 20.84MiB| unsat | 0 | | | |atan-vega-3-chunk-0370.smt2 | 0.032s | 20.772MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0071.smt2 | 0.032s | 20.98MiB| unsat | 0 | | | |atan-vega-3-chunk-0463.smt2 | 0.032s | 21.04MiB| sat | 0 | | | |exp-problem-10-2-chunk-0184.smt2 | 0.032s | 20.804MiB| sat | 0 | | | |atan-vega-3-chunk-0523.smt2 | 0.032s | 20.916MiB| sat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0086.smt2 | 0.032s | 20.764MiB| sat | 0 | | | |CMOS-opamp-chunk-0096.smt2 | 0.032s | 20.82MiB| sat | 0 | | | |atan-vega-3-chunk-0563.smt2 | 0.032s | 20.832MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0009.smt2 | 0.032s | 18.712MiB| unsat | 0 | | | |ball_count_1d_plain.10.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.032s | 18.912MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0073.smt2 | 0.033s | 20.8MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0016.smt2 | 0.033s | 20.792MiB| sat | 0 | | | |Lyapunov1a-chunk-0021.smt2 | 0.033s | 20.728MiB| sat | 0 | | | |sin-344-3-chunk-0046.smt2 | 0.033s | 20.828MiB| sat | 0 | | | |sqrt-problem-13-vars5-chunk-0026.smt2 | 0.033s | 20.788MiB| sat | 0 | | | |sqrt-problem-Melquiond3-chunk-0018.smt2 | 0.033s | 20.6MiB| sat | 0 | | | |atan-vega-3-chunk-0543.smt2 | 0.033s | 20.764MiB| sat | 0 | | | |CMOS-opamp-chunk-0342.smt2 | 0.033s | 20.836MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0044.smt2 | 0.033s | 18.844MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0154.smt2 | 0.033s | 20.892MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.033s | 19.232MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0232.smt2 | 0.033s | 20.768MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0600.smt2 | 0.033s | 20.988MiB| unsat | 0 | | | |sin-344-4-chunk-0050.smt2 | 0.033s | 21.088MiB| sat | 0 | | | |atan-vega-3-chunk-0583.smt2 | 0.033s | 20.82MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0481.smt2 | 0.033s | 20.72MiB| unsat | 0 | | | |atan-vega-3-chunk-0067.smt2 | 0.033s | 20.872MiB| unsat | 0 | | | |CMOS-opamp-chunk-0025.smt2 | 0.033s | 20.636MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0100.smt2 | 0.033s | 20.644MiB| sat | 0 | | | |ball_count_2d_hill.04.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.033s | 18.98MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0098.smt2 | 0.033s | 20.636MiB| sat | 0 | | | |atan-vega-3-chunk-0027.smt2 | 0.033s | 20.764MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0146.smt2 | 0.033s | 18.716MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0661.smt2 | 0.033s | 19.072MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0147.smt2 | 0.033s | 20.756MiB| sat | 0 | | | |ball_count_1d_plain.01.qfree_global_1.smt2 | 0.033s | 18.984MiB| unsat | 0 | | | |CMOS-opamp-chunk-0231.smt2 | 0.033s | 20.572MiB| sat | 0 | | | |exp-problem-10-3-chunk-0063.smt2 | 0.033s | 20.64MiB| sat | 0 | | | |exp-problem-10-2-chunk-0385.smt2 | 0.033s | 20.656MiB| unsat | 0 | | | |CMOS-opamp-chunk-0298.smt2 | 0.033s | 20.848MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0241.smt2 | 0.033s | 20.768MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0209.smt2 | 0.034s | 20.508MiB| sat | 0 | | | |ball_count_1d_plain.10.seq_lazy_lemmas_global_11.smt2 | 0.034s | 19.564MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0160.smt2 | 0.034s | 20.764MiB| sat | 0 | | | |sin-cos-346-b-chunk-0414.smt2 | 0.034s | 20.764MiB| sat | 0 | | | |sin-problem-7-chunk-0335.smt2 | 0.034s | 20.9MiB| sat | 0 | | | |sin-cos-346-b-chunk-0326.smt2 | 0.034s | 20.496MiB| unsat | 0 | | | |ball_count_1d_plain.10.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.034s | 19.324MiB| unsat | 0 | | | |atan-vega-3-chunk-0089.smt2 | 0.034s | 20.812MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0102.smt2 | 0.034s | 20.832MiB| sat | 0 | | | |ball_count_2d_slope.01.seq_lazy_linear_enc_global_1.smt2 | 0.034s | 19.036MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0108.smt2 | 0.034s | 20.752MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0456.smt2 | 0.034s | 18.972MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0522.smt2 | 0.034s | 20.656MiB| sat | 0 | | | |sin-problem-7-chunk-0221.smt2 | 0.034s | 20.912MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0130.smt2 | 0.034s | 20.768MiB| unsat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0075.smt2 | 0.034s | 20.8MiB| sat | 0 | | | |sin-344-3-weak-chunk-0017.smt2 | 0.034s | 20.796MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0024.smt2 | 0.034s | 20.796MiB| sat | 0 | | | |Chua-1-VC1-U-chunk-0044.smt2 | 0.034s | 20.572MiB| sat | 0 | | | |sin-problem-7-chunk-0129.smt2 | 0.034s | 20.72MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0330.smt2 | 0.034s | 20.892MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0237.smt2 | 0.034s | 20.64MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0586.smt2 | 0.034s | 20.816MiB| sat | 0 | | | |bottom-plate-mixer-chunk-0039.smt2 | 0.034s | 20.664MiB| sat | 0 | | | |atan-vega-3-chunk-0553.smt2 | 0.034s | 20.636MiB| sat | 0 | | | |exp-problem-10-2-chunk-0144.smt2 | 0.034s | 20.68MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0312.smt2 | 0.034s | 20.892MiB| sat | 0 | | | |atan-vega-3-chunk-0623.smt2 | 0.034s | 20.904MiB| sat | 0 | | | |sqrt-problem-Melquiond2-chunk-0059.smt2 | 0.034s | 20.772MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0104.smt2 | 0.034s | 19.148MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0572.smt2 | 0.034s | 20.816MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0093.smt2 | 0.035s | 20.48MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0100.smt2 | 0.035s | 20.508MiB| sat | 0 | | | |ball_count_1d_plain.01.seq_lazy_linear_enc_global_15.smt2 | 0.035s | 20.06MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0146.smt2 | 0.035s | 20.696MiB| sat | 0 | | | |exp-problem-10-2-chunk-0112.smt2 | 0.035s | 20.9MiB| sat | 0 | | | |ball_count_2d_plain.02.seq_lazy_lemmas_global_9.smt2 | 0.035s | 19.76MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0032.smt2 | 0.035s | 20.796MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0056.smt2 | 0.035s | 20.784MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0479.smt2 | 0.035s | 20.568MiB| sat | 0 | | | |asin-8-vars4-chunk-0019.smt2 | 0.035s | 20.892MiB| sat | 0 | | | |atan-vega-3-chunk-0533.smt2 | 0.035s | 20.844MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0629.smt2 | 0.035s | 20.828MiB| sat | 0 | | | |atan-problem-2-chunk-0117.smt2 | 0.035s | 21.02MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0093.smt2 | 0.035s | 20.616MiB| sat | 0 | | | |asin-8-vars4-chunk-0034.smt2 | 0.035s | 20.576MiB| sat | 0 | | | |exp-problem-10-2-chunk-0275.smt2 | 0.035s | 20.784MiB| unsat | 0 | | | |ball_count_2d_plain.02.seq_lazy_linear_enc_lemmas_global_7.smt2 | 0.035s | 19.416MiB| unsat | 0 | | | |sin-problem-7-chunk-0105.smt2 | 0.035s | 20.756MiB| unsat | 0 | | | |MulliganEconomicsModel0018e.smt2 | 0.035s | 20.764MiB| sat | 0 | | | |exp-problem-10-3-chunk-0128.smt2 | 0.035s | 20.804MiB| unsat | 0 | | | |sin-problem-7-chunk-0208.smt2 | 0.035s | 20.8MiB| sat | 0 | | | |atan-vega-3-chunk-0483.smt2 | 0.035s | 20.764MiB| sat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.035s | 18.972MiB| unsat | 0 | | | |ball_count_2d_hill.10.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.035s | 19.8MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0224.smt2 | 0.035s | 20.82MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_linear_enc_global_5.smt2 | 0.035s | 19.508MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0691.smt2 | 0.035s | 20.816MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0103.smt2 | 0.035s | 20.804MiB| unsat | 0 | | | |sin-problem-7-weak2-chunk-0075.smt2 | 0.035s | 20.796MiB| sat | 0 | | | |cos-problem-5-chunk-0039.smt2 | 0.035s | 20.804MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0043.smt2 | 0.035s | 20.692MiB| unsat | 0 | | | |CMOS-opamp-chunk-0169.smt2 | 0.036s | 20.888MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.036s | 19.648MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0378.smt2 | 0.036s | 18.828MiB| unsat | 0 | | | |atan-problem-2-chunk-0011.smt2 | 0.036s | 20.68MiB| sat | 0 | | | |MulliganEconomicsModel0013c.smt2 | 0.036s | 20.904MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0087.smt2 | 0.036s | 20.652MiB| unsat | 0 | | | |ball_count_2d_hill.02.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.036s | 18.94MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0042.smt2 | 0.036s | 21.064MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0160.smt2 | 0.036s | 20.724MiB| unsat | 0 | | | |ball_count_2d_plain.01.seq_lazy_linear_enc_global_13.smt2 | 0.036s | 19.74MiB| unsat | 0 | | | |MulliganEconomicsModel0063e.smt2 | 0.036s | 20.692MiB| sat | 0 | | | |ball_count_1d_plain.01.qfree_global_5.smt2 | 0.036s | 19.26MiB| unsat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0015.smt2 | 0.036s | 20.704MiB| unsat | 0 | | | |ball_count_2d_plain.10.seq_lazy_linear_enc_global_13.smt2 | 0.036s | 19.792MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.036s | 20.16MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0164.smt2 | 0.036s | 20.744MiB| sat | 0 | | | |ball_count_1d_plain.10.qfree_global_5.smt2 | 0.036s | 19.096MiB| unsat | 0 | | | |atan-vega-3-chunk-0340.smt2 | 0.036s | 20.84MiB| sat | 0 | | | |CMOS-opamp-chunk-0108.smt2 | 0.036s | 20.98MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0415.smt2 | 0.036s | 20.648MiB| sat | 0 | | | |atan-vega-3-chunk-0220.smt2 | 0.036s | 18.992MiB| unsat | 0 | | | |ball_count_2d_hill.02.seq_lazy_global_3.smt2 | 0.036s | 19.116MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0038.smt2 | 0.036s | 20.676MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0086.smt2 | 0.036s | 20.672MiB| sat | 0 | | | |cbrt-problem-3-chunk-0070.smt2 | 0.036s | 20.76MiB| unsat | 0 | | | |CMOS-opamp-chunk-0047.smt2 | 0.036s | 20.588MiB| unsat | 0 | | | |ball_count_2d_plain.04.qfree_global_1.smt2 | 0.037s | 19.016MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0196.smt2 | 0.037s | 21.02MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0405.smt2 | 0.037s | 20.852MiB| sat | 0 | | | |atan-vega-3-chunk-0503.smt2 | 0.037s | 20.76MiB| sat | 0 | | | |ball_count_1d_plain.01.seq_lazy_lemmas_global_7.smt2 | 0.037s | 19.472MiB| unsat | 0 | | | |hong_2.smt2 | 0.037s | 20.724MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.037s | 19.84MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0102.smt2 | 0.037s | 20.78MiB| unsat | 0 | | | |ArthanKM2-chunk-0002.smt2 | 0.037s | 20.928MiB| sat | 0 | | | |ball_count_2d_plain.01.seq_lazy_global_15.smt2 | 0.037s | 19.828MiB| unsat | 0 | | | |sin-344-3-chunk-0029.smt2 | 0.037s | 20.688MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0508.smt2 | 0.037s | 20.632MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0081.smt2 | 0.037s | 20.728MiB| sat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0049.smt2 | 0.037s | 20.796MiB| unsat | 0 | | | |sin-problem-8-chunk-0026.smt2 | 0.037s | 20.832MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0036.smt2 | 0.037s | 20.956MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0101.smt2 | 0.037s | 20.768MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0078.smt2 | 0.037s | 20.868MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0496.smt2 | 0.037s | 20.956MiB| sat | 0 | | | |ball_count_2d_slope.02.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.037s | 19.496MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0117.smt2 | 0.037s | 21.228MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_linear_enc_global_1.smt2 | 0.038s | 19.024MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0131.smt2 | 0.038s | 20.972MiB| unsat | 0 | | | |MulliganEconomicsModel0030e.smt2 | 0.038s | 20.728MiB| sat | 0 | | | |atan-vega-3-chunk-0513.smt2 | 0.038s | 20.792MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0328.smt2 | 0.038s | 20.508MiB| sat | 0 | | | |Arthan1A-chunk-0020.smt2 | 0.038s | 20.7MiB| sat | 0 | | | |atan-problem-2-chunk-0047.smt2 | 0.038s | 20.684MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0053.smt2 | 0.038s | 20.668MiB| sat | 0 | | | |Chua-2-VC1-L-chunk-0052.smt2 | 0.038s | 20.636MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0307.smt2 | 0.038s | 20.68MiB| unsat | 0 | | | |asin-8-chunk-0024.smt2 | 0.038s | 20.596MiB| sat | 0 | | | |sin-problem-7-chunk-0311.smt2 | 0.038s | 20.816MiB| sat | 0 | | | |cos-problem-5-chunk-0023.smt2 | 0.038s | 20.676MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0369.smt2 | 0.038s | 20.776MiB| sat | 0 | | | |ball_count_1d_plain.01.seq_lazy_lemmas_global_11.smt2 | 0.038s | 19.668MiB| unsat | 0 | | | |atan-vega-3-chunk-0240.smt2 | 0.038s | 20.764MiB| sat | 0 | | | |sin-cos-346-b-chunk-0454.smt2 | 0.038s | 20.848MiB| sat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0034.smt2 | 0.038s | 20.928MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0189.smt2 | 0.038s | 20.808MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0701.smt2 | 0.038s | 18.772MiB| unsat | 0 | | | |MulliganEconomicsModel0024a.smt2 | 0.038s | 20.848MiB| sat | 0 | | | |sin-cos-346-b-chunk-0424.smt2 | 0.038s | 20.804MiB| unsat | 0 | | | |atan-problem-1-chunk-0091.smt2 | 0.038s | 20.62MiB| sat | 0 | | | |exp-problem-10-2-chunk-0285.smt2 | 0.038s | 20.908MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0607.smt2 | 0.038s | 20.76MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_global_7.smt2 | 0.039s | 19.808MiB| unsat | 0 | | | |sin-problem-8-chunk-0054.smt2 | 0.039s | 20.728MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0070.smt2 | 0.039s | 20.844MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0168.smt2 | 0.039s | 20.768MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_global_7.smt2 | 0.039s | 19.644MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0154.smt2 | 0.039s | 20.888MiB| unsat | 0 | | | |etcs_braking_2.01.seq_lazy_lemmas_global_1.smt2 | 0.039s | 21.032MiB| unsat | 0 | | | |atan-vega-3-chunk-0109.smt2 | 0.039s | 20.764MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0190.smt2 | 0.039s | 20.7MiB| unsat | 0 | | | |ball_count_1d_plain.02.qfree_global_9.smt2 | 0.039s | 19.312MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0306.smt2 | 0.039s | 20.688MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0255.smt2 | 0.039s | 20.928MiB| sat | 0 | | | |sin-cos-346-b-chunk-0030.smt2 | 0.039s | 20.648MiB| sat | 0 | | | |sqrt-circles-3-chunk-0016.smt2 | 0.039s | 20.72MiB| sat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_global_7.smt2 | 0.039s | 19.564MiB| unsat | 0 | | | |polypaver-bench-exp-3d-chunk-0028.smt2 | 0.039s | 20.74MiB| sat | 0 | | | |sin-problem-7-chunk-0273.smt2 | 0.039s | 20.976MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0084.smt2 | 0.039s | 20.892MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0214.smt2 | 0.039s | 20.608MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0077.smt2 | 0.039s | 20.68MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0144.smt2 | 0.040s | 20.648MiB| sat | 0 | | | |ball_count_1d_plain.02.seq_lazy_global_7.smt2 | 0.040s | 19.324MiB| unsat | 0 | | | |atan-vega-3-chunk-0593.smt2 | 0.040s | 21.052MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0036.smt2 | 0.040s | 20.628MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0026.smt2 | 0.040s | 20.648MiB| unsat | 0 | | | |Chua-2-VC1-U-chunk-0013.smt2 | 0.040s | 20.764MiB| sat | 0 | | | |sin-cos-346-b-chunk-0444.smt2 | 0.040s | 20.864MiB| sat | 0 | | | |atan-problem-2-weakT-chunk-0030.smt2 | 0.040s | 20.768MiB| unsat | 0 | | | |ball_count_2d_plain.02.qfree_global_7.smt2 | 0.040s | 19.32MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0191.smt2 | 0.040s | 20.832MiB| sat | 0 | | | |polypaver-sqrt43-int-4vars-chunk-0026.smt2 | 0.040s | 20.784MiB| sat | 0 | | | |sin-cos-346-b-chunk-0474.smt2 | 0.040s | 20.84MiB| unsat | 0 | | | |atan-vega-3-chunk-0057.smt2 | 0.040s | 20.668MiB| sat | 0 | | | |CONVOI2-chunk-0018.smt2 | 0.040s | 20.768MiB| sat | 0 | | | |atan-problem-2-weakT-chunk-0041.smt2 | 0.040s | 20.952MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0029.smt2 | 0.040s | 20.736MiB| sat | 0 | | | |Chua-1-IL-L-chunk-0143.smt2 | 0.040s | 20.736MiB| unsat | 0 | | | |ball_count_1d_plain.05.seq_lazy_lemmas_global_3.smt2 | 0.040s | 21.268MiB| unsat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0065.smt2 | 0.040s | 20.7MiB| unsat | 0 | | | |cbrt-problem-3-weak-chunk-0069.smt2 | 0.040s | 20.764MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_global_3.smt2 | 0.040s | 21.084MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0401.smt2 | 0.040s | 20.676MiB| sat | 0 | | | |ball_count_2d_plain.02.seq_lazy_linear_enc_global_3.smt2 | 0.041s | 18.936MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0295.smt2 | 0.041s | 20.856MiB| sat | 0 | | | |ball_count_2d_plain.02.seq_lazy_lemmas_global_13.smt2 | 0.041s | 20.256MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0137.smt2 | 0.041s | 20.78MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0490.smt2 | 0.041s | 20.768MiB| sat | 0 | | | |atan-problem-2-chunk-0092.smt2 | 0.041s | 20.904MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0116.smt2 | 0.041s | 20.888MiB| sat | 0 | | | |exp-problem-10-3-chunk-0073.smt2 | 0.041s | 20.804MiB| sat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0062.smt2 | 0.041s | 20.768MiB| sat | 0 | | | |MulliganEconomicsModel0080e.smt2 | 0.041s | 20.768MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0143.smt2 | 0.041s | 20.936MiB| sat | 0 | | | |ArthanM2-chunk-0012.smt2 | 0.041s | 18.712MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0493.smt2 | 0.041s | 20.792MiB| sat | 0 | | | |atan-vega-3-chunk-0320.smt2 | 0.041s | 20.788MiB| sat | 0 | | | |exp-problem-10-2-chunk-0124.smt2 | 0.041s | 20.828MiB| unsat | 0 | | | |cbrt-problem-3-chunk-0055.smt2 | 0.041s | 20.66MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0193.smt2 | 0.041s | 20.82MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0500.smt2 | 0.041s | 20.76MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0123.smt2 | 0.041s | 20.764MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0700.smt2 | 0.042s | 20.716MiB| unsat | 0 | | | |ball_count_2d_plain.01.redlog_global_11.smt2 | 0.042s | 19.972MiB| unsat | 0 | | | |ball_count_1d_plain.01.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.042s | 18.928MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.042s | 19.176MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0541.smt2 | 0.042s | 20.66MiB| sat | 0 | | | |ball_count_1d_plain.10.seq_lazy_global_3.smt2 | 0.042s | 18.972MiB| unsat | 0 | | | |sin-problem-8-weak-chunk-0068.smt2 | 0.042s | 20.784MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0380.smt2 | 0.042s | 20.968MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0596.smt2 | 0.042s | 20.656MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0073.smt2 | 0.042s | 20.616MiB| sat | 0 | | | |Chua-1-VC2-L-chunk-0064.smt2 | 0.042s | 18.696MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0110.smt2 | 0.042s | 20.792MiB| sat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.042s | 19.764MiB| unsat | 0 | | | |sin-problem-7-chunk-0156.smt2 | 0.042s | 20.744MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0024.smt2 | 0.042s | 20.8MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0093.smt2 | 0.042s | 20.8MiB| sat | 0 | | | |asin-8-vars4-chunk-0046.smt2 | 0.042s | 20.744MiB| unsat | 0 | | | |Chua-1-VC1-U-chunk-0056.smt2 | 0.042s | 20.812MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0566.smt2 | 0.042s | 20.504MiB| sat | 0 | | | |sqrt-problem-Melquiond2-chunk-0091.smt2 | 0.042s | 20.864MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0034.smt2 | 0.042s | 20.784MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0111.smt2 | 0.042s | 20.82MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0167.smt2 | 0.043s | 20.784MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0467.smt2 | 0.043s | 20.696MiB| unsat | 0 | | | |ball_count_1d_plain.01.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.043s | 19.284MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0358.smt2 | 0.043s | 20.996MiB| sat | 0 | | | |ball_count_2d_plain.04.qfree_global_5.smt2 | 0.043s | 21.188MiB| unsat | 0 | | | |atan-vega-3-chunk-0453.smt2 | 0.043s | 20.992MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0576.smt2 | 0.043s | 20.656MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0158.smt2 | 0.043s | 20.752MiB| sat | 0 | | | |atan-vega-3-chunk-0603.smt2 | 0.043s | 20.916MiB| sat | 0 | | | |sin-cos-346-b-chunk-0126.smt2 | 0.043s | 20.696MiB| sat | 0 | | | |ball_count_2d_plain.10.seq_lazy_lemmas_global_1.smt2 | 0.043s | 18.976MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0054.smt2 | 0.043s | 18.956MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0339.smt2 | 0.043s | 20.604MiB| sat | 0 | | | |sin-cos-346-b-chunk-0338.smt2 | 0.043s | 20.9MiB| sat | 0 | | | |atan-problem-2-sqrt-chunk-0039.smt2 | 0.043s | 20.748MiB| sat | 0 | | | |Chua-2-VC2-U-chunk-0086.smt2 | 0.043s | 20.836MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0041.smt2 | 0.043s | 20.836MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0118.smt2 | 0.043s | 20.764MiB| unsat | 0 | | | |sin-problem-8-weak-chunk-0056.smt2 | 0.043s | 20.664MiB| unsat | 0 | | | |ball_count_2d_plain.10.seq_lazy_linear_enc_global_9.smt2 | 0.043s | 19.368MiB| unsat | 0 | | | |atan-vega-3-chunk-0139.smt2 | 0.043s | 21.076MiB| sat | 0 | | | |ball_count_1d_plain.02.seq_lazy_global_11.smt2 | 0.043s | 19.652MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0409.smt2 | 0.043s | 20.636MiB| sat | 0 | | | |exp-problem-10-3-chunk-0096.smt2 | 0.043s | 20.836MiB| unsat | 0 | | | |atan-vega-3-chunk-0300.smt2 | 0.043s | 20.812MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0202.smt2 | 0.043s | 20.812MiB| sat | 0 | | | |polypaver-bench-exp-3d-chunk-0072.smt2 | 0.043s | 20.744MiB| sat | 0 | | | |sin-problem-7-weak-chunk-0149.smt2 | 0.043s | 20.652MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0168.smt2 | 0.043s | 20.824MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0181.smt2 | 0.044s | 18.94MiB| unsat | 0 | | | |Chua-2-IL-L-chunk-0047.smt2 | 0.044s | 18.9MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0272.smt2 | 0.044s | 20.676MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0108.smt2 | 0.044s | 20.732MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0028.smt2 | 0.044s | 20.72MiB| sat | 0 | | | |sin-cos-346-b-chunk-0252.smt2 | 0.044s | 20.812MiB| unsat | 0 | | | |atan-problem-1-chunk-0006.smt2 | 0.044s | 20.608MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0035.smt2 | 0.044s | 20.82MiB| sat | 0 | | | |Chua-2-VC2-U-chunk-0111.smt2 | 0.044s | 20.916MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0134.smt2 | 0.044s | 20.764MiB| unsat | 0 | | | |atan-problem-1-chunk-0081.smt2 | 0.044s | 20.772MiB| unsat | 0 | | | |sqrt-problem-12vars3-chunk-0025.smt2 | 0.044s | 20.72MiB| unsat | 0 | | | |Lyapunov1a-chunk-0011.smt2 | 0.044s | 20.76MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0113.smt2 | 0.044s | 20.764MiB| sat | 0 | | | |ball_count_2d_hill.10.seq_lazy_lemmas_global_7.smt2 | 0.044s | 19.892MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0363.smt2 | 0.044s | 20.74MiB| sat | 0 | | | |exp-problem-10-2-chunk-0090.smt2 | 0.044s | 20.66MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0094.smt2 | 0.045s | 20.884MiB| sat | 0 | | | |atan-vega-3-chunk-0443.smt2 | 0.045s | 20.908MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0035.smt2 | 0.045s | 20.708MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0043.smt2 | 0.045s | 20.8MiB| unsat | 0 | | | |sin-problem-7-weak2-chunk-0123.smt2 | 0.045s | 20.724MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0117.smt2 | 0.045s | 20.712MiB| unsat | 0 | | | |sin-problem-7-weak2-chunk-0057.smt2 | 0.045s | 20.712MiB| sat | 0 | | | |matrix-1-all-8.smt2 | 0.045s | 20.724MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0035.smt2 | 0.045s | 20.78MiB| sat | 0 | | | |Chua-1-IL-L-chunk-0042.smt2 | 0.045s | 18.72MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0320.smt2 | 0.045s | 20.9MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0189.smt2 | 0.045s | 20.732MiB| unsat | 0 | | | |Chua-1-VC2-L-chunk-0039.smt2 | 0.045s | 20.764MiB| unsat | 0 | | | |CMOS-opamp-chunk-0158.smt2 | 0.045s | 20.908MiB| unsat | 0 | | | |atan-vega-3-chunk-0310.smt2 | 0.045s | 20.768MiB| sat | 0 | | | |ball_count_2d_plain.05.seq_lazy_linear_enc_global_5.smt2 | 0.045s | 21.144MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0080.smt2 | 0.045s | 20.716MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0014.smt2 | 0.045s | 20.712MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0231.smt2 | 0.046s | 18.86MiB| unsat | 0 | | | |cbrt-problem-3-chunk-0028.smt2 | 0.046s | 20.952MiB| unsat | 0 | | | |ball_count_2d_plain.05.redlog_global_3.smt2 | 0.046s | 21.164MiB| unsat | 0 | | | |ball_count_2d_hill.01.seq_lazy_lemmas_global_11.smt2 | 0.046s | 20.2MiB| unsat | 0 | | | |atan-problem-1-chunk-0035.smt2 | 0.046s | 20.624MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0101.smt2 | 0.046s | 18.916MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0053.smt2 | 0.046s | 20.692MiB| sat | 0 | | | |sin-problem-10-3-chunk-0033.smt2 | 0.046s | 20.672MiB| unsat | 0 | | | |atan-vega-3-chunk-0011.smt2 | 0.046s | 20.632MiB| sat | 0 | | | |atan-vega-3-chunk-0380.smt2 | 0.046s | 21.244MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0139.smt2 | 0.046s | 20.88MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0223.smt2 | 0.046s | 21.204MiB| sat | 0 | | | |CONVOI2-chunk-0031.smt2 | 0.046s | 20.824MiB| sat | 0 | | | |ball_count_1d_plain.10.qfree_global_1.smt2 | 0.046s | 18.98MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0054.smt2 | 0.046s | 20.964MiB| sat | 0 | | | |Chua-2-VC2-U-chunk-0029.smt2 | 0.046s | 20.848MiB| sat | 0 | | | |atan-vega-3-chunk-0280.smt2 | 0.046s | 20.684MiB| sat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_global_1.smt2 | 0.046s | 18.824MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0206.smt2 | 0.046s | 20.676MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0204.smt2 | 0.046s | 20.768MiB| unsat | 0 | | | |atan-problem-1-weak-chunk-0020.smt2 | 0.046s | 20.76MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0025.smt2 | 0.046s | 20.628MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0610.smt2 | 0.047s | 21.004MiB| sat | 0 | | | |ball_count_2d_plain.05.seq_lazy_linear_enc_global_1.smt2 | 0.047s | 18.916MiB| unsat | 0 | | | |Chua-2-IL-L-chunk-0082.smt2 | 0.047s | 20.836MiB| sat | 0 | | | |Chua-2-VC2-U-chunk-0066.smt2 | 0.047s | 20.96MiB| unsat | 0 | | | |sin-problem-7-chunk-0247.smt2 | 0.047s | 20.976MiB| sat | 0 | | | |ball_count_2d_slope.05.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.047s | 19.452MiB| unsat | 0 | | | |atan-problem-1-chunk-0047.smt2 | 0.047s | 20.836MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0045.smt2 | 0.047s | 18.98MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0194.smt2 | 0.047s | 20.772MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0104.smt2 | 0.048s | 20.76MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0230.smt2 | 0.048s | 20.772MiB| sat | 0 | | | |sin-problem-7-weak2-chunk-0044.smt2 | 0.048s | 20.404MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0198.smt2 | 0.048s | 20.756MiB| sat | 0 | | | |ball_count_2d_slope.01.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.048s | 20.652MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0560.smt2 | 0.048s | 20.66MiB| sat | 0 | | | |ball_count_1d_plain.01.redlog_global_13.smt2 | 0.048s | 19.892MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0045.smt2 | 0.048s | 20.724MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0086.smt2 | 0.048s | 20.76MiB| sat | 0 | | | |sin-problem-10-2-chunk-0034.smt2 | 0.048s | 18.72MiB| unsat | 0 | | | |ball_count_2d_plain.02.redlog_global_15.smt2 | 0.048s | 20.732MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.qfree_global_11.smt2 | 0.048s | 21.668MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0346.smt2 | 0.048s | 20.76MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0159.smt2 | 0.048s | 20.572MiB| sat | 0 | | | |atan-vega-3-chunk-0159.smt2 | 0.048s | 20.94MiB| sat | 0 | | | |asin-8-chunk-0039.smt2 | 0.048s | 20.928MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0091.smt2 | 0.048s | 20.608MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.048s | 20.644MiB| unsat | 0 | | | |ball_count_2d_plain.01.seq_lazy_linear_enc_global_9.smt2 | 0.049s | 19.38MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0069.smt2 | 0.049s | 18.88MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0368.smt2 | 0.049s | 20.768MiB| sat | 0 | | | |atan-vega-3-chunk-0433.smt2 | 0.049s | 20.664MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0064.smt2 | 0.049s | 20.836MiB| sat | 0 | | | |ball_count_2d_hill_simple.04.redlog_global_1.smt2 | 0.049s | 19.032MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0421.smt2 | 0.049s | 20.88MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0374.smt2 | 0.049s | 20.764MiB| unsat | 0 | | | |gen-09.smt2 | 0.049s | 20.808MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.049s | 20.312MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0370.smt2 | 0.049s | 20.736MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0097.smt2 | 0.049s | 20.876MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_linear_enc_global_1.smt2 | 0.049s | 18.892MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_linear_enc_global_7.smt2 | 0.049s | 21.288MiB| unsat | 0 | | | |sin-problem-7-chunk-0283.smt2 | 0.049s | 20.868MiB| unsat | 0 | | | |ball_count_1d_plain.04.seq_lazy_linear_enc_global_3.smt2 | 0.049s | 20.996MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0262.smt2 | 0.049s | 20.708MiB| sat | 0 | | | |ball_count_1d_plain.05.redlog_global_5.smt2 | 0.050s | 21.404MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0038.smt2 | 0.050s | 20.664MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0124.smt2 | 0.050s | 20.784MiB| sat | 0 | | | |sin-cos-346-b-chunk-0549.smt2 | 0.050s | 20.76MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_global_11.smt2 | 0.050s | 19.484MiB| unsat | 0 | | | |atan-vega-3-chunk-0400.smt2 | 0.050s | 20.772MiB| sat | 0 | | | |ball_count_2d_plain.01.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.050s | 19.188MiB| unsat | 0 | | | |ball_count_2d_slope.10.seq_lazy_global_11.smt2 | 0.050s | 20.18MiB| unsat | 0 | | | |sin-problem-7-chunk-0233.smt2 | 0.050s | 20.68MiB| sat | 0 | | | |RL-high-pass-circuit-gain-chunk-0010.smt2 | 0.050s | 20.76MiB| sat | 0 | | | |sqrt-problem-12vars3-chunk-0097.smt2 | 0.050s | 20.76MiB| sat | 0 | | | |ball_count_2d_plain.10.redlog_global_7.smt2 | 0.050s | 19.748MiB| unsat | 0 | | | |ball_count_1d_plain.02.qfree_global_13.smt2 | 0.050s | 19.496MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0155.smt2 | 0.050s | 20.86MiB| unsat | 0 | | | |atan-problem-1-chunk-0071.smt2 | 0.050s | 20.564MiB| sat | 0 | | | |sqrt-problem-12vars3-chunk-0039.smt2 | 0.050s | 20.864MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.qfree_global_13.smt2 | 0.050s | 19.672MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0168.smt2 | 0.050s | 20.672MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_lemmas_global_1.smt2 | 0.050s | 19.036MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_global_3.smt2 | 0.050s | 20.936MiB| unsat | 0 | | | |cbrt-problem-3-weak-chunk-0040.smt2 | 0.050s | 20.988MiB| unsat | 0 | | | |atan-vega-3-chunk-0473.smt2 | 0.050s | 20.752MiB| sat | 0 | | | |matrix-5-all-23.smt2 | 0.050s | 21.464MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0567.smt2 | 0.050s | 20.884MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0299.smt2 | 0.050s | 20.856MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_linear_enc_global_5.smt2 | 0.050s | 19.484MiB| unsat | 0 | | | |ball_count_2d_slope.02.seq_lazy_lemmas_global_7.smt2 | 0.050s | 20.18MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0157.smt2 | 0.050s | 20.668MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0469.smt2 | 0.050s | 20.9MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0278.smt2 | 0.051s | 20.764MiB| sat | 0 | | | |Chua-1-IL-U-chunk-0063.smt2 | 0.051s | 20.724MiB| sat | 0 | | | |Chua-2-VC2-U-chunk-0127.smt2 | 0.051s | 20.88MiB| sat | 0 | | | |CMOS-opamp-chunk-0200.smt2 | 0.051s | 20.672MiB| sat | 0 | | | |sqrt-problem-Melquiond2-chunk-0071.smt2 | 0.051s | 20.852MiB| sat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0050.smt2 | 0.051s | 20.808MiB| sat | 0 | | | |atan-vega-3-chunk-0230.smt2 | 0.051s | 20.592MiB| sat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_linear_enc_global_3.smt2 | 0.051s | 20.764MiB| unsat | 0 | | | |CMOS-opamp-chunk-0286.smt2 | 0.051s | 20.716MiB| sat | 0 | | | |polypaver-sqrt-circles-1a-chunk-0011.smt2 | 0.051s | 20.724MiB| sat | 0 | | | |ball_count_2d_plain.02.seq_lazy_linear_enc_lemmas_global_11.smt2 | 0.051s | 19.616MiB| unsat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0009.smt2 | 0.051s | 20.592MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0061.smt2 | 0.051s | 20.696MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0267.smt2 | 0.052s | 20.76MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0191.smt2 | 0.052s | 20.98MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0161.smt2 | 0.052s | 20.656MiB| sat | 0 | | | |sqrt-problem-12vars3-chunk-0010.smt2 | 0.052s | 20.784MiB| sat | 0 | | | |exp-problem-10-2-chunk-0059.smt2 | 0.052s | 19.084MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0457.smt2 | 0.052s | 20.652MiB| sat | 0 | | | |sin-cos-346-b-chunk-0186.smt2 | 0.052s | 20.744MiB| sat | 0 | | | |ball_count_2d_plain.03.redlog_global_1.smt2 | 0.052s | 18.94MiB| unsat | 0 | | | |Chua-2-IL-L-chunk-0072.smt2 | 0.052s | 18.728MiB| unsat | 0 | | | |sin-problem-7-chunk-0257.smt2 | 0.052s | 21.016MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0120.smt2 | 0.052s | 20.748MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0081.smt2 | 0.052s | 20.608MiB| unsat | 0 | | | |atan-problem-1-chunk-0058.smt2 | 0.052s | 20.736MiB| sat | 0 | | | |Lyapunov1a-chunk-0042.smt2 | 0.052s | 20.948MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0019.smt2 | 0.052s | 20.972MiB| unsat | 0 | | | |Chua-1-VC2-L-chunk-0050.smt2 | 0.052s | 20.656MiB| unsat | 0 | | | |polypaver-bench-exp-3d-chunk-0138.smt2 | 0.052s | 21.064MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0016.smt2 | 0.052s | 20.988MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0639.smt2 | 0.052s | 20.64MiB| unsat | 0 | | | |CMOS-opamp-chunk-0074.smt2 | 0.052s | 20.676MiB| sat | 0 | | | |ball_count_1d_plain.10.seq_lazy_linear_enc_global_15.smt2 | 0.053s | 19.844MiB| unsat | 0 | | | |atan-vega-3-chunk-0199.smt2 | 0.053s | 20.828MiB| unsat | 0 | | | |CMOS-opamp-chunk-0310.smt2 | 0.053s | 20.764MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0714.smt2 | 0.053s | 20.484MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.qfree_global_3.smt2 | 0.053s | 19.052MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0352.smt2 | 0.053s | 20.912MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0217.smt2 | 0.053s | 20.792MiB| sat | 0 | | | |matrix-1-all-10.smt2 | 0.053s | 20.932MiB| sat | 0 | | | |mbo_E21E27.smt2 | 0.053s | 20.756MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0126.smt2 | 0.053s | 20.716MiB| sat | 0 | | | |sin-problem-8-weak-chunk-0027.smt2 | 0.053s | 20.8MiB| sat | 0 | | | |ball_count_2d_plain.02.seq_lazy_global_5.smt2 | 0.053s | 19.108MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0318.smt2 | 0.053s | 20.764MiB| unsat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0121.smt2 | 0.053s | 20.804MiB| sat | 0 | | | |ball_count_2d_hill.02.redlog_global_9.smt2 | 0.053s | 20.672MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0048.smt2 | 0.054s | 20.484MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0227.smt2 | 0.054s | 20.764MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0087.smt2 | 0.054s | 20.864MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0037.smt2 | 0.054s | 20.728MiB| sat | 0 | | | |matrix-1-all-29.smt2 | 0.054s | 20.828MiB| sat | 0 | | | |Lyapunov1a-chunk-0032.smt2 | 0.054s | 20.852MiB| sat | 0 | | | |ball_count_2d_slope.02.seq_lazy_linear_enc_global_15.smt2 | 0.054s | 20.404MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0018.smt2 | 0.054s | 20.632MiB| sat | 0 | | | |exp-problem-10-2-chunk-0325.smt2 | 0.054s | 21.016MiB| unsat | 0 | | | |sin-problem-8-chunk-0067.smt2 | 0.054s | 20.86MiB| sat | 0 | | | |ball_count_2d_hill.02.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.054s | 19.344MiB| unsat | 0 | | | |ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.054s | 18.948MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0425.smt2 | 0.054s | 20.788MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0107.smt2 | 0.054s | 20.988MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0027.smt2 | 0.054s | 20.752MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0390.smt2 | 0.054s | 20.904MiB| sat | 0 | | | |exp-problem-10-2-chunk-0245.smt2 | 0.054s | 20.804MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0109.smt2 | 0.054s | 20.756MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0577.smt2 | 0.054s | 21.036MiB| sat | 0 | | | |atan-vega-3-chunk-0330.smt2 | 0.054s | 20.848MiB| sat | 0 | | | |InVarSynth_LabelEncodingWithUnrolling.bpl_Iteration2_0.smt2 | 0.054s | 21.02MiB| sat | 0 | | | |sin-problem-7-chunk-0322.smt2 | 0.054s | 21.0MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0138.smt2 | 0.054s | 20.772MiB| sat | 0 | | | |exp-problem-10-3-chunk-0032.smt2 | 0.054s | 20.56MiB| sat | 0 | | | |ball_count_2d_hill.01.redlog_global_9.smt2 | 0.054s | 20.684MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0113.smt2 | 0.054s | 20.816MiB| sat | 0 | | | |sin-cos-346-b-chunk-0296.smt2 | 0.054s | 18.94MiB| unsat | 0 | | | |ball_count_2d_plain.10.seq_lazy_global_15.smt2 | 0.054s | 19.812MiB| unsat | 0 | | | |exp-361-neg-6-e-chunk-0216.smt2 | 0.054s | 21.044MiB| sat | 0 | | | |Chua-1-VC1-U-chunk-0083.smt2 | 0.055s | 20.748MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0085.smt2 | 0.055s | 20.464MiB| sat | 0 | | | |sin-cos-346-b-chunk-0285.smt2 | 0.055s | 20.768MiB| sat | 0 | | | |MulliganEconomicsModel0054a.smt2 | 0.055s | 20.836MiB| sat | 0 | | | |ball_count_2d_slope.05.seq_lazy_lemmas_global_1.smt2 | 0.055s | 19.212MiB| unsat | 0 | | | |atan-vega-3-chunk-0390.smt2 | 0.055s | 20.768MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0136.smt2 | 0.055s | 20.78MiB| sat | 0 | | | |Chua-2-VC1-L-chunk-0073.smt2 | 0.055s | 18.82MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_global_11.smt2 | 0.055s | 21.644MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0174.smt2 | 0.055s | 20.764MiB| sat | 0 | | | |atan-vega-3-chunk-0169.smt2 | 0.055s | 20.848MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0173.smt2 | 0.055s | 20.744MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.qfree_global_9.smt2 | 0.055s | 19.488MiB| unsat | 0 | | | |ball_count_2d_plain.10.seq_lazy_lemmas_global_5.smt2 | 0.055s | 19.204MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0039.smt2 | 0.055s | 20.74MiB| sat | 0 | | | |ball_count_1d_plain.03.redlog_global_7.smt2 | 0.055s | 21.548MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0148.smt2 | 0.055s | 20.816MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0469.smt2 | 0.055s | 20.788MiB| sat | 0 | | | |sin-cos-346-b-chunk-0584.smt2 | 0.055s | 20.74MiB| sat | 0 | | | |ball_count_2d_plain.01.seq_lazy_lemmas_global_1.smt2 | 0.055s | 18.872MiB| unsat | 0 | | | |sin-problem-10-2-chunk-0010.smt2 | 0.055s | 20.744MiB| sat | 0 | | | |CMOS-opamp-chunk-0260.smt2 | 0.055s | 18.836MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0216.smt2 | 0.055s | 20.9MiB| sat | 0 | | | |Chua-2-VC1-L-chunk-0119.smt2 | 0.055s | 20.768MiB| sat | 0 | | | |sin-cos-346-b-chunk-0514.smt2 | 0.055s | 20.804MiB| sat | 0 | | | |sin-cos-346-b-chunk-0054.smt2 | 0.055s | 18.8MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0344.smt2 | 0.055s | 20.78MiB| sat | 0 | | | |Chua-1-IL-L-chunk-0090.smt2 | 0.056s | 20.808MiB| sat | 0 | | | |ball_count_2d_slope.02.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.056s | 19.236MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0097.smt2 | 0.056s | 20.744MiB| unsat | 0 | | | |sqrt-problem-13-chunk-0019.smt2 | 0.056s | 20.908MiB| sat | 0 | | | |atan-vega-3-chunk-0179.smt2 | 0.056s | 20.752MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0098.smt2 | 0.056s | 20.988MiB| unsat | 0 | | | |ball_count_2d_slope.02.seq_lazy_global_3.smt2 | 0.056s | 19.592MiB| unsat | 0 | | | |Chua-2-VC2-L-chunk-0013.smt2 | 0.056s | 20.716MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0206.smt2 | 0.056s | 20.908MiB| sat | 0 | | | |ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.056s | 19.408MiB| unsat | 0 | | | |atan-vega-3-chunk-0250.smt2 | 0.056s | 20.592MiB| unsat | 0 | | | |sin-problem-7-weak2-chunk-0100.smt2 | 0.056s | 20.6MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0433.smt2 | 0.056s | 20.784MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0222.smt2 | 0.056s | 20.68MiB| sat | 0 | | | |sin-cos-346-b-chunk-0114.smt2 | 0.056s | 20.832MiB| unsat | 0 | | | |CMOS-opamp-chunk-0086.smt2 | 0.056s | 20.816MiB| sat | 0 | | | |polypaver-bench-exp-3d-chunk-0109.smt2 | 0.056s | 20.772MiB| unsat | 0 | | | |ball_count_1d_plain.03.seq_lazy_lemmas_global_1.smt2 | 0.056s | 18.84MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0064.smt2 | 0.056s | 20.692MiB| unsat | 0 | | | |mbo_E17E23.smt2 | 0.056s | 20.828MiB| unsat | 0 | | | |CMOS-opamp-chunk-0122.smt2 | 0.057s | 21.0MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_global_11.smt2 | 0.057s | 19.68MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.redlog_global_5.smt2 | 0.057s | 21.088MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_linear_enc_global_1.smt2 | 0.057s | 19.064MiB| unsat | 0 | | | |ball_count_2d_plain.03.seq_lazy_lemmas_global_3.smt2 | 0.057s | 20.876MiB| unsat | 0 | | | |ball_count_2d_plain.10.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.057s | 19.004MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0141.smt2 | 0.057s | 20.972MiB| sat | 0 | | | |ball_count_2d_slope.04.seq_lazy_linear_enc_lemmas_global_7.smt2 | 0.057s | 19.816MiB| unsat | 0 | | | |ball_count_2d_hill.02.seq_lazy_lemmas_global_7.smt2 | 0.057s | 19.812MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0183.smt2 | 0.057s | 20.628MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.qfree_global_9.smt2 | 0.057s | 19.328MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_global_11.smt2 | 0.057s | 20.388MiB| unsat | 0 | | | |atan-vega-3-chunk-0270.smt2 | 0.057s | 20.72MiB| sat | 0 | | | |exp-problem-10-3-chunk-0188.smt2 | 0.057s | 20.776MiB| unsat | 0 | | | |Chua-1-VC1-U-chunk-0072.smt2 | 0.057s | 20.648MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0221.smt2 | 0.057s | 18.76MiB| unsat | 0 | | | |atan-problem-2-chunk-0024.smt2 | 0.057s | 20.764MiB| sat | 0 | | | |Chua-1-IL-L-chunk-0078.smt2 | 0.057s | 20.68MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0162.smt2 | 0.057s | 20.604MiB| unsat | 0 | | | |sin-problem-7-chunk-0348.smt2 | 0.057s | 20.9MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0334.smt2 | 0.058s | 21.016MiB| sat | 0 | | | |sqrt-problem-Melquiond2-chunk-0010.smt2 | 0.058s | 20.876MiB| sat | 0 | | | |exp-problem-10-2-chunk-0134.smt2 | 0.058s | 20.644MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0446.smt2 | 0.058s | 20.672MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0093.smt2 | 0.058s | 20.76MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0050.smt2 | 0.058s | 20.656MiB| unsat | 0 | | | |Chua-2-IL-L-chunk-0005.smt2 | 0.058s | 20.668MiB| sat | 0 | | | |ball_count_2d_hill.02.seq_lazy_lemmas_global_11.smt2 | 0.058s | 20.132MiB| unsat | 0 | | | |ball_count_2d_hill.10.seq_lazy_linear_enc_global_15.smt2 | 0.058s | 20.24MiB| unsat | 0 | | | |atan-vega-3-chunk-0633.smt2 | 0.058s | 20.908MiB| sat | 0 | | | |sin-problem-8-weak-chunk-0044.smt2 | 0.058s | 21.016MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0070.smt2 | 0.058s | 20.916MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0094.smt2 | 0.058s | 20.772MiB| sat | 0 | | | |sin-cos-346-b-chunk-0504.smt2 | 0.058s | 20.96MiB| sat | 0 | | | |ball_count_2d_hill_simple.03.qfree_global_7.smt2 | 0.058s | 21.168MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0310.smt2 | 0.058s | 20.944MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0241.smt2 | 0.058s | 20.94MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0265.smt2 | 0.058s | 18.764MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_linear_enc_global_5.smt2 | 0.058s | 19.484MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0204.smt2 | 0.058s | 20.768MiB| sat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0032.smt2 | 0.058s | 20.736MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0120.smt2 | 0.058s | 20.776MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0132.smt2 | 0.058s | 20.94MiB| sat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0080.smt2 | 0.058s | 20.756MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_linear_enc_lemmas_global_7.smt2 | 0.058s | 21.548MiB| unsat | 0 | | | |CMOS-opamp-chunk-0148.smt2 | 0.058s | 20.836MiB| sat | 0 | | | |ball_count_2d_hill.05.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.058s | 19.036MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0711.smt2 | 0.059s | 20.816MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0083.smt2 | 0.059s | 21.008MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0619.smt2 | 0.059s | 20.472MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0087.smt2 | 0.059s | 20.644MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0212.smt2 | 0.059s | 20.812MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0121.smt2 | 0.059s | 20.764MiB| unsat | 0 | | | |CMOS-opamp-chunk-0332.smt2 | 0.059s | 20.768MiB| unsat | 0 | | | |sin-problem-7-chunk-0117.smt2 | 0.059s | 20.816MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0042.smt2 | 0.059s | 20.808MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0545.smt2 | 0.059s | 20.796MiB| sat | 0 | | | |ball_count_2d_plain.03.seq_lazy_linear_enc_global_11.smt2 | 0.059s | 21.904MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0106.smt2 | 0.059s | 20.668MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0290.smt2 | 0.059s | 20.912MiB| sat | 0 | | | |sin-cos-346-b-chunk-0464.smt2 | 0.059s | 20.896MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0069.smt2 | 0.060s | 20.764MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0149.smt2 | 0.060s | 20.824MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0098.smt2 | 0.060s | 20.788MiB| sat | 0 | | | |exp-problem-10-3-chunk-0158.smt2 | 0.060s | 20.792MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0288.smt2 | 0.060s | 20.728MiB| unsat | 0 | | | |atan-vega-3-chunk-0290.smt2 | 0.060s | 20.772MiB| sat | 0 | | | |sin-cos-346-b-chunk-0597.smt2 | 0.060s | 20.908MiB| sat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.060s | 19.668MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0019.smt2 | 0.060s | 20.756MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0022.smt2 | 0.060s | 20.832MiB| unsat | 0 | | | |sqrt-problem-12vars3-chunk-0081.smt2 | 0.060s | 20.808MiB| sat | 0 | | | |ball_count_2d_plain.04.seq_lazy_global_3.smt2 | 0.060s | 21.016MiB| unsat | 0 | | | |CMOS-opamp-chunk-0190.smt2 | 0.060s | 20.84MiB| sat | 0 | | | |exp-problem-10-2-chunk-0234.smt2 | 0.060s | 20.608MiB| sat | 0 | | | |matrix-1-all-2.smt2 | 0.060s | 21.016MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0156.smt2 | 0.061s | 20.8MiB| sat | 0 | | | |sin-problem-7-weak-chunk-0138.smt2 | 0.061s | 20.732MiB| sat | 0 | | | |sqrt-problem-Melquiond2-chunk-0023.smt2 | 0.061s | 20.812MiB| sat | 0 | | | |sin-problem-7-chunk-0172.smt2 | 0.061s | 20.78MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0379.smt2 | 0.061s | 20.88MiB| sat | 0 | | | |ball_count_2d_hill.05.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.061s | 21.624MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0030.smt2 | 0.061s | 20.736MiB| unsat | 0 | | | |ball_count_2d_slope.04.seq_lazy_linear_enc_lemmas_global_11.smt2 | 0.061s | 20.336MiB| unsat | 0 | | | |atan-vega-3-chunk-0360.smt2 | 0.061s | 20.752MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.redlog_global_11.smt2 | 0.061s | 19.74MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_linear_enc_global_9.smt2 | 0.061s | 19.484MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0121.smt2 | 0.061s | 20.748MiB| unsat | 0 | | | |ball_count_2d_plain.03.qfree_global_15.smt2 | 0.061s | 22.024MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_lemmas_global_15.smt2 | 0.061s | 20.34MiB| unsat | 0 | | | |ball_count_2d_hill.10.redlog_global_9.smt2 | 0.061s | 20.924MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_lemmas_global_15.smt2 | 0.061s | 20.536MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.redlog_global_13.smt2 | 0.061s | 22.032MiB| unsat | 0 | | | |mbo_E6.smt2 | 0.062s | 20.748MiB| unsat | 0 | | | |sin-problem-7-chunk-0054.smt2 | 0.062s | 20.756MiB| sat | 0 | | | |cos-3410-b-chunk-0015.smt2 | 0.062s | 20.82MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0117.smt2 | 0.062s | 20.868MiB| unsat | 0 | | | |CONVOI2-chunk-0041.smt2 | 0.062s | 20.992MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0086.smt2 | 0.062s | 18.864MiB| unsat | 0 | | | |ball_count_2d_hill.01.seq_lazy_linear_enc_global_15.smt2 | 0.062s | 20.364MiB| unsat | 0 | | | |atan-vega-3-chunk-0613.smt2 | 0.062s | 21.204MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0681.smt2 | 0.062s | 21.184MiB| unsat | 0 | | | |sin-problem-8-chunk-0043.smt2 | 0.062s | 20.696MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0053.smt2 | 0.062s | 20.912MiB| sat | 0 | | | |ball_count_1d_plain.02.seq_lazy_linear_enc_global_5.smt2 | 0.062s | 19.12MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_linear_enc_global_11.smt2 | 0.062s | 21.464MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.qfree_global_13.smt2 | 0.062s | 19.652MiB| unsat | 0 | | | |atan-problem-2-chunk-0070.smt2 | 0.062s | 20.672MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0633.smt2 | 0.062s | 20.948MiB| sat | 0 | | | |ball_count_1d_plain.04.seq_lazy_linear_enc_lemmas_global_7.smt2 | 0.063s | 21.288MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0620.smt2 | 0.063s | 20.764MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0166.smt2 | 0.063s | 21.052MiB| sat | 0 | | | |atan-vega-3-chunk-0129.smt2 | 0.063s | 20.512MiB| sat | 0 | | | |atan-vega-3-chunk-0260.smt2 | 0.063s | 20.764MiB| sat | 0 | | | |MulliganEconomicsModel0085a.smt2 | 0.063s | 20.624MiB| sat | 0 | | | |exp-problem-10-2-chunk-0358.smt2 | 0.063s | 20.644MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0721.smt2 | 0.063s | 20.832MiB| sat | 0 | | | |ball_count_1d_plain.05.seq_lazy_linear_enc_global_7.smt2 | 0.063s | 21.132MiB| unsat | 0 | | | |atan-problem-1-chunk-0102.smt2 | 0.063s | 20.96MiB| unsat | 0 | | | |atan-vega-3-chunk-0573.smt2 | 0.063s | 20.992MiB| unsat | 0 | | | |ball_count_2d_slope.04.seq_lazy_global_1.smt2 | 0.064s | 19.112MiB| unsat | 0 | | | |atan-vega-3-chunk-0413.smt2 | 0.064s | 20.884MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0657.smt2 | 0.064s | 20.864MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0136.smt2 | 0.064s | 20.76MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0606.smt2 | 0.064s | 20.888MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.064s | 19.576MiB| unsat | 0 | | | |sin-problem-7-chunk-0143.smt2 | 0.064s | 20.784MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0075.smt2 | 0.064s | 20.608MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0015.smt2 | 0.064s | 20.684MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0243.smt2 | 0.064s | 21.08MiB| unsat | 0 | | | |ball_count_1d_plain.01.redlog_global_9.smt2 | 0.065s | 19.624MiB| unsat | 0 | | | |ball_count_2d_hill.10.seq_lazy_lemmas_global_11.smt2 | 0.065s | 20.356MiB| unsat | 0 | | | |ball_count_2d_plain.10.qfree_global_3.smt2 | 0.065s | 19.016MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0018.smt2 | 0.065s | 20.708MiB| sat | 0 | | | |ball_count_2d_plain.04.seq_lazy_linear_enc_global_15.smt2 | 0.065s | 22.02MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_lemmas_global_15.smt2 | 0.065s | 21.52MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_lemmas_global_9.smt2 | 0.065s | 21.668MiB| unsat | 0 | | | |CMOS-opamp-chunk-0275.smt2 | 0.065s | 20.708MiB| sat | 0 | | | |Chua-2-VC2-L-chunk-0052.smt2 | 0.065s | 20.708MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_lemmas_global_15.smt2 | 0.065s | 20.032MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.redlog_global_9.smt2 | 0.065s | 21.64MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0349.smt2 | 0.066s | 20.996MiB| sat | 0 | | | |ball_count_2d_plain.05.qfree_global_9.smt2 | 0.066s | 21.6MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0250.smt2 | 0.066s | 20.844MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0444.smt2 | 0.066s | 20.904MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_linear_enc_global_13.smt2 | 0.066s | 19.796MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0075.smt2 | 0.066s | 20.696MiB| sat | 0 | | | |ball_count_2d_plain.04.seq_lazy_lemmas_global_7.smt2 | 0.066s | 21.756MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.redlog_global_3.smt2 | 0.066s | 19.04MiB| unsat | 0 | | | |ball_count_1d_plain.10.redlog_global_13.smt2 | 0.066s | 19.74MiB| unsat | 0 | | | |ball_count_2d_hill.04.seq_lazy_global_3.smt2 | 0.066s | 21.284MiB| unsat | 0 | | | |asin-8-chunk-0053.smt2 | 0.066s | 20.608MiB| sat | 0 | | | |ball_count_2d_slope.03.seq_lazy_linear_enc_lemmas_global_15.smt2 | 0.066s | 21.068MiB| unsat | 0 | | | |atan-problem-2-weakT-chunk-0054.smt2 | 0.067s | 20.7MiB| sat | 0 | | | |ball_count_2d_plain.03.seq_lazy_linear_enc_global_7.smt2 | 0.067s | 21.152MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0170.smt2 | 0.067s | 20.768MiB| unsat | 0 | | | |ball_count_2d_plain.03.redlog_global_5.smt2 | 0.067s | 21.396MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0074.smt2 | 0.067s | 20.988MiB| unsat | 0 | | | |ball_count_2d_plain.01.qfree_global_3.smt2 | 0.067s | 19.02MiB| unsat | 0 | | | |ball_count_2d_plain.02.qfree_global_11.smt2 | 0.067s | 19.528MiB| unsat | 0 | | | |MulliganEconomicsModel0027c.smt2 | 0.067s | 20.868MiB| unsat | 0 | | | |InVarSynth_PostfixIncrementDecrement.c_Iteration3_0.smt2 | 0.068s | 21.02MiB| unsat | 0 | | | |etcs_braking_2.01.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.068s | 21.34MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0530.smt2 | 0.068s | 20.848MiB| sat | 0 | | | |atan-vega-3-chunk-0493.smt2 | 0.068s | 20.744MiB| sat | 0 | | | |atan-problem-2-sqrt-chunk-0019.smt2 | 0.068s | 20.768MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0230.smt2 | 0.068s | 21.276MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_lemmas_global_7.smt2 | 0.068s | 21.544MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_global_7.smt2 | 0.069s | 21.288MiB| unsat | 0 | | | |ball_count_2d_slope.02.seq_lazy_lemmas_global_11.smt2 | 0.069s | 20.752MiB| unsat | 0 | | | |ball_count_1d_plain.03.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.069s | 21.02MiB| unsat | 0 | | | |ball_count_2d_hill.02.seq_lazy_linear_enc_global_15.smt2 | 0.069s | 20.292MiB| unsat | 0 | | | |ball_count_1d_plain.03.seq_lazy_lemmas_global_5.smt2 | 0.069s | 21.672MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0142.smt2 | 0.069s | 20.768MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0342.smt2 | 0.069s | 21.048MiB| unsat | 0 | | | |ball_count_1d_plain.10.redlog_global_9.smt2 | 0.069s | 19.76MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0242.smt2 | 0.069s | 20.972MiB| sat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.070s | 21.16MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_global_13.smt2 | 0.070s | 21.888MiB| unsat | 0 | | | |ball_count_2d_hill.01.seq_lazy_lemmas_global_7.smt2 | 0.070s | 19.732MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0126.smt2 | 0.070s | 20.88MiB| sat | 0 | | | |exp-problem-10-2-chunk-0028.smt2 | 0.070s | 20.564MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0398.smt2 | 0.070s | 21.068MiB| sat | 0 | | | |ball_count_2d_plain.03.seq_lazy_global_13.smt2 | 0.070s | 21.852MiB| unsat | 0 | | | |ball_count_2d_plain.02.seq_lazy_global_1.smt2 | 0.070s | 18.972MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0515.smt2 | 0.070s | 20.892MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0480.smt2 | 0.070s | 20.752MiB| unsat | 0 | | | |etcs_braking_2.01.qfree_global_3.smt2 | 0.071s | 21.276MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0556.smt2 | 0.071s | 20.86MiB| unsat | 0 | | | |Chua-2-VC2-L-chunk-0062.smt2 | 0.071s | 20.72MiB| sat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_lemmas_global_11.smt2 | 0.071s | 22.02MiB| unsat | 0 | | | |ball_count_2d_hill.02.redlog_global_13.smt2 | 0.071s | 21.012MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0359.smt2 | 0.071s | 20.884MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0276.smt2 | 0.072s | 21.104MiB| sat | 0 | | | |sin-344-4-chunk-0032.smt2 | 0.072s | 20.768MiB| sat | 0 | | | |sin-problem-10-3-chunk-0023.smt2 | 0.072s | 20.764MiB| unsat | 0 | | | |ball_count_2d_hill.10.redlog_global_13.smt2 | 0.072s | 21.236MiB| unsat | 0 | | | |sin-344-3-weak-chunk-0044.smt2 | 0.072s | 20.78MiB| sat | 0 | | | |sin-cos-346-b-chunk-0524.smt2 | 0.072s | 18.82MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0179.smt2 | 0.073s | 20.692MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0039.smt2 | 0.073s | 20.716MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0589.smt2 | 0.073s | 20.984MiB| sat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_lemmas_global_3.smt2 | 0.073s | 21.032MiB| unsat | 0 | | | |atan-problem-2-weakT-chunk-0019.smt2 | 0.073s | 20.648MiB| sat | 0 | | | |ball_count_1d_plain.05.seq_lazy_global_9.smt2 | 0.073s | 21.436MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0070.smt2 | 0.073s | 20.716MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0668.smt2 | 0.074s | 21.056MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0082.smt2 | 0.074s | 18.836MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0519.smt2 | 0.074s | 20.772MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0218.smt2 | 0.074s | 20.808MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0643.smt2 | 0.074s | 21.076MiB| unsat | 0 | | | |ball_count_2d_hill.04.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.074s | 21.272MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0054.smt2 | 0.074s | 20.884MiB| sat | 0 | | | |ball_count_2d_plain.04.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.074s | 21.064MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0305.smt2 | 0.074s | 20.624MiB| sat | 0 | | | |exp-problem-10-2-chunk-0265.smt2 | 0.075s | 20.784MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0728.smt2 | 0.075s | 20.612MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_lemmas_global_15.smt2 | 0.075s | 21.672MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0177.smt2 | 0.075s | 21.024MiB| sat | 0 | | | |exp-problem-10-2-chunk-0335.smt2 | 0.076s | 20.884MiB| unsat | 0 | | | |ball_count_1d_plain.04.seq_lazy_global_5.smt2 | 0.076s | 21.152MiB| unsat | 0 | | | |atan-vega-3-chunk-0189.smt2 | 0.076s | 20.968MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0391.smt2 | 0.076s | 21.1MiB| sat | 0 | | | |ball_count_2d_hill.05.seq_lazy_global_3.smt2 | 0.076s | 21.028MiB| unsat | 0 | | | |atan-vega-3-chunk-0119.smt2 | 0.077s | 20.676MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0058.smt2 | 0.077s | 20.68MiB| unsat | 0 | | | |atan-vega-3-chunk-0423.smt2 | 0.078s | 20.764MiB| sat | 0 | | | |sin-cos-346-b-chunk-0068.smt2 | 0.078s | 18.896MiB| unsat | 0 | | | |InVarSynth_doubleLoopUniformIterations.bpl_Iteration2_0.smt2 | 0.078s | 21.124MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0536.smt2 | 0.078s | 20.62MiB| sat | 0 | | | |ball_count_1d_plain.04.qfree_global_7.smt2 | 0.079s | 21.172MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0048.smt2 | 0.079s | 20.716MiB| sat | 0 | | | |MulliganEconomicsModel0067a.smt2 | 0.079s | 20.82MiB| sat | 0 | | | |InVarSynth_ShortCircuit-SideEffect-SwitchStatement-Safe.c_Iteration1_0.smt2 | 0.079s | 21.704MiB| sat | 0 | | | |ball_count_2d_plain.03.seq_lazy_global_9.smt2 | 0.079s | 21.484MiB| unsat | 0 | | | |ball_count_2d_slope.04.seq_lazy_linear_enc_global_3.smt2 | 0.079s | 21.268MiB| unsat | 0 | | | |sin-problem-7-chunk-0079.smt2 | 0.080s | 20.736MiB| sat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_linear_enc_lemmas_global_11.smt2 | 0.080s | 21.696MiB| unsat | 0 | | | |ball_count_1d_plain.01.seq_lazy_global_3.smt2 | 0.080s | 19.12MiB| unsat | 0 | | | |ball_count_2d_hill.01.redlog_global_13.smt2 | 0.080s | 21.204MiB| unsat | 0 | | | |ball_count_2d_plain.04.redlog_global_13.smt2 | 0.081s | 22.504MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0436.smt2 | 0.081s | 21.036MiB| sat | 0 | | | |exp-problem-10-3-chunk-0178.smt2 | 0.081s | 20.584MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_global_15.smt2 | 0.081s | 19.984MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0085.smt2 | 0.081s | 20.868MiB| sat | 0 | | | |sqrt-circles-2-chunk-0002.smt2 | 0.081s | 20.664MiB| sat | 0 | | | |atan-problem-2-chunk-0107.smt2 | 0.082s | 20.808MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0171.smt2 | 0.082s | 21.264MiB| sat | 0 | | | |ball_count_2d_hill_simple.05.qfree_global_1.smt2 | 0.082s | 18.896MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0199.smt2 | 0.082s | 20.968MiB| sat | 0 | | | |simple_ballistics_reach.01.seq_lazy_linear_enc_global_1.smt2 | 0.082s | 20.888MiB| unsat | 0 | | | |Chua-2-IL-L-chunk-0058.smt2 | 0.082s | 20.86MiB| sat | 0 | | | |ball_count_2d_plain.03.seq_lazy_linear_enc_lemmas_global_15.smt2 | 0.082s | 22.188MiB| unsat | 0 | | | |atan-vega-3-chunk-0077.smt2 | 0.082s | 20.672MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.083s | 21.444MiB| unsat | 0 | | | |ball_count_2d_plain.04.redlog_global_9.smt2 | 0.083s | 22.028MiB| unsat | 0 | | | |ball_count_2d_plain.10.redlog_global_11.smt2 | 0.083s | 19.876MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0323.smt2 | 0.083s | 20.744MiB| sat | 0 | | | |ball_count_1d_plain.10.seq_lazy_lemmas_global_7.smt2 | 0.083s | 19.32MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0631.smt2 | 0.083s | 20.88MiB| sat | 0 | | | |sin-cos-346-b-chunk-0391.smt2 | 0.084s | 20.812MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0286.smt2 | 0.084s | 21.232MiB| sat | 0 | | | |Chua-2-VC2-U-chunk-0051.smt2 | 0.084s | 20.82MiB| sat | 0 | | | |ball_count_2d_hill.04.seq_lazy_lemmas_global_7.smt2 | 0.084s | 21.96MiB| unsat | 0 | | | |ball_count_2d_plain.01.redlog_global_7.smt2 | 0.085s | 19.652MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.085s | 20.216MiB| unsat | 0 | | | |sin-344-3-chunk-0058.smt2 | 0.085s | 20.716MiB| sat | 0 | | | |atan-vega-3-chunk-0149.smt2 | 0.086s | 20.768MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0402.smt2 | 0.086s | 20.908MiB| sat | 0 | | | |sqrt-circles-2-chunk-0015.smt2 | 0.086s | 20.664MiB| unsat | 0 | | | |ball_count_1d_plain.04.seq_lazy_lemmas_global_9.smt2 | 0.087s | 21.472MiB| unsat | 0 | | | |CMOS-opamp-chunk-0246.smt2 | 0.087s | 20.712MiB| unsat | 0 | | | |ball_count_2d_plain.01.seq_lazy_lemmas_global_5.smt2 | 0.087s | 19.376MiB| unsat | 0 | | | |ball_count_2d_hill.05.seq_lazy_lemmas_global_7.smt2 | 0.088s | 21.788MiB| unsat | 0 | | | |sqrt-problem-12vars3-chunk-0055.smt2 | 0.088s | 20.756MiB| sat | 0 | | | |Chua-2-VC1-L-chunk-0062.smt2 | 0.088s | 20.692MiB| sat | 0 | | | |Chua-1-IL-U-chunk-0076.smt2 | 0.088s | 20.804MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_lemmas_global_7.smt2 | 0.089s | 21.952MiB| unsat | 0 | | | |ball_count_1d_plain.05.seq_lazy_linear_enc_global_11.smt2 | 0.089s | 21.572MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_lemmas_global_13.smt2 | 0.089s | 22.092MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_global_9.smt2 | 0.090s | 21.536MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.qfree_global_15.smt2 | 0.090s | 22.268MiB| unsat | 0 | | | |sin-problem-7-chunk-0182.smt2 | 0.090s | 20.656MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0412.smt2 | 0.090s | 21.136MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.redlog_global_15.smt2 | 0.090s | 21.988MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0679.smt2 | 0.092s | 21.2MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0151.smt2 | 0.092s | 18.816MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.qfree_global_5.smt2 | 0.094s | 20.956MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.095s | 22.036MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0621.smt2 | 0.096s | 21.016MiB| sat | 0 | | | |ball_count_2d_slope.03.seq_lazy_lemmas_global_3.smt2 | 0.099s | 21.668MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0690.smt2 | 0.100s | 20.98MiB| sat | 0 | | | |MulliganEconomicsModel0077c.smt2 | 0.102s | 20.844MiB| unsat | 0 | | | |ball_count_2d_plain.05.qfree_global_13.smt2 | 0.102s | 21.952MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0097.smt2 | 0.104s | 21.052MiB| sat | 0 | | | |cos-3410-b-chunk-0027.smt2 | 0.104s | 20.712MiB| sat | 0 | | | |bottom-plate-mixer-chunk-0050.smt2 | 0.106s | 20.628MiB| sat | 0 | | | |exp-problem-10-2-chunk-0375.smt2 | 0.106s | 20.804MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0255.smt2 | 0.108s | 20.724MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0209.smt2 | 0.108s | 20.96MiB| sat | 0 | | | |ball_count_2d_slope.04.seq_lazy_global_5.smt2 | 0.109s | 21.848MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0484.smt2 | 0.109s | 21.116MiB| sat | 0 | | | |polypaver-sqrt43-int-chunk-0053.smt2 | 0.110s | 20.852MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_linear_enc_global_15.smt2 | 0.110s | 22.012MiB| unsat | 0 | | | |ball_count_1d_plain.03.redlog_global_11.smt2 | 0.111s | 21.624MiB| unsat | 0 | | | |mgc_06.smt2 | 0.112s | 21.0MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0651.smt2 | 0.113s | 20.844MiB| unsat | 0 | | | |ball_count_1d_plain.03.seq_lazy_linear_enc_global_13.smt2 | 0.116s | 21.776MiB| unsat | 0 | | | |sin-problem-7-chunk-0192.smt2 | 0.117s | 20.772MiB| sat | 0 | | | |ball_count_2d_plain.05.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.117s | 21.568MiB| unsat | 0 | | | |ball_count_1d_plain.04.seq_lazy_linear_enc_lemmas_global_11.smt2 | 0.122s | 21.704MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_global_5.smt2 | 0.122s | 21.028MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0254.smt2 | 0.124s | 21.032MiB| unsat | 0 | | | |ball_count_1d_plain.05.seq_lazy_global_13.smt2 | 0.124s | 21.788MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0446.smt2 | 0.125s | 21.356MiB| sat | 0 | | | |ball_count_2d_plain.04.seq_lazy_lemmas_global_11.smt2 | 0.126s | 22.052MiB| unsat | 0 | | | |CMOS-opamp-chunk-0320.smt2 | 0.127s | 21.064MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0155.smt2 | 0.127s | 21.076MiB| sat | 0 | | | |mbo_E5E23.smt2 | 0.128s | 21.588MiB| unsat | 0 | | | |ball_count_1d_plain.04.qfree_global_11.smt2 | 0.133s | 21.672MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0426.smt2 | 0.138s | 20.896MiB| sat | 0 | | | |ball_count_1d_plain.03.seq_lazy_linear_enc_global_9.smt2 | 0.139s | 21.24MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_lemmas_global_15.smt2 | 0.143s | 22.668MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_linear_enc_lemmas_global_15.smt2 | 0.153s | 22.252MiB| unsat | 0 | | | |mc91test.t2.c_Iteration5_Loop_3-pieceTemplate.smt2 | 0.155s | 23.332MiB| sat | 0 | | | |ball_count_1d_plain.04.seq_lazy_lemmas_global_13.smt2 | 0.160s | 21.904MiB| unsat | 0 | | | |sin-problem-8-weak-chunk-0079.smt2 | 0.161s | 21.136MiB| unsat | 0 | | | |toeplz.c.i.toeplz.pl.t2.fixed.t2.c_Iteration10_Loop_3-pieceTemplate.smt2 | 0.170s | 22.636MiB| sat | 0 | | | |ball_count_1d_plain.05.qfree_global_15.smt2 | 0.175s | 22.132MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0457.smt2 | 0.180s | 21.348MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_lemmas_global_11.smt2 | 0.190s | 22.848MiB| unsat | 0 | | | |ball_count_2d_hill.04.seq_lazy_lemmas_global_11.smt2 | 0.191s | 22.768MiB| unsat | 0 | | | |ball_count_2d_hill.04.seq_lazy_linear_enc_global_15.smt2 | 0.208s | 23.636MiB| unsat | 0 | | | |etcs_braking_2.01.seq_lazy_lemmas_global_5.smt2 | 0.209s | 22.728MiB| unsat | 0 | | | |standard_init9_ground.i_3_2_2.bpl_1.smt2 | 0.217s | 21.52MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_linear_enc_global_15.smt2 | 0.218s | 23.536MiB| unsat | 0 | | | |ball_count_2d_hill.05.seq_lazy_lemmas_global_11.smt2 | 0.222s | 22.852MiB| unsat | 0 | | | |ball_count_1d_plain.03.seq_lazy_global_15.smt2 | 0.225s | 21.848MiB| unsat | 0 | | | |ball_count_2d_hill.05.seq_lazy_linear_enc_global_15.smt2 | 0.231s | 23.644MiB| unsat | 0 | | | |ball_count_2d_slope.03.seq_lazy_linear_enc_global_7.smt2 | 0.234s | 22.424MiB| unsat | 0 | | | |ball_count_2d_slope.05.seq_lazy_lemmas_global_5.smt2 | 0.234s | 22.44MiB| unsat | 0 | | | |qrdcmp.t2.c_Iteration6_Loop_3-pieceTemplate.smt2 | 0.236s | 23.528MiB| sat | 0 | | | |ball_count_1d_plain.05.seq_lazy_linear_enc_lemmas_global_15.smt2 | 0.258s | 22.092MiB| unsat | 0 | | | |CMOS-opamp-chunk-0180.smt2 | 0.265s | 21.82MiB| unsat | 0 | | | |ball_count_1d_plain.04.redlog_global_15.smt2 | 0.272s | 22.172MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0201.smt2 | 0.322s | 23.156MiB| unsat | 0 | | | |pentagon.t2.c_Iteration9_Loop_3-pieceTemplate.smt2 | 0.340s | 22.96MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0296.smt2 | 0.355s | 21.36MiB| unsat | 0 | | | |p-42.t2.c_Iteration2_Loop_4-pieceTemplate.smt2 | 0.366s | 24.816MiB| sat | 0 | | | |spiral.t2.c_Iteration8_Loop_4-pieceTemplate.smt2 | 0.402s | 24.448MiB| sat | 0 | | | |sort.t2.c_Iteration5_Loop_3-pieceTemplate.smt2 | 0.460s | 25.86MiB| sat | 0 | | | |etcs_braking_2.01.seq_lazy_linear_enc_global_9.smt2 | 0.488s | 24.248MiB| unsat | 0 | | | |Canberra.bpl_Iteration1_Loop_2-pieceTemplate.smt2 | 0.590s | 44.768MiB| unsat | 0 | | | |bf10.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 0.600s | 25.136MiB| sat | 0 | | | |CookSeeZuleger-2013TACAS-Fig3_true-termination.c_Iteration1_Loop_5-phaseTemplate.smt2 | 0.639s | 44.532MiB| unsat | 0 | | | |matrix-1-all-38.smt2 | 0.646s | 21.856MiB| sat | 0 | | | |toeplz.t2.c_Iteration7_Loop_4-pieceTemplate.smt2 | 0.654s | 24.816MiB| sat | 0 | | | |ball_count_2d_slope.05.seq_lazy_linear_enc_global_9.smt2 | 0.717s | 23.728MiB| unsat | 0 | | | |SyntaxSupportDisjunction1.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 0.725s | 26.088MiB| sat | 0 | | | |ball_count_2d_hill.05.redlog_global_9.smt2 | 0.820s | 23.668MiB| unsat | 0 | | | |ball_count_2d_hill.03.redlog_global_9.smt2 | 0.861s | 23.628MiB| unsat | 0 | | | |ball_count_2d_hill.04.redlog_global_9.smt2 | 0.878s | 23.584MiB| unsat | 0 | | | |ball_count_2d_slope.03.seq_lazy_global_9.smt2 | 0.901s | 24.06MiB| unsat | 0 | | | |CookSeeZuleger-2013TACAS-Fig7a_true-termination.c_Iteration1_Loop_5-phaseTemplate.smt2 | 0.951s | 76.368MiB| unsat | 0 | | | |ex11.t2.c_Iteration1_Lasso_5-phaseTemplate.smt2 | 1.155s | 29.556MiB| unsat | 0 | | | |Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2 | 1.233s | 43.136MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0315.smt2 | 1.339s | 22.248MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0123.smt2 | 1.616s | 21.988MiB| unsat | 0 | | | |eric.t2.c_Iteration1_Lasso_5-phaseTemplate.smt2 | 1.759s | 27.032MiB| unsat | 0 | | | |ball_count_2d_slope.03.seq_lazy_linear_enc_global_11.smt2 | 2.548s | 25.608MiB| unsat | 0 | | | |sin-problem-7-weak2-chunk-0113.smt2 | 2.628s | 21.964MiB| unsat | 0 | | | |ball_count_2d_slope.04.seq_lazy_lemmas_global_9.smt2 | 2.672s | 25.024MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0181.smt2 | 3.050s | 22.032MiB| sat | 0 | | | |joey_false-termination.c_Iteration2_Loop_6-phaseTemplate.smt2 | 3.545s | 28.696MiB| unsat | 0 | | | |p-55.t2.c_Iteration3_Loop_4-pieceTemplate.smt2 | 4.674s | 42.912MiB| sat | 0 | | | |TelAviv-Amir-Minimum_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2 | 4.849s | 260.0MiB| unsat | 0 | | | |KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-termination.c_Iteration1_Lasso_affineTemplate.smt2 | 4.987s | 69.096MiB| unsat | 0 | | | |ball_count_2d_hill.05.redlog_global_13.smt2 | 7.249s | 25.872MiB| unsat | 0 | | | |ball_count_2d_hill.03.redlog_global_13.smt2 | 7.274s | 25.936MiB| unsat | 0 | | | |ball_count_2d_hill.04.redlog_global_13.smt2 | 8.065s | 26.004MiB| unsat | 0 | | | |ball_count_2d_slope.05.seq_lazy_global_15.smt2 | 10.086s | 33.98MiB| unknown | 0 | | | |ball_count_2d_slope.03.seq_lazy_global_13.smt2 | 14.067s | 29.652MiB| unknown | 0 | | | |ball_count_2d_slope.04.seq_lazy_lemmas_global_13.smt2 | 14.070s | 30.108MiB| unknown | 0 | | | |ball_count_2d_slope.05.seq_lazy_linear_enc_global_13.smt2 | 14.093s | 37.244MiB| unknown | 0 | | | |mbo_E6E7.smt2 | 14.135s | 22.444MiB| unsat | 0 | | | |2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2 | 14.178s | 25.072MiB| unsat | 0 | | | |BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2 | 14.204s | 31.268MiB| unsat | 0 | | | |mbo_E1E22.smt2 | 14.245s | 219.0MiB| unknown | 0 | | | |ex4.t2.c_Iteration2_Loop_3-pieceTemplate.smt2 | 14.270s | 26.4MiB| sat | 0 | | | |mbo_E13E17.smt2 | 14.293s | 155.0MiB| unknown | 0 | | | |etcs_braking_2.01.seq_lazy_global_15.smt2 | 14.334s | 36.044MiB| unsat | 0 | | | |mbo_E9E13.smt2 | 14.369s | 127.0MiB| unknown | 0 | | | |matrix-2-all-4.smt2 | 14.436s | 184.0MiB| sat | 0 | | | |selectSort.t2.c_Iteration3_Loop_4-pieceTemplate.smt2 | 14.610s | 29.504MiB| sat | 0 | | | |mbo_E15E18.smt2 | 14.637s | 128.0MiB| unknown | 0 | | | |mbo_E4E17.smt2 | 15.363s | 234.0MiB| unknown | 0 | | | |db3.t2.c_Iteration2_Loop_4-pieceTemplate.smt2 | 15.407s | 35.248MiB| sat | 0 | | | |mbo_E1E6.smt2 | 15.729s | 256.0MiB| unknown | 0 | | | |loop_on_input.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 15.758s | 30.3MiB| sat | 0 | | | |Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2 | 16.378s | 26.98MiB| unsat | 0 | | | |mbo_E5E12.smt2 | 16.761s | 126.0MiB| unknown | 0 | | | |MulliganEconomicsModel0057c.smt2 | 18.625s | 29.792MiB| unsat | 0 | | | |fun9.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 19.252s | 31.756MiB| sat | 0 | | | |Garmisch.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 20.556s | 28.556MiB| unsat | 0 | | | |mbo_E7E26.smt2 | 25.611s | 61.176MiB| unsat | 0 | | | |fuhs-inflasso.t2.c_Iteration2_Loop_4-pieceTemplate.smt2 | 26.250s | 32.4MiB| sat | 0 | | | |polyrank3.t2.c_Iteration2_Loop_3-pieceTemplate.smt2 | 28.375s | 37.2MiB| unsat | 0 | | | |nested.t2.c_Iteration3_Loop_3-pieceTemplate.smt2 | 32.195s | 37.812MiB| sat | 0 | | | |standard_copy5_ground.i_3_2_2.bpl_3.smt2 | 32.232s | 24.348MiB| unsat | 0 | | | |matrix-3-all-4.smt2 | 32.738s | 57.98MiB| sat | 0 | | | |byron-1.t2.c_Iteration1_Loop_3-pieceTemplate.smt2 | 32.902s | 29.412MiB| unsat | 0 | | | |Mysore2.bpl_Iteration1_Loop_3-pieceTemplate.smt2 | 32.926s | 57.528MiB| unsat | 0 | | | |Lobnya-Boolean-Reordered.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 37.824s | 37.844MiB| unsat | 0 | | | |SyntaxSupportDivision1.bpl_Iteration1_Lasso_7-nestedTemplate.smt2 | 39.202s | 81.248MiB| sat | 0 | | | |hong_10.smt2 | 39.768s | 41.036MiB| unsat | 0 | | | |Collatz.bpl_Iteration1_Loop_3-nestedTemplate.smt2 | 44.797s | 253.0MiB| unsat | 0 | | | |mbo_E14E22.smt2 | 45.676s | 232.0MiB| sat | 0 | | | |simple-scaled200.bpl_Iteration1_Lasso_7-phaseTemplate.smt2 | 46.259s | 165.0MiB| sat | 0 | | | |Collatz.bpl_Iteration1_Loop_6-phaseTemplate.smt2 | 48.737s | 488.0MiB| unsat | 0 | | | |Collatz.bpl_Iteration1_Lasso_6-nestedTemplate.smt2 | 49.648s | 515.0MiB| unsat | 0 | | | |etcs_braking_2.01.redlog_global_11.smt2 | 50.255s | 39.244MiB| unsat | 0 | | | |mbo_E25.smt2 | 50.270s | 25.832MiB| unsat | 0 | | | |etcs_braking_2.01.redlog_global_7.smt2 | 50.371s | 34.2MiB| unsat | 0 | | | |kissing_4_4.smt2 | 50.665s | 88.336MiB| sat | 0 | | | |polyrank5.t2.c_Iteration1_Loop_7-phaseTemplate.smt2 | 51.104s | 29.724MiB| sat | 0 | | | |SantaBarbara01.bpl_Iteration1_Lasso_4-pieceTemplate.smt2 | 52.024s | 39.576MiB| unsat | 0 | | | |polyrank4.t2.c_Iteration8_Loop_2-pieceTemplate.smt2 | 52.194s | 33.152MiB| unsat | 0 | | | |BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2 | 52.910s | 56.276MiB| unsat | 0 | | | |Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 54.325s | 54.088MiB| unsat | 0 | | | |CookSeeZuleger-2013TACAS-Fig7b.bpl_Iteration1_Loop_3-pieceTemplate.smt2 | 54.380s | 107.0MiB| unsat | 0 | | | |polyrank4.t2.c_Iteration3_Loop_3-pieceTemplate.smt2 | 54.532s | 42.284MiB| unsat | 0 | | | |yPositive-MixedIntReal.bpl_Iteration1_Loop_3-pieceTemplate.smt2 | 56.342s | 47.616MiB| unsat | 0 | | | |iecs.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 56.521s | 58.24MiB| unsat | 0 | | | |sas2.t2.c_Iteration6_Lasso_7-nestedTemplate.smt2 | 56.827s | 56.024MiB| sat | 0 | | | |mbo_E8E24.smt2 | 56.986s | 610.0MiB| unknown | 0 | | | |Masse_true-termination.c_Iteration1_Loop_2-pieceTemplate.smt2 | 58.091s | 98.0MiB| unsat | 0 | | | |mbo_E10E18.smt2 | 58.247s | 614.0MiB| unknown | 0 | | | |LeeJonesBen-Amram-2001POPL-Ex4_true-termination.c_Iteration2_Loop_3-pieceTemplate.smt2 | 58.440s | 58.872MiB| unsat | 0 | | | |mbo_E2E10.smt2 | 58.679s | 770.0MiB| unknown | 0 | | | |mbo_E12E13.smt2 | 58.753s | 748.0MiB| unknown | 0 | | | |mbo_E3E8.smt2 | 59.918s | 909.0MiB| unknown | 0 | | | |eric2.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 59.970s | 81.836MiB| unsat | 0 | | | |mbo_E2E4.smt2 | 60.427s | 880.0MiB| unknown | 0 | | | |mbo_E1E13.smt2 | 61.313s | 886.0MiB| unknown | 0 | | | |mbo_E3E13.smt2 | 62.101s | 843.0MiB| unknown | 0 | | | |mbo_E6E19.smt2 | 62.150s | 946.0MiB| unknown | 0 | | | |Collatz.bpl_Iteration1_Lasso_2-pieceTemplate.smt2 | 64.858s | 520.0MiB| unsat | 0 | | | |Nyala-TwoLex.bpl_Iteration1_Lasso_4-pieceTemplate.smt2 | 66.149s | 225.0MiB| unsat | 0 | | | |polyrank3.t2.c_Iteration8_Loop_4-pieceTemplate.smt2 | 66.426s | 86.54MiB| unsat | 0 | | | |collatz.t2.c_Iteration3_Lasso_6-phaseTemplate.smt2 | 66.646s | 71.112MiB| unsat | 0 | | | |LeeJonesBen-Amram-2001POPL-Ex1_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2 | 70.907s | 99.664MiB| unsat | 0 | | | |KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-termination.c_Iteration1_Lasso_4-lexTemplate.smt2 | 71.341s | 284.0MiB| unsat | 0 | | | |mbo_E20E25.smt2 | 72.091s | 75.592MiB| unsat | 0 | | | |BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2 | 82.090s | 206.0MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0176.smt2 | 84.190s | 35.848MiB| unsat | 0 | | | |mbo_E23E24.smt2 | 84.652s | 101.0MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0265.smt2 | 90.649s | 35.76MiB| unsat | 0 | | | |matrix-5-all-13.smt2 | 92.956s | 543.0MiB| unknown | 0 | | | |eric2.t2.c_Iteration7_Loop_4-pieceTemplate.smt2 | 94.515s | 364.0MiB| unsat | 0 | | | |mbo_E9E23.smt2 | 97.584s | 97.756MiB| unsat | 0 | | | |mbo_E8E14.smt2 | 99.595s | 948.0MiB| unknown | 0 | | | |mbo_E13E27.smt2 | 99.786s | 105.0MiB| unsat | 0 | | | |OpposedDisjuncts.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 110.526s | 307.0MiB| unsat | 0 | | | |mbo_E7E16.smt2 | 113.037s | 115.0MiB| unsat | 0 | | | |GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_6-nestedTemplate.smt2 | 113.241s | 599.0MiB| unsat | 0 | | | |mbo_E4E27.smt2 | 114.586s | 89.876MiB| unsat | 0 | | | |sas2.t2.c_Iteration1_Lasso_4-pieceTemplate.smt2 | 123.257s | 460.0MiB| sat | 0 | | | |firewire.t2.c_Iteration1_Lasso_7-nestedTemplate.smt2 | 124.536s | 570.0MiB| sat | 0 | | | |GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_3-lexTemplate.smt2 | 137.580s | 867.0MiB| unsat | 0 | | | |NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2 | 142.591s | 596.0MiB| unknown | 0 | | | |NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2 | 155.929s | 678.0MiB| unsat | 0 | | | |mbo_E11E20.smt2 | 200.013s | 158.0MiB| timeout | 0 | | | |kissing_4_18.smt2 | 200.013s | 89.7MiB| timeout | 0 | | | |atan-vega-3-weak-chunk-0385.smt2 | 200.015s | 30.004MiB| timeout | 0 | | | |InVarSynth_BugHoareAnnotationWithMinimiation.bpl_Iteration1_0.smt2 | 200.015s | 79.576MiB| timeout | 0 | | | |matrix-4-all-22.smt2 | 200.016s | 189.0MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_global_11.smt2 | 200.016s | 116.0MiB| timeout | 0 | | | |mbo_E2E20.smt2 | 200.017s | 510.0MiB| timeout | 0 | | | |linear_search.i_7_19_3.bpl_3.smt2 | 200.017s | 56.832MiB| timeout | 0 | | | |mbo_E15E28.smt2 | 200.018s | 486.0MiB| timeout | 0 | | | |avg60.i_5_5_4.bpl_3.smt2 | 200.019s | 40.936MiB| timeout | 0 | | | |InVarSynth_threadpooling_out2.mover.bpl_Iteration2_0.smt2 | 200.020s | 106.0MiB| timeout | 0 | | | |seq.i_5_5_5.bpl_3.smt2 | 200.021s | 78.972MiB| timeout | 0 | | | |sin-problem-7-chunk-0297.smt2 | 200.021s | 94.664MiB| timeout | 0 | | | |mbo_E12E23.smt2 | 200.021s | 118.0MiB| timeout | 0 | | | |mbo_E18E22.smt2 | 200.027s | 136.0MiB| timeout | 0 | | | |sqrt-1mcosq-8-chunk-0233.smt2 | 200.028s | 42.512MiB| timeout | 0 | | | |fragtest_simple.i_4_5_4.bpl_3.smt2 | 200.030s | 105.0MiB| timeout | 0 | | | |kissing_3_9.smt2 | 200.032s | 76.948MiB| timeout | 0 | | | |standard_two_index_05.i_3_2_2.bpl_5.smt2 | 200.032s | 301.0MiB| timeout | 0 | | | |matrix-2-all-17.smt2 | 200.032s | 121.0MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_linear_enc_global_5.smt2 | 200.032s | 31.328MiB| timeout | 0 | | | |matrix-3-all-13.smt2 | 200.033s | 277.0MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_13.smt2 | 200.037s | 34.632MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_9.smt2 | 200.037s | 97.572MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_lemmas_global_15.smt2 | 200.038s | 35.372MiB| timeout | 0 | | | |matrix-4-all-4.smt2 | 200.039s | 273.0MiB| timeout | 0 | | | |mbo_E16E25.smt2 | 200.039s | 143.0MiB| timeout | 0 | | | |matrix-4-all-13.smt2 | 200.041s | 35.676MiB| timeout | 0 | | | |kissing_3_11.smt2 | 200.041s | 117.0MiB| timeout | 0 | | | |mbo_E3E23.smt2 | 200.046s | 594.0MiB| timeout | 0 | | | |LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_7-phaseTemplate.smt2 | 200.051s | 400.0MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_global_7.smt2 | 200.054s | 43.556MiB| timeout | 0 | | | |heidy7-simple.t2.c_Iteration2_Lasso_4-pieceTemplate.smt2 | 200.058s | 436.0MiB| timeout | 0 | | | |mbo_E10E28.smt2 | 200.062s | 512.0MiB| timeout | 0 | | | |LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_3-pieceTemplate.smt2 | 200.063s | 457.0MiB| timeout | 0 | | | |efegp.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2 | 200.069s | 563.0MiB| timeout | 0 | | | |mbo_E19E22.smt2 | 200.072s | 482.0MiB| timeout | 0 | | | |p-46.t2.c_Iteration2_Lasso_7-phaseTemplate.smt2 | 200.077s | 426.0MiB| timeout | 0 | | | |yPositive-SIscaled50.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 200.078s | 699.0MiB| timeout | 0 | | | |min_rf_true-termination.c_Iteration1_Loop_4-pieceTemplate.smt2 | 200.082s | 528.0MiB| timeout | 0 | | | |afagp-fail.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2 | 200.084s | 639.0MiB| timeout | 0 | | | |etcs_braking_2.01.seq_lazy_linear_enc_global_13.smt2 | 200.097s | 691.0MiB| timeout | 0 | | | |BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2 | 200.103s | 725.0MiB| timeout | 0 | | | |aviad_true-termination.c_Iteration1_Loop_6-phaseTemplate.smt2 | 200.108s | 944.0MiB| timeout | 0 | | | |aviad_true-termination.c_Iteration1_Loop_3-lexTemplate.smt2 | 200.112s | 1055.0MiB| timeout | 0 | | | |brp_withassume.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 200.134s | 1239.0MiB| timeout | 0 | | | |Gulwani.bpl_Iteration1_Lasso_4-pieceTemplate.smt2 | 200.136s | 1181.0MiB| timeout | 0 | | |