# .

* SAT 476
* UNSAT 604
* TIMEOUT 43
* UNKNOWN 24

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: gcd with copilot
Job tag: gcd_copilot
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: 5644fbf464b19eb0160e2be92675b8691923c1af
Z3 branch: copilot/add-gcd-algorithms-multivariate-polynomials
Z3 options: "-T:200 "
Z3 inputs: inputs/QF_NRA_small
Z3 commit message: Address code review: O(1) var lookup, remove redundant check, reorder tests

Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|exp-problem-10-2-chunk-0059.smt2                             |    0.023s | 19.188MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0101.smt2                        |    0.024s | 18.712MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0534.smt2                             |    0.024s | 18.956MiB| unsat | 0 |  |  |
|Chua-1-VC2-L-chunk-0064.smt2                                 |    0.024s | 18.772MiB| unsat | 0 |  |  |
|ArthanM2-chunk-0012.smt2                                     |    0.024s | 18.868MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0378.smt2                                |    0.025s | 18.788MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0092.smt2                                |    0.025s | 18.968MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0221.smt2                                |    0.025s | 18.876MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0069.smt2                             |    0.026s | 18.864MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0078.smt2                                |    0.026s | 19.024MiB| unsat | 0 |  |  |
|Chua-1-VC2-L-chunk-0027.smt2                                 |    0.026s | 18.844MiB| unsat | 0 |  |  |
|ball_count_1d_plain.01.seq_lazy_global_3.smt2                |    0.026s | 18.94MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0348.smt2                                |    0.027s | 18.796MiB| unsat | 0 |  |  |
|exp-problem-10-3-chunk-0084.smt2                             |    0.027s | 19.04MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0129.smt2                                  |    0.027s | 20.62MiB| sat | 0 |  |  |
|ball_count_1d_plain.02.redlog_global_3.smt2                  |    0.027s | 19.448MiB| unsat | 0 |  |  |
|ball_count_2d_plain.04.seq_lazy_linear_enc_lemmas_global_1.smt2 |    0.027s | 18.868MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.04.redlog_global_1.smt2            |    0.027s | 18.832MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0068.smt2                                |    0.027s | 18.912MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0074.smt2                             |    0.027s | 21.096MiB| unsat | 0 |  |  |
|sin-problem-10-2-chunk-0034.smt2                             |    0.027s | 18.948MiB| unsat | 0 |  |  |
|Chua-1-VC1-L-chunk-0107.smt2                                 |    0.027s | 20.788MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0661.smt2                             |    0.027s | 19.016MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0299.smt2                      |    0.027s | 21.02MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0102.smt2                                |    0.027s | 19.02MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0224.smt2                             |    0.028s | 20.816MiB| unsat | 0 |  |  |
|ball_count_2d_slope.02.seq_lazy_linear_enc_lemmas_global_1.smt2 |    0.028s | 19.16MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0555.smt2                             |    0.028s | 20.788MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0714.smt2                                |    0.028s | 20.764MiB| unsat | 0 |  |  |
|ArthanKM2-chunk-0002.smt2                                    |    0.028s | 20.832MiB| sat | 0 |  |  |
|sin-problem-10-2-chunk-0024.smt2                             |    0.028s | 18.936MiB| unsat | 0 |  |  |
|ball_count_2d_hill.04.seq_lazy_linear_enc_lemmas_global_1.smt2 |    0.028s | 19.096MiB| unsat | 0 |  |  |
|sqrt-problem-13-sqrt1-chunk-0049.smt2                        |    0.028s | 20.888MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0108.smt2                                   |    0.028s | 20.76MiB| sat | 0 |  |  |
|Chua-1-VC2-U-chunk-0097.smt2                                 |    0.028s | 20.8MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0159.smt2                             |    0.028s | 20.732MiB| sat | 0 |  |  |
|ball_count_2d_hill.10.seq_lazy_global_3.smt2                 |    0.028s | 19.296MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.01.redlog_global_3.smt2            |    0.028s | 19.092MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.03.seq_lazy_global_1.smt2          |    0.028s | 18.86MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0113.smt2                             |    0.028s | 20.74MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0231.smt2                                   |    0.028s | 20.612MiB| sat | 0 |  |  |
|exp-problem-10-2-chunk-0385.smt2                             |    0.028s | 20.772MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0171.smt2                        |    0.028s | 19.136MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0047.smt2                                   |    0.028s | 20.8MiB| unsat | 0 |  |  |
|ball_count_2d_plain.05.seq_lazy_linear_enc_global_1.smt2     |    0.029s | 19.024MiB| unsat | 0 |  |  |
|sqrt-problem-13-chunk-0019.smt2                              |    0.029s | 20.82MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0522.smt2                             |    0.029s | 20.768MiB| sat | 0 |  |  |
|atan-problem-2-sqrt-weak-chunk-0075.smt2                     |    0.029s | 20.776MiB| sat | 0 |  |  |
|sqrt-problem-12vars3-chunk-0097.smt2                         |    0.029s | 20.76MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0533.smt2                                  |    0.029s | 20.756MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0629.smt2                             |    0.029s | 20.9MiB| sat | 0 |  |  |
|Chua-2-IL-L-chunk-0021.smt2                                  |    0.029s | 20.656MiB| sat | 0 |  |  |
|Chua-2-IL-U-chunk-0042.smt2                                  |    0.029s | 20.764MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0728.smt2                                |    0.029s | 20.764MiB| sat | 0 |  |  |
|atan-problem-1-chunk-0006.smt2                               |    0.029s | 20.844MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0217.smt2                      |    0.029s | 20.484MiB| sat | 0 |  |  |
|polypaver-sqrt-circles-1a-chunk-0011.smt2                    |    0.029s | 20.764MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0147.smt2                             |    0.029s | 20.76MiB| sat | 0 |  |  |
|exp-problem-10-2-chunk-0144.smt2                             |    0.029s | 20.668MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0567.smt2                                |    0.029s | 20.956MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0280.smt2                                  |    0.029s | 20.72MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0523.smt2                                  |    0.029s | 20.812MiB| sat | 0 |  |  |
|Chua-1-VC1-L-chunk-0046.smt2                                 |    0.029s | 20.612MiB| sat | 0 |  |  |
|cbrt-problem-3-chunk-0070.smt2                               |    0.029s | 20.664MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0262.smt2                                |    0.029s | 20.968MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0298.smt2                                   |    0.029s | 20.672MiB| sat | 0 |  |  |
|Chua-2-IL-L-chunk-0104.smt2                                  |    0.029s | 18.9MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0048.smt2                        |    0.030s | 20.676MiB| sat | 0 |  |  |
|ball_count_2d_slope.04.seq_lazy_global_1.smt2                |    0.030s | 19.084MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0131.smt2                        |    0.030s | 20.764MiB| unsat | 0 |  |  |
|Lyapunov1a-chunk-0021.smt2                                   |    0.030s | 20.66MiB| sat | 0 |  |  |
|Chua-2-VC1-L-chunk-0052.smt2                                 |    0.030s | 20.652MiB| sat | 0 |  |  |
|Chua-2-VC2-U-chunk-0066.smt2                                 |    0.030s | 21.184MiB| unsat | 0 |  |  |
|sqrt-problem-Melquiond2-chunk-0045.smt2                      |    0.030s | 21.02MiB| unsat | 0 |  |  |
|atan-problem-2-chunk-0117.smt2                               |    0.030s | 20.792MiB| unsat | 0 |  |  |
|sin-problem-7-weak2-chunk-0057.smt2                          |    0.030s | 20.792MiB| sat | 0 |  |  |
|atan-problem-1-weak-chunk-0035.smt2                          |    0.030s | 20.684MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0494.smt2                                |    0.030s | 20.796MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0583.smt2                                  |    0.030s | 21.064MiB| sat | 0 |  |  |
|Chua-1-VC2-U-chunk-0024.smt2                                 |    0.030s | 20.612MiB| unsat | 0 |  |  |
|cos-problem-5-chunk-0023.smt2                                |    0.030s | 20.804MiB| unsat | 0 |  |  |
|sin-problem-7-chunk-0361.smt2                                |    0.030s | 19.004MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0059.smt2                        |    0.030s | 20.772MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0098.smt2                          |    0.030s | 20.78MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0045.smt2                                  |    0.030s | 20.804MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0011.smt2                                  |    0.030s | 21.072MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0330.smt2                                  |    0.030s | 20.596MiB| sat | 0 |  |  |
|ball_count_2d_slope.01.seq_lazy_linear_enc_global_5.smt2     |    0.030s | 19.672MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0380.smt2                                  |    0.030s | 21.22MiB| unsat | 0 |  |  |
|Chua-1-VC1-L-chunk-0146.smt2                                 |    0.030s | 18.94MiB| unsat | 0 |  |  |
|Chua-1-IL-U-chunk-0049.smt2                                  |    0.030s | 20.692MiB| sat | 0 |  |  |
|sqrt-circles-3-chunk-0016.smt2                               |    0.030s | 20.852MiB| sat | 0 |  |  |
|bottom-plate-mixer-chunk-0039.smt2                           |    0.030s | 20.616MiB| sat | 0 |  |  |
|Lyapunov1a-chunk-0011.smt2                                   |    0.030s | 20.596MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0424.smt2                                |    0.030s | 20.756MiB| unsat | 0 |  |  |
|cos-problem-5-chunk-0039.smt2                                |    0.030s | 20.668MiB| sat | 0 |  |  |
|sin-problem-7-weak-chunk-0115.smt2                           |    0.031s | 20.836MiB| sat | 0 |  |  |
|sin-problem-8-chunk-0054.smt2                                |    0.031s | 20.632MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0576.smt2                             |    0.031s | 20.784MiB| unsat | 0 |  |  |
|Chua-2-VC2-U-chunk-0127.smt2                                 |    0.031s | 21.472MiB| sat | 0 |  |  |
|Chua-1-VC1-L-chunk-0070.smt2                                 |    0.031s | 20.764MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0390.smt2                                  |    0.031s | 20.836MiB| sat | 0 |  |  |
|exp-problem-10-2-chunk-0112.smt2                             |    0.031s | 20.812MiB| sat | 0 |  |  |
|Chua-2-VC2-L-chunk-0040.smt2                                 |    0.031s | 20.816MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0272.smt2                                |    0.031s | 20.608MiB| sat | 0 |  |  |
|Chua-2-VC2-L-chunk-0029.smt2                                 |    0.031s | 20.608MiB| sat | 0 |  |  |
|Chua-2-IL-U-chunk-0067.smt2                                  |    0.031s | 20.724MiB| sat | 0 |  |  |
|Chua-1-IL-L-chunk-0154.smt2                                  |    0.031s | 21.02MiB| sat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0116.smt2                                |    0.031s | 20.68MiB| sat | 0 |  |  |
|sqrt-problem-13-sqrt1-chunk-0015.smt2                        |    0.031s | 20.68MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.02.seq_lazy_lemmas_global_5.smt2   |    0.031s | 19.204MiB| unsat | 0 |  |  |
|MulliganEconomicsModel0018e.smt2                             |    0.031s | 20.56MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0481.smt2                      |    0.031s | 20.664MiB| unsat | 0 |  |  |
|Chua-1-VC1-L-chunk-0057.smt2                                 |    0.031s | 20.704MiB| sat | 0 |  |  |
|Chua-1-VC1-L-chunk-0081.smt2                                 |    0.031s | 20.836MiB| sat | 0 |  |  |
|exp-problem-10-3-chunk-0010.smt2                             |    0.031s | 20.688MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0043.smt2                                |    0.031s | 20.664MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0139.smt2                                  |    0.031s | 20.576MiB| sat | 0 |  |  |
|Lyapunov1a-chunk-0042.smt2                                   |    0.031s | 20.704MiB| sat | 0 |  |  |
|Chua-1-VC2-L-chunk-0077.smt2                                 |    0.031s | 20.988MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0342.smt2                      |    0.031s | 20.98MiB| unsat | 0 |  |  |
|sqrt-problem-13-sqrt1-chunk-0034.smt2                        |    0.031s | 20.832MiB| unsat | 0 |  |  |
|Chua-1-IL-U-chunk-0025.smt2                                  |    0.031s | 20.64MiB| sat | 0 |  |  |
|exp-problem-10-2-chunk-0194.smt2                             |    0.031s | 20.82MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0183.smt2                             |    0.031s | 20.8MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0623.smt2                                  |    0.031s | 20.808MiB| sat | 0 |  |  |
|exp-problem-10-2-chunk-0214.smt2                             |    0.031s | 20.824MiB| sat | 0 |  |  |
|atan-problem-2-weak-chunk-0157.smt2                          |    0.031s | 20.776MiB| sat | 0 |  |  |
|exp-problem-10-3-chunk-0021.smt2                             |    0.031s | 18.748MiB| unsat | 0 |  |  |
|Chua-1-IL-L-chunk-0117.smt2                                  |    0.031s | 20.956MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0434.smt2                                |    0.032s | 20.828MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0134.smt2                             |    0.032s | 20.812MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0100.smt2                      |    0.032s | 20.8MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0158.smt2                                |    0.032s | 20.792MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.01.seq_lazy_global_7.smt2          |    0.032s | 19.432MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0504.smt2                      |    0.032s | 20.88MiB| sat | 0 |  |  |
|polypaver-bench-exp-3d-chunk-0126.smt2                       |    0.032s | 20.948MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0020.smt2                      |    0.032s | 20.82MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0237.smt2                      |    0.032s | 20.616MiB| sat | 0 |  |  |
|sqrt-problem-Melquiond2-chunk-0081.smt2                      |    0.032s | 20.732MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0454.smt2                                |    0.032s | 20.92MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0099.smt2                                  |    0.032s | 20.664MiB| sat | 0 |  |  |
|Chua-1-IL-L-chunk-0143.smt2                                  |    0.032s | 20.612MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.10.seq_lazy_global_7.smt2          |    0.032s | 19.2MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0691.smt2                             |    0.032s | 20.888MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0510.smt2                             |    0.032s | 20.708MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0553.smt2                                  |    0.032s | 21.016MiB| sat | 0 |  |  |
|polypaver-sqrt43-int-3vars-chunk-0103.smt2                   |    0.032s | 20.66MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0323.smt2                             |    0.032s | 21.092MiB| sat | 0 |  |  |
|Chua-1-VC2-U-chunk-0123.smt2                                 |    0.032s | 20.776MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0196.smt2                      |    0.033s | 20.724MiB| sat | 0 |  |  |
|Chua-2-VC1-L-chunk-0097.smt2                                 |    0.033s | 20.756MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.01.seq_lazy_linear_enc_global_1.smt2 |    0.033s | 18.976MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0400.smt2                                  |    0.033s | 20.788MiB| sat | 0 |  |  |
|Chua-2-VC1-U-chunk-0087.smt2                                 |    0.033s | 21.34MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0326.smt2                                |    0.033s | 20.72MiB| unsat | 0 |  |  |
|sqrt-problem-Melquiond3-chunk-0018.smt2                      |    0.033s | 20.384MiB| sat | 0 |  |  |
|Chua-2-VC1-L-chunk-0108.smt2                                 |    0.033s | 20.744MiB| sat | 0 |  |  |
|MulliganEconomicsModel0013c.smt2                             |    0.033s | 20.536MiB| sat | 0 |  |  |
|Chua-2-IL-U-chunk-0053.smt2                                  |    0.033s | 20.48MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.10.qfree_global_9.smt2             |    0.033s | 19.336MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0310.smt2                                   |    0.033s | 20.796MiB| sat | 0 |  |  |
|Chua-2-VC2-U-chunk-0051.smt2                                 |    0.033s | 20.64MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0062.smt2                                   |    0.033s | 20.828MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0504.smt2                                |    0.033s | 20.8MiB| sat | 0 |  |  |
|asin-8-chunk-0024.smt2                                       |    0.033s | 20.812MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0444.smt2                             |    0.033s | 20.804MiB| sat | 0 |  |  |
|Chua-1-VC1-U-chunk-0044.smt2                                 |    0.033s | 20.744MiB| sat | 0 |  |  |
|exp-problem-10-3-chunk-0042.smt2                             |    0.033s | 20.768MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0025.smt2                                   |    0.033s | 20.76MiB| sat | 0 |  |  |
|sin-problem-7-chunk-0156.smt2                                |    0.033s | 20.856MiB| unsat | 0 |  |  |
|exp-problem-10-3-chunk-0096.smt2                             |    0.033s | 20.824MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0137.smt2                                   |    0.033s | 20.608MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0320.smt2                                  |    0.033s | 20.676MiB| sat | 0 |  |  |
|ball_count_2d_hill.01.seq_lazy_global_3.smt2                 |    0.033s | 19.112MiB| unsat | 0 |  |  |
|Chua-2-VC2-U-chunk-0029.smt2                                 |    0.033s | 20.9MiB| sat | 0 |  |  |
|sqrt-problem-13-sqrt1-chunk-0080.smt2                        |    0.033s | 20.696MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0148.smt2                                   |    0.033s | 20.94MiB| sat | 0 |  |  |
|polypaver-sqrt43-int-3vars-chunk-0086.smt2                   |    0.033s | 20.856MiB| sat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0091.smt2                        |    0.033s | 20.58MiB| sat | 0 |  |  |
|sin-problem-7-weak-chunk-0149.smt2                           |    0.033s | 20.596MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0242.smt2                                |    0.033s | 20.472MiB| sat | 0 |  |  |
|mbo_E6.smt2                                                  |    0.034s | 21.344MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0218.smt2                        |    0.034s | 20.984MiB| unsat | 0 |  |  |
|sin-problem-7-weak2-chunk-0044.smt2                          |    0.034s | 20.884MiB| unsat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0093.smt2                                |    0.034s | 20.78MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0423.smt2                                  |    0.034s | 20.596MiB| sat | 0 |  |  |
|Chua-1-VC2-U-chunk-0073.smt2                                 |    0.034s | 20.812MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0453.smt2                                  |    0.034s | 20.936MiB| unsat | 0 |  |  |
|ball_count_2d_plain.01.seq_lazy_linear_enc_lemmas_global_3.smt2 |    0.034s | 19.0MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0174.smt2                             |    0.034s | 20.704MiB| sat | 0 |  |  |
|ball_count_2d_hill.02.seq_lazy_linear_enc_lemmas_global_1.smt2 |    0.034s | 19.132MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0154.smt2                             |    0.034s | 20.668MiB| unsat | 0 |  |  |
|sin-344-3-weak-chunk-0017.smt2                               |    0.034s | 20.684MiB| sat | 0 |  |  |
|sin-problem-7-chunk-0129.smt2                                |    0.034s | 20.8MiB| unsat | 0 |  |  |
|sin-344-3-chunk-0029.smt2                                    |    0.034s | 20.76MiB| unsat | 0 |  |  |
|log-fun-ineq-g-chunk-0036.smt2                               |    0.034s | 18.712MiB| unsat | 0 |  |  |
|CONVOI2-chunk-0018.smt2                                      |    0.034s | 20.64MiB| sat | 0 |  |  |
|exp-problem-10-3-chunk-0128.smt2                             |    0.034s | 20.636MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0586.smt2                             |    0.034s | 20.7MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.01.qfree_global_9.smt2             |    0.034s | 19.436MiB| unsat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0224.smt2     |    0.034s | 20.756MiB| sat | 0 |  |  |
|sin-problem-7-weak2-chunk-0100.smt2                          |    0.034s | 21.272MiB| unsat | 0 |  |  |
|Chua-1-VC1-L-chunk-0132.smt2                                 |    0.034s | 20.684MiB| unsat | 0 |  |  |
|sin-problem-7-chunk-0091.smt2                                |    0.034s | 20.688MiB| sat | 0 |  |  |
|Chua-2-VC1-U-chunk-0071.smt2                                 |    0.034s | 20.78MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0086.smt2                                   |    0.034s | 20.968MiB| sat | 0 |  |  |
|cbrt-problem-3-weak-chunk-0069.smt2                          |    0.034s | 20.748MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0277.smt2                             |    0.034s | 21.168MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0080.smt2                        |    0.034s | 20.848MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.02.redlog_global_7.smt2            |    0.035s | 19.528MiB| unsat | 0 |  |  |
|ball_count_1d_plain.03.qfree_global_3.smt2                   |    0.035s | 21.072MiB| unsat | 0 |  |  |
|ball_count_2d_slope.05.seq_lazy_lemmas_global_1.smt2         |    0.035s | 19.228MiB| unsat | 0 |  |  |
|ball_count_2d_slope.01.seq_lazy_linear_enc_global_1.smt2     |    0.035s | 19.104MiB| unsat | 0 |  |  |
|ball_count_2d_plain.10.seq_lazy_lemmas_global_1.smt2         |    0.035s | 18.948MiB| unsat | 0 |  |  |
|Chua-2-IL-L-chunk-0072.smt2                                  |    0.035s | 18.828MiB| unsat | 0 |  |  |
|sin-problem-7-chunk-0257.smt2                                |    0.035s | 21.2MiB| sat | 0 |  |  |
|atan-problem-2-weak2-chunk-0093.smt2                         |    0.035s | 21.04MiB| sat | 0 |  |  |
|Chua-1-VC1-L-chunk-0160.smt2                                 |    0.035s | 20.76MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.10.seq_lazy_linear_enc_global_5.smt2 |    0.035s | 19.368MiB| unsat | 0 |  |  |
|Chua-2-VC1-U-chunk-0024.smt2                                 |    0.035s | 20.676MiB| sat | 0 |  |  |
|asin-8-vars4-chunk-0034.smt2                                 |    0.035s | 20.812MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0075.smt2                                |    0.035s | 20.848MiB| sat | 0 |  |  |
|ball_count_1d_plain.02.seq_lazy_linear_enc_lemmas_global_13.smt2 |    0.035s | 20.184MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0041.smt2                          |    0.035s | 20.716MiB| unsat | 0 |  |  |
|sin-problem-7-chunk-0208.smt2                                |    0.035s | 20.996MiB| sat | 0 |  |  |
|Chua-1-VC2-L-chunk-0050.smt2                                 |    0.035s | 20.636MiB| unsat | 0 |  |  |
|sin-problem-7-weak-chunk-0101.smt2                           |    0.035s | 20.648MiB| sat | 0 |  |  |
|ball_count_1d_plain.03.seq_lazy_lemmas_global_1.smt2         |    0.035s | 18.844MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0496.smt2                                |    0.035s | 20.904MiB| sat | 0 |  |  |
|ball_count_2d_plain.04.qfree_global_1.smt2                   |    0.036s | 19.024MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0179.smt2                          |    0.036s | 20.684MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0285.smt2                                |    0.036s | 20.776MiB| sat | 0 |  |  |
|sqrt-problem-13-vars5-chunk-0026.smt2                        |    0.036s | 20.764MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0102.smt2                             |    0.036s | 20.948MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0503.smt2                                  |    0.036s | 20.68MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0342.smt2                                   |    0.036s | 20.872MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0479.smt2                                |    0.036s | 21.02MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0260.smt2                                  |    0.036s | 20.656MiB| sat | 0 |  |  |
|ball_count_2d_plain.03.redlog_global_1.smt2                  |    0.036s | 19.048MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.02.seq_lazy_linear_enc_lemmas_global_3.smt2 |    0.036s | 19.204MiB| unsat | 0 |  |  |
|ball_count_2d_plain.01.seq_lazy_linear_enc_global_13.smt2    |    0.036s | 19.616MiB| unsat | 0 |  |  |
|Chua-1-IL-L-chunk-0054.smt2                                  |    0.036s | 18.796MiB| unsat | 0 |  |  |
|ball_count_2d_plain.01.seq_lazy_global_15.smt2               |    0.036s | 19.916MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0508.smt2                                |    0.036s | 20.76MiB| unsat | 0 |  |  |
|ball_count_2d_hill.02.seq_lazy_lemmas_global_7.smt2          |    0.036s | 19.628MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0168.smt2                          |    0.036s | 20.748MiB| sat | 0 |  |  |
|ball_count_1d_plain.10.qfree_global_5.smt2                   |    0.036s | 19.3MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.02.seq_lazy_lemmas_global_1.smt2   |    0.036s | 19.048MiB| unsat | 0 |  |  |
|ball_count_1d_plain.01.seq_lazy_lemmas_global_11.smt2        |    0.036s | 19.56MiB| unsat | 0 |  |  |
|ball_count_2d_hill.10.seq_lazy_linear_enc_lemmas_global_5.smt2 |    0.036s | 19.468MiB| unsat | 0 |  |  |
|Chua-2-VC2-U-chunk-0111.smt2                                 |    0.036s | 21.036MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.04.seq_lazy_lemmas_global_3.smt2   |    0.036s | 21.18MiB| unsat | 0 |  |  |
|CONVOI2-chunk-0031.smt2                                      |    0.036s | 20.764MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0493.smt2                      |    0.036s | 20.732MiB| sat | 0 |  |  |
|atan-problem-2-chunk-0024.smt2                               |    0.036s | 20.908MiB| sat | 0 |  |  |
|sin-problem-8-weak-chunk-0027.smt2                           |    0.036s | 20.792MiB| sat | 0 |  |  |
|sin-problem-7-chunk-0054.smt2                                |    0.037s | 20.764MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0278.smt2                      |    0.037s | 20.64MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0405.smt2                      |    0.037s | 20.896MiB| sat | 0 |  |  |
|sin-problem-7-chunk-0335.smt2                                |    0.037s | 20.996MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0026.smt2                                |    0.037s | 20.708MiB| unsat | 0 |  |  |
|ball_count_2d_plain.01.redlog_global_11.smt2                 |    0.037s | 19.948MiB| unsat | 0 |  |  |
|exp-problem-10-3-chunk-0168.smt2                             |    0.037s | 20.908MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0490.smt2                             |    0.037s | 20.824MiB| sat | 0 |  |  |
|polypaver-sqrt43-int-4vars-chunk-0026.smt2                   |    0.037s | 20.612MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0474.smt2                                |    0.037s | 21.032MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0057.smt2                                  |    0.037s | 20.66MiB| sat | 0 |  |  |
|gen-09.smt2                                                  |    0.037s | 20.82MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0330.smt2                      |    0.037s | 20.84MiB| sat | 0 |  |  |
|Chua-2-VC2-U-chunk-0086.smt2                                 |    0.037s | 20.968MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0100.smt2                                |    0.037s | 20.656MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.05.seq_lazy_linear_enc_lemmas_global_1.smt2 |    0.037s | 19.052MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0189.smt2                                |    0.037s | 20.836MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0255.smt2                             |    0.037s | 20.792MiB| sat | 0 |  |  |
|atan-problem-1-chunk-0058.smt2                               |    0.037s | 20.736MiB| sat | 0 |  |  |
|asin-8-vars4-chunk-0046.smt2                                 |    0.037s | 20.764MiB| unsat | 0 |  |  |
|ball_count_2d_hill.02.seq_lazy_global_3.smt2                 |    0.037s | 19.232MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0030.smt2                                |    0.037s | 20.764MiB| sat | 0 |  |  |
|polypaver-bench-exp-3d-chunk-0028.smt2                       |    0.037s | 20.796MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0310.smt2                                  |    0.037s | 20.88MiB| sat | 0 |  |  |
|cbrt-problem-3-weak-chunk-0084.smt2                          |    0.037s | 20.812MiB| unsat | 0 |  |  |
|sin-problem-7-chunk-0143.smt2                                |    0.037s | 20.768MiB| sat | 0 |  |  |
|exp-problem-10-2-chunk-0204.smt2                             |    0.037s | 20.84MiB| unsat | 0 |  |  |
|ball_count_1d_plain.05.redlog_global_1.smt2                  |    0.037s | 18.848MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0572.smt2                                |    0.037s | 20.68MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0168.smt2                                |    0.037s | 20.632MiB| sat | 0 |  |  |
|ball_count_1d_plain.10.seq_lazy_lemmas_global_11.smt2        |    0.038s | 19.632MiB| unsat | 0 |  |  |
|ball_count_2d_slope.01.seq_lazy_global_7.smt2                |    0.038s | 19.848MiB| unsat | 0 |  |  |
|Chua-2-VC1-U-chunk-0013.smt2                                 |    0.038s | 20.752MiB| sat | 0 |  |  |
|Chua-1-VC1-L-chunk-0035.smt2                                 |    0.038s | 20.62MiB| unsat | 0 |  |  |
|Chua-1-IL-U-chunk-0063.smt2                                  |    0.038s | 20.848MiB| sat | 0 |  |  |
|sqrt-problem-Melquiond2-chunk-0023.smt2                      |    0.038s | 20.784MiB| sat | 0 |  |  |
|exp-problem-10-3-chunk-0158.smt2                             |    0.038s | 20.644MiB| unsat | 0 |  |  |
|Chua-2-IL-U-chunk-0032.smt2                                  |    0.038s | 20.9MiB| sat | 0 |  |  |
|sin-problem-7-chunk-0221.smt2                                |    0.038s | 20.88MiB| sat | 0 |  |  |
|cbrt-problem-3-weak-chunk-0108.smt2                          |    0.038s | 20.696MiB| unsat | 0 |  |  |
|sin-problem-7-chunk-0182.smt2                                |    0.038s | 20.676MiB| sat | 0 |  |  |
|MulliganEconomicsModel0085a.smt2                             |    0.038s | 20.624MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0252.smt2                                |    0.038s | 20.816MiB| unsat | 0 |  |  |
|ball_count_2d_hill.02.seq_lazy_linear_enc_lemmas_global_5.smt2 |    0.038s | 19.4MiB| unsat | 0 |  |  |
|Chua-2-VC2-U-chunk-0039.smt2                                 |    0.038s | 20.812MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0339.smt2                                |    0.038s | 20.752MiB| sat | 0 |  |  |
|sin-problem-7-chunk-0105.smt2                                |    0.038s | 20.824MiB| unsat | 0 |  |  |
|sqrt-problem-12vars3-chunk-0025.smt2                         |    0.038s | 20.64MiB| unsat | 0 |  |  |
|Chua-2-VC2-L-chunk-0052.smt2                                 |    0.038s | 20.62MiB| unsat | 0 |  |  |
|ball_count_1d_plain.01.qfree_global_1.smt2                   |    0.038s | 18.892MiB| unsat | 0 |  |  |
|ball_count_2d_hill.05.seq_lazy_linear_enc_lemmas_global_1.smt2 |    0.038s | 19.072MiB| unsat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0078.smt2     |    0.038s | 21.14MiB| sat | 0 |  |  |
|ball_count_2d_plain.02.seq_lazy_global_5.smt2                |    0.038s | 19.112MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0111.smt2                        |    0.038s | 20.948MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0464.smt2                                |    0.038s | 20.712MiB| unsat | 0 |  |  |
|Chua-2-VC1-L-chunk-0036.smt2                                 |    0.039s | 20.768MiB| sat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0181.smt2                        |    0.039s | 18.868MiB| unsat | 0 |  |  |
|MulliganEconomicsModel0030e.smt2                             |    0.039s | 20.804MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0456.smt2                      |    0.039s | 18.96MiB| unsat | 0 |  |  |
|ball_count_2d_hill.02.seq_lazy_lemmas_global_11.smt2         |    0.039s | 20.124MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0018.smt2                                |    0.039s | 20.764MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0433.smt2                                  |    0.039s | 20.964MiB| sat | 0 |  |  |
|sin-problem-7-weak-chunk-0073.smt2                           |    0.039s | 20.796MiB| sat | 0 |  |  |
|ball_count_1d_plain.02.qfree_global_9.smt2                   |    0.039s | 19.384MiB| unsat | 0 |  |  |
|ball_count_2d_plain.02.seq_lazy_linear_enc_lemmas_global_7.smt2 |    0.039s | 19.516MiB| unsat | 0 |  |  |
|Chua-1-IL-L-chunk-0129.smt2                                  |    0.039s | 18.78MiB| unsat | 0 |  |  |
|Chua-2-VC2-L-chunk-0062.smt2                                 |    0.039s | 20.764MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0370.smt2                                |    0.039s | 20.808MiB| unsat | 0 |  |  |
|exp-problem-10-3-chunk-0106.smt2                             |    0.039s | 20.9MiB| sat | 0 |  |  |
|exp-problem-10-3-chunk-0063.smt2                             |    0.039s | 20.764MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0363.smt2                             |    0.039s | 20.864MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0607.smt2                                |    0.039s | 21.0MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0144.smt2                      |    0.040s | 20.8MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.01.seq_lazy_global_11.smt2         |    0.040s | 19.488MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0700.smt2                                |    0.040s | 20.88MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0146.smt2                          |    0.040s | 20.6MiB| sat | 0 |  |  |
|ball_count_2d_plain.02.qfree_global_7.smt2                   |    0.040s | 19.44MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0179.smt2                                  |    0.040s | 20.72MiB| sat | 0 |  |  |
|asin-8-vars4-chunk-0019.smt2                                 |    0.040s | 20.612MiB| sat | 0 |  |  |
|ball_count_2d_slope.04.seq_lazy_linear_enc_lemmas_global_7.smt2 |    0.040s | 19.948MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0651.smt2                             |    0.040s | 20.78MiB| unsat | 0 |  |  |
|MulliganEconomicsModel0063e.smt2                             |    0.040s | 20.648MiB| sat | 0 |  |  |
|sin-344-4-chunk-0050.smt2                                    |    0.040s | 21.232MiB| sat | 0 |  |  |
|etcs_braking_2.01.seq_lazy_lemmas_global_1.smt2              |    0.040s | 20.948MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0596.smt2                             |    0.040s | 20.74MiB| unsat | 0 |  |  |
|sin-problem-8-chunk-0043.smt2                                |    0.040s | 20.816MiB| sat | 0 |  |  |
|ball_count_2d_plain.10.qfree_global_3.smt2                   |    0.040s | 19.128MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0139.smt2                                |    0.040s | 20.892MiB| sat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0202.smt2                        |    0.040s | 21.056MiB| sat | 0 |  |  |
|sqrt-problem-12vars3-chunk-0081.smt2                         |    0.040s | 20.776MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0077.smt2                                  |    0.040s | 20.8MiB| unsat | 0 |  |  |
|Chua-1-IL-L-chunk-0090.smt2                                  |    0.041s | 20.828MiB| sat | 0 |  |  |
|exp-problem-10-2-chunk-0016.smt2                             |    0.041s | 20.728MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0513.smt2                                  |    0.041s | 20.816MiB| sat | 0 |  |  |
|ball_count_2d_slope.10.seq_lazy_global_11.smt2               |    0.041s | 20.316MiB| unsat | 0 |  |  |
|atan-problem-2-weakT-chunk-0054.smt2                         |    0.041s | 20.752MiB| sat | 0 |  |  |
|ball_count_1d_plain.03.seq_lazy_linear_enc_lemmas_global_3.smt2 |    0.041s | 20.956MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0541.smt2                                |    0.041s | 20.776MiB| sat | 0 |  |  |
|ball_count_2d_slope.10.seq_lazy_global_7.smt2                |    0.041s | 19.74MiB| unsat | 0 |  |  |
|Chua-2-IL-L-chunk-0082.smt2                                  |    0.041s | 20.688MiB| sat | 0 |  |  |
|ball_count_2d_slope.05.seq_lazy_linear_enc_lemmas_global_3.smt2 |    0.041s | 19.484MiB| unsat | 0 |  |  |
|ball_count_1d_plain.03.seq_lazy_lemmas_global_5.smt2         |    0.041s | 21.476MiB| unsat | 0 |  |  |
|atan-problem-2-weak2-chunk-0082.smt2                         |    0.041s | 18.9MiB| unsat | 0 |  |  |
|sin-problem-10-3-chunk-0033.smt2                             |    0.041s | 20.656MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.02.seq_lazy_linear_enc_global_13.smt2 |    0.041s | 19.716MiB| unsat | 0 |  |  |
|atan-problem-2-weakT-chunk-0041.smt2                         |    0.041s | 20.948MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0340.smt2                                  |    0.041s | 20.772MiB| sat | 0 |  |  |
|ball_count_2d_plain.10.seq_lazy_linear_enc_global_9.smt2     |    0.041s | 19.408MiB| unsat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0143.smt2                                |    0.041s | 21.02MiB| sat | 0 |  |  |
|ball_count_2d_slope.10.seq_lazy_linear_enc_global_1.smt2     |    0.041s | 19.132MiB| unsat | 0 |  |  |
|Chua-1-VC1-U-chunk-0056.smt2                                 |    0.041s | 20.8MiB| sat | 0 |  |  |
|ball_count_2d_hill.03.seq_lazy_global_3.smt2                 |    0.041s | 21.672MiB| unsat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0077.smt2                                |    0.041s | 20.784MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0344.smt2                             |    0.041s | 21.024MiB| sat | 0 |  |  |
|ball_count_1d_plain.02.seq_lazy_global_7.smt2                |    0.042s | 19.26MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0199.smt2                                  |    0.042s | 20.66MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0414.smt2                                |    0.042s | 21.008MiB| sat | 0 |  |  |
|ball_count_1d_plain.01.seq_lazy_linear_enc_lemmas_global_5.smt2 |    0.042s | 19.22MiB| unsat | 0 |  |  |
|atan-problem-2-weak2-chunk-0103.smt2                         |    0.042s | 20.768MiB| sat | 0 |  |  |
|Arthan1A-chunk-0020.smt2                                     |    0.042s | 20.608MiB| sat | 0 |  |  |
|atan-problem-2-chunk-0011.smt2                               |    0.042s | 20.808MiB| sat | 0 |  |  |
|atan-problem-2-weak-chunk-0087.smt2                          |    0.042s | 20.856MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0250.smt2                      |    0.042s | 20.66MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0044.smt2                                |    0.042s | 18.76MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0597.smt2                                |    0.042s | 20.984MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.03.qfree_global_7.smt2             |    0.042s | 21.2MiB| unsat | 0 |  |  |
|matrix-1-all-8.smt2                                          |    0.042s | 20.964MiB| sat | 0 |  |  |
|ball_count_1d_plain.01.qfree_global_5.smt2                   |    0.042s | 19.272MiB| unsat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0027.smt2                                |    0.042s | 20.824MiB| sat | 0 |  |  |
|ball_count_2d_plain.02.seq_lazy_global_1.smt2                |    0.042s | 19.012MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.05.seq_lazy_global_3.smt2          |    0.042s | 20.884MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.01.seq_lazy_linear_enc_global_5.smt2 |    0.042s | 19.136MiB| unsat | 0 |  |  |
|ball_count_1d_plain.05.seq_lazy_lemmas_global_3.smt2         |    0.042s | 21.072MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0312.smt2                             |    0.042s | 20.844MiB| sat | 0 |  |  |
|sqrt-problem-Melquiond2-chunk-0059.smt2                      |    0.042s | 20.76MiB| sat | 0 |  |  |
|atan-problem-2-weak-chunk-0014.smt2                          |    0.042s | 20.74MiB| sat | 0 |  |  |
|ball_count_1d_plain.10.seq_lazy_linear_enc_lemmas_global_1.smt2 |    0.042s | 18.864MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0413.smt2                                  |    0.043s | 20.876MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0198.smt2                                |    0.043s | 20.636MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0444.smt2                                |    0.043s | 20.776MiB| sat | 0 |  |  |
|ball_count_2d_plain.02.seq_lazy_lemmas_global_13.smt2        |    0.043s | 19.824MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0560.smt2                                |    0.043s | 20.776MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0307.smt2                                |    0.043s | 20.788MiB| unsat | 0 |  |  |
|sqrt-circles-2-chunk-0015.smt2                               |    0.043s | 20.844MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.01.seq_lazy_linear_enc_lemmas_global_13.smt2 |    0.043s | 19.912MiB| unsat | 0 |  |  |
|ball_count_2d_plain.10.seq_lazy_linear_enc_global_13.smt2    |    0.043s | 19.644MiB| unsat | 0 |  |  |
|ball_count_2d_slope.04.seq_lazy_linear_enc_lemmas_global_11.smt2 |    0.043s | 20.42MiB| unsat | 0 |  |  |
|ball_count_2d_plain.01.seq_lazy_lemmas_global_1.smt2         |    0.043s | 18.924MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0240.smt2                                  |    0.043s | 20.748MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.02.seq_lazy_linear_enc_global_9.smt2 |    0.043s | 19.488MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0285.smt2                             |    0.043s | 20.672MiB| unsat | 0 |  |  |
|ball_count_2d_hill.10.seq_lazy_lemmas_global_7.smt2          |    0.043s | 19.648MiB| unsat | 0 |  |  |
|ball_count_1d_plain.05.redlog_global_5.smt2                  |    0.044s | 21.144MiB| unsat | 0 |  |  |
|Chua-1-IL-L-chunk-0104.smt2                                  |    0.044s | 20.848MiB| unsat | 0 |  |  |
|ball_count_1d_plain.02.seq_lazy_linear_enc_global_1.smt2     |    0.044s | 19.104MiB| unsat | 0 |  |  |
|MulliganEconomicsModel0006a.smt2                             |    0.044s | 20.648MiB| sat | 0 |  |  |
|atan-problem-2-weak2-chunk-0043.smt2                         |    0.044s | 20.768MiB| unsat | 0 |  |  |
|ball_count_2d_hill.01.seq_lazy_lemmas_global_11.smt2         |    0.044s | 20.116MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0028.smt2                          |    0.044s | 20.696MiB| sat | 0 |  |  |
|atan-problem-2-chunk-0080.smt2                               |    0.044s | 20.64MiB| unsat | 0 |  |  |
|sin-problem-10-3-chunk-0023.smt2                             |    0.044s | 20.84MiB| unsat | 0 |  |  |
|Chua-1-VC1-L-chunk-0120.smt2                                 |    0.044s | 20.796MiB| unsat | 0 |  |  |
|exp-problem-10-3-chunk-0118.smt2                             |    0.044s | 20.78MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0483.smt2                                  |    0.044s | 20.724MiB| sat | 0 |  |  |
|atan-problem-1-chunk-0081.smt2                               |    0.044s | 20.764MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0415.smt2                      |    0.044s | 20.664MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0300.smt2                                  |    0.044s | 20.512MiB| sat | 0 |  |  |
|atan-problem-2-weak-chunk-0189.smt2                          |    0.044s | 20.608MiB| sat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0036.smt2     |    0.044s | 20.608MiB| unsat | 0 |  |  |
|polypaver-bench-exp-3d-chunk-0072.smt2                       |    0.044s | 20.828MiB| sat | 0 |  |  |
|ball_count_2d_plain.10.seq_lazy_global_15.smt2               |    0.044s | 19.936MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0290.smt2                             |    0.044s | 20.844MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0711.smt2                             |    0.045s | 20.728MiB| sat | 0 |  |  |
|ball_count_1d_plain.01.seq_lazy_linear_enc_lemmas_global_1.smt2 |    0.045s | 18.964MiB| unsat | 0 |  |  |
|ball_count_2d_slope.02.seq_lazy_linear_enc_global_15.smt2    |    0.045s | 20.556MiB| unsat | 0 |  |  |
|atan-problem-2-weakT-chunk-0030.smt2                         |    0.045s | 20.656MiB| unsat | 0 |  |  |
|ball_count_1d_plain.10.seq_lazy_global_3.smt2                |    0.045s | 18.972MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0212.smt2                          |    0.045s | 20.748MiB| sat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0024.smt2     |    0.045s | 21.048MiB| sat | 0 |  |  |
|ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_5.smt2 |    0.045s | 19.3MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0134.smt2                          |    0.045s | 20.768MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0230.smt2                                  |    0.045s | 20.736MiB| sat | 0 |  |  |
|atan-problem-2-weak2-chunk-0120.smt2                         |    0.045s | 20.772MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0701.smt2                             |    0.045s | 19.364MiB| unsat | 0 |  |  |
|sqrt-problem-Melquiond2-chunk-0034.smt2                      |    0.045s | 20.664MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0484.smt2                                |    0.045s | 21.284MiB| sat | 0 |  |  |
|sin-problem-7-weak-chunk-0160.smt2                           |    0.046s | 20.86MiB| sat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0230.smt2                                |    0.046s | 20.748MiB| sat | 0 |  |  |
|Chua-2-IL-U-chunk-0094.smt2                                  |    0.046s | 21.172MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0619.smt2                             |    0.046s | 20.424MiB| sat | 0 |  |  |
|Chua-1-VC1-U-chunk-0032.smt2                                 |    0.046s | 20.528MiB| sat | 0 |  |  |
|atan-problem-2-chunk-0059.smt2                               |    0.046s | 20.508MiB| sat | 0 |  |  |
|sqrt-problem-12vars3-chunk-0055.smt2                         |    0.046s | 20.8MiB| sat | 0 |  |  |
|ball_count_1d_plain.01.seq_lazy_lemmas_global_7.smt2         |    0.046s | 19.412MiB| unsat | 0 |  |  |
|ball_count_1d_plain.02.qfree_global_13.smt2                  |    0.046s | 19.736MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0246.smt2                                   |    0.046s | 20.868MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0079.smt2                             |    0.046s | 18.728MiB| unsat | 0 |  |  |
|polypaver-bench-exp-3d-chunk-0085.smt2                       |    0.046s | 20.764MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0545.smt2                             |    0.046s | 20.776MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0110.smt2                                |    0.046s | 21.02MiB| sat | 0 |  |  |
|ball_count_1d_plain.10.redlog_global_13.smt2                 |    0.046s | 19.696MiB| unsat | 0 |  |  |
|polypaver-sqrt43-int-3vars-chunk-0029.smt2                   |    0.046s | 20.756MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0223.smt2                                |    0.046s | 21.108MiB| sat | 0 |  |  |
|sin-problem-10-2-chunk-0010.smt2                             |    0.046s | 20.604MiB| sat | 0 |  |  |
|matrix-1-all-10.smt2                                         |    0.046s | 20.8MiB| sat | 0 |  |  |
|sqrt-problem-Melquiond2-chunk-0091.smt2                      |    0.046s | 20.64MiB| unsat | 0 |  |  |
|atan-problem-1-chunk-0091.smt2                               |    0.046s | 20.652MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0241.smt2                             |    0.046s | 20.76MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0401.smt2                                |    0.046s | 20.644MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0227.smt2                      |    0.047s | 20.88MiB| sat | 0 |  |  |
|sqrt-problem-12vars3-chunk-0010.smt2                         |    0.047s | 20.656MiB| sat | 0 |  |  |
|ball_count_2d_slope.01.seq_lazy_linear_enc_lemmas_global_13.smt2 |    0.047s | 20.872MiB| unsat | 0 |  |  |
|ball_count_1d_plain.01.redlog_global_13.smt2                 |    0.047s | 19.848MiB| unsat | 0 |  |  |
|Chua-2-VC1-L-chunk-0086.smt2                                 |    0.047s | 18.82MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0380.smt2                                |    0.047s | 20.976MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0155.smt2                                |    0.047s | 20.828MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0379.smt2                      |    0.047s | 21.016MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0338.smt2                                |    0.047s | 20.656MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0265.smt2                      |    0.047s | 18.76MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0218.smt2                             |    0.047s | 20.808MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0067.smt2                                  |    0.047s | 20.948MiB| unsat | 0 |  |  |
|ball_count_1d_plain.02.seq_lazy_linear_enc_lemmas_global_9.smt2 |    0.047s | 19.468MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0320.smt2                      |    0.047s | 20.74MiB| sat | 0 |  |  |
|sin-problem-8-weak-chunk-0056.smt2                           |    0.047s | 20.764MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0159.smt2                                  |    0.047s | 20.784MiB| sat | 0 |  |  |
|Chua-1-VC2-U-chunk-0113.smt2                                 |    0.047s | 20.768MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0350.smt2                                  |    0.047s | 18.788MiB| unsat | 0 |  |  |
|MulliganEconomicsModel0024a.smt2                             |    0.047s | 20.94MiB| sat | 0 |  |  |
|sin-problem-7-weak2-chunk-0075.smt2                          |    0.047s | 20.756MiB| sat | 0 |  |  |
|Chua-2-IL-U-chunk-0009.smt2                                  |    0.047s | 18.796MiB| unsat | 0 |  |  |
|Lyapunov1a-chunk-0032.smt2                                   |    0.048s | 20.628MiB| sat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0137.smt2     |    0.048s | 20.764MiB| unsat | 0 |  |  |
|sin-problem-7-weak2-chunk-0123.smt2                          |    0.048s | 20.808MiB| sat | 0 |  |  |
|exp-problem-10-2-chunk-0028.smt2                             |    0.048s | 20.868MiB| sat | 0 |  |  |
|ball_count_1d_plain.03.redlog_global_7.smt2                  |    0.048s | 21.436MiB| unsat | 0 |  |  |
|ball_count_1d_plain.02.seq_lazy_global_11.smt2               |    0.048s | 19.648MiB| unsat | 0 |  |  |
|asin-8-chunk-0053.smt2                                       |    0.048s | 20.932MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0473.smt2                                  |    0.048s | 20.928MiB| sat | 0 |  |  |
|ball_count_2d_hill.01.redlog_global_9.smt2                   |    0.048s | 20.576MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0566.smt2                             |    0.048s | 20.872MiB| sat | 0 |  |  |
|ball_count_2d_plain.05.seq_lazy_linear_enc_global_5.smt2     |    0.048s | 21.156MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0184.smt2                             |    0.048s | 20.66MiB| sat | 0 |  |  |
|Chua-1-IL-L-chunk-0066.smt2                                  |    0.048s | 20.764MiB| unsat | 0 |  |  |
|ball_count_2d_slope.02.seq_lazy_lemmas_global_7.smt2         |    0.048s | 20.312MiB| unsat | 0 |  |  |
|ball_count_1d_plain.05.seq_lazy_linear_enc_global_7.smt2     |    0.048s | 21.352MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0074.smt2                                   |    0.048s | 20.652MiB| sat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0025.smt2                        |    0.048s | 20.816MiB| sat | 0 |  |  |
|Chua-1-VC1-U-chunk-0083.smt2                                 |    0.049s | 21.052MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0657.smt2                                |    0.049s | 21.016MiB| unsat | 0 |  |  |
|sin-problem-7-weak-chunk-0085.smt2                           |    0.049s | 20.792MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0087.smt2                      |    0.049s | 20.72MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0328.smt2                                |    0.049s | 20.764MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0316.smt2                                |    0.049s | 18.912MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0295.smt2                             |    0.049s | 20.788MiB| sat | 0 |  |  |
|atan-problem-2-weak2-chunk-0056.smt2                         |    0.049s | 20.768MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0169.smt2                                  |    0.049s | 20.76MiB| sat | 0 |  |  |
|Chua-2-VC1-U-chunk-0098.smt2                                 |    0.049s | 21.092MiB| unsat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0053.smt2                                |    0.049s | 20.764MiB| sat | 0 |  |  |
|ball_count_2d_plain.04.seq_lazy_lemmas_global_7.smt2         |    0.049s | 21.52MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0346.smt2                             |    0.049s | 20.992MiB| unsat | 0 |  |  |
|ball_count_2d_plain.03.seq_lazy_linear_enc_global_11.smt2    |    0.049s | 22.064MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0306.smt2                                |    0.049s | 20.728MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0250.smt2                                  |    0.049s | 20.9MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0027.smt2                                  |    0.049s | 20.776MiB| sat | 0 |  |  |
|atan-problem-1-chunk-0022.smt2                               |    0.049s | 20.764MiB| sat | 0 |  |  |
|ball_count_1d_plain.02.seq_lazy_linear_enc_global_5.smt2     |    0.049s | 19.148MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0370.smt2                                  |    0.049s | 20.82MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0126.smt2                             |    0.049s | 20.88MiB| sat | 0 |  |  |
|asin-8-chunk-0039.smt2                                       |    0.049s | 20.676MiB| sat | 0 |  |  |
|polypaver-bench-exp-3d-chunk-0109.smt2                       |    0.049s | 20.856MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0536.smt2                                |    0.049s | 20.804MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0096.smt2                                   |    0.049s | 20.708MiB| sat | 0 |  |  |
|atan-problem-1-weak-chunk-0020.smt2                          |    0.049s | 20.764MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0267.smt2                             |    0.050s | 20.788MiB| sat | 0 |  |  |
|sqrt-problem-Melquiond2-chunk-0010.smt2                      |    0.050s | 20.64MiB| sat | 0 |  |  |
|ball_count_2d_plain.04.qfree_global_5.smt2                   |    0.050s | 21.124MiB| unsat | 0 |  |  |
|sin-problem-7-weak-chunk-0126.smt2                           |    0.050s | 20.804MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0301.smt2                             |    0.050s | 20.688MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0200.smt2                                   |    0.050s | 20.844MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0671.smt2                             |    0.050s | 21.016MiB| sat | 0 |  |  |
|Chua-2-VC2-L-chunk-0013.smt2                                 |    0.050s | 20.584MiB| sat | 0 |  |  |
|Chua-2-IL-U-chunk-0107.smt2                                  |    0.050s | 20.94MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0352.smt2                      |    0.050s | 20.848MiB| sat | 0 |  |  |
|exp-problem-10-2-chunk-0164.smt2                             |    0.050s | 20.788MiB| sat | 0 |  |  |
|Chua-1-VC1-L-chunk-0093.smt2                                 |    0.050s | 20.672MiB| sat | 0 |  |  |
|Chua-1-VC2-L-chunk-0039.smt2                                 |    0.050s | 20.796MiB| unsat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0216.smt2                                |    0.050s | 21.096MiB| sat | 0 |  |  |
|exp-problem-10-3-chunk-0032.smt2                             |    0.050s | 20.872MiB| sat | 0 |  |  |
|atan-problem-2-chunk-0070.smt2                               |    0.050s | 20.668MiB| unsat | 0 |  |  |
|atan-problem-2-chunk-0107.smt2                               |    0.051s | 20.836MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.10.seq_lazy_linear_enc_global_1.smt2 |    0.051s | 18.86MiB| unsat | 0 |  |  |
|Chua-2-IL-L-chunk-0037.smt2                                  |    0.051s | 20.612MiB| sat | 0 |  |  |
|Chua-1-IL-U-chunk-0038.smt2                                  |    0.051s | 20.636MiB| sat | 0 |  |  |
|Chua-2-IL-L-chunk-0047.smt2                                  |    0.051s | 18.852MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0606.smt2                             |    0.051s | 21.14MiB| unsat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0130.smt2                                |    0.051s | 20.652MiB| unsat | 0 |  |  |
|sin-problem-8-weak-chunk-0044.smt2                           |    0.051s | 20.764MiB| sat | 0 |  |  |
|ball_count_2d_plain.10.seq_lazy_lemmas_global_5.smt2         |    0.051s | 19.344MiB| unsat | 0 |  |  |
|Chua-1-VC2-U-chunk-0086.smt2                                 |    0.051s | 20.516MiB| sat | 0 |  |  |
|cbrt-problem-3-weak-chunk-0023.smt2                          |    0.051s | 20.8MiB| sat | 0 |  |  |
|mbo_E21E27.smt2                                              |    0.051s | 20.936MiB| unsat | 0 |  |  |
|sin-problem-7-chunk-0273.smt2                                |    0.051s | 20.908MiB| sat | 0 |  |  |
|exp-problem-10-3-chunk-0138.smt2                             |    0.051s | 20.884MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0480.smt2                             |    0.051s | 20.772MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0090.smt2                             |    0.051s | 20.796MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0335.smt2                             |    0.052s | 21.004MiB| unsat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0117.smt2     |    0.052s | 20.872MiB| unsat | 0 |  |  |
|atan-problem-2-chunk-0047.smt2                               |    0.052s | 20.884MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0543.smt2                                  |    0.052s | 20.836MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0633.smt2                                  |    0.052s | 20.904MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0421.smt2                             |    0.052s | 20.676MiB| sat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0241.smt2     |    0.052s | 20.876MiB| sat | 0 |  |  |
|atan-problem-1-chunk-0071.smt2                               |    0.052s | 20.624MiB| sat | 0 |  |  |
|matrix-1-all-47.smt2                                         |    0.052s | 20.652MiB| unsat | 0 |  |  |
|ball_count_2d_plain.02.seq_lazy_linear_enc_lemmas_global_11.smt2 |    0.052s | 20.048MiB| unsat | 0 |  |  |
|sin-problem-7-chunk-0283.smt2                                |    0.052s | 21.216MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0234.smt2                             |    0.052s | 20.768MiB| sat | 0 |  |  |
|ball_count_2d_hill.10.redlog_global_9.smt2                   |    0.052s | 20.68MiB| unsat | 0 |  |  |
|ball_count_2d_hill.02.redlog_global_9.smt2                   |    0.052s | 20.668MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.01.seq_lazy_linear_enc_lemmas_global_9.smt2 |    0.053s | 19.484MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.04.seq_lazy_global_9.smt2          |    0.053s | 21.436MiB| unsat | 0 |  |  |
|ball_count_1d_plain.10.seq_lazy_linear_enc_global_15.smt2    |    0.053s | 19.836MiB| unsat | 0 |  |  |
|Chua-2-IL-L-chunk-0093.smt2                                  |    0.053s | 20.972MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0126.smt2                                |    0.053s | 20.576MiB| sat | 0 |  |  |
|ball_count_2d_plain.05.seq_lazy_global_11.smt2               |    0.053s | 21.656MiB| unsat | 0 |  |  |
|ball_count_2d_slope.02.seq_lazy_global_3.smt2                |    0.053s | 19.236MiB| unsat | 0 |  |  |
|atan-problem-2-sqrt-weak-chunk-0050.smt2                     |    0.053s | 20.796MiB| sat | 0 |  |  |
|atan-problem-2-sqrt-chunk-0039.smt2                          |    0.053s | 20.736MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0210.smt2                                  |    0.053s | 20.768MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0409.smt2                             |    0.053s | 20.752MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0121.smt2                                |    0.053s | 20.612MiB| unsat | 0 |  |  |
|ball_count_2d_plain.04.seq_lazy_global_3.smt2                |    0.053s | 20.792MiB| unsat | 0 |  |  |
|sqrt-problem-12vars3-chunk-0068.smt2                         |    0.053s | 20.5MiB| sat | 0 |  |  |
|sin-problem-7-chunk-0348.smt2                                |    0.053s | 20.768MiB| sat | 0 |  |  |
|ball_count_1d_plain.04.seq_lazy_linear_enc_lemmas_global_7.smt2 |    0.054s | 21.256MiB| unsat | 0 |  |  |
|Chua-1-VC2-U-chunk-0050.smt2                                 |    0.054s | 20.624MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0213.smt2                                   |    0.054s | 20.684MiB| sat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0173.smt2     |    0.054s | 20.812MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0613.smt2                                  |    0.054s | 21.28MiB| sat | 0 |  |  |
|sin-problem-7-chunk-0117.smt2                                |    0.054s | 20.82MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0556.smt2                                |    0.054s | 20.716MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0360.smt2                                  |    0.054s | 20.872MiB| sat | 0 |  |  |
|atan-problem-2-weak-chunk-0076.smt2                          |    0.054s | 20.812MiB| unsat | 0 |  |  |
|atan-problem-2-sqrt-weak-chunk-0065.smt2                     |    0.054s | 20.616MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0463.smt2                                  |    0.054s | 20.764MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0190.smt2                                   |    0.054s | 21.02MiB| sat | 0 |  |  |
|ball_count_1d_plain.02.seq_lazy_lemmas_global_15.smt2        |    0.054s | 19.888MiB| unsat | 0 |  |  |
|cbrt-problem-3-chunk-0055.smt2                               |    0.054s | 20.684MiB| unsat | 0 |  |  |
|atan-problem-2-weak2-chunk-0008.smt2                         |    0.054s | 20.572MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0563.smt2                                  |    0.054s | 21.1MiB| sat | 0 |  |  |
|exp-361-neg-6-e-chunk-0216.smt2                              |    0.054s | 20.824MiB| sat | 0 |  |  |
|InVarSynth_PostfixIncrementDecrement.c_Iteration3_0.smt2     |    0.055s | 21.1MiB| unsat | 0 |  |  |
|Chua-2-IL-U-chunk-0083.smt2                                  |    0.055s | 21.244MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0358.smt2                                |    0.055s | 20.86MiB| sat | 0 |  |  |
|atan-problem-2-chunk-0037.smt2                               |    0.055s | 20.708MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0149.smt2                                  |    0.055s | 20.724MiB| unsat | 0 |  |  |
|sin-problem-7-chunk-0233.smt2                                |    0.055s | 21.244MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0288.smt2                      |    0.055s | 20.764MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0600.smt2                                |    0.055s | 20.776MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.02.qfree_global_3.smt2             |    0.055s | 19.168MiB| unsat | 0 |  |  |
|Chua-2-VC1-U-chunk-0045.smt2                                 |    0.055s | 18.792MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.03.qfree_global_11.smt2            |    0.055s | 22.172MiB| unsat | 0 |  |  |
|atan-problem-2-sqrt-weak-chunk-0032.smt2                     |    0.055s | 21.128MiB| unsat | 0 |  |  |
|Chua-1-VC1-U-chunk-0072.smt2                                 |    0.055s | 20.708MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0433.smt2                             |    0.055s | 20.88MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0085.smt2                                |    0.055s | 20.88MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.04.qfree_global_15.smt2            |    0.056s | 22.156MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0457.smt2                             |    0.056s | 20.696MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.03.seq_lazy_linear_enc_lemmas_global_11.smt2 |    0.056s | 21.732MiB| unsat | 0 |  |  |
|cbrt-problem-3-chunk-0028.smt2                               |    0.056s | 20.764MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0121.smt2                        |    0.056s | 20.988MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0374.smt2                             |    0.056s | 21.032MiB| unsat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0190.smt2     |    0.056s | 20.592MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0275.smt2                             |    0.056s | 20.76MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0245.smt2                             |    0.056s | 20.764MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.03.seq_lazy_linear_enc_global_3.smt2 |    0.056s | 21.02MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0220.smt2                                  |    0.056s | 18.856MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0222.smt2                          |    0.056s | 20.688MiB| sat | 0 |  |  |
|atan-problem-2-sqrt-weak-chunk-0086.smt2                     |    0.056s | 20.556MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0276.smt2                                |    0.057s | 21.248MiB| sat | 0 |  |  |
|CONVOI2-chunk-0041.smt2                                      |    0.057s | 21.02MiB| unsat | 0 |  |  |
|sqrt-problem-Melquiond2-chunk-0071.smt2                      |    0.057s | 20.94MiB| sat | 0 |  |  |
|Chua-2-VC1-U-chunk-0035.smt2                                 |    0.057s | 20.728MiB| sat | 0 |  |  |
|ball_count_2d_slope.10.seq_lazy_linear_enc_lemmas_global_9.smt2 |    0.057s | 20.1MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0193.smt2                             |    0.057s | 20.644MiB| unsat | 0 |  |  |
|ball_count_2d_hill.05.seq_lazy_global_3.smt2                 |    0.057s | 21.2MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0305.smt2                             |    0.057s | 20.636MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0589.smt2                                |    0.058s | 21.084MiB| sat | 0 |  |  |
|cos-3410-b-chunk-0015.smt2                                   |    0.058s | 20.764MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0189.smt2                                  |    0.058s | 20.864MiB| sat | 0 |  |  |
|exp-problem-10-2-chunk-0325.smt2                             |    0.058s | 21.38MiB| unsat | 0 |  |  |
|exp-problem-10-3-chunk-0052.smt2                             |    0.058s | 20.992MiB| sat | 0 |  |  |
|sin-problem-8-weak-chunk-0068.smt2                           |    0.058s | 20.876MiB| sat | 0 |  |  |
|sin-problem-8-chunk-0026.smt2                                |    0.058s | 20.696MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0053.smt2                          |    0.058s | 20.748MiB| sat | 0 |  |  |
|Chua-2-VC1-L-chunk-0119.smt2                                 |    0.058s | 20.764MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0359.smt2                                |    0.058s | 20.936MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0206.smt2                      |    0.058s | 20.728MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0500.smt2                             |    0.058s | 20.844MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0469.smt2                      |    0.058s | 20.836MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0573.smt2                                  |    0.058s | 20.86MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0620.smt2                                |    0.059s | 21.136MiB| sat | 0 |  |  |
|ball_count_2d_plain.02.seq_lazy_linear_enc_global_3.smt2     |    0.059s | 19.024MiB| unsat | 0 |  |  |
|ball_count_2d_plain.05.qfree_global_9.smt2                   |    0.059s | 21.628MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0064.smt2                          |    0.059s | 20.784MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.05.qfree_global_1.smt2             |    0.059s | 18.868MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0681.smt2                             |    0.059s | 20.864MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0102.smt2                             |    0.059s | 20.684MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.04.seq_lazy_linear_enc_global_7.smt2 |    0.059s | 21.232MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0209.smt2                                |    0.060s | 20.616MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0169.smt2                                   |    0.060s | 20.988MiB| sat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0167.smt2                                |    0.060s | 20.804MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.04.redlog_global_5.smt2            |    0.060s | 21.468MiB| unsat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0205.smt2     |    0.060s | 20.724MiB| unsat | 0 |  |  |
|sin-problem-7-chunk-0311.smt2                                |    0.060s | 20.92MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0109.smt2                                  |    0.060s | 20.692MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0142.smt2                                |    0.060s | 20.772MiB| sat | 0 |  |  |
|Chua-1-IL-L-chunk-0042.smt2                                  |    0.060s | 18.82MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0584.smt2                                |    0.060s | 20.796MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0270.smt2                                  |    0.060s | 21.232MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0286.smt2                                   |    0.060s | 21.02MiB| sat | 0 |  |  |
|ball_count_2d_slope.01.seq_lazy_lemmas_global_15.smt2        |    0.060s | 21.444MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0633.smt2                                |    0.060s | 20.964MiB| sat | 0 |  |  |
|ball_count_2d_plain.01.seq_lazy_linear_enc_global_9.smt2     |    0.061s | 19.336MiB| unsat | 0 |  |  |
|hong_2.smt2                                                  |    0.061s | 20.604MiB| unsat | 0 |  |  |
|ball_count_2d_plain.03.seq_lazy_global_13.smt2               |    0.061s | 21.824MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.04.seq_lazy_linear_enc_global_11.smt2 |    0.061s | 21.616MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0610.smt2                                |    0.062s | 21.02MiB| sat | 0 |  |  |
|ball_count_2d_plain.01.redlog_global_7.smt2                  |    0.062s | 19.74MiB| unsat | 0 |  |  |
|ball_count_2d_plain.03.redlog_global_5.smt2                  |    0.062s | 21.4MiB| unsat | 0 |  |  |
|Chua-2-IL-U-chunk-0021.smt2                                  |    0.062s | 20.768MiB| sat | 0 |  |  |
|ball_count_2d_plain.02.redlog_global_15.smt2                 |    0.062s | 20.464MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0019.smt2                             |    0.062s | 20.576MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0070.smt2                        |    0.062s | 20.816MiB| unsat | 0 |  |  |
|ball_count_2d_slope.02.seq_lazy_linear_enc_lemmas_global_5.smt2 |    0.062s | 19.608MiB| unsat | 0 |  |  |
|ball_count_2d_plain.01.seq_lazy_lemmas_global_5.smt2         |    0.062s | 19.184MiB| unsat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0039.smt2                                |    0.063s | 20.836MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0265.smt2                             |    0.063s | 20.736MiB| sat | 0 |  |  |
|sin-344-4-chunk-0032.smt2                                    |    0.063s | 20.86MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0530.smt2                                |    0.063s | 20.812MiB| sat | 0 |  |  |
|ball_count_1d_plain.10.seq_lazy_lemmas_global_7.smt2         |    0.063s | 19.332MiB| unsat | 0 |  |  |
|matrix-1-all-2.smt2                                          |    0.063s | 20.7MiB| sat | 0 |  |  |
|ball_count_2d_slope.10.seq_lazy_linear_enc_lemmas_global_13.smt2 |    0.063s | 20.624MiB| unsat | 0 |  |  |
|ball_count_1d_plain.01.seq_lazy_linear_enc_global_15.smt2    |    0.064s | 19.76MiB| unsat | 0 |  |  |
|ball_count_2d_slope.02.seq_lazy_lemmas_global_11.smt2        |    0.064s | 20.724MiB| unsat | 0 |  |  |
|ball_count_2d_plain.05.redlog_global_3.smt2                  |    0.064s | 21.196MiB| unsat | 0 |  |  |
|ball_count_2d_hill.10.redlog_global_13.smt2                  |    0.064s | 21.208MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0358.smt2                             |    0.064s | 20.72MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0151.smt2                        |    0.064s | 18.8MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0064.smt2                                |    0.064s | 20.868MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.05.redlog_global_9.smt2            |    0.064s | 21.604MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0290.smt2                                  |    0.065s | 20.836MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0162.smt2                      |    0.065s | 20.768MiB| unsat | 0 |  |  |
|Chua-2-VC1-U-chunk-0058.smt2                                 |    0.065s | 20.7MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.10.seq_lazy_global_11.smt2         |    0.066s | 19.676MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0231.smt2                             |    0.066s | 18.776MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0255.smt2                             |    0.066s | 20.744MiB| sat | 0 |  |  |
|ball_count_2d_hill.10.seq_lazy_lemmas_global_11.smt2         |    0.066s | 20.112MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0369.smt2                      |    0.066s | 20.772MiB| sat | 0 |  |  |
|sin-problem-7-chunk-0322.smt2                                |    0.066s | 20.832MiB| unsat | 0 |  |  |
|ball_count_2d_plain.03.qfree_global_15.smt2                  |    0.066s | 22.34MiB| unsat | 0 |  |  |
|mbo_E17E23.smt2                                              |    0.066s | 20.728MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0191.smt2                        |    0.067s | 20.792MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0549.smt2                                |    0.067s | 21.132MiB| unsat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0098.smt2     |    0.067s | 20.696MiB| sat | 0 |  |  |
|ball_count_2d_hill.01.seq_lazy_lemmas_global_7.smt2          |    0.067s | 19.616MiB| unsat | 0 |  |  |
|sin-problem-7-chunk-0172.smt2                                |    0.067s | 20.996MiB| unsat | 0 |  |  |
|ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_1.smt2 |    0.067s | 18.968MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0310.smt2                      |    0.067s | 20.868MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.02.redlog_global_11.smt2           |    0.067s | 19.804MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0204.smt2                             |    0.067s | 20.76MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.05.seq_lazy_lemmas_global_7.smt2   |    0.067s | 21.588MiB| unsat | 0 |  |  |
|ball_count_2d_plain.01.qfree_global_3.smt2                   |    0.067s | 19.196MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0089.smt2                                  |    0.068s | 20.692MiB| sat | 0 |  |  |
|sin-problem-8-chunk-0067.smt2                                |    0.068s | 21.02MiB| sat | 0 |  |  |
|ball_count_1d_plain.04.seq_lazy_global_1.smt2                |    0.068s | 18.932MiB| unsat | 0 |  |  |
|ball_count_2d_hill.02.seq_lazy_linear_enc_global_15.smt2     |    0.068s | 20.188MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0109.smt2                          |    0.068s | 20.648MiB| unsat | 0 |  |  |
|simple_ballistics_reach.01.seq_lazy_linear_enc_global_1.smt2 |    0.068s | 20.952MiB| unsat | 0 |  |  |
|ball_count_2d_slope.01.seq_lazy_global_11.smt2               |    0.068s | 20.368MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.05.seq_lazy_linear_enc_global_15.smt2 |    0.068s | 21.952MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.05.qfree_global_5.smt2             |    0.068s | 21.008MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.03.seq_lazy_lemmas_global_9.smt2   |    0.068s | 21.68MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0124.smt2                             |    0.068s | 20.82MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0515.smt2                      |    0.068s | 20.876MiB| sat | 0 |  |  |
|ball_count_2d_plain.03.seq_lazy_lemmas_global_3.smt2         |    0.069s | 21.0MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0186.smt2                                |    0.069s | 20.752MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0643.smt2                                |    0.069s | 21.16MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0577.smt2                                |    0.069s | 20.768MiB| sat | 0 |  |  |
|ball_count_2d_hill.04.seq_lazy_global_3.smt2                 |    0.069s | 21.172MiB| unsat | 0 |  |  |
|InVarSynth_LabelEncodingWithUnrolling.bpl_Iteration2_0.smt2  |    0.069s | 21.02MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0114.smt2                                |    0.069s | 20.804MiB| unsat | 0 |  |  |
|Chua-1-IL-L-chunk-0078.smt2                                  |    0.069s | 20.688MiB| sat | 0 |  |  |
|atan-problem-2-weak-chunk-0124.smt2                          |    0.070s | 20.796MiB| sat | 0 |  |  |
|ball_count_1d_plain.10.seq_lazy_linear_enc_lemmas_global_5.smt2 |    0.070s | 19.116MiB| unsat | 0 |  |  |
|Chua-2-VC1-L-chunk-0073.smt2                                 |    0.070s | 18.88MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0232.smt2                                |    0.070s | 20.76MiB| unsat | 0 |  |  |
|ball_count_1d_plain.10.qfree_global_1.smt2                   |    0.070s | 19.064MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0069.smt2                      |    0.071s | 20.82MiB| sat | 0 |  |  |
|ball_count_2d_plain.10.seq_lazy_linear_enc_lemmas_global_3.smt2 |    0.071s | 19.224MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0668.smt2                                |    0.071s | 21.176MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0275.smt2                                   |    0.071s | 20.888MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.03.seq_lazy_linear_enc_lemmas_global_7.smt2 |    0.071s | 21.404MiB| unsat | 0 |  |  |
|ball_count_2d_slope.10.seq_lazy_linear_enc_global_5.smt2     |    0.071s | 19.46MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0136.smt2                             |    0.072s | 20.756MiB| sat | 0 |  |  |
|ball_count_2d_slope.10.seq_lazy_lemmas_global_15.smt2        |    0.072s | 21.464MiB| unsat | 0 |  |  |
|sqrt-problem-12vars3-chunk-0039.smt2                         |    0.072s | 20.68MiB| unsat | 0 |  |  |
|Chua-2-VC2-U-chunk-0018.smt2                                 |    0.072s | 20.772MiB| sat | 0 |  |  |
|exp-problem-10-3-chunk-0188.smt2                             |    0.072s | 20.84MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0054.smt2                                |    0.072s | 20.68MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0524.smt2                                |    0.072s | 18.78MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0318.smt2                                |    0.072s | 20.652MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0122.smt2                                   |    0.073s | 21.016MiB| sat | 0 |  |  |
|Chua-1-VC2-U-chunk-0149.smt2                                 |    0.073s | 21.008MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0368.smt2                                |    0.073s | 20.892MiB| sat | 0 |  |  |
|bottom-plate-mixer-chunk-0050.smt2                           |    0.073s | 20.644MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0425.smt2                      |    0.073s | 20.664MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.10.seq_lazy_linear_enc_lemmas_global_9.smt2 |    0.073s | 19.488MiB| unsat | 0 |  |  |
|sqrt-problem-13-sqrt1-chunk-0062.smt2                        |    0.073s | 20.8MiB| sat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0206.smt2                                |    0.073s | 21.1MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0631.smt2                                |    0.073s | 20.8MiB| sat | 0 |  |  |
|ball_count_1d_plain.04.seq_lazy_global_5.smt2                |    0.074s | 21.028MiB| unsat | 0 |  |  |
|MulliganEconomicsModel0067a.smt2                             |    0.074s | 21.076MiB| sat | 0 |  |  |
|matrix-1-all-29.smt2                                         |    0.074s | 20.784MiB| sat | 0 |  |  |
|RL-high-pass-circuit-gain-chunk-0010.smt2                    |    0.074s | 20.696MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0170.smt2                             |    0.074s | 20.744MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0390.smt2                      |    0.074s | 20.84MiB| sat | 0 |  |  |
|ball_count_2d_slope.01.seq_lazy_linear_enc_lemmas_global_9.smt2 |    0.074s | 20.3MiB| unsat | 0 |  |  |
|sqrt-circles-2-chunk-0002.smt2                               |    0.074s | 20.824MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0243.smt2                                |    0.074s | 21.288MiB| unsat | 0 |  |  |
|ball_count_2d_hill.10.seq_lazy_linear_enc_lemmas_global_1.smt2 |    0.075s | 18.984MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0166.smt2                                |    0.075s | 20.912MiB| sat | 0 |  |  |
|ball_count_2d_plain.10.redlog_global_11.smt2                 |    0.075s | 20.056MiB| unsat | 0 |  |  |
|sin-problem-7-weak-chunk-0171.smt2                           |    0.075s | 21.3MiB| sat | 0 |  |  |
|ball_count_2d_plain.02.qfree_global_11.smt2                  |    0.075s | 19.74MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0015.smt2                        |    0.075s | 20.676MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0467.smt2                                |    0.076s | 20.808MiB| unsat | 0 |  |  |
|exp-problem-10-3-chunk-0073.smt2                             |    0.076s | 20.784MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0469.smt2                             |    0.076s | 20.788MiB| sat | 0 |  |  |
|Chua-1-VC1-L-chunk-0019.smt2                                 |    0.076s | 20.936MiB| sat | 0 |  |  |
|sin-344-3-chunk-0058.smt2                                    |    0.076s | 20.848MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0260.smt2                                   |    0.077s | 18.876MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0286.smt2                                |    0.078s | 21.572MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0332.smt2                                   |    0.078s | 20.82MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0721.smt2                             |    0.078s | 21.156MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0391.smt2                                |    0.078s | 21.228MiB| sat | 0 |  |  |
|Chua-1-VC2-U-chunk-0135.smt2                                 |    0.078s | 20.84MiB| unsat | 0 |  |  |
|Chua-1-IL-L-chunk-0016.smt2                                  |    0.078s | 21.016MiB| sat | 0 |  |  |
|Chua-1-VC2-U-chunk-0061.smt2                                 |    0.078s | 20.72MiB| sat | 0 |  |  |
|polypaver-sqrt43-int-3vars-chunk-0075.smt2                   |    0.078s | 20.784MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0334.smt2                             |    0.079s | 20.84MiB| sat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0161.smt2                        |    0.079s | 20.94MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0349.smt2                                |    0.079s | 20.808MiB| sat | 0 |  |  |
|atan-problem-2-weak2-chunk-0136.smt2                         |    0.079s | 21.136MiB| sat | 0 |  |  |
|ball_count_1d_plain.01.redlog_global_9.smt2                  |    0.079s | 19.488MiB| unsat | 0 |  |  |
|etcs_braking_2.01.qfree_global_3.smt2                        |    0.079s | 21.324MiB| unsat | 0 |  |  |
|Chua-2-VC1-L-chunk-0062.smt2                                 |    0.079s | 20.736MiB| sat | 0 |  |  |
|ball_count_2d_hill.01.redlog_global_13.smt2                  |    0.079s | 21.252MiB| unsat | 0 |  |  |
|polypaver-sqrt43-int-3vars-chunk-0043.smt2                   |    0.079s | 20.94MiB| unsat | 0 |  |  |
|atan-problem-1-chunk-0102.smt2                               |    0.079s | 21.096MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0603.smt2                                  |    0.080s | 20.92MiB| sat | 0 |  |  |
|ball_count_2d_hill.10.seq_lazy_linear_enc_global_15.smt2     |    0.080s | 20.216MiB| unsat | 0 |  |  |
|ball_count_2d_plain.03.seq_lazy_global_9.smt2                |    0.080s | 21.6MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0690.smt2                                |    0.081s | 21.284MiB| sat | 0 |  |  |
|ball_count_2d_plain.05.seq_lazy_linear_enc_lemmas_global_13.smt2 |    0.081s | 22.168MiB| unsat | 0 |  |  |
|exp-problem-10-3-chunk-0178.smt2                             |    0.081s | 21.036MiB| sat | 0 |  |  |
|atan-problem-2-chunk-0092.smt2                               |    0.081s | 20.708MiB| unsat | 0 |  |  |
|ball_count_2d_plain.04.seq_lazy_lemmas_global_11.smt2        |    0.081s | 21.892MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.10.seq_lazy_linear_enc_lemmas_global_13.smt2 |    0.081s | 19.82MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0493.smt2                                  |    0.081s | 20.892MiB| sat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0141.smt2                        |    0.082s | 21.016MiB| sat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0183.smt2                      |    0.082s | 20.764MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.03.seq_lazy_lemmas_global_13.smt2  |    0.082s | 22.252MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0375.smt2                             |    0.082s | 20.668MiB| unsat | 0 |  |  |
|ball_count_2d_slope.03.seq_lazy_linear_enc_lemmas_global_15.smt2 |    0.082s | 20.884MiB| unsat | 0 |  |  |
|sin-problem-7-weak-chunk-0138.smt2                           |    0.083s | 20.948MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0443.smt2                                  |    0.084s | 21.264MiB| sat | 0 |  |  |
|atan-vega-3-weak-chunk-0639.smt2                             |    0.084s | 20.752MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.10.qfree_global_13.smt2            |    0.084s | 19.996MiB| unsat | 0 |  |  |
|Chua-1-VC2-U-chunk-0038.smt2                                 |    0.085s | 20.796MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.05.seq_lazy_linear_enc_lemmas_global_5.smt2 |    0.085s | 21.228MiB| unsat | 0 |  |  |
|mgc_06.smt2                                                  |    0.085s | 21.42MiB| unsat | 0 |  |  |
|MulliganEconomicsModel0077c.smt2                             |    0.085s | 20.852MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0402.smt2                                |    0.085s | 21.28MiB| sat | 0 |  |  |
|ball_count_2d_hill.05.seq_lazy_linear_enc_lemmas_global_5.smt2 |    0.085s | 21.532MiB| unsat | 0 |  |  |
|atan-vega-3-weak-chunk-0398.smt2                             |    0.085s | 20.756MiB| sat | 0 |  |  |
|sin-problem-7-weak2-chunk-0088.smt2                          |    0.085s | 18.972MiB| unsat | 0 |  |  |
|ball_count_2d_plain.05.seq_lazy_linear_enc_lemmas_global_9.smt2 |    0.085s | 21.748MiB| unsat | 0 |  |  |
|Chua-1-IL-U-chunk-0076.smt2                                  |    0.085s | 20.984MiB| unsat | 0 |  |  |
|ball_count_1d_plain.04.qfree_global_7.smt2                   |    0.086s | 21.252MiB| unsat | 0 |  |  |
|ball_count_2d_hill.03.seq_lazy_lemmas_global_7.smt2          |    0.086s | 22.232MiB| unsat | 0 |  |  |
|MulliganEconomicsModel0080e.smt2                             |    0.086s | 20.856MiB| sat | 0 |  |  |
|ball_count_2d_plain.04.seq_lazy_linear_enc_global_15.smt2    |    0.086s | 21.912MiB| unsat | 0 |  |  |
|atan-problem-2-sqrt-chunk-0019.smt2                          |    0.086s | 20.74MiB| unsat | 0 |  |  |
|sin-cos-346-b-chunk-0296.smt2                                |    0.086s | 18.92MiB| unsat | 0 |  |  |
|ball_count_2d_hill.05.seq_lazy_lemmas_global_7.smt2          |    0.087s | 22.128MiB| unsat | 0 |  |  |
|Chua-2-IL-L-chunk-0058.smt2                                  |    0.087s | 20.62MiB| sat | 0 |  |  |
|ball_count_1d_plain.05.seq_lazy_linear_enc_global_11.smt2    |    0.087s | 21.644MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.10.seq_lazy_lemmas_global_15.smt2  |    0.087s | 20.228MiB| unsat | 0 |  |  |
|polypaver-sqrt43-int-chunk-0053.smt2                         |    0.088s | 20.772MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.04.seq_lazy_global_13.smt2         |    0.089s | 21.872MiB| unsat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0191.smt2                                |    0.089s | 21.048MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.05.seq_lazy_lemmas_global_11.smt2  |    0.089s | 22.068MiB| unsat | 0 |  |  |
|polypaver-bench-exp-3d-chunk-0138.smt2                       |    0.089s | 20.868MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0435.smt2                      |    0.089s | 20.736MiB| unsat | 0 |  |  |
|ball_count_2d_slope.04.seq_lazy_linear_enc_global_3.smt2     |    0.089s | 21.472MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0679.smt2                                |    0.090s | 21.556MiB| unsat | 0 |  |  |
|polypaver-bench-sqrt-3d-chunk-0446.smt2                      |    0.090s | 20.832MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0412.smt2                                |    0.090s | 21.1MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0621.smt2                                |    0.090s | 21.14MiB| sat | 0 |  |  |
|ball_count_2d_plain.05.seq_lazy_lemmas_global_15.smt2        |    0.091s | 22.628MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.01.qfree_global_13.smt2            |    0.091s | 19.608MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0038.smt2                             |    0.091s | 20.84MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0391.smt2                                |    0.092s | 20.824MiB| sat | 0 |  |  |
|etcs_braking_2.01.seq_lazy_linear_enc_lemmas_global_3.smt2   |    0.092s | 21.472MiB| unsat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0177.smt2                                |    0.092s | 20.98MiB| sat | 0 |  |  |
|atan-problem-2-weakT-chunk-0019.smt2                         |    0.092s | 20.768MiB| sat | 0 |  |  |
|exp-problem-10-2-chunk-0048.smt2                             |    0.093s | 20.784MiB| sat | 0 |  |  |
|cbrt-problem-3-weak-chunk-0040.smt2                          |    0.093s | 21.184MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.03.redlog_global_15.smt2           |    0.093s | 21.98MiB| unsat | 0 |  |  |
|ball_count_2d_hill.01.seq_lazy_linear_enc_global_15.smt2     |    0.094s | 20.316MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0199.smt2                                |    0.094s | 20.932MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0514.smt2                                |    0.094s | 20.976MiB| sat | 0 |  |  |
|matrix-5-all-23.smt2                                         |    0.095s | 21.616MiB| unsat | 0 |  |  |
|atan-vega-3-chunk-0119.smt2                                  |    0.095s | 20.832MiB| sat | 0 |  |  |
|ball_count_2d_hill.03.seq_lazy_linear_enc_lemmas_global_1.smt2 |    0.096s | 18.976MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0436.smt2                                |    0.096s | 21.208MiB| sat | 0 |  |  |
|atan-vega-3-chunk-0593.smt2                                  |    0.097s | 20.944MiB| unsat | 0 |  |  |
|Chua-2-IL-L-chunk-0005.smt2                                  |    0.097s | 20.652MiB| sat | 0 |  |  |
|ball_count_2d_plain.10.redlog_global_7.smt2                  |    0.097s | 19.744MiB| unsat | 0 |  |  |
|atan-problem-1-chunk-0047.smt2                               |    0.098s | 20.796MiB| sat | 0 |  |  |
|Chua-1-IL-L-chunk-0030.smt2                                  |    0.098s | 20.768MiB| unsat | 0 |  |  |
|ball_count_2d_hill.02.redlog_global_13.smt2                  |    0.098s | 21.168MiB| unsat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0054.smt2     |    0.098s | 21.024MiB| sat | 0 |  |  |
|ball_count_1d_plain.04.seq_lazy_linear_enc_global_3.smt2     |    0.098s | 20.976MiB| unsat | 0 |  |  |
|MulliganEconomicsModel0027c.smt2                             |    0.098s | 20.652MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.10.redlog_global_3.smt2            |    0.099s | 19.192MiB| unsat | 0 |  |  |
|ball_count_2d_hill.04.seq_lazy_linear_enc_lemmas_global_5.smt2 |    0.099s | 21.56MiB| unsat | 0 |  |  |
|sqrt-1mcosq-7-chunk-0155.smt2                                |    0.099s | 21.248MiB| sat | 0 |  |  |
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0156.smt2     |    0.100s | 21.008MiB| sat | 0 |  |  |
|MulliganEconomicsModel0054a.smt2                             |    0.100s | 21.068MiB| sat | 0 |  |  |
|InVarSynth_doubleLoopUniformIterations.bpl_Iteration2_0.smt2 |    0.100s | 20.724MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0132.smt2                                |    0.100s | 20.852MiB| sat | 0 |  |  |
|mbo_E5E23.smt2                                               |    0.101s | 21.764MiB| unsat | 0 |  |  |
|ball_count_2d_plain.04.seq_lazy_linear_enc_lemmas_global_5.smt2 |    0.102s | 21.2MiB| unsat | 0 |  |  |
|polypaver-sqrt43-int-3vars-chunk-0121.smt2                   |    0.102s | 20.836MiB| sat | 0 |  |  |
|ball_count_2d_hill_simple.02.seq_lazy_global_15.smt2         |    0.103s | 19.908MiB| unsat | 0 |  |  |
|ball_count_2d_plain.02.seq_lazy_lemmas_global_9.smt2         |    0.104s | 19.724MiB| unsat | 0 |  |  |
|ball_count_2d_hill.04.seq_lazy_lemmas_global_7.smt2          |    0.104s | 22.0MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.05.redlog_global_13.smt2           |    0.105s | 21.98MiB| unsat | 0 |  |  |
|ball_count_2d_plain.05.qfree_global_13.smt2                  |    0.106s | 21.976MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0158.smt2                                   |    0.106s | 20.852MiB| unsat | 0 |  |  |
|InVarSynth_ShortCircuit-SideEffect-SwitchStatement-Safe.c_Iteration1_0.smt2 |    0.107s | 21.568MiB| sat | 0 |  |  |
|atan-problem-2-weak2-chunk-0070.smt2                         |    0.109s | 20.748MiB| sat | 0 |  |  |
|sin-problem-7-chunk-0247.smt2                                |    0.109s | 20.848MiB| sat | 0 |  |  |
|cbrt-problem-3-weak-chunk-0094.smt2                          |    0.109s | 20.944MiB| sat | 0 |  |  |
|ball_count_1d_plain.04.qfree_global_11.smt2                  |    0.109s | 21.712MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0519.smt2                                |    0.109s | 20.58MiB| sat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0035.smt2                        |    0.110s | 20.68MiB| sat | 0 |  |  |
|sin-cos-346-b-chunk-0054.smt2                                |    0.110s | 18.964MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.01.seq_lazy_lemmas_global_15.smt2  |    0.110s | 20.564MiB| unsat | 0 |  |  |
|exp-problem-10-3-chunk-0148.smt2                             |    0.111s | 20.576MiB| unsat | 0 |  |  |
|atan-problem-2-weak2-chunk-0022.smt2                         |    0.111s | 20.768MiB| unsat | 0 |  |  |
|sin-344-3-chunk-0046.smt2                                    |    0.112s | 20.844MiB| sat | 0 |  |  |
|Chua-2-VC2-U-chunk-0097.smt2                                 |    0.112s | 21.024MiB| sat | 0 |  |  |
|ball_count_1d_plain.03.seq_lazy_linear_enc_global_9.smt2     |    0.112s | 21.648MiB| unsat | 0 |  |  |
|sin-344-3-weak-chunk-0044.smt2                               |    0.113s | 20.72MiB| sat | 0 |  |  |
|ball_count_1d_plain.03.redlog_global_11.smt2                 |    0.114s | 21.796MiB| unsat | 0 |  |  |
|cos-3410-b-chunk-0027.smt2                                   |    0.114s | 20.72MiB| sat | 0 |  |  |
|ball_count_2d_hill.03.seq_lazy_linear_enc_lemmas_global_5.smt2 |    0.115s | 21.62MiB| unsat | 0 |  |  |
|ball_count_2d_plain.03.seq_lazy_linear_enc_global_7.smt2     |    0.115s | 21.168MiB| unsat | 0 |  |  |
|sin-problem-7-chunk-0192.smt2                                |    0.115s | 21.024MiB| sat | 0 |  |  |
|sin-problem-7-chunk-0079.smt2                                |    0.116s | 20.736MiB| sat | 0 |  |  |
|ball_count_1d_plain.04.seq_lazy_linear_enc_lemmas_global_11.smt2 |    0.116s | 21.752MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.03.seq_lazy_global_5.smt2          |    0.117s | 21.096MiB| unsat | 0 |  |  |
|atan-problem-1-chunk-0035.smt2                               |    0.117s | 20.652MiB| sat | 0 |  |  |
|ball_count_1d_plain.05.seq_lazy_global_13.smt2               |    0.117s | 21.868MiB| unsat | 0 |  |  |
|ball_count_2d_plain.05.seq_lazy_global_7.smt2                |    0.118s | 21.784MiB| unsat | 0 |  |  |
|ball_count_1d_plain.03.seq_lazy_linear_enc_global_13.smt2    |    0.118s | 21.884MiB| unsat | 0 |  |  |
|exp-problem-10-3-weak-chunk-0230.smt2                        |    0.118s | 21.336MiB| unsat | 0 |  |  |
|ball_count_1d_plain.10.redlog_global_9.smt2                  |    0.119s | 19.628MiB| unsat | 0 |  |  |
|ball_count_2d_plain.04.redlog_global_13.smt2                 |    0.120s | 22.604MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0426.smt2                                |    0.123s | 21.116MiB| sat | 0 |  |  |
|atan-problem-2-sqrt-weak-chunk-0009.smt2                     |    0.125s | 20.764MiB| unsat | 0 |  |  |
|Chua-2-VC1-U-chunk-0117.smt2                                 |    0.132s | 20.804MiB| unsat | 0 |  |  |
|ball_count_1d_plain.05.seq_lazy_global_9.smt2                |    0.132s | 21.536MiB| unsat | 0 |  |  |
|ball_count_2d_plain.03.seq_lazy_linear_enc_lemmas_global_15.smt2 |    0.133s | 22.32MiB| unsat | 0 |  |  |
|ball_count_1d_plain.04.seq_lazy_lemmas_global_9.smt2         |    0.134s | 21.864MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0209.smt2                                |    0.142s | 21.32MiB| sat | 0 |  |  |
|ball_count_2d_plain.04.redlog_global_9.smt2                  |    0.147s | 21.98MiB| unsat | 0 |  |  |
|CMOS-opamp-chunk-0320.smt2                                   |    0.151s | 21.152MiB| unsat | 0 |  |  |
|ball_count_2d_hill_simple.04.seq_lazy_linear_enc_lemmas_global_15.smt2 |    0.158s | 22.36MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0457.smt2                                |    0.160s | 21.336MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0446.smt2                                |    0.162s | 21.536MiB| sat | 0 |  |  |
|ball_count_1d_plain.04.seq_lazy_lemmas_global_13.smt2        |    0.165s | 21.952MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0254.smt2                                |    0.166s | 21.236MiB| unsat | 0 |  |  |
|toeplz.c.i.toeplz.pl.t2.fixed.t2.c_Iteration10_Loop_3-pieceTemplate.smt2 |    0.176s | 22.644MiB| sat | 0 |  |  |
|ball_count_1d_plain.03.seq_lazy_global_15.smt2               |    0.178s | 21.984MiB| unsat | 0 |  |  |
|ball_count_2d_hill.03.seq_lazy_lemmas_global_11.smt2         |    0.182s | 22.924MiB| unsat | 0 |  |  |
|ball_count_1d_plain.05.qfree_global_15.smt2                  |    0.184s | 22.088MiB| unsat | 0 |  |  |
|ball_count_2d_hill.04.seq_lazy_lemmas_global_11.smt2         |    0.188s | 23.244MiB| unsat | 0 |  |  |
|ball_count_2d_hill.03.seq_lazy_linear_enc_global_15.smt2     |    0.199s | 23.584MiB| unsat | 0 |  |  |
|mc91test.t2.c_Iteration5_Loop_3-pieceTemplate.smt2           |    0.200s | 23.536MiB| sat | 0 |  |  |
|ball_count_2d_hill.05.seq_lazy_lemmas_global_11.smt2         |    0.201s | 23.004MiB| unsat | 0 |  |  |
|sin-problem-8-weak-chunk-0079.smt2                           |    0.201s | 20.94MiB| unsat | 0 |  |  |
|etcs_braking_2.01.seq_lazy_lemmas_global_5.smt2              |    0.202s | 22.724MiB| unsat | 0 |  |  |
|standard_init9_ground.i_3_2_2.bpl_1.smt2                     |    0.211s | 21.58MiB| unsat | 0 |  |  |
|ball_count_2d_hill.04.seq_lazy_linear_enc_global_15.smt2     |    0.218s | 23.56MiB| unsat | 0 |  |  |
|ball_count_2d_hill.05.seq_lazy_linear_enc_global_15.smt2     |    0.224s | 23.68MiB| unsat | 0 |  |  |
|ball_count_2d_slope.03.seq_lazy_lemmas_global_3.smt2         |    0.237s | 21.776MiB| unsat | 0 |  |  |
|ball_count_2d_slope.03.seq_lazy_linear_enc_global_7.smt2     |    0.265s | 22.648MiB| unsat | 0 |  |  |
|qrdcmp.t2.c_Iteration6_Loop_3-pieceTemplate.smt2             |    0.265s | 23.512MiB| sat | 0 |  |  |
|ball_count_1d_plain.05.seq_lazy_linear_enc_lemmas_global_15.smt2 |    0.282s | 22.104MiB| unsat | 0 |  |  |
|ball_count_1d_plain.04.redlog_global_15.smt2                 |    0.291s | 22.288MiB| unsat | 0 |  |  |
|p-42.t2.c_Iteration2_Loop_4-pieceTemplate.smt2               |    0.352s | 24.732MiB| sat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0296.smt2                                |    0.352s | 21.664MiB| unsat | 0 |  |  |
|pentagon.t2.c_Iteration9_Loop_3-pieceTemplate.smt2           |    0.369s | 22.94MiB| sat | 0 |  |  |
|CMOS-opamp-chunk-0180.smt2                                   |    0.387s | 21.56MiB| unsat | 0 |  |  |
|ball_count_2d_slope.04.seq_lazy_global_5.smt2                |    0.455s | 22.032MiB| unsat | 0 |  |  |
|etcs_braking_2.01.seq_lazy_linear_enc_global_9.smt2          |    0.460s | 24.332MiB| unsat | 0 |  |  |
|spiral.t2.c_Iteration8_Loop_4-pieceTemplate.smt2             |    0.463s | 24.62MiB| sat | 0 |  |  |
|sort.t2.c_Iteration5_Loop_3-pieceTemplate.smt2               |    0.481s | 25.908MiB| sat | 0 |  |  |
|matrix-1-all-38.smt2                                         |    0.548s | 21.796MiB| sat | 0 |  |  |
|bf10.t2.c_Iteration1_Loop_4-pieceTemplate.smt2               |    0.578s | 25.188MiB| sat | 0 |  |  |
|toeplz.t2.c_Iteration7_Loop_4-pieceTemplate.smt2             |    0.599s | 24.78MiB| sat | 0 |  |  |
|CookSeeZuleger-2013TACAS-Fig3_true-termination.c_Iteration1_Loop_5-phaseTemplate.smt2 |    0.603s | 44.792MiB| unsat | 0 |  |  |
|Canberra.bpl_Iteration1_Loop_2-pieceTemplate.smt2            |    0.626s | 44.704MiB| unsat | 0 |  |  |
|ball_count_2d_slope.05.seq_lazy_linear_enc_global_9.smt2     |    0.694s | 23.688MiB| unsat | 0 |  |  |
|SyntaxSupportDisjunction1.bpl_Iteration1_Loop_4-pieceTemplate.smt2 |    0.752s | 26.132MiB| sat | 0 |  |  |
|ball_count_2d_hill.04.redlog_global_9.smt2                   |    0.858s | 23.924MiB| unsat | 0 |  |  |
|ball_count_2d_hill.05.redlog_global_9.smt2                   |    0.869s | 23.92MiB| unsat | 0 |  |  |
|ball_count_2d_hill.03.redlog_global_9.smt2                   |    0.908s | 23.872MiB| unsat | 0 |  |  |
|CookSeeZuleger-2013TACAS-Fig7a_true-termination.c_Iteration1_Loop_5-phaseTemplate.smt2 |    0.918s | 76.476MiB| unsat | 0 |  |  |
|ball_count_2d_slope.03.seq_lazy_global_9.smt2                |    0.980s | 23.856MiB| unsat | 0 |  |  |
|atan-problem-2-weak-chunk-0201.smt2                          |    1.005s | 22.916MiB| unsat | 0 |  |  |
|ex11.t2.c_Iteration1_Lasso_5-phaseTemplate.smt2              |    1.046s | 29.66MiB| unsat | 0 |  |  |
|Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2 |    1.163s | 43.3MiB| unsat | 0 |  |  |
|exp-problem-10-2-chunk-0315.smt2                             |    1.363s | 22.472MiB| unsat | 0 |  |  |
|ball_count_2d_slope.05.seq_lazy_lemmas_global_5.smt2         |    1.460s | 22.612MiB| unsat | 0 |  |  |
|eric.t2.c_Iteration1_Lasso_5-phaseTemplate.smt2              |    1.603s | 26.944MiB| unsat | 0 |  |  |
|ball_count_2d_slope.04.seq_lazy_lemmas_global_9.smt2         |    2.630s | 25.032MiB| unsat | 0 |  |  |
|ball_count_2d_slope.03.seq_lazy_linear_enc_global_11.smt2    |    2.856s | 25.504MiB| unsat | 0 |  |  |
|sin-problem-7-weak2-chunk-0113.smt2                          |    3.037s | 21.984MiB| unsat | 0 |  |  |
|sin-problem-7-weak-chunk-0181.smt2                           |    3.063s | 22.036MiB| sat | 0 |  |  |
|Chua-2-IL-U-chunk-0123.smt2                                  |    3.487s | 21.784MiB| unsat | 0 |  |  |
|joey_false-termination.c_Iteration2_Loop_6-phaseTemplate.smt2 |    3.521s | 28.648MiB| unsat | 0 |  |  |
|p-55.t2.c_Iteration3_Loop_4-pieceTemplate.smt2               |    4.562s | 42.916MiB| sat | 0 |  |  |
|TelAviv-Amir-Minimum_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2 |    4.700s | 260.0MiB| unsat | 0 |  |  |
|KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-termination.c_Iteration1_Lasso_affineTemplate.smt2 |    4.716s | 69.076MiB| unsat | 0 |  |  |
|ball_count_2d_hill.03.redlog_global_13.smt2                  |    8.239s | 26.064MiB| unsat | 0 |  |  |
|ball_count_2d_hill.04.redlog_global_13.smt2                  |    8.972s | 26.036MiB| unsat | 0 |  |  |
|ball_count_2d_slope.05.seq_lazy_global_15.smt2               |   10.068s | 33.844MiB| unknown | 0 |  |  |
|ball_count_2d_slope.05.seq_lazy_linear_enc_global_13.smt2    |   14.057s | 37.272MiB| unknown | 0 |  |  |
|ball_count_2d_slope.03.seq_lazy_global_13.smt2               |   14.066s | 29.488MiB| unknown | 0 |  |  |
|ball_count_2d_slope.04.seq_lazy_lemmas_global_13.smt2        |   14.067s | 30.004MiB| unknown | 0 |  |  |
|mbo_E6E7.smt2                                                |   14.111s | 22.364MiB| unsat | 0 |  |  |
|ball_count_2d_hill.05.redlog_global_13.smt2                  |   14.131s | 27.112MiB| unknown | 0 |  |  |
|mbo_E13E17.smt2                                              |   14.192s | 154.0MiB| unknown | 0 |  |  |
|2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2 |   14.196s | 24.872MiB| unsat | 0 |  |  |
|mbo_E14E22.smt2                                              |   14.218s | 218.0MiB| unknown | 0 |  |  |
|BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2 |   14.224s | 30.016MiB| unsat | 0 |  |  |
|mbo_E1E22.smt2                                               |   14.226s | 218.0MiB| unknown | 0 |  |  |
|ex4.t2.c_Iteration2_Loop_3-pieceTemplate.smt2                |   14.266s | 26.512MiB| sat | 0 |  |  |
|etcs_braking_2.01.seq_lazy_global_15.smt2                    |   14.341s | 33.884MiB| unsat | 0 |  |  |
|matrix-2-all-4.smt2                                          |   14.346s | 169.0MiB| sat | 0 |  |  |
|mbo_E9E13.smt2                                               |   14.358s | 123.0MiB| unknown | 0 |  |  |
|MulliganEconomicsModel0057c.smt2                             |   14.481s | 30.336MiB| unsat | 0 |  |  |
|mbo_E15E18.smt2                                              |   14.491s | 128.0MiB| unknown | 0 |  |  |
|selectSort.t2.c_Iteration3_Loop_4-pieceTemplate.smt2         |   14.613s | 29.488MiB| sat | 0 |  |  |
|mbo_E4E17.smt2                                               |   15.099s | 234.0MiB| unknown | 0 |  |  |
|mbo_E1E6.smt2                                                |   15.101s | 257.0MiB| unknown | 0 |  |  |
|loop_on_input.t2.c_Iteration1_Loop_4-pieceTemplate.smt2      |   15.393s | 30.488MiB| sat | 0 |  |  |
|db3.t2.c_Iteration2_Loop_4-pieceTemplate.smt2                |   15.534s | 35.252MiB| sat | 0 |  |  |
|Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2 |   16.386s | 26.96MiB| unsat | 0 |  |  |
|mbo_E5E12.smt2                                               |   16.444s | 126.0MiB| unknown | 0 |  |  |
|fun9.t2.c_Iteration1_Loop_4-pieceTemplate.smt2               |   19.157s | 31.852MiB| sat | 0 |  |  |
|Garmisch.bpl_Iteration1_Loop_4-pieceTemplate.smt2            |   21.648s | 29.192MiB| unsat | 0 |  |  |
|fuhs-inflasso.t2.c_Iteration2_Loop_4-pieceTemplate.smt2      |   26.183s | 32.668MiB| sat | 0 |  |  |
|polyrank3.t2.c_Iteration2_Loop_3-pieceTemplate.smt2          |   28.403s | 37.5MiB| unsat | 0 |  |  |
|standard_copy5_ground.i_3_2_2.bpl_3.smt2                     |   32.225s | 23.952MiB| unsat | 0 |  |  |
|nested.t2.c_Iteration3_Loop_3-pieceTemplate.smt2             |   32.319s | 32.644MiB| sat | 0 |  |  |
|byron-1.t2.c_Iteration1_Loop_3-pieceTemplate.smt2            |   32.617s | 31.404MiB| unsat | 0 |  |  |
|matrix-3-all-4.smt2                                          |   32.856s | 52.94MiB| sat | 0 |  |  |
|Mysore2.bpl_Iteration1_Loop_3-pieceTemplate.smt2             |   32.897s | 26.712MiB| unsat | 0 |  |  |
|SyntaxSupportDivision1.bpl_Iteration1_Lasso_7-nestedTemplate.smt2 |   38.498s | 80.792MiB| sat | 0 |  |  |
|Lobnya-Boolean-Reordered.bpl_Iteration1_Loop_4-pieceTemplate.smt2 |   40.328s | 37.476MiB| unsat | 0 |  |  |
|Collatz.bpl_Iteration1_Loop_3-nestedTemplate.smt2            |   44.546s | 253.0MiB| unsat | 0 |  |  |
|simple-scaled200.bpl_Iteration1_Lasso_7-phaseTemplate.smt2   |   45.913s | 171.0MiB| sat | 0 |  |  |
|Collatz.bpl_Iteration1_Loop_6-phaseTemplate.smt2             |   46.971s | 489.0MiB| unsat | 0 |  |  |
|Collatz.bpl_Iteration1_Lasso_6-nestedTemplate.smt2           |   49.127s | 515.0MiB| unsat | 0 |  |  |
|polyrank5.t2.c_Iteration1_Loop_7-phaseTemplate.smt2          |   50.170s | 29.836MiB| sat | 0 |  |  |
|mbo_E25.smt2                                                 |   50.416s | 25.912MiB| unsat | 0 |  |  |
|polyrank4.t2.c_Iteration8_Loop_2-pieceTemplate.smt2          |   50.417s | 30.612MiB| unsat | 0 |  |  |
|kissing_4_4.smt2                                             |   50.571s | 88.748MiB| sat | 0 |  |  |
|mbo_E7E26.smt2                                               |   50.588s | 56.872MiB| unsat | 0 |  |  |
|polyrank4.t2.c_Iteration3_Loop_3-pieceTemplate.smt2          |   51.687s | 40.036MiB| unsat | 0 |  |  |
|yPositive-MixedIntReal.bpl_Iteration1_Loop_3-pieceTemplate.smt2 |   52.146s | 47.548MiB| unsat | 0 |  |  |
|iecs.t2.c_Iteration1_Loop_4-pieceTemplate.smt2               |   52.345s | 56.876MiB| unsat | 0 |  |  |
|eric2.t2.c_Iteration1_Loop_4-pieceTemplate.smt2              |   52.432s | 71.588MiB| unsat | 0 |  |  |
|Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2             |   52.436s | 51.884MiB| unsat | 0 |  |  |
|SantaBarbara01.bpl_Iteration1_Lasso_4-pieceTemplate.smt2     |   52.563s | 38.816MiB| unsat | 0 |  |  |
|BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2 |   52.684s | 54.244MiB| unsat | 0 |  |  |
|CookSeeZuleger-2013TACAS-Fig7b.bpl_Iteration1_Loop_3-pieceTemplate.smt2 |   53.262s | 103.0MiB| unsat | 0 |  |  |
|etcs_braking_2.01.redlog_global_7.smt2                       |   53.402s | 36.36MiB| unsat | 0 |  |  |
|mbo_E23E24.smt2                                              |   53.567s | 49.232MiB| unsat | 0 |  |  |
|LeeJonesBen-Amram-2001POPL-Ex4_true-termination.c_Iteration2_Loop_3-pieceTemplate.smt2 |   53.987s | 57.916MiB| unsat | 0 |  |  |
|mbo_E4E27.smt2                                               |   54.785s | 70.484MiB| unsat | 0 |  |  |
|KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-termination.c_Iteration1_Lasso_4-lexTemplate.smt2 |   55.127s | 280.0MiB| unsat | 0 |  |  |
|collatz.t2.c_Iteration3_Lasso_6-phaseTemplate.smt2           |   56.124s | 66.648MiB| unsat | 0 |  |  |
|LeeJonesBen-Amram-2001POPL-Ex1_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2 |   56.303s | 84.392MiB| unsat | 0 |  |  |
|sas2.t2.c_Iteration6_Lasso_7-nestedTemplate.smt2             |   56.777s | 54.064MiB| sat | 0 |  |  |
|mbo_E10E18.smt2                                              |   56.907s | 620.0MiB| unknown | 0 |  |  |
|mbo_E8E24.smt2                                               |   56.937s | 609.0MiB| unknown | 0 |  |  |
|polyrank3.t2.c_Iteration8_Loop_4-pieceTemplate.smt2          |   56.994s | 83.596MiB| unsat | 0 |  |  |
|mbo_E13E27.smt2                                              |   57.715s | 90.304MiB| unsat | 0 |  |  |
|mbo_E12E13.smt2                                              |   58.259s | 798.0MiB| unknown | 0 |  |  |
|etcs_braking_2.01.redlog_global_11.smt2                      |   58.577s | 52.368MiB| unsat | 0 |  |  |
|mbo_E9E23.smt2                                               |   58.614s | 87.148MiB| unsat | 0 |  |  |
|mbo_E2E4.smt2                                                |   58.637s | 884.0MiB| unknown | 0 |  |  |
|Masse_true-termination.c_Iteration1_Loop_2-pieceTemplate.smt2 |   58.661s | 97.384MiB| unsat | 0 |  |  |
|mbo_E1E13.smt2                                               |   58.716s | 880.0MiB| unknown | 0 |  |  |
|mbo_E3E8.smt2                                                |   59.011s | 909.0MiB| unknown | 0 |  |  |
|mbo_E2E10.smt2                                               |   59.027s | 770.0MiB| unknown | 0 |  |  |
|mbo_E6E19.smt2                                               |   60.635s | 952.0MiB| unknown | 0 |  |  |
|mbo_E7E16.smt2                                               |   60.747s | 99.0MiB| unsat | 0 |  |  |
|mbo_E3E13.smt2                                               |   60.966s | 849.0MiB| unknown | 0 |  |  |
|Nyala-TwoLex.bpl_Iteration1_Lasso_4-pieceTemplate.smt2       |   61.478s | 224.0MiB| unsat | 0 |  |  |
|Collatz.bpl_Iteration1_Lasso_2-pieceTemplate.smt2            |   63.855s | 519.0MiB| unsat | 0 |  |  |
|eric2.t2.c_Iteration7_Loop_4-pieceTemplate.smt2              |   69.560s | 316.0MiB| unsat | 0 |  |  |
|mbo_E20E25.smt2                                              |   72.876s | 53.796MiB| unsat | 0 |  |  |
|mbo_E3E23.smt2                                               |   77.595s | 490.0MiB| unsat | 0 |  |  |
|mbo_E15E28.smt2                                              |   79.098s | 478.0MiB| unsat | 0 |  |  |
|BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2 |   80.791s | 200.0MiB| unsat | 0 |  |  |
|mbo_E19E22.smt2                                              |   81.181s | 479.0MiB| unsat | 0 |  |  |
|mbo_E12E23.smt2                                              |   88.566s | 79.812MiB| unsat | 0 |  |  |
|firewire.t2.c_Iteration1_Lasso_7-nestedTemplate.smt2         |   88.619s | 95.964MiB| sat | 0 |  |  |
|matrix-5-all-13.smt2                                         |   94.370s | 383.0MiB| unknown | 0 |  |  |
|mbo_E11E20.smt2                                              |   97.243s | 81.232MiB| unsat | 0 |  |  |
|mbo_E8E14.smt2                                               |   99.889s | 949.0MiB| unknown | 0 |  |  |
|OpposedDisjuncts.bpl_Iteration1_Loop_4-pieceTemplate.smt2    |  108.435s | 296.0MiB| unsat | 0 |  |  |
|GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_6-nestedTemplate.smt2 |  113.319s | 599.0MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0265.smt2                                |  121.639s | 35.94MiB| unsat | 0 |  |  |
|sas2.t2.c_Iteration1_Lasso_4-pieceTemplate.smt2              |  122.287s | 450.0MiB| sat | 0 |  |  |
|mbo_E18E22.smt2                                              |  124.219s | 127.0MiB| unsat | 0 |  |  |
|sqrt-1mcosq-8-chunk-0176.smt2                                |  129.494s | 35.956MiB| unsat | 0 |  |  |
|GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_3-lexTemplate.smt2 |  133.246s | 867.0MiB| unsat | 0 |  |  |
|mbo_E16E25.smt2                                              |  177.530s | 162.0MiB| unsat | 0 |  |  |
|hong_10.smt2                                                 |  200.011s | 43.392MiB| timeout | 0 |  |  |
|linear_search.i_7_19_3.bpl_3.smt2                            |  200.011s | 51.592MiB| timeout | 0 |  |  |
|matrix-2-all-17.smt2                                         |  200.012s | 65.768MiB| timeout | 0 |  |  |
|atan-vega-3-weak-chunk-0385.smt2                             |  200.013s | 29.432MiB| timeout | 0 |  |  |
|InVarSynth_BugHoareAnnotationWithMinimiation.bpl_Iteration1_0.smt2 |  200.013s | 79.648MiB| timeout | 0 |  |  |
|fragtest_simple.i_4_5_4.bpl_3.smt2                           |  200.014s | 99.56MiB| timeout | 0 |  |  |
|kissing_3_9.smt2                                             |  200.015s | 76.572MiB| timeout | 0 |  |  |
|seq.i_5_5_5.bpl_3.smt2                                       |  200.015s | 80.18MiB| timeout | 0 |  |  |
|kissing_4_18.smt2                                            |  200.015s | 89.984MiB| timeout | 0 |  |  |
|matrix-4-all-22.smt2                                         |  200.016s | 150.0MiB| timeout | 0 |  |  |
|simple_ballistics_reach.01.seq_lazy_global_11.smt2           |  200.018s | 37.32MiB| timeout | 0 |  |  |
|standard_two_index_05.i_3_2_2.bpl_5.smt2                     |  200.019s | 109.0MiB| timeout | 0 |  |  |
|sin-problem-7-chunk-0297.smt2                                |  200.020s | 95.012MiB| timeout | 0 |  |  |
|InVarSynth_threadpooling_out2.mover.bpl_Iteration2_0.smt2    |  200.022s | 87.08MiB| timeout | 0 |  |  |
|matrix-3-all-13.smt2                                         |  200.024s | 234.0MiB| timeout | 0 |  |  |
|kissing_3_11.smt2                                            |  200.025s | 135.0MiB| timeout | 0 |  |  |
|matrix-4-all-4.smt2                                          |  200.029s | 278.0MiB| timeout | 0 |  |  |
|matrix-4-all-13.smt2                                         |  200.030s | 201.0MiB| timeout | 0 |  |  |
|avg60.i_5_5_4.bpl_3.smt2                                     |  200.030s | 38.54MiB| timeout | 0 |  |  |
|simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_9.smt2 |  200.032s | 56.484MiB| timeout | 0 |  |  |
|sqrt-1mcosq-8-chunk-0233.smt2                                |  200.033s | 73.264MiB| timeout | 0 |  |  |
|etcs_braking_2.01.seq_lazy_linear_enc_global_13.smt2         |  200.035s | 46.132MiB| timeout | 0 |  |  |
|simple_ballistics_reach.01.seq_lazy_lemmas_global_15.smt2    |  200.037s | 41.78MiB| timeout | 0 |  |  |
|mbo_E10E28.smt2                                              |  200.043s | 497.0MiB| timeout | 0 |  |  |
|heidy7-simple.t2.c_Iteration2_Lasso_4-pieceTemplate.smt2     |  200.045s | 367.0MiB| timeout | 0 |  |  |
|simple_ballistics_reach.01.seq_lazy_global_7.smt2            |  200.048s | 46.388MiB| timeout | 0 |  |  |
|mbo_E2E20.smt2                                               |  200.050s | 522.0MiB| timeout | 0 |  |  |
|simple_ballistics_reach.01.seq_lazy_linear_enc_global_5.smt2 |  200.051s | 146.0MiB| timeout | 0 |  |  |
|LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_7-phaseTemplate.smt2 |  200.056s | 459.0MiB| timeout | 0 |  |  |
|LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_3-pieceTemplate.smt2 |  200.061s | 507.0MiB| timeout | 0 |  |  |
|efegp.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2             |  200.070s | 525.0MiB| timeout | 0 |  |  |
|min_rf_true-termination.c_Iteration1_Loop_4-pieceTemplate.smt2 |  200.075s | 537.0MiB| timeout | 0 |  |  |
|afagp-fail.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2        |  200.075s | 564.0MiB| timeout | 0 |  |  |
|yPositive-SIscaled50.bpl_Iteration1_Loop_4-pieceTemplate.smt2 |  200.078s | 699.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.086s | 435.0MiB| timeout | 0 |  |  |
|simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_13.smt2 |  200.086s | 37.984MiB| timeout | 0 |  |  |
|NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2 |  200.090s | 748.0MiB| timeout | 0 |  |  |
|aviad_true-termination.c_Iteration1_Loop_6-phaseTemplate.smt2 |  200.098s | 844.0MiB| timeout | 0 |  |  |
|NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2 |  200.115s | 822.0MiB| timeout | 0 |  |  |
|aviad_true-termination.c_Iteration1_Loop_3-lexTemplate.smt2  |  200.126s | 1066.0MiB| timeout | 0 |  |  |
|Gulwani.bpl_Iteration1_Lasso_4-pieceTemplate.smt2            |  200.129s | 1205.0MiB| timeout | 0 |  |  |
|brp_withassume.t2.c_Iteration1_Loop_4-pieceTemplate.smt2     |  200.137s | 1314.0MiB| timeout | 0 |  |  |