# . * SAT 477 * UNSAT 605 * TIMEOUT 43 * UNKNOWN 22 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: master run
Job tag: bnsat_false
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: 51ae6eecccb3b4ea9e47261091933da3854cc537
Z3 branch: master
Z3 options: "-T:200"
Z3 inputs: inputs/QF_NRA_small
Z3 commit message: Merge pull request #8856 from angelica-moreira/memory-safety-pipeline

Add ASan/UBSan memory safety CI workflow
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |sin-cos-346-b-chunk-0316.smt2 | 0.025s | 18.716MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0079.smt2 | 0.025s | 18.84MiB| unsat | 0 | | | |Chua-1-VC2-L-chunk-0064.smt2 | 0.025s | 19.1MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0221.smt2 | 0.025s | 18.876MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_linear_enc_global_1.smt2 | 0.026s | 19.048MiB| unsat | 0 | | | |Chua-1-VC2-L-chunk-0027.smt2 | 0.026s | 19.116MiB| unsat | 0 | | | |ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.026s | 19.244MiB| unsat | 0 | | | |log-fun-ineq-g-chunk-0036.smt2 | 0.026s | 19.108MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0129.smt2 | 0.026s | 18.712MiB| unsat | 0 | | | |atan-vega-3-chunk-0220.smt2 | 0.026s | 18.776MiB| unsat | 0 | | | |ArthanM2-chunk-0012.smt2 | 0.026s | 19.048MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0378.smt2 | 0.027s | 18.932MiB| unsat | 0 | | | |ball_count_1d_plain.02.redlog_global_3.smt2 | 0.027s | 19.104MiB| unsat | 0 | | | |sin-problem-8-weak-chunk-0044.smt2 | 0.027s | 20.82MiB| sat | 0 | | | |atan-vega-3-chunk-0230.smt2 | 0.027s | 20.496MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0146.smt2 | 0.027s | 18.776MiB| unsat | 0 | | | |CMOS-opamp-chunk-0260.smt2 | 0.027s | 18.804MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0066.smt2 | 0.027s | 20.688MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_global_1.smt2 | 0.027s | 19.088MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.redlog_global_1.smt2 | 0.028s | 18.972MiB| unsat | 0 | | | |ball_count_1d_plain.10.seq_lazy_global_3.smt2 | 0.028s | 18.984MiB| unsat | 0 | | | |sin-problem-7-chunk-0129.smt2 | 0.028s | 20.816MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0081.smt2 | 0.028s | 20.704MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0661.smt2 | 0.028s | 18.876MiB| unsat | 0 | | | |polypaver-sqrt-circles-1a-chunk-0011.smt2 | 0.028s | 20.86MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0183.smt2 | 0.028s | 20.488MiB| sat | 0 | | | |sin-344-3-chunk-0058.smt2 | 0.028s | 20.724MiB| sat | 0 | | | |sin-cos-346-b-chunk-0102.smt2 | 0.028s | 18.828MiB| unsat | 0 | | | |CMOS-opamp-chunk-0231.smt2 | 0.028s | 20.752MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0104.smt2 | 0.028s | 18.848MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0009.smt2 | 0.028s | 18.672MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0117.smt2 | 0.028s | 20.992MiB| unsat | 0 | | | |sin-problem-7-weak2-chunk-0044.smt2 | 0.029s | 20.764MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0069.smt2 | 0.029s | 18.972MiB| unsat | 0 | | | |sin-problem-7-chunk-0233.smt2 | 0.029s | 21.056MiB| sat | 0 | | | |sin-cos-346-b-chunk-0078.smt2 | 0.029s | 18.832MiB| unsat | 0 | | | |Chua-2-VC2-L-chunk-0029.smt2 | 0.029s | 21.096MiB| sat | 0 | | | |ball_count_2d_plain.04.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.029s | 18.988MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0045.smt2 | 0.029s | 21.164MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0042.smt2 | 0.029s | 20.88MiB| sat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0050.smt2 | 0.029s | 20.668MiB| sat | 0 | | | |polypaver-bench-exp-3d-chunk-0126.smt2 | 0.029s | 20.896MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.redlog_global_11.smt2 | 0.029s | 19.74MiB| unsat | 0 | | | |atan-problem-1-chunk-0022.smt2 | 0.029s | 20.508MiB| sat | 0 | | | |Chua-1-VC2-L-chunk-0050.smt2 | 0.029s | 20.628MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.redlog_global_3.smt2 | 0.029s | 19.136MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0144.smt2 | 0.029s | 20.792MiB| sat | 0 | | | |exp-problem-10-2-chunk-0385.smt2 | 0.029s | 20.764MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0171.smt2 | 0.029s | 18.78MiB| unsat | 0 | | | |ball_count_2d_slope.02.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.030s | 19.068MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0016.smt2 | 0.030s | 20.704MiB| sat | 0 | | | |exp-problem-10-3-chunk-0084.smt2 | 0.030s | 18.968MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0044.smt2 | 0.030s | 18.864MiB| unsat | 0 | | | |ball_count_2d_slope.02.seq_lazy_global_3.smt2 | 0.030s | 19.352MiB| unsat | 0 | | | |atan-problem-1-chunk-0006.smt2 | 0.030s | 20.78MiB| sat | 0 | | | |atan-vega-3-chunk-0583.smt2 | 0.030s | 20.828MiB| sat | 0 | | | |ArthanKM2-chunk-0002.smt2 | 0.030s | 20.7MiB| sat | 0 | | | |sin-problem-10-3-chunk-0033.smt2 | 0.030s | 20.732MiB| unsat | 0 | | | |CMOS-opamp-chunk-0025.smt2 | 0.030s | 20.604MiB| sat | 0 | | | |sin-problem-7-chunk-0361.smt2 | 0.030s | 18.848MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0237.smt2 | 0.030s | 20.84MiB| sat | 0 | | | |exp-problem-10-3-chunk-0010.smt2 | 0.030s | 20.804MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0043.smt2 | 0.030s | 20.864MiB| sat | 0 | | | |sin-problem-7-chunk-0156.smt2 | 0.030s | 20.716MiB| unsat | 0 | | | |matrix-1-all-47.smt2 | 0.030s | 20.7MiB| unsat | 0 | | | |sin-problem-7-chunk-0091.smt2 | 0.030s | 20.656MiB| sat | 0 | | | |ball_count_1d_plain.03.seq_lazy_lemmas_global_1.smt2 | 0.030s | 19.02MiB| unsat | 0 | | | |cbrt-problem-3-chunk-0070.smt2 | 0.030s | 20.704MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0091.smt2 | 0.030s | 20.764MiB| sat | 0 | | | |sin-cos-346-b-chunk-0572.smt2 | 0.030s | 20.716MiB| sat | 0 | | | |sin-cos-346-b-chunk-0242.smt2 | 0.030s | 20.848MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0144.smt2 | 0.031s | 20.764MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.031s | 19.564MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0181.smt2 | 0.031s | 18.744MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0115.smt2 | 0.031s | 20.652MiB| sat | 0 | | | |atan-vega-3-chunk-0129.smt2 | 0.031s | 20.432MiB| sat | 0 | | | |CMOS-opamp-chunk-0342.smt2 | 0.031s | 20.776MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0130.smt2 | 0.031s | 20.676MiB| unsat | 0 | | | |sin-problem-7-chunk-0257.smt2 | 0.031s | 20.932MiB| sat | 0 | | | |sin-problem-7-weak2-chunk-0057.smt2 | 0.031s | 20.628MiB| sat | 0 | | | |exp-problem-10-3-chunk-0148.smt2 | 0.031s | 20.764MiB| unsat | 0 | | | |Chua-1-VC1-U-chunk-0044.smt2 | 0.031s | 20.584MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_lemmas_global_5.smt2 | 0.031s | 19.248MiB| unsat | 0 | | | |MulliganEconomicsModel0018e.smt2 | 0.031s | 20.808MiB| sat | 0 | | | |atan-vega-3-chunk-0210.smt2 | 0.031s | 21.156MiB| sat | 0 | | | |sin-cos-346-b-chunk-0092.smt2 | 0.031s | 19.056MiB| unsat | 0 | | | |atan-vega-3-chunk-0045.smt2 | 0.031s | 20.804MiB| sat | 0 | | | |atan-vega-3-chunk-0011.smt2 | 0.031s | 20.872MiB| sat | 0 | | | |CMOS-opamp-chunk-0108.smt2 | 0.031s | 20.872MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0159.smt2 | 0.031s | 20.644MiB| sat | 0 | | | |exp-problem-10-2-chunk-0184.smt2 | 0.031s | 20.764MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0123.smt2 | 0.031s | 20.508MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0083.smt2 | 0.032s | 20.764MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0100.smt2 | 0.032s | 20.88MiB| sat | 0 | | | |Lyapunov1a-chunk-0021.smt2 | 0.032s | 20.76MiB| sat | 0 | | | |sin-cos-346-b-chunk-0348.smt2 | 0.032s | 18.72MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0576.smt2 | 0.032s | 20.8MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0126.smt2 | 0.032s | 20.92MiB| sat | 0 | | | |Chua-1-IL-L-chunk-0154.smt2 | 0.032s | 20.736MiB| sat | 0 | | | |atan-problem-2-chunk-0117.smt2 | 0.032s | 20.968MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0555.smt2 | 0.032s | 20.836MiB| sat | 0 | | | |Chua-2-VC2-U-chunk-0039.smt2 | 0.032s | 20.88MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0160.smt2 | 0.032s | 20.62MiB| unsat | 0 | | | |sin-344-3-weak-chunk-0017.smt2 | 0.032s | 20.844MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0024.smt2 | 0.032s | 20.876MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0728.smt2 | 0.032s | 20.584MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0024.smt2 | 0.032s | 20.588MiB| unsat | 0 | | | |gen-09.smt2 | 0.032s | 20.796MiB| sat | 0 | | | |sin-344-3-chunk-0029.smt2 | 0.032s | 20.8MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0020.smt2 | 0.032s | 20.588MiB| sat | 0 | | | |ball_count_2d_plain.02.seq_lazy_linear_enc_lemmas_global_7.smt2 | 0.032s | 19.516MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0059.smt2 | 0.032s | 20.672MiB| unsat | 0 | | | |atan-vega-3-chunk-0139.smt2 | 0.032s | 20.796MiB| sat | 0 | | | |atan-vega-3-chunk-0330.smt2 | 0.032s | 20.712MiB| sat | 0 | | | |sin-problem-8-chunk-0026.smt2 | 0.032s | 20.816MiB| unsat | 0 | | | |CMOS-opamp-chunk-0137.smt2 | 0.032s | 20.764MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0097.smt2 | 0.032s | 20.648MiB| sat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0034.smt2 | 0.032s | 20.788MiB| unsat | 0 | | | |bottom-plate-mixer-chunk-0039.smt2 | 0.032s | 20.648MiB| sat | 0 | | | |ball_count_2d_hill.01.seq_lazy_global_3.smt2 | 0.032s | 19.104MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0029.smt2 | 0.032s | 20.868MiB| sat | 0 | | | |cbrt-problem-3-chunk-0055.smt2 | 0.032s | 20.82MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0299.smt2 | 0.032s | 20.576MiB| sat | 0 | | | |CMOS-opamp-chunk-0148.smt2 | 0.032s | 20.836MiB| sat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0086.smt2 | 0.032s | 20.648MiB| sat | 0 | | | |sqrt-problem-12vars3-chunk-0068.smt2 | 0.032s | 20.74MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0157.smt2 | 0.032s | 20.72MiB| sat | 0 | | | |exp-problem-10-3-chunk-0021.smt2 | 0.032s | 18.728MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0048.smt2 | 0.033s | 20.832MiB| sat | 0 | | | |sin-cos-346-b-chunk-0209.smt2 | 0.033s | 20.864MiB| sat | 0 | | | |sin-problem-7-chunk-0054.smt2 | 0.033s | 20.74MiB| sat | 0 | | | |sin-cos-346-b-chunk-0434.smt2 | 0.033s | 20.972MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0036.smt2 | 0.033s | 20.744MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0196.smt2 | 0.033s | 20.72MiB| sat | 0 | | | |exp-problem-10-2-chunk-0134.smt2 | 0.033s | 20.788MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0093.smt2 | 0.033s | 20.72MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0619.smt2 | 0.033s | 20.684MiB| sat | 0 | | | |sqrt-problem-13-vars5-chunk-0026.smt2 | 0.033s | 20.768MiB| sat | 0 | | | |Chua-1-IL-U-chunk-0038.smt2 | 0.033s | 20.712MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0102.smt2 | 0.033s | 20.98MiB| sat | 0 | | | |ball_count_2d_plain.10.seq_lazy_lemmas_global_1.smt2 | 0.033s | 19.064MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0056.smt2 | 0.033s | 20.732MiB| sat | 0 | | | |CMOS-opamp-chunk-0213.smt2 | 0.033s | 20.648MiB| sat | 0 | | | |atan-problem-2-chunk-0059.smt2 | 0.033s | 20.972MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0490.smt2 | 0.033s | 20.68MiB| sat | 0 | | | |ball_count_2d_hill_simple.10.qfree_global_9.smt2 | 0.033s | 19.288MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0504.smt2 | 0.033s | 20.592MiB| sat | 0 | | | |sin-cos-346-b-chunk-0252.smt2 | 0.033s | 20.788MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0310.smt2 | 0.033s | 20.768MiB| sat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_linear_enc_global_5.smt2 | 0.033s | 19.316MiB| unsat | 0 | | | |atan-problem-2-chunk-0080.smt2 | 0.033s | 20.82MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0600.smt2 | 0.033s | 20.924MiB| unsat | 0 | | | |asin-8-vars4-chunk-0034.smt2 | 0.033s | 20.768MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0190.smt2 | 0.033s | 20.764MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0508.smt2 | 0.033s | 20.864MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0265.smt2 | 0.033s | 18.86MiB| unsat | 0 | | | |ball_count_1d_plain.01.seq_lazy_lemmas_global_11.smt2 | 0.033s | 19.688MiB| unsat | 0 | | | |atan-vega-3-chunk-0027.smt2 | 0.033s | 20.716MiB| sat | 0 | | | |atan-vega-3-chunk-0159.smt2 | 0.033s | 20.768MiB| sat | 0 | | | |Chua-1-IL-U-chunk-0025.smt2 | 0.033s | 20.684MiB| sat | 0 | | | |atan-vega-3-chunk-0553.smt2 | 0.033s | 21.012MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0103.smt2 | 0.033s | 20.852MiB| unsat | 0 | | | |Lyapunov1a-chunk-0011.smt2 | 0.033s | 20.46MiB| sat | 0 | | | |Chua-2-VC2-L-chunk-0052.smt2 | 0.033s | 20.664MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0078.smt2 | 0.033s | 20.636MiB| sat | 0 | | | |mbo_E6.smt2 | 0.034s | 21.012MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0218.smt2 | 0.034s | 20.916MiB| unsat | 0 | | | |ball_count_1d_plain.01.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.034s | 19.364MiB| unsat | 0 | | | |atan-vega-3-chunk-0423.smt2 | 0.034s | 20.736MiB| sat | 0 | | | |atan-vega-3-chunk-0453.smt2 | 0.034s | 20.936MiB| unsat | 0 | | | |ball_count_2d_slope.05.seq_lazy_lemmas_global_1.smt2 | 0.034s | 19.188MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0158.smt2 | 0.034s | 20.76MiB| sat | 0 | | | |sin-cos-346-b-chunk-0126.smt2 | 0.034s | 20.684MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0504.smt2 | 0.034s | 20.92MiB| sat | 0 | | | |Chua-2-VC2-U-chunk-0066.smt2 | 0.034s | 20.664MiB| unsat | 0 | | | |CMOS-opamp-chunk-0062.smt2 | 0.034s | 20.752MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0154.smt2 | 0.034s | 20.684MiB| unsat | 0 | | | |hong_2.smt2 | 0.034s | 20.676MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0339.smt2 | 0.034s | 20.848MiB| sat | 0 | | | |exp-problem-10-2-chunk-0102.smt2 | 0.034s | 20.796MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0398.smt2 | 0.034s | 20.888MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0481.smt2 | 0.034s | 20.98MiB| unsat | 0 | | | |CONVOI2-chunk-0018.smt2 | 0.034s | 20.768MiB| sat | 0 | | | |exp-problem-10-3-chunk-0042.smt2 | 0.034s | 20.656MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0081.smt2 | 0.034s | 20.66MiB| sat | 0 | | | |sin-problem-7-chunk-0208.smt2 | 0.034s | 20.764MiB| sat | 0 | | | |sin-cos-346-b-chunk-0454.smt2 | 0.034s | 20.684MiB| sat | 0 | | | |Chua-1-VC2-L-chunk-0077.smt2 | 0.034s | 21.256MiB| sat | 0 | | | |exp-problem-10-3-chunk-0096.smt2 | 0.034s | 20.724MiB| unsat | 0 | | | |Chua-1-VC2-L-chunk-0039.smt2 | 0.034s | 20.828MiB| unsat | 0 | | | |atan-problem-2-weakT-chunk-0019.smt2 | 0.034s | 20.92MiB| sat | 0 | | | |sin-problem-7-weak2-chunk-0088.smt2 | 0.034s | 18.752MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0036.smt2 | 0.034s | 20.904MiB| unsat | 0 | | | |atan-vega-3-chunk-0623.smt2 | 0.034s | 20.816MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0069.smt2 | 0.034s | 20.84MiB| unsat | 0 | | | |atan-vega-3-chunk-0523.smt2 | 0.034s | 20.936MiB| sat | 0 | | | |sin-cos-346-b-chunk-0424.smt2 | 0.034s | 20.836MiB| unsat | 0 | | | |CMOS-opamp-chunk-0298.smt2 | 0.034s | 20.88MiB| sat | 0 | | | |CMOS-opamp-chunk-0047.smt2 | 0.034s | 20.784MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0405.smt2 | 0.035s | 20.796MiB| sat | 0 | | | |sin-problem-8-chunk-0054.smt2 | 0.035s | 20.78MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0053.smt2 | 0.035s | 20.696MiB| sat | 0 | | | |sin-cos-346-b-chunk-0272.smt2 | 0.035s | 20.596MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0541.smt2 | 0.035s | 20.624MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0067.smt2 | 0.035s | 20.528MiB| sat | 0 | | | |sin-cos-346-b-chunk-0068.smt2 | 0.035s | 18.992MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.035s | 19.2MiB| unsat | 0 | | | |MulliganEconomicsModel0063e.smt2 | 0.035s | 20.828MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0444.smt2 | 0.035s | 20.944MiB| sat | 0 | | | |atan-vega-3-chunk-0057.smt2 | 0.035s | 20.816MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0057.smt2 | 0.035s | 20.508MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0369.smt2 | 0.035s | 20.796MiB| sat | 0 | | | |atan-vega-3-chunk-0483.smt2 | 0.035s | 20.84MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0224.smt2 | 0.035s | 20.764MiB| sat | 0 | | | |Chua-1-IL-U-chunk-0049.smt2 | 0.035s | 20.896MiB| sat | 0 | | | |sqrt-circles-3-chunk-0016.smt2 | 0.035s | 20.92MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0510.smt2 | 0.035s | 20.784MiB| unsat | 0 | | | |CMOS-opamp-chunk-0275.smt2 | 0.035s | 20.744MiB| sat | 0 | | | |atan-vega-3-chunk-0280.smt2 | 0.035s | 20.992MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0086.smt2 | 0.035s | 20.728MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0080.smt2 | 0.035s | 20.936MiB| sat | 0 | | | |sin-problem-7-weak2-chunk-0075.smt2 | 0.035s | 20.656MiB| sat | 0 | | | |exp-problem-10-2-chunk-0090.smt2 | 0.035s | 20.744MiB| unsat | 0 | | | |ball_count_2d_plain.04.qfree_global_1.smt2 | 0.036s | 19.084MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0146.smt2 | 0.036s | 21.06MiB| sat | 0 | | | |sqrt-problem-Melquiond3-chunk-0018.smt2 | 0.036s | 20.772MiB| sat | 0 | | | |ball_count_2d_slope.01.seq_lazy_linear_enc_global_1.smt2 | 0.036s | 18.916MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0108.smt2 | 0.036s | 20.74MiB| sat | 0 | | | |MulliganEconomicsModel0013c.smt2 | 0.036s | 20.652MiB| sat | 0 | | | |atan-vega-3-chunk-0503.smt2 | 0.036s | 20.808MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0250.smt2 | 0.036s | 20.648MiB| sat | 0 | | | |sin-problem-7-chunk-0221.smt2 | 0.036s | 20.82MiB| sat | 0 | | | |exp-problem-10-2-chunk-0265.smt2 | 0.036s | 20.68MiB| sat | 0 | | | |asin-8-vars4-chunk-0019.smt2 | 0.036s | 20.74MiB| sat | 0 | | | |atan-vega-3-chunk-0613.smt2 | 0.036s | 20.764MiB| sat | 0 | | | |ball_count_2d_plain.01.seq_lazy_linear_enc_global_13.smt2 | 0.036s | 19.74MiB| unsat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0015.smt2 | 0.036s | 20.648MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.redlog_global_3.smt2 | 0.036s | 19.204MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.036s | 20.156MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0139.smt2 | 0.036s | 20.792MiB| sat | 0 | | | |ball_count_2d_hill.02.seq_lazy_global_3.smt2 | 0.036s | 19.268MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_global_7.smt2 | 0.036s | 19.36MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0194.smt2 | 0.036s | 20.476MiB| unsat | 0 | | | |atan-problem-2-sqrt-chunk-0019.smt2 | 0.036s | 20.872MiB| unsat | 0 | | | |CONVOI2-chunk-0031.smt2 | 0.036s | 20.68MiB| sat | 0 | | | |Chua-1-VC1-U-chunk-0056.smt2 | 0.036s | 20.816MiB| sat | 0 | | | |sin-cos-346-b-chunk-0524.smt2 | 0.036s | 18.78MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0034.smt2 | 0.036s | 20.624MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0496.smt2 | 0.036s | 20.716MiB| sat | 0 | | | |ball_count_2d_slope.01.seq_lazy_global_7.smt2 | 0.037s | 19.756MiB| unsat | 0 | | | |atan-vega-3-chunk-0413.smt2 | 0.037s | 20.752MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_linear_enc_global_1.smt2 | 0.037s | 18.924MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0073.smt2 | 0.037s | 20.604MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.redlog_global_7.smt2 | 0.037s | 19.292MiB| unsat | 0 | | | |MulliganEconomicsModel0030e.smt2 | 0.037s | 20.868MiB| sat | 0 | | | |sin-cos-346-b-chunk-0326.smt2 | 0.037s | 20.86MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0070.smt2 | 0.037s | 20.724MiB| unsat | 0 | | | |Chua-2-IL-L-chunk-0047.smt2 | 0.037s | 18.768MiB| unsat | 0 | | | |atan-vega-3-chunk-0543.smt2 | 0.037s | 20.668MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0479.smt2 | 0.037s | 20.824MiB| sat | 0 | | | |ball_count_2d_hill.02.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.037s | 18.972MiB| unsat | 0 | | | |CMOS-opamp-chunk-0310.smt2 | 0.037s | 20.796MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0374.smt2 | 0.037s | 20.636MiB| unsat | 0 | | | |ball_count_1d_plain.02.qfree_global_9.smt2 | 0.037s | 19.504MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.037s | 19.712MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0545.smt2 | 0.037s | 20.616MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0168.smt2 | 0.037s | 20.712MiB| sat | 0 | | | |ball_count_2d_plain.10.qfree_global_3.smt2 | 0.037s | 19.172MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_global_3.smt2 | 0.037s | 20.912MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0306.smt2 | 0.037s | 20.656MiB| unsat | 0 | | | |polypaver-bench-exp-3d-chunk-0028.smt2 | 0.037s | 20.932MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0084.smt2 | 0.037s | 20.704MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0206.smt2 | 0.037s | 20.704MiB| unsat | 0 | | | |atan-problem-1-chunk-0091.smt2 | 0.037s | 20.624MiB| sat | 0 | | | |cos-problem-5-chunk-0039.smt2 | 0.037s | 20.728MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0179.smt2 | 0.038s | 20.824MiB| unsat | 0 | | | |ball_count_1d_plain.03.qfree_global_3.smt2 | 0.038s | 21.028MiB| unsat | 0 | | | |Chua-2-VC1-U-chunk-0087.smt2 | 0.038s | 21.348MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0522.smt2 | 0.038s | 20.82MiB| sat | 0 | | | |atan-vega-3-chunk-0433.smt2 | 0.038s | 20.828MiB| sat | 0 | | | |polypaver-sqrt43-int-4vars-chunk-0026.smt2 | 0.038s | 20.844MiB| sat | 0 | | | |sin-cos-346-b-chunk-0474.smt2 | 0.038s | 20.944MiB| unsat | 0 | | | |ball_count_1d_plain.01.qfree_global_5.smt2 | 0.038s | 19.208MiB| unsat | 0 | | | |sin-problem-7-chunk-0311.smt2 | 0.038s | 21.02MiB| sat | 0 | | | |sin-cos-346-b-chunk-0338.smt2 | 0.038s | 20.796MiB| sat | 0 | | | |cos-problem-5-chunk-0023.smt2 | 0.038s | 20.664MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_linear_enc_global_13.smt2 | 0.038s | 19.608MiB| unsat | 0 | | | |ball_count_1d_plain.10.qfree_global_5.smt2 | 0.038s | 19.116MiB| unsat | 0 | | | |ball_count_2d_hill.10.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.038s | 19.512MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0111.smt2 | 0.038s | 20.908MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0029.smt2 | 0.038s | 20.656MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0255.smt2 | 0.038s | 20.804MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0415.smt2 | 0.038s | 20.78MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0071.smt2 | 0.038s | 20.984MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0091.smt2 | 0.038s | 20.808MiB| unsat | 0 | | | |ball_count_1d_plain.01.qfree_global_1.smt2 | 0.038s | 19.052MiB| unsat | 0 | | | |MulliganEconomicsModel0024a.smt2 | 0.038s | 20.856MiB| sat | 0 | | | |ball_count_2d_plain.02.seq_lazy_global_5.smt2 | 0.038s | 19.232MiB| unsat | 0 | | | |ball_count_1d_plain.10.seq_lazy_lemmas_global_11.smt2 | 0.039s | 19.568MiB| unsat | 0 | | | |ball_count_1d_plain.10.seq_lazy_linear_enc_global_15.smt2 | 0.039s | 19.916MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0711.smt2 | 0.039s | 20.876MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_global_11.smt2 | 0.039s | 20.28MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0198.smt2 | 0.039s | 20.852MiB| sat | 0 | | | |ball_count_2d_plain.02.qfree_global_7.smt2 | 0.039s | 19.232MiB| unsat | 0 | | | |atan-vega-3-chunk-0533.smt2 | 0.039s | 20.788MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0108.smt2 | 0.039s | 20.808MiB| unsat | 0 | | | |ball_count_1d_plain.01.seq_lazy_lemmas_global_7.smt2 | 0.039s | 19.44MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0028.smt2 | 0.039s | 20.748MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0075.smt2 | 0.039s | 20.652MiB| sat | 0 | | | |atan-vega-3-chunk-0067.smt2 | 0.039s | 20.84MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0120.smt2 | 0.039s | 20.82MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0086.smt2 | 0.039s | 21.004MiB| sat | 0 | | | |ball_count_2d_hill.04.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.039s | 19.084MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.qfree_global_9.smt2 | 0.039s | 19.368MiB| unsat | 0 | | | |sin-problem-7-weak2-chunk-0100.smt2 | 0.039s | 21.052MiB| unsat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0065.smt2 | 0.039s | 20.656MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0062.smt2 | 0.039s | 20.868MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0189.smt2 | 0.039s | 20.84MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0222.smt2 | 0.039s | 20.804MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0312.smt2 | 0.039s | 20.872MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0014.smt2 | 0.039s | 20.824MiB| sat | 0 | | | |Chua-2-VC1-L-chunk-0097.smt2 | 0.040s | 20.764MiB| unsat | 0 | | | |ball_count_2d_plain.04.qfree_global_5.smt2 | 0.040s | 21.044MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0285.smt2 | 0.040s | 20.764MiB| sat | 0 | | | |ball_count_2d_plain.01.redlog_global_11.smt2 | 0.040s | 20.096MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0456.smt2 | 0.040s | 18.912MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0307.smt2 | 0.040s | 20.792MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0028.smt2 | 0.040s | 20.808MiB| sat | 0 | | | |sin-problem-8-chunk-0043.smt2 | 0.040s | 20.78MiB| sat | 0 | | | |ball_count_2d_hill.02.seq_lazy_lemmas_global_7.smt2 | 0.040s | 19.844MiB| unsat | 0 | | | |atan-problem-2-weakT-chunk-0041.smt2 | 0.040s | 20.916MiB| sat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_lemmas_global_1.smt2 | 0.040s | 19.012MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0721.smt2 | 0.040s | 21.016MiB| sat | 0 | | | |sin-cos-346-b-chunk-0030.smt2 | 0.040s | 20.628MiB| sat | 0 | | | |ball_count_2d_plain.02.seq_lazy_linear_enc_lemmas_global_11.smt2 | 0.040s | 19.828MiB| unsat | 0 | | | |ball_count_2d_plain.04.seq_lazy_global_3.smt2 | 0.040s | 20.992MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0493.smt2 | 0.040s | 20.908MiB| sat | 0 | | | |sin-problem-7-weak-chunk-0101.smt2 | 0.040s | 20.864MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0639.smt2 | 0.040s | 20.888MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0063.smt2 | 0.040s | 20.704MiB| sat | 0 | | | |exp-problem-10-2-chunk-0285.smt2 | 0.040s | 20.776MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0435.smt2 | 0.040s | 20.704MiB| unsat | 0 | | | |atan-vega-3-chunk-0400.smt2 | 0.041s | 20.764MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0037.smt2 | 0.041s | 20.792MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0087.smt2 | 0.041s | 20.932MiB| unsat | 0 | | | |atan-problem-2-weakT-chunk-0030.smt2 | 0.041s | 20.688MiB| unsat | 0 | | | |ball_count_2d_slope.10.seq_lazy_global_7.smt2 | 0.041s | 19.888MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0174.smt2 | 0.041s | 20.768MiB| sat | 0 | | | |sin-344-4-chunk-0050.smt2 | 0.041s | 21.464MiB| sat | 0 | | | |etcs_braking_2.01.seq_lazy_lemmas_global_1.smt2 | 0.041s | 21.148MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0330.smt2 | 0.041s | 20.824MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0100.smt2 | 0.041s | 20.844MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0024.smt2 | 0.041s | 20.76MiB| sat | 0 | | | |Chua-2-VC2-L-chunk-0062.smt2 | 0.041s | 20.768MiB| sat | 0 | | | |atan-vega-3-chunk-0250.smt2 | 0.041s | 20.732MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0143.smt2 | 0.041s | 20.812MiB| unsat | 0 | | | |CMOS-opamp-chunk-0086.smt2 | 0.041s | 20.868MiB| sat | 0 | | | |atan-vega-3-chunk-0350.smt2 | 0.041s | 18.9MiB| unsat | 0 | | | |ball_count_2d_slope.02.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.041s | 19.572MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0536.smt2 | 0.041s | 20.8MiB| sat | 0 | | | |sin-cos-346-b-chunk-0607.smt2 | 0.041s | 20.808MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0391.smt2 | 0.042s | 20.724MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0038.smt2 | 0.042s | 20.68MiB| sat | 0 | | | |ball_count_2d_plain.05.seq_lazy_linear_enc_global_1.smt2 | 0.042s | 18.932MiB| unsat | 0 | | | |ball_count_2d_plain.02.seq_lazy_linear_enc_global_3.smt2 | 0.042s | 19.136MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0295.smt2 | 0.042s | 20.768MiB| sat | 0 | | | |Arthan1A-chunk-0020.smt2 | 0.042s | 20.648MiB| sat | 0 | | | |exp-problem-10-3-chunk-0168.smt2 | 0.042s | 20.784MiB| sat | 0 | | | |ball_count_2d_hill.02.seq_lazy_lemmas_global_11.smt2 | 0.042s | 20.112MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0101.smt2 | 0.042s | 18.788MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0073.smt2 | 0.042s | 20.772MiB| sat | 0 | | | |sin-problem-7-chunk-0105.smt2 | 0.042s | 20.852MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0164.smt2 | 0.042s | 20.772MiB| sat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0062.smt2 | 0.042s | 20.768MiB| sat | 0 | | | |exp-problem-10-3-chunk-0128.smt2 | 0.042s | 20.808MiB| unsat | 0 | | | |sin-problem-8-weak-chunk-0056.smt2 | 0.042s | 20.68MiB| unsat | 0 | | | |MulliganEconomicsModel0080e.smt2 | 0.042s | 20.884MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.042s | 20.232MiB| unsat | 0 | | | |sqrt-problem-12vars3-chunk-0025.smt2 | 0.042s | 20.752MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_linear_enc_global_9.smt2 | 0.042s | 19.488MiB| unsat | 0 | | | |ball_count_1d_plain.05.seq_lazy_lemmas_global_3.smt2 | 0.042s | 21.176MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0151.smt2 | 0.042s | 18.916MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_global_3.smt2 | 0.042s | 21.272MiB| unsat | 0 | | | |sqrt-circles-2-chunk-0002.smt2 | 0.042s | 20.752MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0278.smt2 | 0.043s | 20.736MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_global_11.smt2 | 0.043s | 19.6MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0050.smt2 | 0.043s | 20.616MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0127.smt2 | 0.043s | 20.948MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0032.smt2 | 0.043s | 20.708MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0301.smt2 | 0.043s | 20.708MiB| sat | 0 | | | |Chua-2-VC2-L-chunk-0013.smt2 | 0.043s | 20.76MiB| sat | 0 | | | |atan-problem-1-chunk-0071.smt2 | 0.043s | 20.62MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0596.smt2 | 0.043s | 20.668MiB| unsat | 0 | | | |atan-vega-3-chunk-0340.smt2 | 0.043s | 20.76MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0586.smt2 | 0.043s | 20.828MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0093.smt2 | 0.043s | 20.764MiB| sat | 0 | | | |sin-problem-7-chunk-0192.smt2 | 0.043s | 20.992MiB| sat | 0 | | | |ball_count_2d_slope.10.seq_lazy_linear_enc_global_1.smt2 | 0.043s | 19.104MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0107.smt2 | 0.043s | 20.652MiB| unsat | 0 | | | |sqrt-problem-12vars3-chunk-0081.smt2 | 0.043s | 20.872MiB| sat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0009.smt2 | 0.043s | 20.644MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0032.smt2 | 0.043s | 20.656MiB| sat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0080.smt2 | 0.043s | 20.736MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0168.smt2 | 0.043s | 20.796MiB| sat | 0 | | | |sqrt-problem-12vars3-chunk-0010.smt2 | 0.044s | 20.64MiB| sat | 0 | | | |exp-problem-10-2-chunk-0059.smt2 | 0.044s | 19.28MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0117.smt2 | 0.044s | 20.752MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0112.smt2 | 0.044s | 20.892MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0137.smt2 | 0.044s | 20.64MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0212.smt2 | 0.044s | 20.892MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0629.smt2 | 0.044s | 20.908MiB| sat | 0 | | | |ball_count_2d_hill_simple.03.qfree_global_7.smt2 | 0.044s | 21.14MiB| unsat | 0 | | | |sin-problem-10-2-chunk-0024.smt2 | 0.044s | 18.8MiB| unsat | 0 | | | |atan-problem-1-chunk-0058.smt2 | 0.044s | 20.796MiB| sat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_linear_enc_global_7.smt2 | 0.044s | 21.104MiB| unsat | 0 | | | |polypaver-bench-exp-3d-chunk-0072.smt2 | 0.044s | 20.94MiB| sat | 0 | | | |ball_count_2d_hill.05.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.044s | 19.032MiB| unsat | 0 | | | |ball_count_1d_plain.10.seq_lazy_lemmas_global_7.smt2 | 0.044s | 19.34MiB| unsat | 0 | | | |ball_count_1d_plain.05.redlog_global_1.smt2 | 0.044s | 18.972MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0241.smt2 | 0.044s | 20.732MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0167.smt2 | 0.045s | 20.768MiB| sat | 0 | | | |atan-vega-3-chunk-0199.smt2 | 0.045s | 20.68MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0657.smt2 | 0.045s | 20.852MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0131.smt2 | 0.045s | 20.696MiB| unsat | 0 | | | |ball_count_1d_plain.03.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.045s | 20.928MiB| unsat | 0 | | | |ball_count_2d_plain.02.seq_lazy_lemmas_global_13.smt2 | 0.045s | 19.876MiB| unsat | 0 | | | |atan-vega-3-chunk-0169.smt2 | 0.045s | 20.464MiB| sat | 0 | | | |exp-problem-10-2-chunk-0358.smt2 | 0.045s | 20.672MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_global_11.smt2 | 0.045s | 19.68MiB| unsat | 0 | | | |sqrt-problem-13-sqrt1-chunk-0049.smt2 | 0.045s | 20.584MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0143.smt2 | 0.045s | 20.804MiB| sat | 0 | | | |atan-vega-3-chunk-0099.smt2 | 0.045s | 20.488MiB| sat | 0 | | | |atan-problem-1-chunk-0081.smt2 | 0.045s | 20.744MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0691.smt2 | 0.045s | 20.656MiB| sat | 0 | | | |exp-problem-10-3-chunk-0106.smt2 | 0.045s | 20.768MiB| sat | 0 | | | |Chua-1-IL-L-chunk-0090.smt2 | 0.046s | 20.652MiB| sat | 0 | | | |Chua-1-VC1-U-chunk-0032.smt2 | 0.046s | 20.66MiB| sat | 0 | | | |ball_count_2d_hill.10.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.046s | 18.936MiB| unsat | 0 | | | |Chua-1-IL-U-chunk-0063.smt2 | 0.046s | 20.764MiB| sat | 0 | | | |sin-cos-346-b-chunk-0494.smt2 | 0.046s | 20.784MiB| sat | 0 | | | |matrix-1-all-8.smt2 | 0.046s | 20.936MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0045.smt2 | 0.046s | 18.984MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0534.smt2 | 0.046s | 19.224MiB| unsat | 0 | | | |polypaver-bench-exp-3d-chunk-0085.smt2 | 0.046s | 20.552MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0409.smt2 | 0.046s | 20.804MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0202.smt2 | 0.046s | 21.016MiB| sat | 0 | | | |ball_count_1d_plain.02.seq_lazy_linear_enc_global_5.smt2 | 0.046s | 19.228MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0230.smt2 | 0.046s | 21.316MiB| unsat | 0 | | | |atan-vega-3-chunk-0310.smt2 | 0.046s | 20.836MiB| sat | 0 | | | |CMOS-opamp-chunk-0190.smt2 | 0.046s | 20.808MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0126.smt2 | 0.046s | 20.992MiB| sat | 0 | | | |ball_count_2d_hill.10.seq_lazy_lemmas_global_7.smt2 | 0.046s | 19.66MiB| unsat | 0 | | | |mbo_E17E23.smt2 | 0.046s | 20.74MiB| unsat | 0 | | | |CMOS-opamp-chunk-0169.smt2 | 0.047s | 20.844MiB| sat | 0 | | | |sqrt-problem-13-chunk-0019.smt2 | 0.047s | 20.524MiB| sat | 0 | | | |Chua-2-VC1-L-chunk-0052.smt2 | 0.047s | 20.736MiB| sat | 0 | | | |atan-vega-3-chunk-0179.smt2 | 0.047s | 20.844MiB| sat | 0 | | | |Chua-2-VC1-L-chunk-0086.smt2 | 0.047s | 18.804MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0086.smt2 | 0.047s | 20.692MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0425.smt2 | 0.047s | 20.788MiB| unsat | 0 | | | |ball_count_2d_plain.01.seq_lazy_global_15.smt2 | 0.047s | 19.748MiB| unsat | 0 | | | |asin-8-vars4-chunk-0046.smt2 | 0.047s | 20.776MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0076.smt2 | 0.047s | 20.648MiB| unsat | 0 | | | |atan-vega-3-chunk-0320.smt2 | 0.047s | 20.692MiB| sat | 0 | | | |ball_count_1d_plain.02.seq_lazy_lemmas_global_15.smt2 | 0.047s | 20.02MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0262.smt2 | 0.047s | 20.556MiB| sat | 0 | | | |ball_count_2d_hill.10.redlog_global_9.smt2 | 0.047s | 20.648MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0290.smt2 | 0.047s | 20.748MiB| sat | 0 | | | |atan-problem-1-weak-chunk-0020.smt2 | 0.047s | 20.636MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0464.smt2 | 0.047s | 20.828MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0025.smt2 | 0.047s | 20.724MiB| sat | 0 | | | |atan-problem-2-chunk-0037.smt2 | 0.048s | 20.732MiB| unsat | 0 | | | |atan-problem-2-chunk-0011.smt2 | 0.048s | 20.672MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0043.smt2 | 0.048s | 20.92MiB| unsat | 0 | | | |Chua-2-VC2-L-chunk-0040.smt2 | 0.048s | 20.768MiB| sat | 0 | | | |sin-cos-346-b-chunk-0018.smt2 | 0.048s | 20.62MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0241.smt2 | 0.048s | 20.852MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0189.smt2 | 0.048s | 20.752MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_linear_enc_global_5.smt2 | 0.048s | 19.404MiB| unsat | 0 | | | |atan-vega-3-chunk-0380.smt2 | 0.048s | 20.788MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0223.smt2 | 0.048s | 20.916MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0121.smt2 | 0.048s | 20.78MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_linear_enc_lemmas_global_7.smt2 | 0.048s | 21.58MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0046.smt2 | 0.048s | 20.764MiB| sat | 0 | | | |sqrt-problem-Melquiond2-chunk-0059.smt2 | 0.048s | 20.628MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0318.smt2 | 0.048s | 20.804MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0469.smt2 | 0.048s | 20.644MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0230.smt2 | 0.049s | 20.908MiB| sat | 0 | | | |Chua-2-IL-U-chunk-0094.smt2 | 0.049s | 20.864MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0166.smt2 | 0.049s | 20.872MiB| sat | 0 | | | |atan-vega-3-chunk-0089.smt2 | 0.049s | 20.68MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0082.smt2 | 0.049s | 20.728MiB| sat | 0 | | | |ball_count_1d_plain.03.seq_lazy_lemmas_global_5.smt2 | 0.049s | 21.292MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0390.smt2 | 0.049s | 20.764MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0519.smt2 | 0.049s | 20.62MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0320.smt2 | 0.049s | 20.804MiB| sat | 0 | | | |atan-vega-3-chunk-0370.smt2 | 0.049s | 20.916MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0147.smt2 | 0.049s | 20.708MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0567.smt2 | 0.049s | 21.06MiB| sat | 0 | | | |ball_count_1d_plain.04.seq_lazy_linear_enc_global_3.smt2 | 0.049s | 21.12MiB| unsat | 0 | | | |atan-problem-2-chunk-0024.smt2 | 0.049s | 21.08MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0111.smt2 | 0.049s | 21.02MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0344.smt2 | 0.049s | 20.836MiB| sat | 0 | | | |sin-cos-346-b-chunk-0414.smt2 | 0.050s | 20.764MiB| sat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0075.smt2 | 0.050s | 20.612MiB| sat | 0 | | | |ball_count_1d_plain.04.seq_lazy_global_1.smt2 | 0.050s | 19.048MiB| unsat | 0 | | | |atan-vega-3-chunk-0290.smt2 | 0.050s | 20.94MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0116.smt2 | 0.050s | 20.672MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0110.smt2 | 0.050s | 20.88MiB| sat | 0 | | | |exp-problem-10-2-chunk-0346.smt2 | 0.050s | 20.76MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0577.smt2 | 0.050s | 21.02MiB| sat | 0 | | | |atan-vega-3-chunk-0463.smt2 | 0.050s | 20.796MiB| sat | 0 | | | |ball_count_2d_slope.02.seq_lazy_lemmas_global_7.smt2 | 0.050s | 20.316MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0204.smt2 | 0.050s | 20.844MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0077.smt2 | 0.050s | 20.608MiB| sat | 0 | | | |CMOS-opamp-chunk-0096.smt2 | 0.050s | 20.804MiB| sat | 0 | | | |ball_count_1d_plain.05.redlog_global_5.smt2 | 0.051s | 21.232MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0191.smt2 | 0.051s | 20.772MiB| sat | 0 | | | |Chua-1-IL-L-chunk-0104.smt2 | 0.051s | 21.132MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0035.smt2 | 0.051s | 20.792MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0700.smt2 | 0.051s | 20.78MiB| unsat | 0 | | | |atan-problem-2-chunk-0047.smt2 | 0.051s | 20.68MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0158.smt2 | 0.051s | 20.756MiB| unsat | 0 | | | |ball_count_1d_plain.01.redlog_global_13.smt2 | 0.051s | 19.916MiB| unsat | 0 | | | |CONVOI2-chunk-0041.smt2 | 0.051s | 21.016MiB| unsat | 0 | | | |Chua-2-IL-L-chunk-0072.smt2 | 0.051s | 18.824MiB| unsat | 0 | | | |ball_count_1d_plain.02.qfree_global_13.smt2 | 0.051s | 19.74MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.qfree_global_1.smt2 | 0.051s | 18.98MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0380.smt2 | 0.051s | 20.832MiB| sat | 0 | | | |sin-cos-346-b-chunk-0597.smt2 | 0.051s | 20.92MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0093.smt2 | 0.051s | 20.956MiB| sat | 0 | | | |atan-problem-1-weak-chunk-0035.smt2 | 0.051s | 20.66MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0053.smt2 | 0.051s | 20.812MiB| sat | 0 | | | |ball_count_2d_plain.02.redlog_global_15.smt2 | 0.051s | 20.556MiB| unsat | 0 | | | |Chua-2-IL-L-chunk-0058.smt2 | 0.051s | 20.772MiB| sat | 0 | | | |Lyapunov1a-chunk-0042.smt2 | 0.051s | 20.9MiB| sat | 0 | | | |sin-problem-7-chunk-0143.smt2 | 0.051s | 20.644MiB| sat | 0 | | | |ball_count_2d_plain.10.seq_lazy_global_15.smt2 | 0.051s | 19.916MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0363.smt2 | 0.051s | 20.66MiB| sat | 0 | | | |sin-problem-7-weak-chunk-0149.smt2 | 0.051s | 20.712MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0334.smt2 | 0.052s | 21.02MiB| sat | 0 | | | |exp-problem-10-2-chunk-0224.smt2 | 0.052s | 20.76MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0227.smt2 | 0.052s | 20.732MiB| sat | 0 | | | |ball_count_2d_slope.02.seq_lazy_lemmas_global_11.smt2 | 0.052s | 20.792MiB| unsat | 0 | | | |atan-vega-3-chunk-0603.smt2 | 0.052s | 21.056MiB| sat | 0 | | | |ball_count_2d_plain.03.redlog_global_1.smt2 | 0.052s | 19.096MiB| unsat | 0 | | | |sqrt-problem-12vars3-chunk-0097.smt2 | 0.052s | 21.016MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0021.smt2 | 0.052s | 20.432MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0094.smt2 | 0.052s | 20.768MiB| sat | 0 | | | |ball_count_2d_plain.04.seq_lazy_lemmas_global_7.smt2 | 0.052s | 21.548MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.052s | 19.684MiB| unsat | 0 | | | |ball_count_2d_plain.03.seq_lazy_linear_enc_global_11.smt2 | 0.052s | 21.784MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0118.smt2 | 0.052s | 20.712MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.052s | 19.024MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_global_11.smt2 | 0.052s | 20.284MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_linear_enc_global_5.smt2 | 0.052s | 19.308MiB| unsat | 0 | | | |matrix-1-all-10.smt2 | 0.052s | 20.768MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0433.smt2 | 0.052s | 20.76MiB| sat | 0 | | | |Chua-1-VC1-L-chunk-0132.smt2 | 0.052s | 20.656MiB| unsat | 0 | | | |ball_count_2d_hill.10.seq_lazy_global_3.smt2 | 0.052s | 19.168MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_linear_enc_global_5.smt2 | 0.052s | 21.028MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0085.smt2 | 0.053s | 20.936MiB| sat | 0 | | | |MulliganEconomicsModel0006a.smt2 | 0.053s | 20.66MiB| sat | 0 | | | |sin-problem-7-weak-chunk-0138.smt2 | 0.053s | 20.508MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0421.smt2 | 0.053s | 20.668MiB| sat | 0 | | | |sin-problem-8-weak-chunk-0068.smt2 | 0.053s | 21.06MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0121.smt2 | 0.053s | 20.64MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0275.smt2 | 0.053s | 20.824MiB| unsat | 0 | | | |atan-vega-3-chunk-0360.smt2 | 0.053s | 20.736MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0040.smt2 | 0.053s | 20.98MiB| unsat | 0 | | | |atan-vega-3-chunk-0300.smt2 | 0.053s | 20.976MiB| sat | 0 | | | |atan-vega-3-chunk-0473.smt2 | 0.053s | 20.924MiB| sat | 0 | | | |atan-vega-3-chunk-0270.smt2 | 0.053s | 20.508MiB| sat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_linear_enc_global_11.smt2 | 0.053s | 21.552MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0401.smt2 | 0.053s | 20.744MiB| sat | 0 | | | |sin-cos-346-b-chunk-0484.smt2 | 0.053s | 20.96MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0161.smt2 | 0.054s | 20.884MiB| sat | 0 | | | |ball_count_1d_plain.01.seq_lazy_linear_enc_global_15.smt2 | 0.054s | 19.692MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_global_7.smt2 | 0.054s | 19.18MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0136.smt2 | 0.054s | 20.98MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0671.smt2 | 0.054s | 20.932MiB| sat | 0 | | | |ball_count_2d_slope.04.seq_lazy_linear_enc_lemmas_global_7.smt2 | 0.054s | 19.888MiB| unsat | 0 | | | |ball_count_2d_hill.02.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.054s | 19.556MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0074.smt2 | 0.054s | 20.912MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0556.smt2 | 0.054s | 20.7MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0217.smt2 | 0.054s | 20.668MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0098.smt2 | 0.054s | 20.576MiB| sat | 0 | | | |atan-vega-3-chunk-0240.smt2 | 0.054s | 20.792MiB| sat | 0 | | | |ball_count_2d_hill.04.seq_lazy_global_3.smt2 | 0.054s | 21.212MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0391.smt2 | 0.054s | 21.052MiB| sat | 0 | | | |cos-3410-b-chunk-0027.smt2 | 0.054s | 20.796MiB| sat | 0 | | | |Chua-1-IL-L-chunk-0016.smt2 | 0.054s | 20.988MiB| sat | 0 | | | |asin-8-chunk-0039.smt2 | 0.054s | 20.736MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0070.smt2 | 0.054s | 20.644MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0008.smt2 | 0.054s | 20.756MiB| unsat | 0 | | | |ball_count_2d_slope.04.seq_lazy_global_1.smt2 | 0.055s | 18.964MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0124.smt2 | 0.055s | 20.896MiB| sat | 0 | | | |sin-cos-346-b-chunk-0620.smt2 | 0.055s | 20.768MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0026.smt2 | 0.055s | 20.728MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.redlog_global_5.smt2 | 0.055s | 21.148MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0328.smt2 | 0.055s | 20.992MiB| sat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_linear_enc_lemmas_global_11.smt2 | 0.055s | 21.788MiB| unsat | 0 | | | |ball_count_2d_hill.01.seq_lazy_lemmas_global_11.smt2 | 0.055s | 20.272MiB| unsat | 0 | | | |asin-8-chunk-0024.smt2 | 0.055s | 20.808MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0109.smt2 | 0.055s | 20.624MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_linear_enc_global_3.smt2 | 0.055s | 21.188MiB| unsat | 0 | | | |CMOS-opamp-chunk-0286.smt2 | 0.055s | 20.728MiB| sat | 0 | | | |atan-problem-2-sqrt-weak-chunk-0032.smt2 | 0.055s | 20.764MiB| unsat | 0 | | | |sin-problem-7-chunk-0273.smt2 | 0.055s | 20.856MiB| sat | 0 | | | |ball_count_1d_plain.10.redlog_global_9.smt2 | 0.055s | 19.48MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0132.smt2 | 0.055s | 20.964MiB| sat | 0 | | | |ball_count_2d_hill.01.redlog_global_9.smt2 | 0.055s | 20.616MiB| unsat | 0 | | | |sin-problem-7-chunk-0283.smt2 | 0.055s | 21.116MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0701.smt2 | 0.055s | 18.94MiB| unsat | 0 | | | |CMOS-opamp-chunk-0074.smt2 | 0.055s | 20.8MiB| sat | 0 | | | |atan-vega-3-chunk-0563.smt2 | 0.055s | 20.856MiB| sat | 0 | | | |exp-361-neg-6-e-chunk-0216.smt2 | 0.055s | 20.848MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0093.smt2 | 0.056s | 20.764MiB| sat | 0 | | | |CMOS-opamp-chunk-0122.smt2 | 0.056s | 20.784MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0087.smt2 | 0.056s | 20.68MiB| sat | 0 | | | |ball_count_2d_plain.01.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.056s | 19.184MiB| unsat | 0 | | | |ball_count_2d_plain.03.seq_lazy_lemmas_global_3.smt2 | 0.056s | 20.96MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0073.smt2 | 0.056s | 18.792MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0245.smt2 | 0.056s | 20.848MiB| unsat | 0 | | | |ball_count_2d_plain.10.seq_lazy_linear_enc_global_9.smt2 | 0.056s | 19.404MiB| unsat | 0 | | | |Chua-2-VC2-U-chunk-0018.smt2 | 0.056s | 20.772MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0019.smt2 | 0.056s | 20.768MiB| unsat | 0 | | | |sin-problem-10-2-chunk-0010.smt2 | 0.056s | 20.56MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0370.smt2 | 0.056s | 20.944MiB| unsat | 0 | | | |mbo_E21E27.smt2 | 0.056s | 20.764MiB| unsat | 0 | | | |atan-vega-3-chunk-0513.smt2 | 0.057s | 20.88MiB| sat | 0 | | | |sin-cos-346-b-chunk-0444.smt2 | 0.057s | 20.832MiB| sat | 0 | | | |atan-problem-2-weakT-chunk-0054.smt2 | 0.057s | 20.82MiB| sat | 0 | | | |Chua-2-IL-L-chunk-0005.smt2 | 0.057s | 20.848MiB| sat | 0 | | | |sin-cos-346-b-chunk-0560.smt2 | 0.057s | 20.92MiB| sat | 0 | | | |CMOS-opamp-chunk-0200.smt2 | 0.057s | 20.812MiB| sat | 0 | | | |exp-problem-10-3-weak-chunk-0141.smt2 | 0.057s | 21.028MiB| sat | 0 | | | |sin-cos-346-b-chunk-0232.smt2 | 0.057s | 20.756MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0651.smt2 | 0.057s | 20.98MiB| unsat | 0 | | | |ball_count_1d_plain.03.redlog_global_7.smt2 | 0.057s | 21.388MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.qfree_global_3.smt2 | 0.057s | 19.02MiB| unsat | 0 | | | |ball_count_1d_plain.10.redlog_global_13.smt2 | 0.057s | 19.872MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0085.smt2 | 0.057s | 20.816MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0113.smt2 | 0.057s | 20.784MiB| sat | 0 | | | |ball_count_1d_plain.10.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.057s | 18.972MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0010.smt2 | 0.058s | 20.644MiB| sat | 0 | | | |ball_count_2d_plain.01.redlog_global_7.smt2 | 0.058s | 19.56MiB| unsat | 0 | | | |atan-problem-2-chunk-0092.smt2 | 0.058s | 20.748MiB| unsat | 0 | | | |ball_count_2d_hill.10.seq_lazy_lemmas_global_11.smt2 | 0.058s | 20.316MiB| unsat | 0 | | | |atan-vega-3-chunk-0109.smt2 | 0.058s | 20.768MiB| sat | 0 | | | |atan-problem-2-sqrt-chunk-0039.smt2 | 0.058s | 20.692MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0053.smt2 | 0.058s | 20.652MiB| sat | 0 | | | |Chua-1-VC1-U-chunk-0072.smt2 | 0.058s | 20.66MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_global_11.smt2 | 0.059s | 21.648MiB| unsat | 0 | | | |atan-vega-3-chunk-0633.smt2 | 0.059s | 20.792MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0714.smt2 | 0.059s | 20.744MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0035.smt2 | 0.059s | 20.732MiB| sat | 0 | | | |ball_count_2d_plain.10.seq_lazy_linear_enc_global_13.smt2 | 0.059s | 19.74MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.qfree_global_11.smt2 | 0.059s | 21.76MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0054.smt2 | 0.059s | 20.652MiB| sat | 0 | | | |sin-344-3-chunk-0046.smt2 | 0.060s | 20.852MiB| sat | 0 | | | |sin-cos-346-b-chunk-0186.smt2 | 0.060s | 20.76MiB| sat | 0 | | | |sin-problem-7-chunk-0172.smt2 | 0.060s | 20.864MiB| unsat | 0 | | | |CMOS-opamp-chunk-0332.smt2 | 0.060s | 20.876MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0042.smt2 | 0.060s | 18.936MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0218.smt2 | 0.060s | 20.78MiB| unsat | 0 | | | |ball_count_2d_plain.03.seq_lazy_global_13.smt2 | 0.060s | 21.888MiB| unsat | 0 | | | |Chua-2-VC1-L-chunk-0119.smt2 | 0.060s | 20.764MiB| sat | 0 | | | |ball_count_2d_hill.04.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.060s | 21.436MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0359.smt2 | 0.060s | 20.856MiB| unsat | 0 | | | |exp-problem-10-3-chunk-0138.smt2 | 0.060s | 20.856MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0061.smt2 | 0.060s | 20.704MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0277.smt2 | 0.060s | 20.844MiB| unsat | 0 | | | |ball_count_2d_hill.02.redlog_global_9.smt2 | 0.060s | 20.636MiB| unsat | 0 | | | |polypaver-sqrt43-int-chunk-0053.smt2 | 0.061s | 20.668MiB| unsat | 0 | | | |cos-3410-b-chunk-0015.smt2 | 0.061s | 20.764MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0606.smt2 | 0.061s | 21.072MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0173.smt2 | 0.061s | 20.84MiB| unsat | 0 | | | |ball_count_2d_plain.10.seq_lazy_lemmas_global_5.smt2 | 0.061s | 19.232MiB| unsat | 0 | | | |ball_count_2d_plain.05.redlog_global_3.smt2 | 0.061s | 20.956MiB| unsat | 0 | | | |CMOS-opamp-chunk-0246.smt2 | 0.061s | 21.02MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0155.smt2 | 0.061s | 20.984MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0379.smt2 | 0.061s | 21.028MiB| sat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.061s | 19.78MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0566.smt2 | 0.061s | 20.992MiB| sat | 0 | | | |sin-problem-7-chunk-0079.smt2 | 0.062s | 20.86MiB| sat | 0 | | | |sin-cos-346-b-chunk-0549.smt2 | 0.062s | 20.78MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0039.smt2 | 0.062s | 20.856MiB| unsat | 0 | | | |ball_count_2d_plain.01.seq_lazy_linear_enc_global_9.smt2 | 0.062s | 19.46MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.062s | 19.836MiB| unsat | 0 | | | |ball_count_2d_plain.01.qfree_global_3.smt2 | 0.062s | 18.976MiB| unsat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0121.smt2 | 0.062s | 20.716MiB| sat | 0 | | | |ball_count_1d_plain.04.qfree_global_7.smt2 | 0.063s | 21.276MiB| unsat | 0 | | | |ball_count_1d_plain.04.seq_lazy_linear_enc_lemmas_global_7.smt2 | 0.063s | 21.2MiB| unsat | 0 | | | |MulliganEconomicsModel0085a.smt2 | 0.063s | 20.712MiB| sat | 0 | | | |sin-problem-7-chunk-0117.smt2 | 0.063s | 20.772MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0107.smt2 | 0.063s | 20.744MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0134.smt2 | 0.063s | 20.688MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_lemmas_global_7.smt2 | 0.063s | 21.536MiB| unsat | 0 | | | |sqrt-problem-Melquiond2-chunk-0023.smt2 | 0.064s | 20.796MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0436.smt2 | 0.064s | 20.788MiB| sat | 0 | | | |exp-problem-10-2-chunk-0325.smt2 | 0.064s | 21.088MiB| unsat | 0 | | | |sin-problem-7-chunk-0247.smt2 | 0.064s | 21.188MiB| sat | 0 | | | |sqrt-problem-Melquiond2-chunk-0071.smt2 | 0.064s | 20.932MiB| sat | 0 | | | |exp-problem-10-2-chunk-0038.smt2 | 0.064s | 20.752MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0064.smt2 | 0.064s | 20.68MiB| unsat | 0 | | | |atan-problem-1-chunk-0102.smt2 | 0.064s | 20.936MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0633.smt2 | 0.064s | 20.892MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0349.smt2 | 0.065s | 20.916MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0170.smt2 | 0.065s | 20.604MiB| unsat | 0 | | | |sin-344-4-chunk-0032.smt2 | 0.065s | 20.908MiB| sat | 0 | | | |ball_count_2d_slope.05.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.065s | 19.348MiB| unsat | 0 | | | |ball_count_2d_hill.02.seq_lazy_linear_enc_global_15.smt2 | 0.065s | 20.196MiB| unsat | 0 | | | |sin-problem-10-2-chunk-0034.smt2 | 0.065s | 18.912MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0206.smt2 | 0.065s | 21.072MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0041.smt2 | 0.065s | 20.676MiB| unsat | 0 | | | |ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.065s | 19.548MiB| unsat | 0 | | | |ball_count_2d_plain.04.seq_lazy_linear_enc_global_15.smt2 | 0.065s | 21.996MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0216.smt2 | 0.065s | 20.812MiB| sat | 0 | | | |ball_count_2d_slope.01.seq_lazy_lemmas_global_15.smt2 | 0.065s | 21.508MiB| unsat | 0 | | | |ball_count_2d_slope.10.seq_lazy_linear_enc_global_5.smt2 | 0.065s | 19.488MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0162.smt2 | 0.065s | 20.824MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0305.smt2 | 0.065s | 20.772MiB| sat | 0 | | | |ball_count_2d_plain.01.seq_lazy_lemmas_global_5.smt2 | 0.065s | 19.224MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0267.smt2 | 0.066s | 20.812MiB| sat | 0 | | | |ball_count_2d_plain.10.redlog_global_7.smt2 | 0.066s | 19.708MiB| unsat | 0 | | | |atan-problem-1-chunk-0035.smt2 | 0.066s | 20.756MiB| sat | 0 | | | |ball_count_2d_hill.10.redlog_global_13.smt2 | 0.066s | 21.172MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0214.smt2 | 0.066s | 20.744MiB| sat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_lemmas_global_15.smt2 | 0.066s | 20.284MiB| unsat | 0 | | | |matrix-1-all-29.smt2 | 0.067s | 20.812MiB| sat | 0 | | | |ball_count_2d_hill_simple.05.qfree_global_5.smt2 | 0.067s | 21.164MiB| unsat | 0 | | | |polypaver-bench-exp-3d-chunk-0109.smt2 | 0.067s | 20.988MiB| unsat | 0 | | | |InVarSynth_PostfixIncrementDecrement.c_Iteration3_0.smt2 | 0.068s | 20.884MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0069.smt2 | 0.068s | 20.78MiB| sat | 0 | | | |atan-vega-3-chunk-0149.smt2 | 0.068s | 20.628MiB| unsat | 0 | | | |ball_count_1d_plain.10.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.068s | 19.208MiB| unsat | 0 | | | |ball_count_2d_slope.02.seq_lazy_linear_enc_global_15.smt2 | 0.068s | 20.736MiB| unsat | 0 | | | |ball_count_1d_plain.01.redlog_global_9.smt2 | 0.068s | 19.444MiB| unsat | 0 | | | |ball_count_2d_hill.05.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.068s | 21.788MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0480.smt2 | 0.068s | 20.816MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_global_7.smt2 | 0.069s | 19.404MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_global_11.smt2 | 0.069s | 19.5MiB| unsat | 0 | | | |sqrt-circles-2-chunk-0015.smt2 | 0.069s | 20.748MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.seq_lazy_lemmas_global_15.smt2 | 0.069s | 20.312MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0243.smt2 | 0.069s | 20.972MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0335.smt2 | 0.070s | 20.988MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0358.smt2 | 0.070s | 20.716MiB| sat | 0 | | | |ball_count_2d_plain.05.seq_lazy_global_7.smt2 | 0.070s | 21.368MiB| unsat | 0 | | | |ball_count_2d_slope.01.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.070s | 20.572MiB| unsat | 0 | | | |ball_count_2d_plain.05.qfree_global_9.smt2 | 0.070s | 21.452MiB| unsat | 0 | | | |sin-problem-7-chunk-0182.smt2 | 0.070s | 20.936MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0530.smt2 | 0.070s | 20.764MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0193.smt2 | 0.070s | 20.916MiB| unsat | 0 | | | |ball_count_2d_hill.05.seq_lazy_global_3.smt2 | 0.070s | 21.156MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0515.smt2 | 0.070s | 20.704MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0035.smt2 | 0.071s | 20.856MiB| sat | 0 | | | |sin-cos-346-b-chunk-0584.smt2 | 0.071s | 20.76MiB| sat | 0 | | | |CMOS-opamp-chunk-0158.smt2 | 0.071s | 20.808MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0296.smt2 | 0.071s | 18.856MiB| unsat | 0 | | | |ball_count_1d_plain.02.seq_lazy_linear_enc_global_1.smt2 | 0.072s | 19.044MiB| unsat | 0 | | | |sqrt-problem-12vars3-chunk-0055.smt2 | 0.072s | 20.864MiB| sat | 0 | | | |exp-problem-10-2-chunk-0255.smt2 | 0.073s | 20.768MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0643.smt2 | 0.073s | 20.936MiB| unsat | 0 | | | |ball_count_2d_slope.04.seq_lazy_linear_enc_lemmas_global_11.smt2 | 0.073s | 20.424MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0375.smt2 | 0.073s | 20.768MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0078.smt2 | 0.073s | 20.712MiB| sat | 0 | | | |sin-problem-7-chunk-0348.smt2 | 0.073s | 20.804MiB| sat | 0 | | | |sin-cos-346-b-chunk-0631.smt2 | 0.073s | 20.928MiB| sat | 0 | | | |sin-problem-7-weak-chunk-0160.smt2 | 0.074s | 20.664MiB| sat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_global_9.smt2 | 0.074s | 21.536MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.qfree_global_15.smt2 | 0.074s | 21.868MiB| unsat | 0 | | | |atan-vega-3-chunk-0390.smt2 | 0.074s | 20.648MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0191.smt2 | 0.074s | 20.836MiB| sat | 0 | | | |exp-problem-10-3-chunk-0073.smt2 | 0.074s | 20.768MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0342.smt2 | 0.074s | 20.972MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_lemmas_global_9.smt2 | 0.074s | 21.716MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0681.smt2 | 0.075s | 20.76MiB| unsat | 0 | | | |sqrt-1mcosq-7-chunk-0027.smt2 | 0.075s | 20.672MiB| sat | 0 | | | |ball_count_2d_plain.01.seq_lazy_lemmas_global_1.smt2 | 0.075s | 18.888MiB| unsat | 0 | | | |sin-344-3-weak-chunk-0044.smt2 | 0.076s | 20.748MiB| sat | 0 | | | |exp-problem-10-3-chunk-0188.smt2 | 0.076s | 21.024MiB| unsat | 0 | | | |MulliganEconomicsModel0054a.smt2 | 0.077s | 20.868MiB| sat | 0 | | | |sin-problem-7-weak-chunk-0171.smt2 | 0.077s | 21.5MiB| sat | 0 | | | |ball_count_2d_plain.03.redlog_global_5.smt2 | 0.077s | 21.328MiB| unsat | 0 | | | |ball_count_2d_hill_simple.02.seq_lazy_global_15.smt2 | 0.077s | 19.744MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.077s | 19.672MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0412.smt2 | 0.077s | 21.088MiB| unsat | 0 | | | |ball_count_2d_hill_simple.10.qfree_global_13.smt2 | 0.077s | 19.74MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_linear_enc_lemmas_global_9.smt2 | 0.077s | 22.044MiB| unsat | 0 | | | |atan-vega-3-chunk-0077.smt2 | 0.077s | 20.924MiB| unsat | 0 | | | |atan-vega-3-chunk-0573.smt2 | 0.077s | 20.864MiB| unsat | 0 | | | |Chua-2-VC1-U-chunk-0117.smt2 | 0.078s | 20.768MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0668.smt2 | 0.078s | 21.076MiB| unsat | 0 | | | |ball_count_1d_plain.04.qfree_global_11.smt2 | 0.078s | 21.772MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0199.smt2 | 0.078s | 20.888MiB| sat | 0 | | | |simple_ballistics_reach.01.seq_lazy_linear_enc_global_1.smt2 | 0.078s | 21.056MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_lemmas_global_3.smt2 | 0.078s | 20.888MiB| unsat | 0 | | | |atan-vega-3-chunk-0119.smt2 | 0.078s | 20.732MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0276.smt2 | 0.079s | 21.136MiB| sat | 0 | | | |exp-problem-10-3-chunk-0178.smt2 | 0.079s | 20.768MiB| sat | 0 | | | |ball_count_2d_hill_simple.05.redlog_global_9.smt2 | 0.079s | 21.536MiB| unsat | 0 | | | |atan-vega-3-chunk-0593.smt2 | 0.080s | 20.772MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0231.smt2 | 0.080s | 18.804MiB| unsat | 0 | | | |MulliganEconomicsModel0067a.smt2 | 0.080s | 21.044MiB| sat | 0 | | | |RL-high-pass-circuit-gain-chunk-0010.smt2 | 0.080s | 20.596MiB| sat | 0 | | | |sin-problem-7-weak2-chunk-0123.smt2 | 0.080s | 20.796MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0013.smt2 | 0.081s | 20.608MiB| sat | 0 | | | |Chua-2-VC2-U-chunk-0051.smt2 | 0.081s | 20.724MiB| sat | 0 | | | |bottom-plate-mixer-chunk-0050.smt2 | 0.081s | 20.84MiB| sat | 0 | | | |InVarSynth_doubleLoopUniformIterations.bpl_Iteration2_0.smt2 | 0.081s | 21.072MiB| unsat | 0 | | | |ball_count_2d_plain.02.seq_lazy_global_1.smt2 | 0.081s | 18.888MiB| unsat | 0 | | | |ball_count_2d_slope.03.seq_lazy_linear_enc_lemmas_global_15.smt2 | 0.081s | 21.176MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0323.smt2 | 0.081s | 20.808MiB| sat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0075.smt2 | 0.081s | 20.72MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0589.smt2 | 0.082s | 20.968MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0457.smt2 | 0.082s | 20.748MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0098.smt2 | 0.082s | 20.84MiB| unsat | 0 | | | |ball_count_2d_hill.02.redlog_global_13.smt2 | 0.082s | 21.216MiB| unsat | 0 | | | |matrix-5-all-23.smt2 | 0.082s | 21.392MiB| unsat | 0 | | | |atan-vega-3-chunk-0260.smt2 | 0.083s | 20.768MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0286.smt2 | 0.083s | 21.02MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0500.smt2 | 0.083s | 20.76MiB| unsat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0098.smt2 | 0.084s | 20.752MiB| sat | 0 | | | |etcs_braking_2.01.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.084s | 21.52MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0142.smt2 | 0.084s | 20.82MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0120.smt2 | 0.084s | 20.768MiB| sat | 0 | | | |ball_count_2d_plain.04.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.084s | 21.276MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0679.smt2 | 0.085s | 21.02MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.085s | 21.992MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_lemmas_global_7.smt2 | 0.085s | 22.008MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0402.smt2 | 0.085s | 21.108MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0205.smt2 | 0.085s | 20.952MiB| unsat | 0 | | | |atan-vega-3-chunk-0493.smt2 | 0.085s | 20.708MiB| sat | 0 | | | |ball_count_2d_plain.03.qfree_global_15.smt2 | 0.085s | 22.388MiB| unsat | 0 | | | |ball_count_2d_slope.10.seq_lazy_lemmas_global_15.smt2 | 0.086s | 21.672MiB| unsat | 0 | | | |Chua-1-IL-L-chunk-0030.smt2 | 0.086s | 20.744MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0204.smt2 | 0.086s | 20.692MiB| sat | 0 | | | |sin-cos-346-b-chunk-0514.smt2 | 0.086s | 20.792MiB| sat | 0 | | | |sin-cos-346-b-chunk-0114.smt2 | 0.086s | 20.792MiB| unsat | 0 | | | |sin-problem-7-chunk-0335.smt2 | 0.087s | 20.964MiB| sat | 0 | | | |Lyapunov1a-chunk-0032.smt2 | 0.087s | 20.792MiB| sat | 0 | | | |atan-problem-1-chunk-0047.smt2 | 0.087s | 20.716MiB| sat | 0 | | | |Chua-1-IL-L-chunk-0054.smt2 | 0.087s | 18.76MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0254.smt2 | 0.087s | 21.116MiB| unsat | 0 | | | |Chua-1-VC1-L-chunk-0019.smt2 | 0.087s | 20.76MiB| sat | 0 | | | |polypaver-bench-exp-3d-chunk-0138.smt2 | 0.087s | 20.776MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.redlog_global_15.smt2 | 0.087s | 21.964MiB| unsat | 0 | | | |polypaver-sqrt43-int-3vars-chunk-0043.smt2 | 0.087s | 20.72MiB| unsat | 0 | | | |ball_count_2d_plain.02.seq_lazy_lemmas_global_9.smt2 | 0.088s | 19.7MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0070.smt2 | 0.088s | 20.688MiB| sat | 0 | | | |Chua-2-VC2-U-chunk-0097.smt2 | 0.088s | 20.996MiB| sat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_lemmas_global_13.smt2 | 0.088s | 22.24MiB| unsat | 0 | | | |ball_count_2d_hill.01.redlog_global_13.smt2 | 0.088s | 21.08MiB| unsat | 0 | | | |exp-problem-10-3-weak-chunk-0015.smt2 | 0.088s | 20.768MiB| sat | 0 | | | |Chua-2-VC1-U-chunk-0058.smt2 | 0.089s | 20.824MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0467.smt2 | 0.090s | 20.692MiB| unsat | 0 | | | |ball_count_2d_plain.10.redlog_global_11.smt2 | 0.090s | 19.888MiB| unsat | 0 | | | |ball_count_2d_hill.05.seq_lazy_lemmas_global_7.smt2 | 0.090s | 21.808MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0082.smt2 | 0.090s | 18.82MiB| unsat | 0 | | | |ball_count_1d_plain.05.seq_lazy_linear_enc_global_7.smt2 | 0.090s | 21.224MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_global_13.smt2 | 0.091s | 21.888MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0368.smt2 | 0.091s | 20.764MiB| sat | 0 | | | |ball_count_2d_plain.10.seq_lazy_linear_enc_lemmas_global_3.smt2 | 0.091s | 19.232MiB| unsat | 0 | | | |etcs_braking_2.01.qfree_global_3.smt2 | 0.091s | 21.472MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0021.smt2 | 0.091s | 20.848MiB| sat | 0 | | | |atan-vega-3-weak-chunk-0469.smt2 | 0.091s | 20.872MiB| sat | 0 | | | |ball_count_2d_slope.03.seq_lazy_lemmas_global_3.smt2 | 0.092s | 21.544MiB| unsat | 0 | | | |atan-vega-3-chunk-0189.smt2 | 0.092s | 20.652MiB| sat | 0 | | | |exp-problem-10-3-chunk-0052.smt2 | 0.092s | 20.632MiB| sat | 0 | | | |atan-problem-2-weak2-chunk-0022.smt2 | 0.092s | 20.66MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0054.smt2 | 0.092s | 20.8MiB| sat | 0 | | | |ball_count_2d_plain.02.qfree_global_11.smt2 | 0.092s | 19.732MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0183.smt2 | 0.093s | 20.772MiB| sat | 0 | | | |cbrt-problem-3-weak-chunk-0023.smt2 | 0.094s | 20.672MiB| sat | 0 | | | |exp-problem-10-2-chunk-0124.smt2 | 0.094s | 20.768MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0113.smt2 | 0.094s | 20.748MiB| sat | 0 | | | |ball_count_2d_hill_simple.05.redlog_global_13.smt2 | 0.094s | 21.996MiB| unsat | 0 | | | |ball_count_2d_hill_simple.04.seq_lazy_linear_enc_lemmas_global_15.smt2 | 0.095s | 22.428MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.096s | 21.096MiB| unsat | 0 | | | |atan-vega-3-weak-chunk-0136.smt2 | 0.096s | 20.832MiB| sat | 0 | | | |ball_count_1d_plain.01.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.096s | 18.976MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0209.smt2 | 0.096s | 20.916MiB| sat | 0 | | | |Chua-1-VC2-U-chunk-0135.smt2 | 0.096s | 20.952MiB| unsat | 0 | | | |ball_count_2d_hill_simple.03.seq_lazy_global_5.smt2 | 0.097s | 20.928MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_linear_enc_lemmas_global_1.smt2 | 0.097s | 18.972MiB| unsat | 0 | | | |sin-problem-8-chunk-0067.smt2 | 0.097s | 20.84MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0177.smt2 | 0.097s | 21.032MiB| sat | 0 | | | |Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0156.smt2 | 0.098s | 21.16MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0610.smt2 | 0.098s | 21.008MiB| sat | 0 | | | |ball_count_1d_plain.01.seq_lazy_global_3.smt2 | 0.098s | 19.16MiB| unsat | 0 | | | |ball_count_1d_plain.05.seq_lazy_global_9.smt2 | 0.098s | 21.344MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0288.smt2 | 0.099s | 20.708MiB| unsat | 0 | | | |ball_count_2d_hill_simple.01.qfree_global_13.smt2 | 0.099s | 19.588MiB| unsat | 0 | | | |asin-8-chunk-0053.smt2 | 0.099s | 20.764MiB| sat | 0 | | | |cbrt-problem-3-chunk-0028.smt2 | 0.100s | 20.872MiB| unsat | 0 | | | |sin-cos-346-b-chunk-0054.smt2 | 0.100s | 18.928MiB| unsat | 0 | | | |matrix-1-all-2.smt2 | 0.100s | 20.832MiB| sat | 0 | | | |sqrt-1mcosq-7-chunk-0155.smt2 | 0.100s | 20.944MiB| sat | 0 | | | |atan-problem-2-chunk-0107.smt2 | 0.101s | 20.776MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0621.smt2 | 0.101s | 21.02MiB| sat | 0 | | | |atan-problem-2-chunk-0070.smt2 | 0.101s | 20.772MiB| unsat | 0 | | | |sin-problem-7-chunk-0322.smt2 | 0.102s | 20.888MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0234.smt2 | 0.102s | 20.768MiB| sat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0352.smt2 | 0.103s | 20.788MiB| sat | 0 | | | |ball_count_2d_plain.03.seq_lazy_linear_enc_lemmas_global_15.smt2 | 0.103s | 22.324MiB| unsat | 0 | | | |Chua-1-IL-U-chunk-0076.smt2 | 0.103s | 20.9MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0048.smt2 | 0.104s | 20.652MiB| sat | 0 | | | |atan-vega-3-chunk-0443.smt2 | 0.104s | 20.884MiB| sat | 0 | | | |ball_count_1d_plain.03.seq_lazy_linear_enc_global_13.smt2 | 0.104s | 21.816MiB| unsat | 0 | | | |ball_count_2d_hill.01.seq_lazy_lemmas_global_7.smt2 | 0.105s | 19.82MiB| unsat | 0 | | | |ball_count_2d_plain.03.seq_lazy_linear_enc_global_7.smt2 | 0.105s | 21.224MiB| unsat | 0 | | | |ball_count_2d_plain.05.qfree_global_13.smt2 | 0.105s | 21.82MiB| unsat | 0 | | | |ball_count_2d_hill.01.seq_lazy_linear_enc_global_15.smt2 | 0.105s | 20.168MiB| unsat | 0 | | | |sin-problem-10-3-chunk-0023.smt2 | 0.105s | 20.768MiB| unsat | 0 | | | |ball_count_2d_plain.04.seq_lazy_lemmas_global_11.smt2 | 0.105s | 22.296MiB| unsat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_lemmas_global_11.smt2 | 0.105s | 22.02MiB| unsat | 0 | | | |ball_count_2d_slope.10.seq_lazy_linear_enc_lemmas_global_13.smt2 | 0.105s | 20.5MiB| unsat | 0 | | | |Chua-1-VC2-U-chunk-0149.smt2 | 0.106s | 20.996MiB| unsat | 0 | | | |atan-problem-2-weak2-chunk-0103.smt2 | 0.106s | 20.904MiB| sat | 0 | | | |ball_count_1d_plain.04.seq_lazy_lemmas_global_9.smt2 | 0.106s | 21.54MiB| unsat | 0 | | | |sin-problem-8-weak-chunk-0027.smt2 | 0.106s | 20.728MiB| sat | 0 | | | |ball_count_1d_plain.05.seq_lazy_linear_enc_global_11.smt2 | 0.107s | 21.64MiB| unsat | 0 | | | |ball_count_1d_plain.10.qfree_global_1.smt2 | 0.107s | 19.032MiB| unsat | 0 | | | |MulliganEconomicsModel0077c.smt2 | 0.108s | 20.768MiB| unsat | 0 | | | |MulliganEconomicsModel0027c.smt2 | 0.108s | 20.728MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_linear_enc_lemmas_global_5.smt2 | 0.109s | 21.524MiB| unsat | 0 | | | |Chua-1-VC1-U-chunk-0083.smt2 | 0.109s | 20.768MiB| unsat | 0 | | | |mgc_06.smt2 | 0.110s | 20.76MiB| unsat | 0 | | | |ball_count_2d_plain.05.seq_lazy_lemmas_global_15.smt2 | 0.110s | 22.552MiB| unsat | 0 | | | |ball_count_1d_plain.03.seq_lazy_linear_enc_global_9.smt2 | 0.110s | 21.34MiB| unsat | 0 | | | |atan-problem-2-weak-chunk-0064.smt2 | 0.111s | 20.992MiB| sat | 0 | | | |ball_count_2d_hill_simple.05.seq_lazy_linear_enc_global_15.smt2 | 0.111s | 22.052MiB| unsat | 0 | | | |ball_count_2d_hill.10.seq_lazy_linear_enc_global_15.smt2 | 0.112s | 20.208MiB| unsat | 0 | | | |ball_count_2d_hill.04.seq_lazy_lemmas_global_7.smt2 | 0.113s | 21.896MiB| unsat | 0 | | | |polypaver-bench-sqrt-3d-chunk-0446.smt2 | 0.114s | 20.712MiB| sat | 0 | | | |sqrt-problem-12vars3-chunk-0039.smt2 | 0.115s | 20.692MiB| unsat | 0 | | | |ball_count_1d_plain.04.seq_lazy_global_5.smt2 | 0.116s | 21.072MiB| unsat | 0 | | | |InVarSynth_LabelEncodingWithUnrolling.bpl_Iteration2_0.smt2 | 0.116s | 21.024MiB| sat | 0 | | | |ball_count_2d_slope.04.seq_lazy_linear_enc_global_3.smt2 | 0.116s | 21.092MiB| unsat | 0 | | | |ball_count_1d_plain.03.redlog_global_11.smt2 | 0.117s | 21.7MiB| unsat | 0 | | | |mbo_E5E23.smt2 | 0.117s | 22.092MiB| unsat | 0 | | | |ball_count_2d_plain.03.seq_lazy_global_9.smt2 | 0.117s | 21.544MiB| unsat | 0 | | | |ball_count_1d_plain.04.seq_lazy_linear_enc_lemmas_global_11.smt2 | 0.120s | 21.748MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0446.smt2 | 0.127s | 21.272MiB| sat | 0 | | | |InVarSynth_ShortCircuit-SideEffect-SwitchStatement-Safe.c_Iteration1_0.smt2 | 0.128s | 21.64MiB| sat | 0 | | | |ball_count_2d_slope.04.seq_lazy_global_5.smt2 | 0.129s | 21.788MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0426.smt2 | 0.129s | 20.88MiB| sat | 0 | | | |ball_count_2d_plain.04.redlog_global_9.smt2 | 0.133s | 21.988MiB| unsat | 0 | | | |ball_count_1d_plain.05.seq_lazy_global_13.smt2 | 0.133s | 21.788MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0690.smt2 | 0.141s | 21.1MiB| sat | 0 | | | |ball_count_2d_plain.04.redlog_global_13.smt2 | 0.145s | 22.588MiB| unsat | 0 | | | |CMOS-opamp-chunk-0320.smt2 | 0.149s | 21.236MiB| unsat | 0 | | | |ball_count_1d_plain.04.seq_lazy_lemmas_global_13.smt2 | 0.157s | 22.016MiB| unsat | 0 | | | |ball_count_1d_plain.05.qfree_global_15.smt2 | 0.161s | 21.804MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0457.smt2 | 0.178s | 21.36MiB| unsat | 0 | | | |toeplz.c.i.toeplz.pl.t2.fixed.t2.c_Iteration10_Loop_3-pieceTemplate.smt2 | 0.183s | 22.864MiB| sat | 0 | | | |ball_count_2d_hill.05.seq_lazy_lemmas_global_11.smt2 | 0.185s | 22.82MiB| unsat | 0 | | | |sin-problem-8-weak-chunk-0079.smt2 | 0.186s | 20.872MiB| unsat | 0 | | | |ball_count_2d_hill.04.seq_lazy_linear_enc_global_15.smt2 | 0.187s | 23.5MiB| unsat | 0 | | | |ball_count_2d_hill.04.seq_lazy_lemmas_global_11.smt2 | 0.193s | 22.888MiB| unsat | 0 | | | |ball_count_2d_hill.03.seq_lazy_lemmas_global_11.smt2 | 0.193s | 22.824MiB| unsat | 0 | | | |etcs_braking_2.01.seq_lazy_lemmas_global_5.smt2 | 0.201s | 22.6MiB| unsat | 0 | | | |ball_count_2d_hill.05.seq_lazy_linear_enc_global_15.smt2 | 0.204s | 23.708MiB| unsat | 0 | | | |mc91test.t2.c_Iteration5_Loop_3-pieceTemplate.smt2 | 0.217s | 23.48MiB| sat | 0 | | | |ball_count_2d_hill.03.seq_lazy_linear_enc_global_15.smt2 | 0.218s | 23.484MiB| unsat | 0 | | | |standard_init9_ground.i_3_2_2.bpl_1.smt2 | 0.223s | 21.6MiB| unsat | 0 | | | |ball_count_1d_plain.03.seq_lazy_global_15.smt2 | 0.228s | 22.092MiB| unsat | 0 | | | |qrdcmp.t2.c_Iteration6_Loop_3-pieceTemplate.smt2 | 0.249s | 23.632MiB| sat | 0 | | | |ball_count_2d_slope.05.seq_lazy_lemmas_global_5.smt2 | 0.253s | 22.408MiB| unsat | 0 | | | |ball_count_2d_slope.03.seq_lazy_linear_enc_global_7.smt2 | 0.256s | 22.36MiB| unsat | 0 | | | |ball_count_1d_plain.04.redlog_global_15.smt2 | 0.271s | 22.156MiB| unsat | 0 | | | |ball_count_1d_plain.05.seq_lazy_linear_enc_lemmas_global_15.smt2 | 0.285s | 22.132MiB| unsat | 0 | | | |CMOS-opamp-chunk-0180.smt2 | 0.307s | 21.408MiB| unsat | 0 | | | |pentagon.t2.c_Iteration9_Loop_3-pieceTemplate.smt2 | 0.320s | 22.848MiB| sat | 0 | | | |atan-problem-2-weak-chunk-0201.smt2 | 0.324s | 23.056MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0296.smt2 | 0.357s | 21.276MiB| unsat | 0 | | | |p-42.t2.c_Iteration2_Loop_4-pieceTemplate.smt2 | 0.415s | 24.692MiB| sat | 0 | | | |sort.t2.c_Iteration5_Loop_3-pieceTemplate.smt2 | 0.462s | 26.28MiB| sat | 0 | | | |spiral.t2.c_Iteration8_Loop_4-pieceTemplate.smt2 | 0.489s | 24.58MiB| sat | 0 | | | |etcs_braking_2.01.seq_lazy_linear_enc_global_9.smt2 | 0.506s | 24.26MiB| unsat | 0 | | | |toeplz.t2.c_Iteration7_Loop_4-pieceTemplate.smt2 | 0.595s | 24.964MiB| sat | 0 | | | |bf10.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 0.615s | 25.092MiB| sat | 0 | | | |CookSeeZuleger-2013TACAS-Fig3_true-termination.c_Iteration1_Loop_5-phaseTemplate.smt2 | 0.638s | 44.712MiB| unsat | 0 | | | |Canberra.bpl_Iteration1_Loop_2-pieceTemplate.smt2 | 0.715s | 44.852MiB| unsat | 0 | | | |matrix-1-all-38.smt2 | 0.733s | 21.796MiB| sat | 0 | | | |SyntaxSupportDisjunction1.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 0.747s | 26.08MiB| sat | 0 | | | |ball_count_2d_slope.05.seq_lazy_linear_enc_global_9.smt2 | 0.766s | 23.712MiB| unsat | 0 | | | |ball_count_2d_hill.03.redlog_global_9.smt2 | 0.822s | 23.436MiB| unsat | 0 | | | |ball_count_2d_hill.05.redlog_global_9.smt2 | 0.826s | 23.652MiB| unsat | 0 | | | |ball_count_2d_hill.04.redlog_global_9.smt2 | 0.849s | 23.66MiB| unsat | 0 | | | |ball_count_2d_slope.03.seq_lazy_global_9.smt2 | 0.929s | 24.008MiB| unsat | 0 | | | |CookSeeZuleger-2013TACAS-Fig7a_true-termination.c_Iteration1_Loop_5-phaseTemplate.smt2 | 0.936s | 76.208MiB| unsat | 0 | | | |ex11.t2.c_Iteration1_Lasso_5-phaseTemplate.smt2 | 1.087s | 29.512MiB| unsat | 0 | | | |Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2 | 1.164s | 43.148MiB| unsat | 0 | | | |exp-problem-10-2-chunk-0315.smt2 | 1.379s | 22.388MiB| unsat | 0 | | | |Chua-2-IL-U-chunk-0123.smt2 | 1.673s | 22.092MiB| unsat | 0 | | | |eric.t2.c_Iteration1_Lasso_5-phaseTemplate.smt2 | 1.900s | 27.044MiB| unsat | 0 | | | |ball_count_2d_slope.04.seq_lazy_lemmas_global_9.smt2 | 2.596s | 25.152MiB| unsat | 0 | | | |ball_count_2d_slope.03.seq_lazy_linear_enc_global_11.smt2 | 2.770s | 25.54MiB| unsat | 0 | | | |sin-problem-7-weak2-chunk-0113.smt2 | 3.148s | 22.0MiB| unsat | 0 | | | |joey_false-termination.c_Iteration2_Loop_6-phaseTemplate.smt2 | 3.658s | 28.748MiB| unsat | 0 | | | |sin-problem-7-weak-chunk-0181.smt2 | 3.718s | 21.98MiB| sat | 0 | | | |p-55.t2.c_Iteration3_Loop_4-pieceTemplate.smt2 | 4.564s | 42.896MiB| sat | 0 | | | |TelAviv-Amir-Minimum_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2 | 4.673s | 260.0MiB| unsat | 0 | | | |KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-termination.c_Iteration1_Lasso_affineTemplate.smt2 | 5.379s | 69.152MiB| unsat | 0 | | | |ball_count_2d_hill.05.redlog_global_13.smt2 | 6.819s | 25.812MiB| unsat | 0 | | | |ball_count_2d_hill.03.redlog_global_13.smt2 | 7.591s | 25.964MiB| unsat | 0 | | | |ball_count_2d_hill.04.redlog_global_13.smt2 | 8.023s | 25.9MiB| unsat | 0 | | | |ball_count_2d_slope.05.seq_lazy_global_15.smt2 | 10.091s | 33.96MiB| unknown | 0 | | | |ball_count_2d_slope.03.seq_lazy_global_13.smt2 | 14.066s | 29.632MiB| unknown | 0 | | | |ball_count_2d_slope.05.seq_lazy_linear_enc_global_13.smt2 | 14.077s | 37.4MiB| unknown | 0 | | | |ball_count_2d_slope.04.seq_lazy_lemmas_global_13.smt2 | 14.085s | 30.196MiB| unknown | 0 | | | |mbo_E6E7.smt2 | 14.133s | 22.48MiB| unsat | 0 | | | |2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2 | 14.197s | 25.104MiB| unsat | 0 | | | |BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2 | 14.209s | 31.144MiB| unsat | 0 | | | |mbo_E13E17.smt2 | 14.248s | 150.0MiB| unknown | 0 | | | |ex4.t2.c_Iteration2_Loop_3-pieceTemplate.smt2 | 14.251s | 26.528MiB| sat | 0 | | | |mbo_E1E22.smt2 | 14.256s | 219.0MiB| unknown | 0 | | | |mbo_E9E13.smt2 | 14.319s | 127.0MiB| unknown | 0 | | | |etcs_braking_2.01.seq_lazy_global_15.smt2 | 14.351s | 36.088MiB| unsat | 0 | | | |matrix-2-all-4.smt2 | 14.408s | 239.0MiB| sat | 0 | | | |mbo_E15E18.smt2 | 14.593s | 128.0MiB| unknown | 0 | | | |selectSort.t2.c_Iteration3_Loop_4-pieceTemplate.smt2 | 14.660s | 29.384MiB| sat | 0 | | | |mbo_E4E17.smt2 | 15.082s | 235.0MiB| unknown | 0 | | | |db3.t2.c_Iteration2_Loop_4-pieceTemplate.smt2 | 15.474s | 34.608MiB| sat | 0 | | | |mbo_E5E12.smt2 | 15.491s | 126.0MiB| unknown | 0 | | | |loop_on_input.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 15.756s | 30.396MiB| sat | 0 | | | |mbo_E1E6.smt2 | 15.952s | 256.0MiB| unknown | 0 | | | |Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2 | 16.382s | 27.036MiB| unsat | 0 | | | |MulliganEconomicsModel0057c.smt2 | 18.614s | 29.892MiB| unsat | 0 | | | |fun9.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 19.234s | 31.508MiB| sat | 0 | | | |Garmisch.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 20.740s | 28.52MiB| unsat | 0 | | | |mbo_E7E26.smt2 | 25.686s | 60.996MiB| unsat | 0 | | | |fuhs-inflasso.t2.c_Iteration2_Loop_4-pieceTemplate.smt2 | 26.361s | 32.504MiB| sat | 0 | | | |polyrank3.t2.c_Iteration2_Loop_3-pieceTemplate.smt2 | 28.947s | 34.716MiB| unsat | 0 | | | |nested.t2.c_Iteration3_Loop_3-pieceTemplate.smt2 | 32.201s | 39.528MiB| sat | 0 | | | |standard_copy5_ground.i_3_2_2.bpl_3.smt2 | 32.236s | 24.052MiB| unsat | 0 | | | |byron-1.t2.c_Iteration1_Loop_3-pieceTemplate.smt2 | 32.790s | 29.72MiB| unsat | 0 | | | |matrix-3-all-4.smt2 | 32.813s | 58.036MiB| sat | 0 | | | |Mysore2.bpl_Iteration1_Loop_3-pieceTemplate.smt2 | 32.870s | 57.548MiB| unsat | 0 | | | |SyntaxSupportDivision1.bpl_Iteration1_Lasso_7-nestedTemplate.smt2 | 39.029s | 81.04MiB| sat | 0 | | | |Lobnya-Boolean-Reordered.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 40.297s | 37.8MiB| unsat | 0 | | | |Collatz.bpl_Iteration1_Loop_3-nestedTemplate.smt2 | 44.534s | 253.0MiB| unsat | 0 | | | |mbo_E14E22.smt2 | 45.280s | 231.0MiB| sat | 0 | | | |simple-scaled200.bpl_Iteration1_Lasso_7-phaseTemplate.smt2 | 46.259s | 170.0MiB| sat | 0 | | | |Collatz.bpl_Iteration1_Loop_6-phaseTemplate.smt2 | 47.740s | 489.0MiB| unsat | 0 | | | |Collatz.bpl_Iteration1_Lasso_6-nestedTemplate.smt2 | 49.381s | 509.0MiB| unsat | 0 | | | |polyrank5.t2.c_Iteration1_Loop_7-phaseTemplate.smt2 | 50.171s | 28.908MiB| sat | 0 | | | |etcs_braking_2.01.redlog_global_7.smt2 | 50.210s | 34.212MiB| unsat | 0 | | | |mbo_E25.smt2 | 50.248s | 25.704MiB| unsat | 0 | | | |etcs_braking_2.01.redlog_global_11.smt2 | 50.253s | 40.148MiB| unsat | 0 | | | |polyrank4.t2.c_Iteration8_Loop_2-pieceTemplate.smt2 | 50.314s | 35.816MiB| unsat | 0 | | | |kissing_4_4.smt2 | 50.709s | 88.504MiB| sat | 0 | | | |polyrank4.t2.c_Iteration3_Loop_3-pieceTemplate.smt2 | 51.189s | 40.028MiB| unsat | 0 | | | |SantaBarbara01.bpl_Iteration1_Lasso_4-pieceTemplate.smt2 | 51.795s | 38.792MiB| unsat | 0 | | | |BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2 | 52.088s | 54.64MiB| unsat | 0 | | | |Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 52.519s | 51.768MiB| unsat | 0 | | | |yPositive-MixedIntReal.bpl_Iteration1_Loop_3-pieceTemplate.smt2 | 52.699s | 47.228MiB| unsat | 0 | | | |mbo_E23E24.smt2 | 52.876s | 101.0MiB| unsat | 0 | | | |iecs.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 53.029s | 56.956MiB| unsat | 0 | | | |LeeJonesBen-Amram-2001POPL-Ex4_true-termination.c_Iteration2_Loop_3-pieceTemplate.smt2 | 53.319s | 67.18MiB| unsat | 0 | | | |eric2.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 53.496s | 71.46MiB| unsat | 0 | | | |CookSeeZuleger-2013TACAS-Fig7b.bpl_Iteration1_Loop_3-pieceTemplate.smt2 | 53.878s | 104.0MiB| unsat | 0 | | | |mbo_E7E16.smt2 | 53.909s | 116.0MiB| unsat | 0 | | | |mbo_E4E27.smt2 | 54.792s | 70.264MiB| unsat | 0 | | | |LeeJonesBen-Amram-2001POPL-Ex1_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2 | 54.854s | 84.66MiB| unsat | 0 | | | |mbo_E13E27.smt2 | 55.515s | 89.96MiB| unsat | 0 | | | |collatz.t2.c_Iteration3_Lasso_6-phaseTemplate.smt2 | 56.357s | 66.744MiB| unsat | 0 | | | |mbo_E18E22.smt2 | 56.413s | 81.296MiB| unsat | 0 | | | |polyrank3.t2.c_Iteration8_Loop_4-pieceTemplate.smt2 | 56.585s | 83.604MiB| unsat | 0 | | | |sas2.t2.c_Iteration6_Lasso_7-nestedTemplate.smt2 | 56.781s | 54.504MiB| sat | 0 | | | |mbo_E12E13.smt2 | 57.065s | 748.0MiB| unknown | 0 | | | |Masse_true-termination.c_Iteration1_Loop_2-pieceTemplate.smt2 | 57.203s | 97.384MiB| unsat | 0 | | | |mbo_E2E10.smt2 | 57.682s | 770.0MiB| unknown | 0 | | | |mbo_E8E24.smt2 | 59.026s | 618.0MiB| unknown | 0 | | | |mbo_E10E18.smt2 | 59.051s | 614.0MiB| unknown | 0 | | | |mbo_E1E13.smt2 | 59.249s | 880.0MiB| unknown | 0 | | | |mbo_E3E8.smt2 | 59.541s | 901.0MiB| unknown | 0 | | | |mbo_E2E4.smt2 | 59.836s | 884.0MiB| unknown | 0 | | | |mbo_E20E25.smt2 | 59.885s | 76.656MiB| unsat | 0 | | | |mbo_E9E23.smt2 | 60.172s | 97.668MiB| unsat | 0 | | | |mbo_E3E13.smt2 | 60.504s | 838.0MiB| unknown | 0 | | | |mbo_E6E19.smt2 | 62.119s | 942.0MiB| unknown | 0 | | | |Nyala-TwoLex.bpl_Iteration1_Lasso_4-pieceTemplate.smt2 | 62.530s | 224.0MiB| unsat | 0 | | | |Collatz.bpl_Iteration1_Lasso_2-pieceTemplate.smt2 | 64.150s | 516.0MiB| unsat | 0 | | | |eric2.t2.c_Iteration7_Loop_4-pieceTemplate.smt2 | 66.684s | 316.0MiB| unsat | 0 | | | |KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-termination.c_Iteration1_Lasso_4-lexTemplate.smt2 | 69.824s | 286.0MiB| unsat | 0 | | | |mbo_E3E23.smt2 | 78.883s | 489.0MiB| unsat | 0 | | | |mbo_E15E28.smt2 | 79.128s | 478.0MiB| unsat | 0 | | | |mbo_E19E22.smt2 | 80.356s | 479.0MiB| unsat | 0 | | | |BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2 | 80.700s | 201.0MiB| unsat | 0 | | | |mbo_E12E23.smt2 | 83.072s | 79.2MiB| unsat | 0 | | | |firewire.t2.c_Iteration1_Lasso_7-nestedTemplate.smt2 | 87.436s | 96.076MiB| sat | 0 | | | |mbo_E11E20.smt2 | 91.725s | 81.044MiB| unsat | 0 | | | |matrix-5-all-13.smt2 | 94.437s | 563.0MiB| unknown | 0 | | | |mbo_E8E14.smt2 | 98.664s | 949.0MiB| unknown | 0 | | | |OpposedDisjuncts.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 106.875s | 296.0MiB| unsat | 0 | | | |GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_6-nestedTemplate.smt2 | 115.498s | 600.0MiB| unsat | 0 | | | |sqrt-1mcosq-8-chunk-0265.smt2 | 121.112s | 35.944MiB| unsat | 0 | | | |sas2.t2.c_Iteration1_Lasso_4-pieceTemplate.smt2 | 122.595s | 450.0MiB| sat | 0 | | | |sqrt-1mcosq-8-chunk-0176.smt2 | 130.598s | 35.772MiB| unsat | 0 | | | |GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_3-lexTemplate.smt2 | 134.918s | 866.0MiB| unsat | 0 | | | |mbo_E16E25.smt2 | 185.332s | 161.0MiB| unsat | 0 | | | |simple_ballistics_reach.01.seq_lazy_lemmas_global_15.smt2 | 200.010s | 34.388MiB| timeout | 0 | | | |sqrt-1mcosq-8-chunk-0233.smt2 | 200.011s | 80.092MiB| timeout | 0 | | | |matrix-4-all-4.smt2 | 200.012s | 261.0MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_global_11.smt2 | 200.012s | 50.196MiB| timeout | 0 | | | |linear_search.i_7_19_3.bpl_3.smt2 | 200.012s | 55.456MiB| timeout | 0 | | | |kissing_4_18.smt2 | 200.013s | 89.812MiB| timeout | 0 | | | |InVarSynth_BugHoareAnnotationWithMinimiation.bpl_Iteration1_0.smt2 | 200.014s | 79.628MiB| timeout | 0 | | | |atan-vega-3-weak-chunk-0385.smt2 | 200.015s | 29.232MiB| timeout | 0 | | | |matrix-4-all-22.smt2 | 200.015s | 150.0MiB| timeout | 0 | | | |fragtest_simple.i_4_5_4.bpl_3.smt2 | 200.015s | 105.0MiB| timeout | 0 | | | |sin-problem-7-chunk-0297.smt2 | 200.016s | 94.668MiB| timeout | 0 | | | |seq.i_5_5_5.bpl_3.smt2 | 200.017s | 75.028MiB| timeout | 0 | | | |avg60.i_5_5_4.bpl_3.smt2 | 200.017s | 41.048MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_linear_enc_global_5.smt2 | 200.017s | 54.044MiB| timeout | 0 | | | |kissing_3_9.smt2 | 200.018s | 76.368MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_9.smt2 | 200.018s | 33.628MiB| timeout | 0 | | | |InVarSynth_threadpooling_out2.mover.bpl_Iteration2_0.smt2 | 200.020s | 99.0MiB| timeout | 0 | | | |mbo_E2E20.smt2 | 200.023s | 521.0MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_13.smt2 | 200.024s | 32.536MiB| timeout | 0 | | | |standard_two_index_05.i_3_2_2.bpl_5.smt2 | 200.026s | 301.0MiB| timeout | 0 | | | |mbo_E10E28.smt2 | 200.026s | 497.0MiB| timeout | 0 | | | |etcs_braking_2.01.seq_lazy_linear_enc_global_13.smt2 | 200.026s | 53.752MiB| timeout | 0 | | | |matrix-4-all-13.smt2 | 200.032s | 41.492MiB| timeout | 0 | | | |matrix-2-all-17.smt2 | 200.036s | 65.744MiB| timeout | 0 | | | |kissing_3_11.smt2 | 200.043s | 143.0MiB| timeout | 0 | | | |matrix-3-all-13.smt2 | 200.045s | 231.0MiB| timeout | 0 | | | |simple_ballistics_reach.01.seq_lazy_global_7.smt2 | 200.051s | 34.6MiB| timeout | 0 | | | |LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_7-phaseTemplate.smt2 | 200.056s | 462.0MiB| timeout | 0 | | | |efegp.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2 | 200.061s | 511.0MiB| timeout | 0 | | | |LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_3-pieceTemplate.smt2 | 200.062s | 474.0MiB| timeout | 0 | | | |heidy7-simple.t2.c_Iteration2_Lasso_4-pieceTemplate.smt2 | 200.064s | 372.0MiB| timeout | 0 | | | |hong_10.smt2 | 200.065s | 43.98MiB| timeout | 0 | | | |afagp-fail.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2 | 200.068s | 573.0MiB| timeout | 0 | | | |min_rf_true-termination.c_Iteration1_Loop_4-pieceTemplate.smt2 | 200.074s | 525.0MiB| timeout | 0 | | | |BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2 | 200.077s | 726.0MiB| timeout | 0 | | | |yPositive-SIscaled50.bpl_Iteration1_Loop_4-pieceTemplate.smt2 | 200.089s | 701.0MiB| timeout | 0 | | | |aviad_true-termination.c_Iteration1_Loop_6-phaseTemplate.smt2 | 200.099s | 1016.0MiB| timeout | 0 | | | |p-46.t2.c_Iteration2_Lasso_7-phaseTemplate.smt2 | 200.107s | 442.0MiB| timeout | 0 | | | |aviad_true-termination.c_Iteration1_Loop_3-lexTemplate.smt2 | 200.109s | 1041.0MiB| timeout | 0 | | | |NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2 | 200.115s | 860.0MiB| timeout | 0 | | | |NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2 | 200.118s | 755.0MiB| timeout | 0 | | | |brp_withassume.t2.c_Iteration1_Loop_4-pieceTemplate.smt2 | 200.123s | 1306.0MiB| timeout | 0 | | | |Gulwani.bpl_Iteration1_Lasso_4-pieceTemplate.smt2 | 200.124s | 1198.0MiB| timeout | 0 | | |