# . * SAT 477 * UNSAT 605 * TIMEOUT 43 * UNKNOWN 22 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: master run
Job tag: bnsat_false
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: 84a7566c3aa816b422455fe580f51263718e26b4
Z3 branch: master
Z3 options: "-T:200"
Z3 inputs: inputs/QF_NRA_small
Z3 commit message: Merge pull request #8878 from Z3Prover/copilot/rename-qf-s-benchmark

Rename "Qf S Benchmark" to "ZIPT Benchmark"
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |Chua-1-VC2-L-chunk-0064.smt2 | 0.023s | 18.712MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0204.smt2 | 0.023s | 20.776MiB| sat | 0 | | | |ball_count_2d_plain.05.seq_lazy_linear_enc_global_1.smt2 | 0.024s | 18.976MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0651.smt2 | 0.025s | 21.004MiB| unsat | 0 | | | |sin-problem-10-2-chunk-0024.smt2 | 0.025s | 18.76MiB| unsat | 0 | | | |atan-problem-1-chunk-0022.smt2 | 0.025s | 21.004MiB| sat | 0 | | | |sin-cos-346-b-chunk-0221.smt2 | 0.025s | 18.768MiB| unsat | 0 | | | |Chua-1-VC2-L-chunk-0027.smt2 | 0.026s | 18.912MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0079.smt2 | 0.026s | 18.728MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0092.smt2 | 0.026s | 18.872MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_global_1.smt2 | 0.026s | 18.888MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_linear_enc_global_1.smt2 | 0.027s | 18.92MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.redlog_global_1.smt2 | 0.027s | 18.972MiB| unsat | 0 | | | |sin-problem-7-chunk-0361.smt2 | 0.027s | 18.996MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0129.smt2 | 0.027s | 18.844MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0102.smt2 | 0.027s | 18.976MiB| unsat | 0 | | | |CMOS-opamp-chunk-0231.smt2 | 0.027s | 20.772MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0009.smt2 | 0.027s | 18.904MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0117.smt2 | 0.027s | 20.836MiB| unsat | 0 | | | |ball_count_2d_slope.02.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.028s | 19.324MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0078.smt2 | 0.028s | 18.836MiB| unsat | 0 | | | |ball_count_2d_plain.04.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.028s | 18.868MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0141.smt2 | 0.028s | 20.76MiB| sat | 0 | | | |atan-problem-2-chunk-0080.smt2 | 0.028s | 20.832MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0042.smt2 | 0.028s | 18.944MiB| unsat | 0 | | | |atan-vega-3-chunk-0230.smt2 | 0.028s | 20.636MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0019.smt2 | 0.028s | 20.508MiB| unsat | 0 | | | |atan-vega-3-chunk-0099.smt2 | 0.028s | 20.828MiB| sat | 0 | | | |atan-vega-3-chunk-0027.smt2 | 0.028s | 20.712MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0147.smt2 | 0.028s | 20.892MiB| sat | 0 | | | |exp-problem-10-2-chunk-0184.smt2 | 0.028s | 20.672MiB| sat | 0 | | | |ball_count_1d_plain.03.seq_lazy_lemmas_global_1.smt2 | 0.028s | 18.972MiB| unsat | 0 | | | |CMOS-opamp-chunk-0074.smt2 | 0.028s | 20.684MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0144.smt2 | 0.029s | 20.664MiB| sat | 0 | | | |sin-problem-7-weak2-chunk-0044.smt2 | 0.029s | 20.748MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0348.smt2 | 0.029s | 18.872MiB| unsat | 0 | | | |sin-problem-7-chunk-0233.smt2 | 0.029s | 20.768MiB| sat | 0 | | | |ball_count_1d_plain.02.redlog_global_3.smt2 | 0.029s | 19.224MiB| unsat | 0 | | | |CMOS-opamp-chunk-0342.smt2 | 0.029s | 20.832MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0044.smt2 | 0.029s | 18.852MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0042.smt2 | 0.029s | 20.76MiB| sat | 0 | | | |sin-cos-346-b-chunk-0504.smt2 | 0.029s | 20.94MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0555.smt2 | 0.029s | 20.716MiB| sat | 0 | | | |log-fun-ineq-g-chunk-0036.smt2 | 0.029s | 18.904MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_lemmas_global_5.smt2 | 0.029s | 19.444MiB| unsat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0049.smt2 | 0.029s | 20.896MiB| unsat | 0 | | | |Chua-1-IL-U-chunk-0049.smt2 | 0.029s | 20.884MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0159.smt2 | 0.029s | 20.636MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0661.smt2 | 0.029s | 19.1MiB| unsat | 0 | | | |sin-problem-7-chunk-0091.smt2 | 0.029s | 20.728MiB| sat | 0 | | | |ball_count_2d_hill.01.seq_lazy_global_3.smt2 | 0.029s | 19.072MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0016.smt2 | 0.029s | 20.76MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0171.smt2 | 0.029s | 18.98MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0157.smt2 | 0.029s | 20.592MiB| sat | 0 | | | |CMOS-opamp-chunk-0298.smt2 | 0.029s | 20.66MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0048.smt2 | 0.030s | 20.78MiB| sat | 0 | | | |atan-problem-2-chunk-0107.smt2 | 0.030s | 20.808MiB| unsat | 0 | | | |sqrt-problem-13-chunk-0019.smt2 | 0.030s | 20.552MiB| sat | 0 | | | |Chua-1-IL-U-chunk-0038.smt2 | 0.030s | 20.868MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_global_7.smt2 | 0.030s | 19.204MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0522.smt2 | 0.030s | 20.896MiB| sat | 0 | | | |Chua-2-VC2-L-chunk-0029.smt2 | 0.030s | 20.4MiB| sat | 0 | | | |polypaver-bench-exp-3d-chunk-0126.smt2 | 0.030s | 20.848MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0241.smt2 | 0.030s | 20.552MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0728.smt2 | 0.030s | 20.596MiB| sat | 0 | | | |atan-vega-3-chunk-0210.smt2 | 0.030s | 20.76MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0059.smt2 | 0.030s | 20.64MiB| unsat | 0 | | | |atan-vega-3-chunk-0045.smt2 | 0.030s | 20.56MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0146.smt2 | 0.030s | 18.792MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0144.smt2 | 0.030s | 20.936MiB| sat | 0 | | | |exp-problem-10-2-chunk-0214.smt2 | 0.030s | 20.888MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0104.smt2 | 0.030s | 18.976MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0104.smt2 | 0.031s | 20.752MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0196.smt2 | 0.031s | 20.828MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0100.smt2 | 0.031s | 20.764MiB| sat | 0 | | | |atan-vega-3-chunk-0400.smt2 | 0.031s | 20.876MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0070.smt2 | 0.031s | 20.784MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_linear_enc_global_1.smt2 | 0.031s | 19.144MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0504.smt2 | 0.031s | 20.78MiB| sat | 0 | | | |atan-problem-2-chunk-0059.smt2 | 0.031s | 20.604MiB| sat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0075.smt2 | 0.031s | 20.744MiB| sat | 0 | | | |atan-problem-2-chunk-0117.smt2 | 0.031s | 20.62MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0160.smt2 | 0.031s | 20.712MiB| unsat | 0 | | | |atan-problem-1-chunk-0071.smt2 | 0.031s | 20.68MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0024.smt2 | 0.031s | 20.808MiB| unsat | 0 | | | |ArthanKM2-chunk-0002.smt2 | 0.031s | 20.636MiB| sat | 0 | | | |sin-344-3-chunk-0029.smt2 | 0.031s | 20.724MiB| unsat | 0 | | | |MulliganEconomicsModel0018e.smt2 | 0.031s | 20.78MiB| sat | 0 | | | |CONVOI2-chunk-0018.smt2 | 0.031s | 20.84MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0237.smt2 | 0.031s | 20.648MiB| sat | 0 | | | |exp-problem-10-3-chunk-0010.smt2 | 0.031s | 20.728MiB| sat | 0 | | | |ball_count_2d_hill.10.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.031s | 19.556MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0081.smt2 | 0.031s | 20.968MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0224.smt2 | 0.031s | 20.836MiB| sat | 0 | | | |sin-problem-10-2-chunk-0010.smt2 | 0.031s | 20.968MiB| sat | 0 | | | |sin-problem-7-weak2-chunk-0100.smt2 | 0.031s | 20.916MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0107.smt2 | 0.031s | 20.764MiB| unsat | 0 | | | |ball_count_2d_hill.10.seq_lazy_global_3.smt2 | 0.031s | 19.296MiB| unsat | 0 | | | |atan-vega-3-chunk-0463.smt2 | 0.031s | 20.88MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0069.smt2 | 0.031s | 20.916MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0091.smt2 | 0.031s | 20.652MiB| sat | 0 | | | |sin-problem-7-weak2-chunk-0075.smt2 | 0.031s | 20.768MiB| sat | 0 | | | |sin-cos-346-b-chunk-0209.smt2 | 0.032s | 20.928MiB| sat | 0 | | | |sin-cos-346-b-chunk-0434.smt2 | 0.032s | 20.788MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0036.smt2 | 0.032s | 20.748MiB| sat | 0 | | | |exp-problem-10-2-chunk-0134.smt2 | 0.032s | 20.856MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0093.smt2 | 0.032s | 20.664MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0073.smt2 | 0.032s | 20.712MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0378.smt2 | 0.032s | 19.016MiB| unsat | 0 | | | |sqrt-problem-13-vars5-chunk-0026.smt2 | 0.032s | 20.664MiB| sat | 0 | | | |ball_count_2d_slope.05.seq_lazy_lemmas_global_1.smt2 | 0.032s | 19.16MiB| unsat | 0 | | | |atan-vega-3-chunk-0503.smt2 | 0.032s | 20.84MiB| sat | 0 | | | |Chua-2-VC2-L-chunk-0040.smt2 | 0.032s | 20.828MiB| sat | 0 | | | |ball_count_2d_hill_simple.10.qfree_global_9.smt2 | 0.032s | 19.312MiB| unsat | 0 | | | |sin-problem-7-chunk-0257.smt2 | 0.032s | 21.084MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0093.smt2 | 0.032s | 21.016MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0024.smt2 | 0.032s | 20.824MiB| sat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0015.smt2 | 0.032s | 20.708MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0217.smt2 | 0.032s | 20.616MiB| sat | 0 | | | |atan-vega-3-chunk-0139.smt2 | 0.032s | 20.58MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.qfree_global_9.smt2 | 0.032s | 19.496MiB| unsat | 0 | | | |Chua-1-VC2-L-chunk-0077.smt2 | 0.032s | 20.728MiB| sat | 0 | | | |exp-problem-10-3-chunk-0096.smt2 | 0.032s | 20.86MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0415.smt2 | 0.032s | 20.632MiB| sat | 0 | | | |sin-cos-346-b-chunk-0030.smt2 | 0.032s | 20.8MiB| sat | 0 | | | |polypaver-sqrt-circles-1a-chunk-0011.smt2 | 0.032s | 20.848MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0691.smt2 | 0.032s | 20.764MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0510.smt2 | 0.032s | 20.732MiB| unsat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0103.smt2 | 0.032s | 20.78MiB| unsat | 0 | | | |Lyapunov1a-chunk-0011.smt2 | 0.032s | 20.676MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0071.smt2 | 0.032s | 21.008MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0029.smt2 | 0.032s | 20.844MiB| sat | 0 | | | |atan-vega-3-chunk-0280.smt2 | 0.032s | 20.904MiB| sat | 0 | | | |exp-problem-10-2-chunk-0038.smt2 | 0.032s | 20.796MiB| sat | 0 | | | |exp-problem-10-3-chunk-0063.smt2 | 0.032s | 20.688MiB| sat | 0 | | | |CMOS-opamp-chunk-0096.smt2 | 0.032s | 20.508MiB| sat | 0 | | | |sin-problem-7-weak-chunk-0149.smt2 | 0.032s | 20.688MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0218.smt2 | 0.033s | 20.924MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0405.smt2 | 0.033s | 20.876MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0131.smt2 | 0.033s | 20.732MiB| unsat | 0 | | | |ball_count_2d_plain.10.seq_lazy_lemmas_global_1.smt2 | 0.033s | 18.872MiB| unsat | 0 | | | |atan-vega-3-chunk-0543.smt2 | 0.033s | 20.612MiB| sat | 0 | | | |Chua-2-VC2-U-chunk-0066.smt2 | 0.033s | 20.764MiB| unsat | 0 | | | |CMOS-opamp-chunk-0310.smt2 | 0.033s | 20.692MiB| sat | 0 | | | |sin-problem-7-weak2-chunk-0057.smt2 | 0.033s | 20.832MiB| sat | 0 | | | |CMOS-opamp-chunk-0062.smt2 | 0.033s | 20.776MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_linear_enc_global_5.smt2 | 0.033s | 19.076MiB| unsat | 0 | | | |asin-8-vars4-chunk-0034.smt2 | 0.033s | 20.788MiB| sat | 0 | | | |exp-problem-10-2-chunk-0102.smt2 | 0.033s | 20.868MiB| unsat | 0 | | | |sqrt-problem-12vars3-chunk-0039.smt2 | 0.033s | 20.768MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0020.smt2 | 0.033s | 20.876MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0508.smt2 | 0.033s | 20.816MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0042.smt2 | 0.033s | 20.812MiB| sat | 0 | | | |atan-vega-3-chunk-0011.smt2 | 0.033s | 20.76MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_linear_enc_global_1.smt2 | 0.033s | 18.912MiB| unsat | 0 | | | |Chua-1-IL-U-chunk-0025.smt2 | 0.033s | 20.624MiB| sat | 0 | | | |exp-problem-10-3-chunk-0138.smt2 | 0.033s | 20.76MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0036.smt2 | 0.033s | 20.908MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0066.smt2 | 0.033s | 20.836MiB| unsat | 0 | | | |ball_count_1d_plain.01.qfree_global_1.smt2 | 0.033s | 18.976MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0277.smt2 | 0.033s | 21.02MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0080.smt2 | 0.033s | 20.956MiB| sat | 0 | | | |sqrt-problem-12vars3-chunk-0068.smt2 | 0.033s | 20.672MiB| sat | 0 | | | |CMOS-opamp-chunk-0169.smt2 | 0.034s | 20.896MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.034s | 19.516MiB| unsat | 0 | | | |Lyapunov1a-chunk-0021.smt2 | 0.034s | 20.808MiB| sat | 0 | | | |ball_count_1d_plain.03.qfree_global_3.smt2 | 0.034s | 20.908MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0158.smt2 | 0.034s | 20.68MiB| sat | 0 | | | |exp-problem-10-3-chunk-0084.smt2 | 0.034s | 18.912MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0108.smt2 | 0.034s | 20.764MiB| sat | 0 | | | |CMOS-opamp-chunk-0213.smt2 | 0.034s | 20.516MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0479.smt2 | 0.034s | 20.764MiB| sat | 0 | | | |Chua-2-VC1-L-chunk-0052.smt2 | 0.034s | 20.68MiB| sat | 0 | | | |sqrt-problem-Melquiond2-chunk-0045.smt2 | 0.034s | 20.76MiB| unsat | 0 | | | |ball_count_2d_slope.02.seq_lazy_global_3.smt2 | 0.034s | 19.228MiB| unsat | 0 | | | |CMOS-opamp-chunk-0332.smt2 | 0.034s | 20.864MiB| unsat | 0 | | | |ball_count_1d_plain.01.qfree_global_5.smt2 | 0.034s | 19.184MiB| unsat | 0 | | | |atan-vega-3-chunk-0583.smt2 | 0.034s | 21.096MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0190.smt2 | 0.034s | 20.712MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0081.smt2 | 0.034s | 20.676MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0586.smt2 | 0.034s | 20.792MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0029.smt2 | 0.034s | 20.852MiB| sat | 0 | | | |Chua-1-VC2-L-chunk-0050.smt2 | 0.034s | 20.724MiB| unsat | 0 | | | |polypaver-bench-exp-3d-chunk-0028.smt2 | 0.034s | 20.94MiB| sat | 0 | | | |sin-cos-346-b-chunk-0424.smt2 | 0.034s | 20.864MiB| unsat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0086.smt2 | 0.034s | 20.744MiB| sat | 0 | | | |exp-problem-10-2-chunk-0090.smt2 | 0.034s | 20.84MiB| unsat | 0 | | | |ball_count_1d_plain.10.seq_lazy_lemmas_global_11.smt2 | 0.035s | 19.664MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0181.smt2 | 0.035s | 18.692MiB| unsat | 0 | | | |atan-vega-3-chunk-0453.smt2 | 0.035s | 20.972MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0146.smt2 | 0.035s | 20.8MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0102.smt2 | 0.035s | 20.732MiB| sat | 0 | | | |sqrt-problem-Melquiond3-chunk-0018.smt2 | 0.035s | 20.604MiB| sat | 0 | | | |ball_count_2d_plain.02.qfree_global_7.smt2 | 0.035s | 19.364MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0130.smt2 | 0.035s | 20.728MiB| unsat | 0 | | | |atan-vega-3-chunk-0533.smt2 | 0.035s | 20.924MiB| sat | 0 | | | |atan-problem-1-weak-chunk-0035.smt2 | 0.035s | 20.576MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0600.smt2 | 0.035s | 20.996MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0109.smt2 | 0.035s | 20.872MiB| unsat | 0 | | | |CMOS-opamp-chunk-0025.smt2 | 0.035s | 21.0MiB| sat | 0 | | | |Chua-2-VC2-L-chunk-0062.smt2 | 0.035s | 20.756MiB| sat | 0 | | | |Chua-2-VC2-U-chunk-0018.smt2 | 0.035s | 20.952MiB| sat | 0 | | | |ball_count_2d_plain.04.seq_lazy_global_3.smt2 | 0.035s | 21.2MiB| unsat | 0 | | | |atan-vega-3-chunk-0523.smt2 | 0.035s | 20.684MiB| sat | 0 | | | |cbrt-problem-3-chunk-0070.smt2 | 0.035s | 20.796MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0021.smt2 | 0.035s | 18.808MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0115.smt2 | 0.036s | 20.76MiB| sat | 0 | | | |atan-vega-3-chunk-0423.smt2 | 0.036s | 20.804MiB| sat | 0 | | | |ball_count_1d_plain.01.seq_lazy_linear_enc_global_15.smt2 | 0.036s | 19.816MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_linear_enc_global_1.smt2 | 0.036s | 18.868MiB| unsat | 0 | | | |MulliganEconomicsModel0030e.smt2 | 0.036s | 21.112MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0108.smt2 | 0.036s | 20.96MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0154.smt2 | 0.036s | 20.816MiB| unsat | 0 | | | |Chua-1-VC1-U-chunk-0044.smt2 | 0.036s | 20.628MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0116.smt2 | 0.036s | 20.652MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0339.smt2 | 0.036s | 20.676MiB| sat | 0 | | | |sin-problem-10-3-chunk-0033.smt2 | 0.036s | 20.64MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0481.smt2 | 0.036s | 20.78MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0164.smt2 | 0.036s | 20.868MiB| sat | 0 | | | |ball_count_1d_plain.01.seq_lazy_lemmas_global_11.smt2 | 0.036s | 19.568MiB| unsat | 0 | | | |ball_count_2d_hill.02.seq_lazy_global_3.smt2 | 0.036s | 19.136MiB| unsat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0065.smt2 | 0.036s | 20.72MiB| unsat | 0 | | | |sqrt-problem-12vars3-chunk-0081.smt2 | 0.036s | 20.772MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0493.smt2 | 0.036s | 20.716MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0241.smt2 | 0.036s | 20.812MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0572.smt2 | 0.036s | 20.852MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0025.smt2 | 0.036s | 20.752MiB| sat | 0 | | | |ball_count_2d_slope.01.seq_lazy_global_7.smt2 | 0.037s | 19.628MiB| unsat | 0 | | | |Chua-1-IL-U-chunk-0063.smt2 | 0.037s | 20.8MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0050.smt2 | 0.037s | 20.7MiB| unsat | 0 | | | |ball_count_2d_plain.02.seq_lazy_lemmas_global_13.smt2 | 0.037s | 20.028MiB| unsat | 0 | | | |MulliganEconomicsModel0013c.smt2 | 0.037s | 20.672MiB| sat | 0 | | | |atan-vega-3-chunk-0433.smt2 | 0.037s | 20.764MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_global_7.smt2 | 0.037s | 19.888MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0490.smt2 | 0.037s | 20.748MiB| sat | 0 | | | |ball_count_2d_plain.01.seq_lazy_linear_enc_global_13.smt2 | 0.037s | 19.82MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0101.smt2 | 0.037s | 18.716MiB| unsat | 0 | | | |sin-344-4-chunk-0050.smt2 | 0.037s | 21.468MiB| sat | 0 | | | |sin-problem-7-chunk-0129.smt2 | 0.037s | 21.032MiB| unsat | 0 | | | |sin-problem-7-chunk-0311.smt2 | 0.037s | 20.876MiB| sat | 0 | | | |ball_count_2d_plain.02.seq_lazy_linear_enc_lemmas_global_7.smt2 | 0.037s | 19.396MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0168.smt2 | 0.037s | 20.86MiB| sat | 0 | | | |ball_count_2d_plain.10.qfree_global_3.smt2 | 0.037s | 19.204MiB| unsat | 0 | | | |sin-problem-7-chunk-0208.smt2 | 0.037s | 20.836MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0370.smt2 | 0.037s | 20.864MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0143.smt2 | 0.037s | 20.62MiB| unsat | 0 | | | |atan-vega-3-chunk-0310.smt2 | 0.037s | 21.012MiB| sat | 0 | | | |atan-vega-3-chunk-0623.smt2 | 0.037s | 20.936MiB| sat | 0 | | | |Chua-2-VC2-L-chunk-0052.smt2 | 0.037s | 20.732MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0206.smt2 | 0.037s | 20.8MiB| unsat | 0 | | | |ball_count_2d_hill.05.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.037s | 19.012MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0204.smt2 | 0.037s | 20.776MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0168.smt2 | 0.037s | 20.816MiB| sat | 0 | | | |mbo_E6.smt2 | 0.038s | 20.92MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0090.smt2 | 0.038s | 20.812MiB| sat | 0 | | | |ball_count_2d_plain.04.qfree_global_1.smt2 | 0.038s | 18.884MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0414.smt2 | 0.038s | 20.992MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0576.smt2 | 0.038s | 20.64MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0250.smt2 | 0.038s | 20.728MiB| sat | 0 | | | |sin-problem-7-chunk-0221.smt2 | 0.038s | 20.796MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0629.smt2 | 0.038s | 20.968MiB| sat | 0 | | | |sin-problem-7-chunk-0182.smt2 | 0.038s | 20.92MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.038s | 19.228MiB| unsat | 0 | | | |ball_count_2d_plain.01.seq_lazy_global_15.smt2 | 0.038s | 19.728MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0545.smt2 | 0.038s | 20.692MiB| sat | 0 | | | |exp-problem-10-3-chunk-0128.smt2 | 0.038s | 20.768MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0086.smt2 | 0.038s | 20.928MiB| sat | 0 | | | |sin-problem-7-chunk-0156.smt2 | 0.038s | 20.748MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_global_3.smt2 | 0.038s | 20.98MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0098.smt2 | 0.038s | 20.616MiB| sat | 0 | | | |atan-vega-3-chunk-0250.smt2 | 0.038s | 20.768MiB| unsat | 0 | | | |atan-vega-3-chunk-0370.smt2 | 0.038s | 20.772MiB| sat | 0 | | | |exp-problem-10-2-chunk-0285.smt2 | 0.038s | 20.68MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0290.smt2 | 0.038s | 20.684MiB| sat | 0 | | | |ball_count_1d_plain.10.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.038s | 18.916MiB| unsat | 0 | | | |ball_count_1d_plain.01.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.039s | 19.28MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_linear_enc_global_1.smt2 | 0.039s | 18.896MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.redlog_global_7.smt2 | 0.039s | 19.336MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0112.smt2 | 0.039s | 20.7MiB| sat | 0 | | | |exp-problem-10-3-chunk-0168.smt2 | 0.039s | 20.92MiB| sat | 0 | | | |atan-problem-2-weakT-chunk-0030.smt2 | 0.039s | 20.588MiB| unsat | 0 | | | |ball_count_2d_hill.02.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.039s | 18.928MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0154.smt2 | 0.039s | 20.736MiB| sat | 0 | | | |sin-cos-346-b-chunk-0252.smt2 | 0.039s | 20.84MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0039.smt2 | 0.039s | 20.88MiB| sat | 0 | | | |atan-vega-3-chunk-0057.smt2 | 0.039s | 20.72MiB| sat | 0 | | | |Chua-2-VC2-L-chunk-0013.smt2 | 0.039s | 20.824MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0369.smt2 | 0.039s | 20.808MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_lemmas_global_1.smt2 | 0.039s | 19.056MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0024.smt2 | 0.039s | 20.676MiB| sat | 0 | | | |sin-cos-346-b-chunk-0454.smt2 | 0.039s | 20.664MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_linear_enc_global_9.smt2 | 0.039s | 19.328MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_global_7.smt2 | 0.039s | 19.392MiB| unsat | 0 | | | |atan-vega-3-chunk-0553.smt2 | 0.039s | 21.072MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0312.smt2 | 0.039s | 20.748MiB| sat | 0 | | | |sin-problem-7-chunk-0143.smt2 | 0.039s | 20.66MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0363.smt2 | 0.039s | 20.776MiB| sat | 0 | | | |atan-vega-3-chunk-0573.smt2 | 0.039s | 21.04MiB| unsat | 0 | | | |ball_count_1d_plain.05.redlog_global_5.smt2 | 0.040s | 21.0MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_global_7.smt2 | 0.040s | 19.62MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0179.smt2 | 0.040s | 20.916MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_global_11.smt2 | 0.040s | 19.624MiB| unsat | 0 | | | |atan-vega-3-chunk-0390.smt2 | 0.040s | 20.768MiB| sat | 0 | | | |sin-cos-346-b-chunk-0272.smt2 | 0.040s | 20.748MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0056.smt2 | 0.040s | 21.036MiB| sat | 0 | | | |exp-problem-10-2-chunk-0265.smt2 | 0.040s | 20.732MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0067.smt2 | 0.040s | 20.808MiB| sat | 0 | | | |ball_count_2d_plain.10.redlog_global_11.smt2 | 0.040s | 19.94MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0444.smt2 | 0.040s | 20.672MiB| sat | 0 | | | |polypaver-bench-exp-3d-chunk-0085.smt2 | 0.040s | 21.024MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0100.smt2 | 0.040s | 20.628MiB| sat | 0 | | | |atan-vega-3-chunk-0483.smt2 | 0.040s | 20.852MiB| sat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.040s | 18.868MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0053.smt2 | 0.040s | 20.764MiB| sat | 0 | | | |ArthanM2-chunk-0012.smt2 | 0.040s | 18.712MiB| unsat | 0 | | | |CMOS-opamp-chunk-0137.smt2 | 0.040s | 20.668MiB| sat | 0 | | | |exp-problem-10-3-chunk-0188.smt2 | 0.040s | 20.768MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_global_3.smt2 | 0.040s | 21.236MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0464.smt2 | 0.040s | 20.804MiB| unsat | 0 | | | |atan-problem-2-chunk-0011.smt2 | 0.041s | 20.636MiB| sat | 0 | | | |ball_count_2d_hill_simple.03.qfree_global_7.smt2 | 0.041s | 21.072MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0073.smt2 | 0.041s | 20.764MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0120.smt2 | 0.041s | 20.728MiB| unsat | 0 | | | |ball_count_2d_plain.10.seq_lazy_linear_enc_global_9.smt2 | 0.041s | 19.432MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0306.smt2 | 0.041s | 20.644MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0143.smt2 | 0.041s | 21.216MiB| sat | 0 | | | |CONVOI2-chunk-0031.smt2 | 0.041s | 20.816MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0222.smt2 | 0.041s | 20.856MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0078.smt2 | 0.041s | 20.764MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0111.smt2 | 0.041s | 20.852MiB| unsat | 0 | | | |atan-vega-3-chunk-0129.smt2 | 0.042s | 20.596MiB| sat | 0 | | | |sin-cos-346-b-chunk-0126.smt2 | 0.042s | 20.764MiB| sat | 0 | | | |sin-problem-8-weak-chunk-0068.smt2 | 0.042s | 20.96MiB| sat | 0 | | | |asin-8-chunk-0024.smt2 | 0.042s | 20.792MiB| sat | 0 | | | |sin-344-3-weak-chunk-0017.smt2 | 0.042s | 20.824MiB| sat | 0 | | | |MulliganEconomicsModel0063e.smt2 | 0.042s | 20.64MiB| sat | 0 | | | |etcs_braking_2.01.seq_lazy_lemmas_global_1.smt2 | 0.042s | 21.148MiB| unsat | 0 | | | |sin-problem-8-chunk-0043.smt2 | 0.042s | 20.764MiB| sat | 0 | | | |cos-problem-5-chunk-0023.smt2 | 0.042s | 20.64MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0390.smt2 | 0.042s | 20.688MiB| sat | 0 | | | |ball_count_1d_plain.02.qfree_global_9.smt2 | 0.042s | 19.504MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_linear_enc_global_13.smt2 | 0.042s | 19.748MiB| unsat | 0 | | | |cbrt-problem-3-weak-chunk-0023.smt2 | 0.042s | 20.824MiB| sat | 0 | | | |ball_count_1d_plain.02.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.042s | 19.492MiB| unsat | 0 | | | |atan-vega-3-chunk-0360.smt2 | 0.042s | 20.824MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.redlog_global_11.smt2 | 0.042s | 19.784MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0097.smt2 | 0.042s | 20.764MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0084.smt2 | 0.042s | 20.676MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0296.smt2 | 0.042s | 18.756MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0278.smt2 | 0.043s | 20.604MiB| sat | 0 | | | |exp-problem-10-2-chunk-0016.smt2 | 0.043s | 20.596MiB| sat | 0 | | | |MulliganEconomicsModel0006a.smt2 | 0.043s | 20.588MiB| sat | 0 | | | |sin-problem-8-chunk-0054.smt2 | 0.043s | 20.66MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0087.smt2 | 0.043s | 20.84MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0137.smt2 | 0.043s | 20.632MiB| unsat | 0 | | | |asin-8-vars4-chunk-0019.smt2 | 0.043s | 20.8MiB| sat | 0 | | | |sin-cos-346-b-chunk-0474.smt2 | 0.043s | 20.824MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0028.smt2 | 0.043s | 20.74MiB| sat | 0 | | | |hong_2.smt2 | 0.043s | 20.636MiB| unsat | 0 | | | |Chua-2-VC1-U-chunk-0045.smt2 | 0.043s | 18.78MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0519.smt2 | 0.043s | 20.736MiB| sat | 0 | | | |atan-problem-2-weakT-chunk-0041.smt2 | 0.043s | 20.936MiB| sat | 0 | | | |exp-problem-10-2-chunk-0346.smt2 | 0.043s | 20.76MiB| unsat | 0 | | | |ball_count_1d_plain.10.redlog_global_13.smt2 | 0.043s | 19.72MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0139.smt2 | 0.043s | 20.884MiB| sat | 0 | | | |sin-problem-7-chunk-0273.smt2 | 0.043s | 20.936MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0167.smt2 | 0.044s | 20.964MiB| sat | 0 | | | |ball_count_1d_plain.10.seq_lazy_linear_enc_global_15.smt2 | 0.044s | 19.752MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0700.smt2 | 0.044s | 20.888MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0316.smt2 | 0.044s | 18.964MiB| unsat | 0 | | | |ball_count_1d_plain.10.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.044s | 19.168MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0023.smt2 | 0.044s | 20.824MiB| sat | 0 | | | |ball_count_1d_plain.01.redlog_global_13.smt2 | 0.044s | 19.872MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0068.smt2 | 0.044s | 18.908MiB| unsat | 0 | | | |ball_count_2d_hill.01.seq_lazy_lemmas_global_11.smt2 | 0.044s | 20.18MiB| unsat | 0 | | | |matrix-1-all-8.smt2 | 0.044s | 20.908MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0374.smt2 | 0.044s | 21.352MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0596.smt2 | 0.044s | 20.728MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0265.smt2 | 0.044s | 18.952MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0111.smt2 | 0.044s | 20.892MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0093.smt2 | 0.044s | 20.88MiB| sat | 0 | | | |asin-8-vars4-chunk-0046.smt2 | 0.044s | 20.86MiB| unsat | 0 | | | |polypaver-bench-exp-3d-chunk-0072.smt2 | 0.044s | 20.816MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0701.smt2 | 0.044s | 18.712MiB| unsat | 0 | | | |asin-8-chunk-0039.smt2 | 0.044s | 20.784MiB| sat | 0 | | | |MulliganEconomicsModel0024a.smt2 | 0.044s | 20.66MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0070.smt2 | 0.044s | 20.696MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0305.smt2 | 0.044s | 20.696MiB| sat | 0 | | | |sin-cos-346-b-chunk-0401.smt2 | 0.044s | 20.668MiB| sat | 0 | | | |ball_count_2d_slope.04.seq_lazy_global_1.smt2 | 0.045s | 18.976MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0657.smt2 | 0.045s | 20.584MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0026.smt2 | 0.045s | 20.828MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_global_11.smt2 | 0.045s | 19.508MiB| unsat | 0 | | | |Chua-1-VC1-U-chunk-0032.smt2 | 0.045s | 20.68MiB| sat | 0 | | | |ball_count_1d_plain.01.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.045s | 19.056MiB| unsat | 0 | | | |ball_count_1d_plain.03.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.045s | 20.884MiB| unsat | 0 | | | |ball_count_2d_hill.02.seq_lazy_lemmas_global_11.smt2 | 0.045s | 20.248MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0174.smt2 | 0.045s | 20.728MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0421.smt2 | 0.045s | 20.908MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0021.smt2 | 0.045s | 20.56MiB| sat | 0 | | | |atan-problem-1-chunk-0006.smt2 | 0.045s | 20.488MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0556.smt2 | 0.045s | 20.756MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0075.smt2 | 0.045s | 20.796MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0330.smt2 | 0.045s | 20.928MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0057.smt2 | 0.045s | 20.668MiB| sat | 0 | | | |ball_count_1d_plain.10.qfree_global_5.smt2 | 0.045s | 19.208MiB| unsat | 0 | | | |sqrt-problem-12vars3-chunk-0025.smt2 | 0.045s | 20.804MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_lemmas_global_15.smt2 | 0.045s | 19.952MiB| unsat | 0 | | | |CMOS-opamp-chunk-0148.smt2 | 0.045s | 20.916MiB| sat | 0 | | | |sin-problem-8-weak-chunk-0027.smt2 | 0.045s | 20.616MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0480.smt2 | 0.045s | 20.872MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0059.smt2 | 0.045s | 20.832MiB| sat | 0 | | | |atan-problem-2-chunk-0070.smt2 | 0.045s | 20.884MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0607.smt2 | 0.045s | 20.884MiB| unsat | 0 | | | |atan-vega-3-chunk-0413.smt2 | 0.046s | 20.772MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0093.smt2 | 0.046s | 20.76MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0230.smt2 | 0.046s | 20.844MiB| sat | 0 | | | |sqrt-problem-12vars3-chunk-0010.smt2 | 0.046s | 20.604MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0087.smt2 | 0.046s | 20.82MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0231.smt2 | 0.046s | 18.844MiB| unsat | 0 | | | |atan-vega-3-chunk-0513.smt2 | 0.046s | 20.776MiB| sat | 0 | | | |Arthan1A-chunk-0020.smt2 | 0.046s | 20.56MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0136.smt2 | 0.046s | 20.888MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0456.smt2 | 0.046s | 18.884MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0307.smt2 | 0.046s | 20.716MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0288.smt2 | 0.046s | 20.748MiB| unsat | 0 | | | |ball_count_2d_hill.02.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.046s | 19.32MiB| unsat | 0 | | | |ball_count_2d_plain.04.seq_lazy_lemmas_global_7.smt2 | 0.046s | 21.564MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.046s | 19.852MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0320.smt2 | 0.046s | 20.98MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0577.smt2 | 0.046s | 21.144MiB| sat | 0 | | | |ball_count_2d_hill.04.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.046s | 19.156MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0255.smt2 | 0.046s | 20.784MiB| sat | 0 | | | |atan-problem-1-chunk-0058.smt2 | 0.046s | 20.684MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.046s | 20.128MiB| unsat | 0 | | | |sin-problem-7-chunk-0192.smt2 | 0.046s | 20.752MiB| sat | 0 | | | |Chua-2-VC1-L-chunk-0119.smt2 | 0.046s | 20.768MiB| sat | 0 | | | |ball_count_1d_plain.05.seq_lazy_lemmas_global_3.smt2 | 0.046s | 20.996MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_linear_enc_global_7.smt2 | 0.046s | 21.276MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0101.smt2 | 0.046s | 20.8MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0113.smt2 | 0.046s | 20.6MiB| sat | 0 | | | |exp-problem-10-2-chunk-0385.smt2 | 0.046s | 20.864MiB| unsat | 0 | | | |ball_count_1d_plain.05.redlog_global_1.smt2 | 0.046s | 18.844MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0242.smt2 | 0.046s | 20.82MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0711.smt2 | 0.047s | 20.776MiB| sat | 0 | | | |sin-problem-7-weak-chunk-0085.smt2 | 0.047s | 20.416MiB| sat | 0 | | | |ball_count_2d_plain.01.redlog_global_11.smt2 | 0.047s | 19.888MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0198.smt2 | 0.047s | 20.872MiB| sat | 0 | | | |atan-problem-2-chunk-0047.smt2 | 0.047s | 20.768MiB| unsat | 0 | | | |ball_count_1d_plain.01.redlog_global_9.smt2 | 0.047s | 19.416MiB| unsat | 0 | | | |atan-vega-3-chunk-0633.smt2 | 0.047s | 21.132MiB| sat | 0 | | | |atan-vega-3-chunk-0169.smt2 | 0.047s | 20.876MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0173.smt2 | 0.047s | 20.76MiB| unsat | 0 | | | |CMOS-opamp-chunk-0246.smt2 | 0.047s | 20.784MiB| unsat | 0 | | | |atan-problem-1-chunk-0047.smt2 | 0.047s | 20.812MiB| sat | 0 | | | |ball_count_2d_hill_simple.03.qfree_global_11.smt2 | 0.047s | 21.648MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0118.smt2 | 0.047s | 20.736MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0202.smt2 | 0.047s | 20.944MiB| sat | 0 | | | |ball_count_2d_plain.02.seq_lazy_linear_enc_lemmas_global_11.smt2 | 0.047s | 19.748MiB| unsat | 0 | | | |bottom-plate-mixer-chunk-0039.smt2 | 0.047s | 20.412MiB| sat | 0 | | | |ball_count_2d_slope.02.seq_lazy_lemmas_global_7.smt2 | 0.047s | 20.304MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0008.smt2 | 0.047s | 20.728MiB| unsat | 0 | | | |ball_count_2d_plain.10.seq_lazy_global_15.smt2 | 0.047s | 19.916MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0496.smt2 | 0.047s | 20.644MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0344.smt2 | 0.047s | 20.844MiB| sat | 0 | | | |ball_count_2d_plain.04.qfree_global_5.smt2 | 0.048s | 21.188MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0295.smt2 | 0.048s | 20.88MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0301.smt2 | 0.048s | 20.624MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0072.smt2 | 0.048s | 18.84MiB| unsat | 0 | | | |gen-09.smt2 | 0.048s | 20.7MiB| sat | 0 | | | |atan-vega-3-chunk-0330.smt2 | 0.048s | 20.76MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0223.smt2 | 0.048s | 21.1MiB| sat | 0 | | | |matrix-1-all-10.smt2 | 0.048s | 20.728MiB| sat | 0 | | | |atan-vega-3-chunk-0159.smt2 | 0.048s | 20.592MiB| sat | 0 | | | |ball_count_2d_plain.03.seq_lazy_global_9.smt2 | 0.048s | 21.372MiB| unsat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0086.smt2 | 0.048s | 20.9MiB| sat | 0 | | | |sin-cos-346-b-chunk-0262.smt2 | 0.048s | 21.02MiB| sat | 0 | | | |ball_count_2d_plain.02.seq_lazy_global_5.smt2 | 0.048s | 19.296MiB| unsat | 0 | | | |cos-problem-5-chunk-0039.smt2 | 0.048s | 20.744MiB| sat | 0 | | | |atan-vega-3-chunk-0199.smt2 | 0.049s | 20.924MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0227.smt2 | 0.049s | 20.96MiB| sat | 0 | | | |exp-problem-10-2-chunk-0059.smt2 | 0.049s | 18.84MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.redlog_global_5.smt2 | 0.049s | 21.428MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0444.smt2 | 0.049s | 20.704MiB| sat | 0 | | | |sin-problem-7-weak-chunk-0126.smt2 | 0.049s | 20.668MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0082.smt2 | 0.049s | 20.604MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0155.smt2 | 0.049s | 20.852MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0494.smt2 | 0.049s | 20.832MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.049s | 19.948MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0053.smt2 | 0.049s | 20.704MiB| sat | 0 | | | |sin-problem-7-chunk-0105.smt2 | 0.049s | 20.812MiB| unsat | 0 | | | |sin-problem-8-weak-chunk-0056.smt2 | 0.049s | 20.656MiB| unsat | 0 | | | |ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.049s | 19.36MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0409.smt2 | 0.049s | 20.7MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0126.smt2 | 0.049s | 20.988MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0183.smt2 | 0.049s | 20.732MiB| sat | 0 | | | |CMOS-opamp-chunk-0086.smt2 | 0.049s | 20.908MiB| sat | 0 | | | |atan-problem-1-weak-chunk-0020.smt2 | 0.049s | 20.888MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0161.smt2 | 0.050s | 20.764MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0094.smt2 | 0.050s | 20.972MiB| sat | 0 | | | |ball_count_2d_plain.01.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.050s | 19.412MiB| unsat | 0 | | | |ball_count_2d_slope.02.seq_lazy_lemmas_global_11.smt2 | 0.050s | 20.692MiB| unsat | 0 | | | |atan-problem-2-weakT-chunk-0054.smt2 | 0.050s | 20.824MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0032.smt2 | 0.050s | 20.78MiB| sat | 0 | | | |ball_count_2d_slope.04.seq_lazy_linear_enc_lemmas_global_7.smt2 | 0.050s | 19.896MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.qfree_global_1.smt2 | 0.050s | 19.016MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0597.smt2 | 0.050s | 20.94MiB| sat | 0 | | | |ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.050s | 18.98MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0425.smt2 | 0.050s | 20.676MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0085.smt2 | 0.050s | 20.656MiB| sat | 0 | | | |CMOS-opamp-chunk-0190.smt2 | 0.050s | 20.812MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0567.smt2 | 0.050s | 20.804MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0077.smt2 | 0.050s | 20.792MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0123.smt2 | 0.050s | 20.74MiB| unsat | 0 | | | |CMOS-opamp-chunk-0047.smt2 | 0.050s | 20.856MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0014.smt2 | 0.050s | 20.872MiB| sat | 0 | | | |atan-vega-3-chunk-0077.smt2 | 0.050s | 20.736MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0469.smt2 | 0.050s | 20.672MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0334.smt2 | 0.051s | 21.292MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0087.smt2 | 0.051s | 21.068MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_global_11.smt2 | 0.051s | 20.356MiB| unsat | 0 | | | |ball_count_2d_plain.02.seq_lazy_linear_enc_global_3.smt2 | 0.051s | 19.32MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0073.smt2 | 0.051s | 18.756MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0051.smt2 | 0.051s | 20.764MiB| sat | 0 | | | |Chua-1-IL-L-chunk-0054.smt2 | 0.051s | 18.832MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0338.smt2 | 0.051s | 20.696MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0110.smt2 | 0.051s | 20.764MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0189.smt2 | 0.051s | 21.02MiB| unsat | 0 | | | |atan-vega-3-chunk-0240.smt2 | 0.051s | 20.664MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0040.smt2 | 0.051s | 20.512MiB| unsat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0032.smt2 | 0.051s | 20.78MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0194.smt2 | 0.051s | 20.7MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0032.smt2 | 0.051s | 20.764MiB| sat | 0 | | | |cbrt-problem-3-chunk-0055.smt2 | 0.051s | 20.78MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0046.smt2 | 0.051s | 20.768MiB| sat | 0 | | | |exp-problem-10-2-chunk-0335.smt2 | 0.052s | 20.9MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0224.smt2 | 0.052s | 20.9MiB| unsat | 0 | | | |CMOS-opamp-chunk-0122.smt2 | 0.052s | 20.76MiB| sat | 0 | | | |exp-problem-10-2-chunk-0069.smt2 | 0.052s | 18.956MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0127.smt2 | 0.052s | 21.024MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0053.smt2 | 0.052s | 20.756MiB| sat | 0 | | | |ball_count_2d_plain.03.seq_lazy_linear_enc_global_7.smt2 | 0.052s | 21.372MiB| unsat | 0 | | | |CMOS-opamp-chunk-0200.smt2 | 0.052s | 20.852MiB| sat | 0 | | | |ball_count_1d_plain.02.qfree_global_13.smt2 | 0.052s | 19.62MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0232.smt2 | 0.052s | 20.972MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0352.smt2 | 0.052s | 20.844MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0027.smt2 | 0.052s | 20.768MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0043.smt2 | 0.052s | 20.704MiB| sat | 0 | | | |asin-8-chunk-0053.smt2 | 0.052s | 20.768MiB| sat | 0 | | | |ball_count_1d_plain.04.seq_lazy_linear_enc_global_3.smt2 | 0.052s | 20.868MiB| unsat | 0 | | | |ball_count_2d_hill.10.seq_lazy_lemmas_global_7.smt2 | 0.052s | 19.9MiB| unsat | 0 | | | |ball_count_2d_hill.02.redlog_global_9.smt2 | 0.052s | 20.608MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0549.smt2 | 0.053s | 21.016MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0619.smt2 | 0.053s | 20.704MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0035.smt2 | 0.053s | 20.488MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0328.smt2 | 0.053s | 20.824MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0541.smt2 | 0.053s | 20.736MiB| sat | 0 | | | |exp-problem-10-2-chunk-0325.smt2 | 0.053s | 21.032MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0212.smt2 | 0.053s | 20.884MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0671.smt2 | 0.053s | 21.292MiB| sat | 0 | | | |MulliganEconomicsModel0085a.smt2 | 0.053s | 20.888MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0380.smt2 | 0.053s | 20.832MiB| sat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0050.smt2 | 0.053s | 21.068MiB| sat | 0 | | | |sin-problem-10-2-chunk-0034.smt2 | 0.053s | 18.788MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0218.smt2 | 0.053s | 20.888MiB| unsat | 0 | | | |atan-vega-3-chunk-0067.smt2 | 0.053s | 20.696MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_linear_enc_global_5.smt2 | 0.053s | 19.488MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_global_11.smt2 | 0.053s | 20.308MiB| unsat | 0 | | | |Chua-1-VC2-L-chunk-0039.smt2 | 0.053s | 20.668MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0216.smt2 | 0.053s | 21.032MiB| sat | 0 | | | |matrix-1-all-47.smt2 | 0.053s | 20.7MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.redlog_global_3.smt2 | 0.053s | 18.988MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_linear_enc_global_5.smt2 | 0.053s | 21.06MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0106.smt2 | 0.053s | 21.168MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0323.smt2 | 0.053s | 20.92MiB| sat | 0 | | | |sqrt-problem-Melquiond2-chunk-0034.smt2 | 0.053s | 20.58MiB| sat | 0 | | | |atan-vega-3-chunk-0563.smt2 | 0.053s | 20.9MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0191.smt2 | 0.054s | 20.76MiB| sat | 0 | | | |atan-vega-3-chunk-0603.smt2 | 0.054s | 20.812MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0047.smt2 | 0.054s | 18.784MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0018.smt2 | 0.054s | 20.812MiB| sat | 0 | | | |ball_count_2d_plain.03.redlog_global_1.smt2 | 0.054s | 19.044MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0714.smt2 | 0.054s | 20.48MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_lemmas_global_3.smt2 | 0.054s | 21.088MiB| unsat | 0 | | | |atan-vega-3-chunk-0270.smt2 | 0.054s | 21.008MiB| sat | 0 | | | |sqrt-circles-3-chunk-0016.smt2 | 0.054s | 20.78MiB| sat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0034.smt2 | 0.054s | 20.672MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0054.smt2 | 0.054s | 20.676MiB| sat | 0 | | | |CMOS-opamp-chunk-0275.smt2 | 0.054s | 20.664MiB| sat | 0 | | | |sqrt-problem-Melquiond2-chunk-0091.smt2 | 0.054s | 20.852MiB| unsat | 0 | | | |polypaver-bench-exp-3d-chunk-0109.smt2 | 0.054s | 20.756MiB| unsat | 0 | | | |atan-problem-1-chunk-0091.smt2 | 0.054s | 20.62MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0124.smt2 | 0.055s | 20.784MiB| sat | 0 | | | |atan-problem-2-chunk-0037.smt2 | 0.055s | 20.648MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.055s | 19.112MiB| unsat | 0 | | | |ball_count_1d_plain.10.seq_lazy_global_3.smt2 | 0.055s | 19.148MiB| unsat | 0 | | | |Lyapunov1a-chunk-0042.smt2 | 0.055s | 20.944MiB| sat | 0 | | | |atan-vega-3-chunk-0380.smt2 | 0.055s | 20.908MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0189.smt2 | 0.055s | 20.72MiB| sat | 0 | | | |ball_count_1d_plain.05.seq_lazy_linear_enc_global_7.smt2 | 0.055s | 21.176MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0484.smt2 | 0.055s | 21.22MiB| sat | 0 | | | |exp-problem-10-2-chunk-0048.smt2 | 0.056s | 20.752MiB| sat | 0 | | | |ball_count_2d_plain.01.seq_lazy_linear_enc_global_9.smt2 | 0.056s | 19.372MiB| unsat | 0 | | | |sin-344-3-chunk-0046.smt2 | 0.056s | 20.912MiB| sat | 0 | | | |sin-cos-346-b-chunk-0326.smt2 | 0.056s | 20.704MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.056s | 20.464MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0186.smt2 | 0.056s | 20.696MiB| sat | 0 | | | |CONVOI2-chunk-0041.smt2 | 0.056s | 20.812MiB| unsat | 0 | | | |ball_count_2d_plain.10.seq_lazy_lemmas_global_5.smt2 | 0.056s | 19.332MiB| unsat | 0 | | | |ball_count_1d_plain.01.seq_lazy_lemmas_global_7.smt2 | 0.056s | 19.512MiB| unsat | 0 | | | |atan-vega-3-chunk-0290.smt2 | 0.056s | 20.748MiB| sat | 0 | | | |atan-problem-2-weakT-chunk-0019.smt2 | 0.056s | 20.632MiB| sat | 0 | | | |atan-vega-3-chunk-0320.smt2 | 0.056s | 20.72MiB| sat | 0 | | | |Chua-1-VC1-U-chunk-0056.smt2 | 0.056s | 20.636MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0162.smt2 | 0.056s | 20.816MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0255.smt2 | 0.057s | 20.776MiB| sat | 0 | | | |MulliganEconomicsModel0054a.smt2 | 0.057s | 20.788MiB| sat | 0 | | | |sqrt-problem-12vars3-chunk-0097.smt2 | 0.057s | 21.196MiB| sat | 0 | | | |ball_count_2d_plain.10.redlog_global_7.smt2 | 0.057s | 19.66MiB| unsat | 0 | | | |sin-344-4-chunk-0032.smt2 | 0.057s | 20.764MiB| sat | 0 | | | |ball_count_1d_plain.01.seq_lazy_global_3.smt2 | 0.057s | 19.176MiB| unsat | 0 | | | |ball_count_1d_plain.03.redlog_global_7.smt2 | 0.057s | 21.208MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.qfree_global_3.smt2 | 0.057s | 18.972MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0074.smt2 | 0.057s | 20.836MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0134.smt2 | 0.057s | 20.792MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_linear_enc_global_3.smt2 | 0.057s | 20.956MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0062.smt2 | 0.057s | 20.872MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0566.smt2 | 0.057s | 20.764MiB| sat | 0 | | | |atan-vega-3-chunk-0350.smt2 | 0.057s | 18.952MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0054.smt2 | 0.057s | 18.748MiB| unsat | 0 | | | |ball_count_1d_plain.10.seq_lazy_lemmas_global_7.smt2 | 0.057s | 19.432MiB| unsat | 0 | | | |exp-361-neg-6-e-chunk-0216.smt2 | 0.057s | 20.824MiB| sat | 0 | | | |sin-problem-7-chunk-0079.smt2 | 0.058s | 20.852MiB| sat | 0 | | | |ball_count_2d_hill.10.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.058s | 19.048MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0349.smt2 | 0.058s | 21.004MiB| sat | 0 | | | |atan-vega-3-chunk-0189.smt2 | 0.058s | 20.768MiB| sat | 0 | | | |ball_count_2d_plain.05.seq_lazy_global_11.smt2 | 0.058s | 21.792MiB| unsat | 0 | | | |ball_count_2d_plain.05.redlog_global_3.smt2 | 0.058s | 21.344MiB| unsat | 0 | | | |ball_count_2d_hill.01.seq_lazy_linear_enc_global_15.smt2 | 0.058s | 20.212MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0534.smt2 | 0.058s | 18.98MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0121.smt2 | 0.058s | 20.764MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0132.smt2 | 0.058s | 20.732MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0061.smt2 | 0.058s | 20.652MiB| sat | 0 | | | |Chua-1-IL-L-chunk-0078.smt2 | 0.058s | 20.624MiB| sat | 0 | | | |sin-cos-346-b-chunk-0631.smt2 | 0.058s | 20.804MiB| sat | 0 | | | |ball_count_1d_plain.04.seq_lazy_linear_enc_lemmas_global_7.smt2 | 0.059s | 21.204MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0138.smt2 | 0.059s | 20.736MiB| sat | 0 | | | |atan-vega-3-chunk-0179.smt2 | 0.059s | 20.576MiB| sat | 0 | | | |exp-problem-10-3-chunk-0148.smt2 | 0.059s | 20.728MiB| unsat | 0 | | | |ball_count_2d_hill.10.seq_lazy_lemmas_global_11.smt2 | 0.059s | 20.404MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_global_11.smt2 | 0.059s | 19.448MiB| unsat | 0 | | | |cos-3410-b-chunk-0027.smt2 | 0.059s | 20.656MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0299.smt2 | 0.059s | 20.644MiB| sat | 0 | | | |ball_count_2d_hill.10.redlog_global_9.smt2 | 0.059s | 20.652MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0536.smt2 | 0.059s | 20.812MiB| sat | 0 | | | |sqrt-problem-12vars3-chunk-0055.smt2 | 0.060s | 20.688MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0469.smt2 | 0.060s | 20.86MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0041.smt2 | 0.060s | 20.78MiB| unsat | 0 | | | |atan-problem-1-chunk-0081.smt2 | 0.060s | 20.916MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0019.smt2 | 0.060s | 20.768MiB| sat | 0 | | | |sin-problem-7-weak2-chunk-0088.smt2 | 0.060s | 18.972MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0120.smt2 | 0.060s | 20.716MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0155.smt2 | 0.060s | 21.06MiB| sat | 0 | | | |atan-vega-3-chunk-0089.smt2 | 0.061s | 20.76MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0117.smt2 | 0.061s | 20.768MiB| unsat | 0 | | | |ball_count_2d_plain.05.qfree_global_9.smt2 | 0.061s | 21.648MiB| unsat | 0 | | | |ball_count_1d_plain.04.seq_lazy_global_1.smt2 | 0.061s | 18.976MiB| unsat | 0 | | | |sin-problem-10-3-chunk-0023.smt2 | 0.061s | 20.692MiB| unsat | 0 | | | |ball_count_2d_hill.02.seq_lazy_lemmas_global_7.smt2 | 0.061s | 19.696MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0206.smt2 | 0.061s | 20.952MiB| sat | 0 | | | |sin-problem-8-chunk-0026.smt2 | 0.061s | 20.628MiB| unsat | 0 | | | |ball_count_2d_plain.04.seq_lazy_linear_enc_global_15.smt2 | 0.061s | 22.032MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0639.smt2 | 0.061s | 20.688MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0097.smt2 | 0.062s | 20.764MiB| unsat | 0 | | | |Chua-2-IL-L-chunk-0005.smt2 | 0.062s | 20.668MiB| sat | 0 | | | |ball_count_2d_plain.04.seq_lazy_lemmas_global_11.smt2 | 0.062s | 22.276MiB| unsat | 0 | | | |CMOS-opamp-chunk-0108.smt2 | 0.062s | 21.064MiB| sat | 0 | | | |mbo_E21E27.smt2 | 0.062s | 20.82MiB| unsat | 0 | | | |Chua-1-VC1-U-chunk-0072.smt2 | 0.062s | 20.856MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0359.smt2 | 0.062s | 20.808MiB| unsat | 0 | | | |ball_count_1d_plain.10.qfree_global_1.smt2 | 0.062s | 18.972MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0039.smt2 | 0.063s | 20.856MiB| unsat | 0 | | | |matrix-1-all-29.smt2 | 0.063s | 20.772MiB| sat | 0 | | | |ball_count_2d_plain.05.seq_lazy_lemmas_global_15.smt2 | 0.063s | 22.596MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0158.smt2 | 0.063s | 20.628MiB| unsat | 0 | | | |atan-vega-3-chunk-0260.smt2 | 0.063s | 20.832MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0070.smt2 | 0.063s | 20.72MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_global_15.smt2 | 0.063s | 19.816MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0107.smt2 | 0.063s | 20.936MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_lemmas_global_15.smt2 | 0.063s | 21.648MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0230.smt2 | 0.063s | 21.276MiB| unsat | 0 | | | |sin-problem-7-chunk-0283.smt2 | 0.063s | 21.02MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0193.smt2 | 0.063s | 20.772MiB| unsat | 0 | | | |sin-problem-7-chunk-0348.smt2 | 0.063s | 20.956MiB| sat | 0 | | | |atan-problem-1-chunk-0102.smt2 | 0.063s | 20.772MiB| unsat | 0 | | | |atan-vega-3-chunk-0593.smt2 | 0.064s | 20.8MiB| unsat | 0 | | | |ball_count_2d_plain.02.seq_lazy_lemmas_global_9.smt2 | 0.064s | 19.696MiB| unsat | 0 | | | |ball_count_2d_plain.01.redlog_global_7.smt2 | 0.064s | 19.708MiB| unsat | 0 | | | |polypaver-sqrt43-int-4vars-chunk-0026.smt2 | 0.064s | 20.624MiB| sat | 0 | | | |ball_count_2d_plain.03.redlog_global_5.smt2 | 0.064s | 21.328MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0681.smt2 | 0.064s | 20.86MiB| unsat | 0 | | | |ball_count_2d_slope.04.seq_lazy_linear_enc_lemmas_global_11.smt2 | 0.064s | 20.308MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0132.smt2 | 0.064s | 20.784MiB| sat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0080.smt2 | 0.064s | 20.96MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.qfree_global_13.smt2 | 0.064s | 19.72MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0136.smt2 | 0.065s | 20.72MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0037.smt2 | 0.065s | 20.76MiB| sat | 0 | | | |ball_count_2d_plain.03.seq_lazy_lemmas_global_3.smt2 | 0.065s | 20.928MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0121.smt2 | 0.065s | 20.512MiB| unsat | 0 | | | |ball_count_2d_plain.10.seq_lazy_linear_enc_global_13.smt2 | 0.065s | 19.764MiB| unsat | 0 | | | |ball_count_2d_plain.02.redlog_global_15.smt2 | 0.065s | 20.24MiB| unsat | 0 | | | |ball_count_2d_plain.03.seq_lazy_global_13.smt2 | 0.065s | 21.756MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.065s | 19.9MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0433.smt2 | 0.065s | 20.912MiB| sat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_global_13.smt2 | 0.066s | 21.828MiB| unsat | 0 | | | |ball_count_2d_slope.02.seq_lazy_linear_enc_global_15.smt2 | 0.066s | 20.344MiB| unsat | 0 | | | |ball_count_2d_hill.10.redlog_global_13.smt2 | 0.066s | 21.116MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0342.smt2 | 0.066s | 20.872MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.qfree_global_5.smt2 | 0.066s | 21.16MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_lemmas_global_15.smt2 | 0.066s | 20.28MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_global_9.smt2 | 0.067s | 21.764MiB| unsat | 0 | | | |cbrt-problem-3-chunk-0028.smt2 | 0.067s | 20.772MiB| unsat | 0 | | | |ball_count_2d_slope.05.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.067s | 19.432MiB| unsat | 0 | | | |ball_count_1d_plain.03.seq_lazy_lemmas_global_5.smt2 | 0.067s | 21.204MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0275.smt2 | 0.067s | 20.612MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0245.smt2 | 0.067s | 20.748MiB| unsat | 0 | | | |simple_ballistics_reach.01.seq_lazy_linear_enc_global_1.smt2 | 0.067s | 21.0MiB| unsat | 0 | | | |ball_count_2d_hill.04.seq_lazy_global_3.smt2 | 0.067s | 21.324MiB| unsat | 0 | | | |CMOS-opamp-chunk-0260.smt2 | 0.067s | 18.884MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_linear_enc_global_11.smt2 | 0.067s | 21.664MiB| unsat | 0 | | | |ball_count_2d_slope.02.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.067s | 19.732MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0633.smt2 | 0.067s | 20.836MiB| sat | 0 | | | |ball_count_2d_hill_simple.05.redlog_global_9.smt2 | 0.067s | 21.612MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_global_7.smt2 | 0.068s | 21.28MiB| unsat | 0 | | | |Lyapunov1a-chunk-0032.smt2 | 0.068s | 20.776MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0043.smt2 | 0.068s | 20.824MiB| unsat | 0 | | | |sin-problem-7-weak2-chunk-0123.smt2 | 0.068s | 20.796MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0170.smt2 | 0.068s | 20.816MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0028.smt2 | 0.068s | 20.764MiB| sat | 0 | | | |sin-problem-7-chunk-0172.smt2 | 0.068s | 21.008MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0379.smt2 | 0.068s | 20.792MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0035.smt2 | 0.068s | 20.636MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0412.smt2 | 0.068s | 21.372MiB| unsat | 0 | | | |atan-vega-3-chunk-0220.smt2 | 0.068s | 18.792MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0514.smt2 | 0.068s | 20.864MiB| sat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_lemmas_global_15.smt2 | 0.068s | 20.268MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0010.smt2 | 0.069s | 20.684MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0199.smt2 | 0.069s | 21.064MiB| sat | 0 | | | |exp-problem-10-2-chunk-0358.smt2 | 0.069s | 20.776MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0721.smt2 | 0.069s | 21.008MiB| sat | 0 | | | |atan-vega-3-chunk-0473.smt2 | 0.069s | 21.04MiB| sat | 0 | | | |ball_count_2d_plain.01.seq_lazy_lemmas_global_5.smt2 | 0.069s | 19.348MiB| unsat | 0 | | | |mbo_E17E23.smt2 | 0.069s | 20.968MiB| unsat | 0 | | | |sin-problem-7-chunk-0054.smt2 | 0.070s | 20.752MiB| sat | 0 | | | |sin-cos-346-b-chunk-0358.smt2 | 0.070s | 20.764MiB| sat | 0 | | | |atan-vega-3-chunk-0340.smt2 | 0.070s | 20.664MiB| sat | 0 | | | |matrix-5-all-23.smt2 | 0.070s | 21.528MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_linear_enc_lemmas_global_7.smt2 | 0.070s | 21.464MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0015.smt2 | 0.070s | 20.764MiB| sat | 0 | | | |sqrt-circles-2-chunk-0002.smt2 | 0.070s | 20.84MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0166.smt2 | 0.071s | 20.852MiB| sat | 0 | | | |ball_count_1d_plain.02.seq_lazy_linear_enc_global_5.smt2 | 0.071s | 19.268MiB| unsat | 0 | | | |ball_count_2d_hill.04.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.071s | 21.508MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0234.smt2 | 0.071s | 20.676MiB| sat | 0 | | | |atan-problem-2-chunk-0024.smt2 | 0.071s | 20.78MiB| sat | 0 | | | |sin-problem-7-weak-chunk-0160.smt2 | 0.072s | 21.036MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0668.smt2 | 0.072s | 21.072MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_lemmas_global_9.smt2 | 0.072s | 21.616MiB| unsat | 0 | | | |sin-344-3-chunk-0058.smt2 | 0.072s | 20.888MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0435.smt2 | 0.072s | 20.716MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0243.smt2 | 0.072s | 21.048MiB| unsat | 0 | | | |InVarSynth_PostfixIncrementDecrement.c_Iteration3_0.smt2 | 0.073s | 21.12MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.qfree_global_15.smt2 | 0.073s | 21.84MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0457.smt2 | 0.073s | 20.868MiB| sat | 0 | | | |etcs_braking_2.01.qfree_global_3.smt2 | 0.073s | 21.364MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0086.smt2 | 0.073s | 18.716MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0171.smt2 | 0.073s | 21.204MiB| sat | 0 | | | |atan-problem-2-sqrt-chunk-0039.smt2 | 0.073s | 20.828MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0054.smt2 | 0.073s | 20.64MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0267.smt2 | 0.074s | 20.768MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0083.smt2 | 0.074s | 20.768MiB| sat | 0 | | | |sin-problem-7-chunk-0335.smt2 | 0.074s | 20.864MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0103.smt2 | 0.074s | 20.828MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0589.smt2 | 0.074s | 21.008MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0530.smt2 | 0.074s | 20.724MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0643.smt2 | 0.074s | 20.984MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0064.smt2 | 0.074s | 20.704MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0368.smt2 | 0.075s | 20.912MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0098.smt2 | 0.075s | 21.02MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0135.smt2 | 0.075s | 20.948MiB| unsat | 0 | | | |ball_count_1d_plain.10.redlog_global_9.smt2 | 0.075s | 19.656MiB| unsat | 0 | | | |atan-problem-2-sqrt-chunk-0019.smt2 | 0.075s | 20.772MiB| unsat | 0 | | | |ball_count_2d_slope.04.seq_lazy_linear_enc_global_3.smt2 | 0.075s | 21.372MiB| unsat | 0 | | | |atan-problem-2-chunk-0092.smt2 | 0.076s | 21.0MiB| unsat | 0 | | | |cbrt-problem-3-weak-chunk-0094.smt2 | 0.076s | 20.788MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0021.smt2 | 0.076s | 20.976MiB| sat | 0 | | | |MulliganEconomicsModel0080e.smt2 | 0.076s | 20.844MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0058.smt2 | 0.076s | 20.832MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0069.smt2 | 0.077s | 21.024MiB| sat | 0 | | | |ball_count_2d_hill.01.seq_lazy_lemmas_global_7.smt2 | 0.077s | 19.736MiB| unsat | 0 | | | |atan-problem-1-chunk-0035.smt2 | 0.077s | 20.768MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0035.smt2 | 0.077s | 20.724MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0121.smt2 | 0.077s | 20.808MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0467.smt2 | 0.078s | 20.78MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.078s | 22.152MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0030.smt2 | 0.078s | 20.764MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0375.smt2 | 0.078s | 20.836MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0436.smt2 | 0.079s | 21.008MiB| sat | 0 | | | |ball_count_2d_plain.05.qfree_global_13.smt2 | 0.079s | 21.808MiB| unsat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0062.smt2 | 0.079s | 20.616MiB| sat | 0 | | | |sin-cos-346-b-chunk-0391.smt2 | 0.080s | 20.764MiB| sat | 0 | | | |polypaver-sqrt43-int-chunk-0053.smt2 | 0.080s | 20.732MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0191.smt2 | 0.080s | 20.676MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0086.smt2 | 0.080s | 20.904MiB| sat | 0 | | | |ball_count_1d_plain.05.seq_lazy_linear_enc_global_11.smt2 | 0.080s | 21.676MiB| unsat | 0 | | | |InVarSynth_LabelEncodingWithUnrolling.bpl_Iteration2_0.smt2 | 0.080s | 20.944MiB| sat | 0 | | | |CMOS-opamp-chunk-0286.smt2 | 0.080s | 20.792MiB| sat | 0 | | | |CMOS-opamp-chunk-0158.smt2 | 0.080s | 20.764MiB| unsat | 0 | | | |polypaver-bench-exp-3d-chunk-0138.smt2 | 0.080s | 20.68MiB| unsat | 0 | | | |MulliganEconomicsModel0027c.smt2 | 0.080s | 20.724MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0286.smt2 | 0.081s | 21.088MiB| sat | 0 | | | |sin-problem-7-chunk-0247.smt2 | 0.081s | 21.008MiB| sat | 0 | | | |ball_count_2d_hill.05.seq_lazy_global_3.smt2 | 0.081s | 21.272MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0500.smt2 | 0.081s | 20.888MiB| unsat | 0 | | | |ball_count_2d_hill.02.redlog_global_13.smt2 | 0.082s | 21.452MiB| unsat | 0 | | | |ball_count_2d_hill.01.redlog_global_9.smt2 | 0.082s | 20.672MiB| unsat | 0 | | | |ball_count_2d_hill.01.redlog_global_13.smt2 | 0.082s | 21.224MiB| unsat | 0 | | | |atan-vega-3-chunk-0149.smt2 | 0.083s | 20.636MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0276.smt2 | 0.083s | 20.996MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0402.smt2 | 0.083s | 21.1MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0205.smt2 | 0.083s | 20.852MiB| unsat | 0 | | | |ball_count_2d_slope.10.seq_lazy_lemmas_global_15.smt2 | 0.083s | 21.508MiB| unsat | 0 | | | |atan-vega-3-chunk-0109.smt2 | 0.083s | 20.764MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0391.smt2 | 0.083s | 21.024MiB| sat | 0 | | | |sin-cos-346-b-chunk-0114.smt2 | 0.083s | 20.788MiB| unsat | 0 | | | |Chua-1-VC1-U-chunk-0083.smt2 | 0.084s | 21.016MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0142.smt2 | 0.084s | 20.748MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0076.smt2 | 0.084s | 20.464MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_linear_enc_global_5.smt2 | 0.084s | 19.48MiB| unsat | 0 | | | |ball_count_2d_plain.01.qfree_global_3.smt2 | 0.084s | 19.004MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0113.smt2 | 0.084s | 20.82MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.084s | 20.624MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0679.smt2 | 0.085s | 21.02MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0038.smt2 | 0.085s | 20.792MiB| sat | 0 | | | |sin-cos-346-b-chunk-0524.smt2 | 0.085s | 18.912MiB| unsat | 0 | | | |sin-problem-7-chunk-0117.smt2 | 0.086s | 20.916MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.086s | 19.68MiB| unsat | 0 | | | |ball_count_2d_plain.03.qfree_global_15.smt2 | 0.086s | 22.084MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0620.smt2 | 0.087s | 20.848MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0606.smt2 | 0.087s | 21.016MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0082.smt2 | 0.087s | 18.736MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.qfree_global_13.smt2 | 0.087s | 19.604MiB| unsat | 0 | | | |ball_count_2d_plain.02.seq_lazy_global_1.smt2 | 0.087s | 18.836MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0124.smt2 | 0.087s | 20.756MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0515.smt2 | 0.087s | 20.82MiB| sat | 0 | | | |atan-vega-3-chunk-0119.smt2 | 0.087s | 20.772MiB| sat | 0 | | | |ball_count_2d_plain.01.seq_lazy_lemmas_global_1.smt2 | 0.088s | 19.04MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_lemmas_global_7.smt2 | 0.088s | 21.444MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0071.smt2 | 0.089s | 20.932MiB| sat | 0 | | | |ball_count_1d_plain.03.seq_lazy_linear_enc_global_13.smt2 | 0.089s | 21.76MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0446.smt2 | 0.090s | 20.768MiB| sat | 0 | | | |ball_count_2d_hill.03.seq_lazy_lemmas_global_7.smt2 | 0.090s | 21.9MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0064.smt2 | 0.090s | 20.768MiB| sat | 0 | | | |ball_count_2d_plain.10.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.090s | 19.2MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0178.smt2 | 0.090s | 20.608MiB| sat | 0 | | | |exp-problem-10-3-chunk-0052.smt2 | 0.090s | 20.744MiB| sat | 0 | | | |ball_count_2d_hill_simple.10.redlog_global_3.smt2 | 0.090s | 19.14MiB| unsat | 0 | | | |ball_count_2d_slope.04.seq_lazy_global_5.smt2 | 0.090s | 21.864MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0022.smt2 | 0.090s | 20.744MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.redlog_global_15.smt2 | 0.090s | 22.076MiB| unsat | 0 | | | |ball_count_1d_plain.04.qfree_global_7.smt2 | 0.091s | 21.08MiB| unsat | 0 | | | |Chua-2-VC1-U-chunk-0013.smt2 | 0.091s | 20.868MiB| sat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_global_5.smt2 | 0.091s | 21.072MiB| unsat | 0 | | | |ball_count_2d_hill.05.seq_lazy_lemmas_global_7.smt2 | 0.091s | 21.868MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0149.smt2 | 0.092s | 21.012MiB| unsat | 0 | | | |sin-344-3-weak-chunk-0044.smt2 | 0.092s | 20.672MiB| sat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_lemmas_global_13.smt2 | 0.092s | 22.148MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0398.smt2 | 0.093s | 20.984MiB| sat | 0 | | | |sin-problem-7-chunk-0322.smt2 | 0.093s | 20.928MiB| unsat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0009.smt2 | 0.093s | 20.752MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0156.smt2 | 0.094s | 20.664MiB| sat | 0 | | | |sin-cos-346-b-chunk-0560.smt2 | 0.094s | 20.784MiB| sat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_linear_enc_lemmas_global_11.smt2 | 0.094s | 21.804MiB| unsat | 0 | | | |Chua-2-IL-L-chunk-0058.smt2 | 0.094s | 20.74MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_linear_enc_global_5.smt2 | 0.094s | 19.404MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0318.smt2 | 0.094s | 20.872MiB| unsat | 0 | | | |sin-problem-8-weak-chunk-0044.smt2 | 0.095s | 20.828MiB| sat | 0 | | | |exp-problem-10-3-chunk-0073.smt2 | 0.095s | 20.764MiB| sat | 0 | | | |atan-vega-3-chunk-0493.smt2 | 0.095s | 20.764MiB| sat | 0 | | | |matrix-1-all-2.smt2 | 0.096s | 21.02MiB| sat | 0 | | | |ball_count_1d_plain.04.seq_lazy_global_5.smt2 | 0.097s | 21.3MiB| unsat | 0 | | | |Chua-2-VC1-U-chunk-0117.smt2 | 0.097s | 20.628MiB| unsat | 0 | | | |MulliganEconomicsModel0077c.smt2 | 0.098s | 20.684MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0097.smt2 | 0.098s | 21.024MiB| sat | 0 | | | |atan-vega-3-chunk-0613.smt2 | 0.098s | 21.272MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0310.smt2 | 0.098s | 20.76MiB| sat | 0 | | | |ball_count_2d_hill.04.seq_lazy_lemmas_global_7.smt2 | 0.098s | 21.772MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_linear_enc_lemmas_global_15.smt2 | 0.098s | 22.316MiB| unsat | 0 | | | |ball_count_2d_slope.03.seq_lazy_linear_enc_lemmas_global_15.smt2 | 0.098s | 21.008MiB| unsat | 0 | | | |ball_count_2d_slope.03.seq_lazy_lemmas_global_3.smt2 | 0.099s | 21.672MiB| unsat | 0 | | | |MulliganEconomicsModel0067a.smt2 | 0.099s | 20.656MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0098.smt2 | 0.099s | 20.832MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0075.smt2 | 0.099s | 20.8MiB| sat | 0 | | | |etcs_braking_2.01.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.100s | 21.784MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.100s | 21.784MiB| unsat | 0 | | | |Chua-1-IL-U-chunk-0076.smt2 | 0.100s | 21.032MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0183.smt2 | 0.101s | 20.784MiB| sat | 0 | | | |ball_count_2d_plain.02.qfree_global_11.smt2 | 0.101s | 19.632MiB| unsat | 0 | | | |sin-problem-8-chunk-0067.smt2 | 0.102s | 21.18MiB| sat | 0 | | | |sin-cos-346-b-chunk-0584.smt2 | 0.102s | 20.788MiB| sat | 0 | | | |sin-cos-346-b-chunk-0285.smt2 | 0.103s | 20.732MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0043.smt2 | 0.103s | 20.768MiB| unsat | 0 | | | |sqrt-circles-2-chunk-0015.smt2 | 0.104s | 20.768MiB| unsat | 0 | | | |bottom-plate-mixer-chunk-0050.smt2 | 0.105s | 20.768MiB| sat | 0 | | | |ball_count_2d_hill_simple.05.redlog_global_13.smt2 | 0.106s | 22.036MiB| unsat | 0 | | | |ball_count_2d_hill.05.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.107s | 21.328MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0621.smt2 | 0.107s | 20.972MiB| sat | 0 | | | |ball_count_1d_plain.05.seq_lazy_global_9.smt2 | 0.108s | 21.4MiB| unsat | 0 | | | |atan-vega-3-chunk-0443.smt2 | 0.109s | 20.992MiB| sat | 0 | | | |mbo_E5E23.smt2 | 0.109s | 21.56MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0177.smt2 | 0.109s | 21.024MiB| sat | 0 | | | |ball_count_2d_hill.02.seq_lazy_linear_enc_global_15.smt2 | 0.110s | 20.256MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.110s | 20.12MiB| unsat | 0 | | | |ball_count_1d_plain.03.redlog_global_11.smt2 | 0.111s | 21.708MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.114s | 21.388MiB| unsat | 0 | | | |cos-3410-b-chunk-0015.smt2 | 0.114s | 20.912MiB| sat | 0 | | | |ball_count_1d_plain.04.qfree_global_11.smt2 | 0.114s | 21.532MiB| unsat | 0 | | | |ball_count_2d_hill.10.seq_lazy_linear_enc_global_15.smt2 | 0.115s | 20.316MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0426.smt2 | 0.115s | 21.104MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0690.smt2 | 0.116s | 21.032MiB| sat | 0 | | | |ball_count_2d_plain.04.redlog_global_13.smt2 | 0.118s | 22.564MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_linear_enc_global_15.smt2 | 0.118s | 21.932MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0610.smt2 | 0.120s | 20.924MiB| sat | 0 | | | |ball_count_1d_plain.04.seq_lazy_linear_enc_lemmas_global_11.smt2 | 0.121s | 22.032MiB| unsat | 0 | | | |ball_count_1d_plain.04.seq_lazy_lemmas_global_9.smt2 | 0.121s | 21.564MiB| unsat | 0 | | | |ball_count_1d_plain.05.seq_lazy_global_13.smt2 | 0.121s | 21.736MiB| unsat | 0 | | | |atan-vega-3-chunk-0300.smt2 | 0.121s | 21.04MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0151.smt2 | 0.121s | 18.98MiB| unsat | 0 | | | |ball_count_2d_plain.03.seq_lazy_linear_enc_global_11.smt2 | 0.122s | 21.792MiB| unsat | 0 | | | |RL-high-pass-circuit-gain-chunk-0010.smt2 | 0.124s | 20.768MiB| sat | 0 | | | |InVarSynth_ShortCircuit-SideEffect-SwitchStatement-Safe.c_Iteration1_0.smt2 | 0.125s | 21.636MiB| sat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_lemmas_global_11.smt2 | 0.125s | 22.016MiB| unsat | 0 | | | |mgc_06.smt2 | 0.126s | 20.868MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0209.smt2 | 0.127s | 21.024MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0254.smt2 | 0.129s | 21.16MiB| unsat | 0 | | | |InVarSynth_doubleLoopUniformIterations.bpl_Iteration2_0.smt2 | 0.131s | 20.848MiB| unsat | 0 | | | |ball_count_2d_plain.04.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.136s | 21.524MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.138s | 21.384MiB| unsat | 0 | | | |ball_count_2d_plain.03.seq_lazy_linear_enc_lemmas_global_15.smt2 | 0.145s | 22.328MiB| unsat | 0 | | | |CMOS-opamp-chunk-0320.smt2 | 0.149s | 21.064MiB| unsat | 0 | | | |ball_count_1d_plain.03.seq_lazy_linear_enc_global_9.smt2 | 0.153s | 21.532MiB| unsat | 0 | | | |sin-problem-8-weak-chunk-0079.smt2 | 0.156s | 21.116MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0446.smt2 | 0.168s | 21.6MiB| sat | 0 | | | |ball_count_2d_plain.04.redlog_global_9.smt2 | 0.170s | 21.984MiB| unsat | 0 | | | |toeplz.c.i.toeplz.pl.t2.fixed.t2.c_Iteration10_Loop_3-pieceTemplate.smt2 | 0.172s | 22.872MiB| sat | 0 | | | |ball_count_1d_plain.03.seq_lazy_global_15.smt2 | 0.173s | 21.96MiB| unsat | 0 | | | |ball_count_2d_hill.04.seq_lazy_lemmas_global_11.smt2 | 0.178s | 22.976MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0457.smt2 | 0.179s | 21.268MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_lemmas_global_11.smt2 | 0.188s | 22.964MiB| unsat | 0 | | | |mc91test.t2.c_Iteration5_Loop_3-pieceTemplate.smt2 | 0.189s | 23.468MiB| sat | 0 | | | |ball_count_1d_plain.04.seq_lazy_lemmas_global_13.smt2 | 0.192s | 22.024MiB| unsat | 0 | | | |ball_count_2d_hill.05.seq_lazy_lemmas_global_11.smt2 | 0.199s | 22.824MiB| unsat | 0 | | | |ball_count_1d_plain.05.qfree_global_15.smt2 | 0.199s | 21.956MiB| unsat | 0 | | | |etcs_braking_2.01.seq_lazy_lemmas_global_5.smt2 | 0.211s | 22.62MiB| unsat | 0 | | | |ball_count_2d_hill.05.seq_lazy_linear_enc_global_15.smt2 | 0.219s | 23.7MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_linear_enc_global_15.smt2 | 0.220s | 23.564MiB| unsat | 0 | | | |ball_count_2d_hill.04.seq_lazy_linear_enc_global_15.smt2 | 0.224s | 23.556MiB| unsat | 0 | | | |standard_init9_ground.i_3_2_2.bpl_1.smt2 | 0.237s | 21.588MiB| unsat | 0 | | | |ball_count_2d_slope.03.seq_lazy_linear_enc_global_7.smt2 | 0.242s | 22.444MiB| unsat | 0 | | | |ball_count_2d_slope.05.seq_lazy_lemmas_global_5.smt2 | 0.269s | 22.388MiB| unsat | 0 | | | |qrdcmp.t2.c_Iteration6_Loop_3-pieceTemplate.smt2 | 0.269s | 23.46MiB| sat | 0 | | | |ball_count_1d_plain.04.redlog_global_15.smt2 | 0.276s | 22.28MiB| unsat | 0 | | | |ball_count_1d_plain.05.seq_lazy_linear_enc_lemmas_global_15.smt2 | 0.283s | 22.32MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0201.smt2 | 0.308s | 23.024MiB| unsat | 0 | | | |pentagon.t2.c_Iteration9_Loop_3-pieceTemplate.smt2 | 0.322s | 22.84MiB| sat | 0 | | | |CMOS-opamp-chunk-0180.smt2 | 0.339s | 21.436MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0296.smt2 | 0.367s | 21.44MiB| unsat | 0 | | | |p-42.t2.c_Iteration2_Loop_4-pieceTemplate.smt2 | 0.426s | 24.888MiB| sat | 0 | | | |sort.t2.c_Iteration5_Loop_3-pieceTemplate.smt2 | 0.439s | 26.024MiB| sat | 0 | | | |etcs_braking_2.01.seq_lazy_linear_enc_global_9.smt2 | 0.463s | 24.072MiB| unsat | 0 | | | |spiral.t2.c_Iteration8_Loop_4-pieceTemplate.smt2 | 0.484s | 24.488MiB| sat | 0 | | | |CookSeeZuleger-2013TACAS-Fig3_true-termination.c_Iteration1_Loop_5-phaseTemplate.smt2 | 0.557s | 44.624MiB| unsat | 0 | | | |matrix-1-all-38.smt2 | 0.595s | 21.84MiB| sat | 0 | | | |toeplz.t2.c_Iteration7_Loop_4-pieceTemplate.smt2 | 0.614s | 24.948MiB| sat | 0 | | | |bf10.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 0.617s | 25.22MiB| sat | 0 | | | |ball_count_2d_slope.05.seq_lazy_linear_enc_global_9.smt2 | 0.734s | 23.864MiB| unsat | 0 | | | |Canberra.bpl_Iteration1_Loop_2-pieceTemplate.smt2 | 0.739s | 44.86MiB| unsat | 0 | | | |SyntaxSupportDisjunction1.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 0.752s | 26.204MiB| sat | 0 | | | |CookSeeZuleger-2013TACAS-Fig7a_true-termination.c_Iteration1_Loop_5-phaseTemplate.smt2 | 0.759s | 76.228MiB| unsat | 0 | | | |ball_count_2d_hill.04.redlog_global_9.smt2 | 0.808s | 23.54MiB| unsat | 0 | | | |ball_count_2d_hill.05.redlog_global_9.smt2 | 0.839s | 23.436MiB| unsat | 0 | | | |ball_count_2d_hill.03.redlog_global_9.smt2 | 0.845s | 23.488MiB| unsat | 0 | | | |ball_count_2d_slope.03.seq_lazy_global_9.smt2 | 1.002s | 23.984MiB| unsat | 0 | | | |ex11.t2.c_Iteration1_Lasso_5-phaseTemplate.smt2 | 1.149s | 29.684MiB| unsat | 0 | | | |Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2 | 1.229s | 43.14MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0315.smt2 | 1.248s | 22.26MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0123.smt2 | 1.672s | 22.088MiB| unsat | 0 | | | |eric.t2.c_Iteration1_Lasso_5-phaseTemplate.smt2 | 1.806s | 26.972MiB| unsat | 0 | | | |ball_count_2d_slope.04.seq_lazy_lemmas_global_9.smt2 | 2.470s | 25.212MiB| unsat | 0 | | | |ball_count_2d_slope.03.seq_lazy_linear_enc_global_11.smt2 | 2.622s | 25.72MiB| unsat | 0 | | | |sin-problem-7-weak2-chunk-0113.smt2 | 2.960s | 22.016MiB| unsat | 0 | | | |joey_false-termination.c_Iteration2_Loop_6-phaseTemplate.smt2 | 3.576s | 28.74MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0181.smt2 | 3.687s | 21.932MiB| sat | 0 | | | |p-55.t2.c_Iteration3_Loop_4-pieceTemplate.smt2 | 4.373s | 42.912MiB| sat | 0 | | | |TelAviv-Amir-Minimum_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2 | 4.691s | 260.0MiB| unsat | 0 | | | |KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-termination.c_Iteration1_Lasso_affineTemplate.smt2 | 4.922s | 69.056MiB| unsat | 0 | | | |ball_count_2d_hill.05.redlog_global_13.smt2 | 6.635s | 25.96MiB| unsat | 0 | | | |ball_count_2d_hill.03.redlog_global_13.smt2 | 7.767s | 25.788MiB| unsat | 0 | | | |ball_count_2d_hill.04.redlog_global_13.smt2 | 7.850s | 26.016MiB| unsat | 0 | | | |ball_count_2d_slope.05.seq_lazy_global_15.smt2 | 10.071s | 33.944MiB| unknown | 0 | | | |ball_count_2d_slope.05.seq_lazy_linear_enc_global_13.smt2 | 14.060s | 37.18MiB| unknown | 0 | | | |ball_count_2d_slope.03.seq_lazy_global_13.smt2 | 14.062s | 29.484MiB| unknown | 0 | | | |ball_count_2d_slope.04.seq_lazy_lemmas_global_13.smt2 | 14.083s | 30.148MiB| unknown | 0 | | | |mbo_E6E7.smt2 | 14.123s | 22.52MiB| unsat | 0 | | | |2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2 | 14.183s | 25.224MiB| unsat | 0 | | | |BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2 | 14.195s | 32.704MiB| unsat | 0 | | | |mbo_E13E17.smt2 | 14.207s | 154.0MiB| unknown | 0 | | | |ex4.t2.c_Iteration2_Loop_3-pieceTemplate.smt2 | 14.249s | 26.488MiB| sat | 0 | | | |mbo_E1E22.smt2 | 14.256s | 219.0MiB| unknown | 0 | | | |mbo_E9E13.smt2 | 14.318s | 121.0MiB| unknown | 0 | | | |etcs_braking_2.01.seq_lazy_global_15.smt2 | 14.356s | 36.76MiB| unsat | 0 | | | |matrix-2-all-4.smt2 | 14.421s | 186.0MiB| sat | 0 | | | |selectSort.t2.c_Iteration3_Loop_4-pieceTemplate.smt2 | 14.600s | 29.296MiB| sat | 0 | | | |mbo_E15E18.smt2 | 14.607s | 126.0MiB| unknown | 0 | | | |mbo_E4E17.smt2 | 15.103s | 234.0MiB| unknown | 0 | | | |db3.t2.c_Iteration2_Loop_4-pieceTemplate.smt2 | 15.451s | 34.528MiB| sat | 0 | | | |loop_on_input.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 15.775s | 30.344MiB| sat | 0 | | | |mbo_E5E12.smt2 | 16.347s | 126.0MiB| unknown | 0 | | | |Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2 | 16.373s | 27.012MiB| unsat | 0 | | | |mbo_E1E6.smt2 | 16.569s | 256.0MiB| unknown | 0 | | | |polyrank5.t2.c_Iteration1_Loop_7-phaseTemplate.smt2 | 16.904s | 27.812MiB| sat | 0 | | | |MulliganEconomicsModel0057c.smt2 | 18.613s | 30.14MiB| unsat | 0 | | | |fun9.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 19.123s | 31.964MiB| sat | 0 | | | |Garmisch.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 21.826s | 28.736MiB| unsat | 0 | | | |mbo_E7E26.smt2 | 25.625s | 61.04MiB| unsat | 0 | | | |fuhs-inflasso.t2.c_Iteration2_Loop_4-pieceTemplate.smt2 | 26.219s | 32.508MiB| sat | 0 | | | |polyrank3.t2.c_Iteration2_Loop_3-pieceTemplate.smt2 | 28.618s | 34.496MiB| unsat | 0 | | | |nested.t2.c_Iteration3_Loop_3-pieceTemplate.smt2 | 32.185s | 48.016MiB| sat | 0 | | | |standard_copy5_ground.i_3_2_2.bpl_3.smt2 | 32.273s | 24.256MiB| unsat | 0 | | | |matrix-3-all-4.smt2 | 32.586s | 70.484MiB| sat | 0 | | | |Mysore2.bpl_Iteration1_Loop_3-pieceTemplate.smt2 | 32.856s | 57.688MiB| unsat | 0 | | | |byron-1.t2.c_Iteration1_Loop_3-pieceTemplate.smt2 | 32.862s | 29.836MiB| unsat | 0 | | | |SyntaxSupportDivision1.bpl_Iteration1_Lasso_7-nestedTemplate.smt2 | 39.100s | 81.54MiB| sat | 0 | | | |Lobnya-Boolean-Reordered.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 40.087s | 37.524MiB| unsat | 0 | | | |Collatz.bpl_Iteration1_Loop_3-nestedTemplate.smt2 | 44.661s | 253.0MiB| unsat | 0 | | | |mbo_E14E22.smt2 | 45.559s | 232.0MiB| sat | 0 | | | |simple-scaled200.bpl_Iteration1_Lasso_7-phaseTemplate.smt2 | 46.033s | 170.0MiB| sat | 0 | | | |Collatz.bpl_Iteration1_Lasso_6-nestedTemplate.smt2 | 47.895s | 512.0MiB| unsat | 0 | | | |Collatz.bpl_Iteration1_Loop_6-phaseTemplate.smt2 | 48.683s | 488.0MiB| unsat | 0 | | | |hong_10.smt2 | 49.782s | 42.82MiB| unsat | 0 | | | |mbo_E25.smt2 | 50.254s | 25.696MiB| unsat | 0 | | | |etcs_braking_2.01.redlog_global_11.smt2 | 50.268s | 41.832MiB| unsat | 0 | | | |etcs_braking_2.01.redlog_global_7.smt2 | 50.386s | 33.8MiB| unsat | 0 | | | |polyrank4.t2.c_Iteration8_Loop_2-pieceTemplate.smt2 | 50.450s | 27.952MiB| unsat | 0 | | | |kissing_4_4.smt2 | 50.718s | 88.424MiB| sat | 0 | | | |polyrank4.t2.c_Iteration3_Loop_3-pieceTemplate.smt2 | 51.819s | 40.1MiB| unsat | 0 | | | |SantaBarbara01.bpl_Iteration1_Lasso_4-pieceTemplate.smt2 | 51.893s | 39.024MiB| unsat | 0 | | | |yPositive-MixedIntReal.bpl_Iteration1_Loop_3-pieceTemplate.smt2 | 51.967s | 51.164MiB| unsat | 0 | | | |iecs.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 52.152s | 56.976MiB| unsat | 0 | | | |Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 52.295s | 51.86MiB| unsat | 0 | | | |eric2.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 52.327s | 71.528MiB| unsat | 0 | | | |BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2 | 52.650s | 54.204MiB| unsat | 0 | | | |mbo_E23E24.smt2 | 52.846s | 102.0MiB| unsat | 0 | | | |mbo_E7E16.smt2 | 52.925s | 116.0MiB| unsat | 0 | | | |LeeJonesBen-Amram-2001POPL-Ex4_true-termination.c_Iteration2_Loop_3-pieceTemplate.smt2 | 53.182s | 75.7MiB| unsat | 0 | | | |mbo_E4E27.smt2 | 53.385s | 70.264MiB| unsat | 0 | | | |CookSeeZuleger-2013TACAS-Fig7b.bpl_Iteration1_Loop_3-pieceTemplate.smt2 | 53.449s | 103.0MiB| unsat | 0 | | | |mbo_E13E27.smt2 | 55.272s | 90.16MiB| unsat | 0 | | | |mbo_E18E22.smt2 | 55.694s | 83.524MiB| unsat | 0 | | | |polyrank3.t2.c_Iteration8_Loop_4-pieceTemplate.smt2 | 55.861s | 83.712MiB| unsat | 0 | | | |mbo_E10E18.smt2 | 56.423s | 614.0MiB| unknown | 0 | | | |mbo_E12E13.smt2 | 56.611s | 759.0MiB| unknown | 0 | | | |collatz.t2.c_Iteration3_Lasso_6-phaseTemplate.smt2 | 56.804s | 66.68MiB| unsat | 0 | | | |sas2.t2.c_Iteration6_Lasso_7-nestedTemplate.smt2 | 56.823s | 54.012MiB| sat | 0 | | | |mbo_E8E24.smt2 | 56.844s | 614.0MiB| unknown | 0 | | | |LeeJonesBen-Amram-2001POPL-Ex1_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2 | 57.201s | 84.508MiB| unsat | 0 | | | |mbo_E2E4.smt2 | 58.281s | 884.0MiB| unknown | 0 | | | |Masse_true-termination.c_Iteration1_Loop_2-pieceTemplate.smt2 | 58.619s | 97.536MiB| unsat | 0 | | | |mbo_E2E10.smt2 | 58.938s | 770.0MiB| unknown | 0 | | | |mbo_E3E8.smt2 | 58.959s | 909.0MiB| unknown | 0 | | | |mbo_E20E25.smt2 | 59.116s | 76.44MiB| unsat | 0 | | | |mbo_E6E19.smt2 | 60.380s | 951.0MiB| unknown | 0 | | | |mbo_E3E13.smt2 | 60.808s | 843.0MiB| unknown | 0 | | | |mbo_E9E23.smt2 | 60.823s | 97.58MiB| unsat | 0 | | | |mbo_E1E13.smt2 | 61.075s | 887.0MiB| unknown | 0 | | | |Nyala-TwoLex.bpl_Iteration1_Lasso_4-pieceTemplate.smt2 | 61.673s | 225.0MiB| unsat | 0 | | | |Collatz.bpl_Iteration1_Lasso_2-pieceTemplate.smt2 | 64.117s | 518.0MiB| unsat | 0 | | | |eric2.t2.c_Iteration7_Loop_4-pieceTemplate.smt2 | 66.746s | 316.0MiB| unsat | 0 | | | |KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-termination.c_Iteration1_Lasso_4-lexTemplate.smt2 | 70.285s | 283.0MiB| unsat | 0 | | | |mbo_E19E22.smt2 | 78.231s | 479.0MiB| unsat | 0 | | | |mbo_E15E28.smt2 | 78.694s | 478.0MiB| unsat | 0 | | | |mbo_E3E23.smt2 | 78.862s | 489.0MiB| unsat | 0 | | | |BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2 | 79.058s | 200.0MiB| unsat | 0 | | | |firewire.t2.c_Iteration1_Lasso_7-nestedTemplate.smt2 | 87.065s | 95.96MiB| sat | 0 | | | |matrix-5-all-13.smt2 | 94.639s | 550.0MiB| unknown | 0 | | | |mbo_E12E23.smt2 | 95.958s | 79.328MiB| unsat | 0 | | | |mbo_E11E20.smt2 | 97.362s | 81.092MiB| unsat | 0 | | | |mbo_E8E14.smt2 | 98.737s | 948.0MiB| unknown | 0 | | | |OpposedDisjuncts.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 106.257s | 297.0MiB| unsat | 0 | | | |GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_6-nestedTemplate.smt2 | 112.713s | 599.0MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0265.smt2 | 120.985s | 36.076MiB| unsat | 0 | | | |sas2.t2.c_Iteration1_Lasso_4-pieceTemplate.smt2 | 124.493s | 450.0MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0176.smt2 | 128.851s | 35.784MiB| unsat | 0 | | | |GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_3-lexTemplate.smt2 | 132.266s | 867.0MiB| unsat | 0 | | | |simple_ballistics_reach.01.seq_lazy_global_7.smt2 | 200.010s | 34.828MiB| timeout | 0 | | | |sqrt-1mcosq-8-chunk-0233.smt2 | 200.012s | 81.032MiB| timeout | 0 | | | |seq.i_5_5_5.bpl_3.smt2 | 200.013s | 77.8MiB| timeout | 0 | | | |kissing_4_18.smt2 | 200.013s | 89.768MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_lemmas_global_15.smt2 | 200.013s | 34.516MiB| timeout | 0 | | | |fragtest_simple.i_4_5_4.bpl_3.smt2 | 200.013s | 106.0MiB| timeout | 0 | | | |matrix-4-all-22.smt2 | 200.014s | 150.0MiB| timeout | 0 | | | |atan-vega-3-weak-chunk-0385.smt2 | 200.016s | 29.224MiB| timeout | 0 | | | |InVarSynth_BugHoareAnnotationWithMinimiation.bpl_Iteration1_0.smt2 | 200.016s | 79.456MiB| timeout | 0 | | | |linear_search.i_7_19_3.bpl_3.smt2 | 200.017s | 57.668MiB| timeout | 0 | | | |InVarSynth_threadpooling_out2.mover.bpl_Iteration2_0.smt2 | 200.019s | 108.0MiB| timeout | 0 | | | |standard_two_index_05.i_3_2_2.bpl_5.smt2 | 200.020s | 301.0MiB| timeout | 0 | | | |matrix-3-all-13.smt2 | 200.022s | 243.0MiB| timeout | 0 | | | |sin-problem-7-chunk-0297.smt2 | 200.022s | 95.156MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_global_11.smt2 | 200.023s | 50.188MiB| timeout | 0 | | | |avg60.i_5_5_4.bpl_3.smt2 | 200.027s | 40.972MiB| timeout | 0 | | | |kissing_3_9.smt2 | 200.028s | 93.632MiB| timeout | 0 | | | |mbo_E10E28.smt2 | 200.030s | 497.0MiB| timeout | 0 | | | |matrix-2-all-17.smt2 | 200.033s | 63.764MiB| timeout | 0 | | | |mbo_E16E25.smt2 | 200.034s | 158.0MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_13.smt2 | 200.035s | 32.644MiB| timeout | 0 | | | |matrix-4-all-4.smt2 | 200.036s | 273.0MiB| timeout | 0 | | | |etcs_braking_2.01.seq_lazy_linear_enc_global_13.smt2 | 200.037s | 53.62MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_linear_enc_global_5.smt2 | 200.039s | 54.192MiB| timeout | 0 | | | |mbo_E2E20.smt2 | 200.042s | 521.0MiB| timeout | 0 | | | |kissing_3_11.smt2 | 200.043s | 143.0MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_9.smt2 | 200.048s | 33.268MiB| timeout | 0 | | | |matrix-4-all-13.smt2 | 200.052s | 41.536MiB| timeout | 0 | | | |heidy7-simple.t2.c_Iteration2_Lasso_4-pieceTemplate.smt2 | 200.064s | 374.0MiB| timeout | 0 | | | |LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_7-phaseTemplate.smt2 | 200.065s | 457.0MiB| timeout | 0 | | | |afagp-fail.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2 | 200.071s | 572.0MiB| timeout | 0 | | | |min_rf_true-termination.c_Iteration1_Loop_4-pieceTemplate.smt2 | 200.072s | 532.0MiB| timeout | 0 | | | |efegp.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2 | 200.077s | 513.0MiB| timeout | 0 | | | |yPositive-SIscaled50.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 200.078s | 700.0MiB| timeout | 0 | | | |BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2 | 200.080s | 726.0MiB| timeout | 0 | | | |p-46.t2.c_Iteration2_Lasso_7-phaseTemplate.smt2 | 200.084s | 440.0MiB| timeout | 0 | | | |LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_3-pieceTemplate.smt2 | 200.087s | 513.0MiB| timeout | 0 | | | |aviad_true-termination.c_Iteration1_Loop_6-phaseTemplate.smt2 | 200.089s | 911.0MiB| timeout | 0 | | | |brp_withassume.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 200.113s | 1047.0MiB| timeout | 0 | | | |NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2 | 200.117s | 829.0MiB| timeout | 0 | | | |aviad_true-termination.c_Iteration1_Loop_3-lexTemplate.smt2 | 200.125s | 1062.0MiB| timeout | 0 | | | |NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2 | 200.129s | 775.0MiB| timeout | 0 | | | |Gulwani.bpl_Iteration1_Lasso_4-pieceTemplate.smt2 | 200.131s | 1165.0MiB| timeout | 0 | | |