Comparing data and data


# SUMMARY
- LHS tests = 1147
- RHS tests = 1147
- LHS success = 1147  (100.0%)
- RHS success = 1147  (100.0%)


## METADATA

<details><summary>METADATA</summary>

# LHS
<pre>
Ramon benchmark for Z3
-
Job description: master run
Job tag: bnsat_false
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: 84a7566c3aa816b422455fe580f51263718e26b4
Z3 branch: master
Z3 options: "-T:200"
Z3 inputs: inputs/QF_NRA_small
Z3 commit message: Merge pull request #8878 from Z3Prover/copilot/rename-qf-s-benchmark

Rename "Qf S Benchmark" to "ZIPT Benchmark"

</pre>
# RHS
<pre>
Ramon benchmark for Z3
-
Job description: master run
Job tag: bnsat_false
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: 84a7566c3aa816b422455fe580f51263718e26b4
Z3 branch: master
Z3 options: "-T:200"
Z3 inputs: inputs/QF_NRA_small
Z3 commit message: Merge pull request #8878 from Z3Prover/copilot/rename-qf-s-benchmark

Rename "Qf S Benchmark" to "ZIPT Benchmark"

</pre>
</details>


## TOP 20 RUNTIME INCREASE

<details><summary>TOP 20 RUNTIME INCREASE</summary>

|FILE                                                                                        |TIME_L     |TIME_R     |DIFF(s)    |DIFF(%)|
|-------------|-------------:|-------------:|--------------:|------------:|
|2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2                            |  14.183s  |  14.183s  |   0.000s  | 0.0%|
|Arthan1A-chunk-0020.smt2                                                                    |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|ArthanKM2-chunk-0002.smt2                                                                   |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|ArthanM2-chunk-0012.smt2                                                                    |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2           |   1.229s  |   1.229s  |   0.000s  | 0.0%|
|BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2                           |  52.650s  |  52.650s  |   0.000s  | 0.0%|
|Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2                                            |  52.295s  |  52.295s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2     | 200.080s  | 200.080s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2    |  14.195s  |  14.195s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2   |  79.058s  |  79.058s  |   0.000s  | 0.0%|
|Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2                          |  16.373s  |  16.373s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0025.smt2                                                                  |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0047.smt2                                                                  |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0062.smt2                                                                  |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0074.smt2                                                                  |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0086.smt2                                                                  |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0096.smt2                                                                  |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0108.smt2                                                                  |   0.062s  |   0.062s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0122.smt2                                                                  |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0137.smt2                                                                  |   0.040s  |   0.040s  |   0.000s  | 0.0%|
</details>


## TOP 20 RUNTIME INCREASE (RELATIVE)

<details><summary>TOP 20 RUNTIME INCREASE (RELATIVE)</summary>

|FILE                                                                                        |TIME_L     |TIME_R     |DIFF(s)    |DIFF(%)|
|-------------|-------------:|-------------:|--------------:|------------:|
|2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2                            |  14.183s  |  14.183s  |   0.000s  | 0.0%|
|Arthan1A-chunk-0020.smt2                                                                    |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|ArthanKM2-chunk-0002.smt2                                                                   |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|ArthanM2-chunk-0012.smt2                                                                    |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2           |   1.229s  |   1.229s  |   0.000s  | 0.0%|
|BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2                           |  52.650s  |  52.650s  |   0.000s  | 0.0%|
|Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2                                            |  52.295s  |  52.295s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2     | 200.080s  | 200.080s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2    |  14.195s  |  14.195s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2   |  79.058s  |  79.058s  |   0.000s  | 0.0%|
|Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2                          |  16.373s  |  16.373s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0025.smt2                                                                  |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0047.smt2                                                                  |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0062.smt2                                                                  |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0074.smt2                                                                  |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0086.smt2                                                                  |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0096.smt2                                                                  |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0108.smt2                                                                  |   0.062s  |   0.062s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0122.smt2                                                                  |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0137.smt2                                                                  |   0.040s  |   0.040s  |   0.000s  | 0.0%|
</details>


## TOP 20 RUNTIME DECREASE

<details><summary>TOP 20 RUNTIME DECREASE</summary>

|FILE                                                                                        |TIME_L     |TIME_R     |DIFF(s)    |DIFF(%)|
|-------------|-------------:|-------------:|--------------:|------------:|
|2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2                            |  14.183s  |  14.183s  |   0.000s  | 0.0%|
|Arthan1A-chunk-0020.smt2                                                                    |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|ArthanKM2-chunk-0002.smt2                                                                   |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|ArthanM2-chunk-0012.smt2                                                                    |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2           |   1.229s  |   1.229s  |   0.000s  | 0.0%|
|BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2                           |  52.650s  |  52.650s  |   0.000s  | 0.0%|
|Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2                                            |  52.295s  |  52.295s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2     | 200.080s  | 200.080s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2    |  14.195s  |  14.195s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2   |  79.058s  |  79.058s  |   0.000s  | 0.0%|
|Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2                          |  16.373s  |  16.373s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0025.smt2                                                                  |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0047.smt2                                                                  |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0062.smt2                                                                  |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0074.smt2                                                                  |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0086.smt2                                                                  |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0096.smt2                                                                  |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0108.smt2                                                                  |   0.062s  |   0.062s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0122.smt2                                                                  |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0137.smt2                                                                  |   0.040s  |   0.040s  |   0.000s  | 0.0%|
</details>


## TOP 20 RUNTIME DECREASE (RELATIVE)

<details><summary>TOP 20 RUNTIME DECREASE (RELATIVE)</summary>

|FILE                                                                                        |TIME_L     |TIME_R     |DIFF(s)    |DIFF(%)|
|-------------|-------------:|-------------:|--------------:|------------:|
|2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2                            |  14.183s  |  14.183s  |   0.000s  | 0.0%|
|Arthan1A-chunk-0020.smt2                                                                    |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|ArthanKM2-chunk-0002.smt2                                                                   |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|ArthanM2-chunk-0012.smt2                                                                    |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2           |   1.229s  |   1.229s  |   0.000s  | 0.0%|
|BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2                           |  52.650s  |  52.650s  |   0.000s  | 0.0%|
|Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2                                            |  52.295s  |  52.295s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2     | 200.080s  | 200.080s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2    |  14.195s  |  14.195s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2   |  79.058s  |  79.058s  |   0.000s  | 0.0%|
|Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2                          |  16.373s  |  16.373s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0025.smt2                                                                  |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0047.smt2                                                                  |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0062.smt2                                                                  |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0074.smt2                                                                  |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0086.smt2                                                                  |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0096.smt2                                                                  |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0108.smt2                                                                  |   0.062s  |   0.062s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0122.smt2                                                                  |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0137.smt2                                                                  |   0.040s  |   0.040s  |   0.000s  | 0.0%|
</details>


## TOP 20 LHS FILES, BY RUNTIME

<details><summary>TOP 20 LHS FILES, BY RUNTIME</summary>

|FILE                                                                                       |TIME     |MEM        |
|------------|----------:|---------:|
|Gulwani.bpl_Iteration1_Lasso_4-pieceTemplate.smt2                                          | 200.131s |1165.0MiB|
|NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2            | 200.129s |775.0MiB|
|aviad_true-termination.c_Iteration1_Loop_3-lexTemplate.smt2                                | 200.125s |1062.0MiB|
|NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2           | 200.117s |829.0MiB|
|brp_withassume.t2.c_Iteration1_Loop_4-pieceTemplate.smt2                                   | 200.113s |1047.0MiB|
|aviad_true-termination.c_Iteration1_Loop_6-phaseTemplate.smt2                              | 200.089s |911.0MiB|
|LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_3-pieceTemplate.smt2    | 200.087s |513.0MiB|
|p-46.t2.c_Iteration2_Lasso_7-phaseTemplate.smt2                                            | 200.084s |440.0MiB|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2    | 200.080s |726.0MiB|
|yPositive-SIscaled50.bpl_Iteration1_Loop_4-pieceTemplate.smt2                              | 200.078s |700.0MiB|
|efegp.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2                                           | 200.077s |513.0MiB|
|min_rf_true-termination.c_Iteration1_Loop_4-pieceTemplate.smt2                             | 200.072s |532.0MiB|
|afagp-fail.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2                                      | 200.071s |572.0MiB|
|LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_7-phaseTemplate.smt2    | 200.065s |457.0MiB|
|heidy7-simple.t2.c_Iteration2_Lasso_4-pieceTemplate.smt2                                   | 200.064s |374.0MiB|
|matrix-4-all-13.smt2                                                                       | 200.052s |41.536MiB|
|simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_9.smt2                        | 200.048s |33.268MiB|
|kissing_3_11.smt2                                                                          | 200.043s |143.0MiB|
|mbo_E2E20.smt2                                                                             | 200.042s |521.0MiB|
|simple_ballistics_reach.01.seq_lazy_linear_enc_global_5.smt2                               | 200.039s |54.192MiB|
</details>


## TOP 20 RHS FILES, BY RUNTIME

<details><summary>TOP 20 RHS FILES, BY RUNTIME</summary>

|FILE                                                                                       |TIME     |MEM        |
|------------|----------:|---------:|
|Gulwani.bpl_Iteration1_Lasso_4-pieceTemplate.smt2                                          | 200.131s |1165.0MiB|
|NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2            | 200.129s |775.0MiB|
|aviad_true-termination.c_Iteration1_Loop_3-lexTemplate.smt2                                | 200.125s |1062.0MiB|
|NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2           | 200.117s |829.0MiB|
|brp_withassume.t2.c_Iteration1_Loop_4-pieceTemplate.smt2                                   | 200.113s |1047.0MiB|
|aviad_true-termination.c_Iteration1_Loop_6-phaseTemplate.smt2                              | 200.089s |911.0MiB|
|LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_3-pieceTemplate.smt2    | 200.087s |513.0MiB|
|p-46.t2.c_Iteration2_Lasso_7-phaseTemplate.smt2                                            | 200.084s |440.0MiB|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2    | 200.080s |726.0MiB|
|yPositive-SIscaled50.bpl_Iteration1_Loop_4-pieceTemplate.smt2                              | 200.078s |700.0MiB|
|efegp.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2                                           | 200.077s |513.0MiB|
|min_rf_true-termination.c_Iteration1_Loop_4-pieceTemplate.smt2                             | 200.072s |532.0MiB|
|afagp-fail.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2                                      | 200.071s |572.0MiB|
|LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_7-phaseTemplate.smt2    | 200.065s |457.0MiB|
|heidy7-simple.t2.c_Iteration2_Lasso_4-pieceTemplate.smt2                                   | 200.064s |374.0MiB|
|matrix-4-all-13.smt2                                                                       | 200.052s |41.536MiB|
|simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_9.smt2                        | 200.048s |33.268MiB|
|kissing_3_11.smt2                                                                          | 200.043s |143.0MiB|
|mbo_E2E20.smt2                                                                             | 200.042s |521.0MiB|
|simple_ballistics_reach.01.seq_lazy_linear_enc_global_5.smt2                               | 200.039s |54.192MiB|
</details>


## TOP 20 MEMORY INCREASE

<details><summary>TOP 20 MEMORY INCREASE</summary>

|FILE                                                                                        |MEM_L         |MEM_R         |DIFF            |DIFF(%)|
|-------------|-------------:|-------------:|--------------:|------------:|
|2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2                            |25.224MiB|25.224MiB|0B| 0.0%|
|Arthan1A-chunk-0020.smt2                                                                    |20.56MiB|20.56MiB|0B| 0.0%|
|ArthanKM2-chunk-0002.smt2                                                                   |20.636MiB|20.636MiB|0B| 0.0%|
|ArthanM2-chunk-0012.smt2                                                                    |18.712MiB|18.712MiB|0B| 0.0%|
|Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2           |43.14MiB|43.14MiB|0B| 0.0%|
|BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2                           |54.204MiB|54.204MiB|0B| 0.0%|
|Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2                                            |51.86MiB|51.86MiB|0B| 0.0%|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2     |726.0MiB|726.0MiB|0B| 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2    |32.704MiB|32.704MiB|0B| 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2   |200.0MiB|200.0MiB|0B| 0.0%|
|Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2                          |27.012MiB|27.012MiB|0B| 0.0%|
|CMOS-opamp-chunk-0025.smt2                                                                  |21.0MiB|21.0MiB|0B| 0.0%|
|CMOS-opamp-chunk-0047.smt2                                                                  |20.856MiB|20.856MiB|0B| 0.0%|
|CMOS-opamp-chunk-0062.smt2                                                                  |20.776MiB|20.776MiB|0B| 0.0%|
|CMOS-opamp-chunk-0074.smt2                                                                  |20.684MiB|20.684MiB|0B| 0.0%|
|CMOS-opamp-chunk-0086.smt2                                                                  |20.908MiB|20.908MiB|0B| 0.0%|
|CMOS-opamp-chunk-0096.smt2                                                                  |20.508MiB|20.508MiB|0B| 0.0%|
|CMOS-opamp-chunk-0108.smt2                                                                  |21.064MiB|21.064MiB|0B| 0.0%|
|CMOS-opamp-chunk-0122.smt2                                                                  |20.76MiB|20.76MiB|0B| 0.0%|
|CMOS-opamp-chunk-0137.smt2                                                                  |20.668MiB|20.668MiB|0B| 0.0%|
</details>


## TOP 20 MEMORY INCREASE (RELATIVE)

<details><summary>TOP 20 MEMORY INCREASE (RELATIVE)</summary>

|FILE                                                                                        |MEM_L         |MEM_R         |DIFF            |DIFF(%)|
|-------------|-------------:|-------------:|--------------:|------------:|
|2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2                            |25.224MiB|25.224MiB|0B| 0.0%|
|Arthan1A-chunk-0020.smt2                                                                    |20.56MiB|20.56MiB|0B| 0.0%|
|ArthanKM2-chunk-0002.smt2                                                                   |20.636MiB|20.636MiB|0B| 0.0%|
|ArthanM2-chunk-0012.smt2                                                                    |18.712MiB|18.712MiB|0B| 0.0%|
|Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2           |43.14MiB|43.14MiB|0B| 0.0%|
|BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2                           |54.204MiB|54.204MiB|0B| 0.0%|
|Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2                                            |51.86MiB|51.86MiB|0B| 0.0%|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2     |726.0MiB|726.0MiB|0B| 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2    |32.704MiB|32.704MiB|0B| 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2   |200.0MiB|200.0MiB|0B| 0.0%|
|Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2                          |27.012MiB|27.012MiB|0B| 0.0%|
|CMOS-opamp-chunk-0025.smt2                                                                  |21.0MiB|21.0MiB|0B| 0.0%|
|CMOS-opamp-chunk-0047.smt2                                                                  |20.856MiB|20.856MiB|0B| 0.0%|
|CMOS-opamp-chunk-0062.smt2                                                                  |20.776MiB|20.776MiB|0B| 0.0%|
|CMOS-opamp-chunk-0074.smt2                                                                  |20.684MiB|20.684MiB|0B| 0.0%|
|CMOS-opamp-chunk-0086.smt2                                                                  |20.908MiB|20.908MiB|0B| 0.0%|
|CMOS-opamp-chunk-0096.smt2                                                                  |20.508MiB|20.508MiB|0B| 0.0%|
|CMOS-opamp-chunk-0108.smt2                                                                  |21.064MiB|21.064MiB|0B| 0.0%|
|CMOS-opamp-chunk-0122.smt2                                                                  |20.76MiB|20.76MiB|0B| 0.0%|
|CMOS-opamp-chunk-0137.smt2                                                                  |20.668MiB|20.668MiB|0B| 0.0%|
</details>


## TOP 20 MEMORY DECREASE

<details><summary>TOP 20 MEMORY DECREASE</summary>

|FILE                                                                                        |MEM_L         |MEM_R         |DIFF            |DIFF(%)|
|-------------|-------------:|-------------:|--------------:|------------:|
|2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2                            |25.224MiB|25.224MiB|0B| 0.0%|
|Arthan1A-chunk-0020.smt2                                                                    |20.56MiB|20.56MiB|0B| 0.0%|
|ArthanKM2-chunk-0002.smt2                                                                   |20.636MiB|20.636MiB|0B| 0.0%|
|ArthanM2-chunk-0012.smt2                                                                    |18.712MiB|18.712MiB|0B| 0.0%|
|Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2           |43.14MiB|43.14MiB|0B| 0.0%|
|BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2                           |54.204MiB|54.204MiB|0B| 0.0%|
|Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2                                            |51.86MiB|51.86MiB|0B| 0.0%|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2     |726.0MiB|726.0MiB|0B| 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2    |32.704MiB|32.704MiB|0B| 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2   |200.0MiB|200.0MiB|0B| 0.0%|
|Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2                          |27.012MiB|27.012MiB|0B| 0.0%|
|CMOS-opamp-chunk-0025.smt2                                                                  |21.0MiB|21.0MiB|0B| 0.0%|
|CMOS-opamp-chunk-0047.smt2                                                                  |20.856MiB|20.856MiB|0B| 0.0%|
|CMOS-opamp-chunk-0062.smt2                                                                  |20.776MiB|20.776MiB|0B| 0.0%|
|CMOS-opamp-chunk-0074.smt2                                                                  |20.684MiB|20.684MiB|0B| 0.0%|
|CMOS-opamp-chunk-0086.smt2                                                                  |20.908MiB|20.908MiB|0B| 0.0%|
|CMOS-opamp-chunk-0096.smt2                                                                  |20.508MiB|20.508MiB|0B| 0.0%|
|CMOS-opamp-chunk-0108.smt2                                                                  |21.064MiB|21.064MiB|0B| 0.0%|
|CMOS-opamp-chunk-0122.smt2                                                                  |20.76MiB|20.76MiB|0B| 0.0%|
|CMOS-opamp-chunk-0137.smt2                                                                  |20.668MiB|20.668MiB|0B| 0.0%|
</details>


## TOP 20 MEMORY DECREASE (RELATIVE)

<details><summary>TOP 20 MEMORY DECREASE (RELATIVE)</summary>

|FILE                                                                                        |MEM_L         |MEM_R         |DIFF            |DIFF(%)|
|-------------|-------------:|-------------:|--------------:|------------:|
|2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2                            |25.224MiB|25.224MiB|0B| 0.0%|
|Arthan1A-chunk-0020.smt2                                                                    |20.56MiB|20.56MiB|0B| 0.0%|
|ArthanKM2-chunk-0002.smt2                                                                   |20.636MiB|20.636MiB|0B| 0.0%|
|ArthanM2-chunk-0012.smt2                                                                    |18.712MiB|18.712MiB|0B| 0.0%|
|Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2           |43.14MiB|43.14MiB|0B| 0.0%|
|BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2                           |54.204MiB|54.204MiB|0B| 0.0%|
|Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2                                            |51.86MiB|51.86MiB|0B| 0.0%|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2     |726.0MiB|726.0MiB|0B| 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2    |32.704MiB|32.704MiB|0B| 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2   |200.0MiB|200.0MiB|0B| 0.0%|
|Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2                          |27.012MiB|27.012MiB|0B| 0.0%|
|CMOS-opamp-chunk-0025.smt2                                                                  |21.0MiB|21.0MiB|0B| 0.0%|
|CMOS-opamp-chunk-0047.smt2                                                                  |20.856MiB|20.856MiB|0B| 0.0%|
|CMOS-opamp-chunk-0062.smt2                                                                  |20.776MiB|20.776MiB|0B| 0.0%|
|CMOS-opamp-chunk-0074.smt2                                                                  |20.684MiB|20.684MiB|0B| 0.0%|
|CMOS-opamp-chunk-0086.smt2                                                                  |20.908MiB|20.908MiB|0B| 0.0%|
|CMOS-opamp-chunk-0096.smt2                                                                  |20.508MiB|20.508MiB|0B| 0.0%|
|CMOS-opamp-chunk-0108.smt2                                                                  |21.064MiB|21.064MiB|0B| 0.0%|
|CMOS-opamp-chunk-0122.smt2                                                                  |20.76MiB|20.76MiB|0B| 0.0%|
|CMOS-opamp-chunk-0137.smt2                                                                  |20.668MiB|20.668MiB|0B| 0.0%|
</details>


## TOP 20 LHS FILES, BY PEAK MEMORY USAGE

<details><summary>TOP 20 LHS FILES, BY PEAK MEMORY USAGE</summary>

|FILE                                                                                       |TIME     |MEM        |
|------------|----------:|---------:|
|Gulwani.bpl_Iteration1_Lasso_4-pieceTemplate.smt2                                          | 200.131s |1165.0MiB|
|aviad_true-termination.c_Iteration1_Loop_3-lexTemplate.smt2                                | 200.125s |1062.0MiB|
|brp_withassume.t2.c_Iteration1_Loop_4-pieceTemplate.smt2                                   | 200.113s |1047.0MiB|
|mbo_E6E19.smt2                                                                             |  60.380s |951.0MiB|
|mbo_E8E14.smt2                                                                             |  98.737s |948.0MiB|
|aviad_true-termination.c_Iteration1_Loop_6-phaseTemplate.smt2                              | 200.089s |911.0MiB|
|mbo_E3E8.smt2                                                                              |  58.959s |909.0MiB|
|mbo_E1E13.smt2                                                                             |  61.075s |887.0MiB|
|mbo_E2E4.smt2                                                                              |  58.281s |884.0MiB|
|GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_3-lexTemplate.smt2   | 132.266s |867.0MiB|
|mbo_E3E13.smt2                                                                             |  60.808s |843.0MiB|
|NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2           | 200.117s |829.0MiB|
|NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2            | 200.129s |775.0MiB|
|mbo_E2E10.smt2                                                                             |  58.938s |770.0MiB|
|mbo_E12E13.smt2                                                                            |  56.611s |759.0MiB|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2    | 200.080s |726.0MiB|
|yPositive-SIscaled50.bpl_Iteration1_Loop_4-pieceTemplate.smt2                              | 200.078s |700.0MiB|
|mbo_E8E24.smt2                                                                             |  56.844s |614.0MiB|
|mbo_E10E18.smt2                                                                            |  56.423s |614.0MiB|
|GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_6-nestedTemplate.smt2 | 112.713s |599.0MiB|
</details>


## TOP 20 RHS FILES, BY PEAK MEMORY USAGE

<details><summary>TOP 20 RHS FILES, BY PEAK MEMORY USAGE</summary>

|FILE                                                                                       |TIME     |MEM        |
|------------|----------:|---------:|
|Gulwani.bpl_Iteration1_Lasso_4-pieceTemplate.smt2                                          | 200.131s |1165.0MiB|
|aviad_true-termination.c_Iteration1_Loop_3-lexTemplate.smt2                                | 200.125s |1062.0MiB|
|brp_withassume.t2.c_Iteration1_Loop_4-pieceTemplate.smt2                                   | 200.113s |1047.0MiB|
|mbo_E6E19.smt2                                                                             |  60.380s |951.0MiB|
|mbo_E8E14.smt2                                                                             |  98.737s |948.0MiB|
|aviad_true-termination.c_Iteration1_Loop_6-phaseTemplate.smt2                              | 200.089s |911.0MiB|
|mbo_E3E8.smt2                                                                              |  58.959s |909.0MiB|
|mbo_E1E13.smt2                                                                             |  61.075s |887.0MiB|
|mbo_E2E4.smt2                                                                              |  58.281s |884.0MiB|
|GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_3-lexTemplate.smt2   | 132.266s |867.0MiB|
|mbo_E3E13.smt2                                                                             |  60.808s |843.0MiB|
|NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2           | 200.117s |829.0MiB|
|NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2            | 200.129s |775.0MiB|
|mbo_E2E10.smt2                                                                             |  58.938s |770.0MiB|
|mbo_E12E13.smt2                                                                            |  56.611s |759.0MiB|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2    | 200.080s |726.0MiB|
|yPositive-SIscaled50.bpl_Iteration1_Loop_4-pieceTemplate.smt2                              | 200.078s |700.0MiB|
|mbo_E8E24.smt2                                                                             |  56.844s |614.0MiB|
|mbo_E10E18.smt2                                                                            |  56.423s |614.0MiB|
|GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_6-nestedTemplate.smt2 | 112.713s |599.0MiB|
</details>


## FULL COMPARISON

<details><summary>FULL COMPARISON</summary>

|FILE                                                                                        |TIME_L     |TIME_R     |DIFF(s)    |DIFF(%)|
|-------------|-------------:|-------------:|--------------:|------------:|
|2013POPL-BenAmGen-Ex4.2.bpl_Iteration1_Loop_2-pieceTemplate.smt2                            |  14.183s  |  14.183s  |   0.000s  | 0.0%|
|Arthan1A-chunk-0020.smt2                                                                    |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|ArthanKM2-chunk-0002.smt2                                                                   |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|ArthanM2-chunk-0012.smt2                                                                    |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|Ben-Amram-2010LMCS-Ex2.3_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2           |   1.229s  |   1.229s  |   0.000s  | 0.0%|
|BenAmram-2010LMCS-Ex2.3.bpl_Iteration1_Lasso_2-pieceTemplate.smt2                           |  52.650s  |  52.650s  |   0.000s  | 0.0%|
|Boulder.bpl_Iteration1_Loop_4-pieceTemplate.smt2                                            |  52.295s  |  52.295s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005CAV-Fig1_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2     | 200.080s  | 200.080s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl_Iteration1_Lasso_7-phaseTemplate.smt2    |  14.195s  |  14.195s  |   0.000s  | 0.0%|
|BradleyMannaSipma-2005ICALP-Fig1_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2   |  79.058s  |  79.058s  |   0.000s  | 0.0%|
|Braverman-2006CAV-Ex1-int.bpl_Iteration1_Loop_4-phaseTemplate.smt2                          |  16.373s  |  16.373s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0025.smt2                                                                  |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0047.smt2                                                                  |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0062.smt2                                                                  |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0074.smt2                                                                  |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0086.smt2                                                                  |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0096.smt2                                                                  |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0108.smt2                                                                  |   0.062s  |   0.062s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0122.smt2                                                                  |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0137.smt2                                                                  |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0148.smt2                                                                  |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0158.smt2                                                                  |   0.080s  |   0.080s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0169.smt2                                                                  |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0180.smt2                                                                  |   0.339s  |   0.339s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0190.smt2                                                                  |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0200.smt2                                                                  |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0213.smt2                                                                  |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0231.smt2                                                                  |   0.027s  |   0.027s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0246.smt2                                                                  |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0260.smt2                                                                  |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0275.smt2                                                                  |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0286.smt2                                                                  |   0.080s  |   0.080s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0298.smt2                                                                  |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0310.smt2                                                                  |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0320.smt2                                                                  |   0.149s  |   0.149s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0332.smt2                                                                  |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|CMOS-opamp-chunk-0342.smt2                                                                  |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|CONVOI2-chunk-0018.smt2                                                                     |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|CONVOI2-chunk-0031.smt2                                                                     |   0.041s  |   0.041s  |   0.000s  | 0.0%|
|CONVOI2-chunk-0041.smt2                                                                     |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|Canberra.bpl_Iteration1_Loop_2-pieceTemplate.smt2                                           |   0.739s  |   0.739s  |   0.000s  | 0.0%|
|Chua-1-IL-L-chunk-0016.smt2                                                                 |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|Chua-1-IL-L-chunk-0030.smt2                                                                 |   0.078s  |   0.078s  |   0.000s  | 0.0%|
|Chua-1-IL-L-chunk-0042.smt2                                                                 |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|Chua-1-IL-L-chunk-0054.smt2                                                                 |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|Chua-1-IL-L-chunk-0066.smt2                                                                 |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|Chua-1-IL-L-chunk-0078.smt2                                                                 |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|Chua-1-IL-L-chunk-0090.smt2                                                                 |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|Chua-1-IL-L-chunk-0104.smt2                                                                 |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|Chua-1-IL-L-chunk-0117.smt2                                                                 |   0.027s  |   0.027s  |   0.000s  | 0.0%|
|Chua-1-IL-L-chunk-0129.smt2                                                                 |   0.027s  |   0.027s  |   0.000s  | 0.0%|
|Chua-1-IL-L-chunk-0143.smt2                                                                 |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|Chua-1-IL-L-chunk-0154.smt2                                                                 |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|Chua-1-IL-U-chunk-0025.smt2                                                                 |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|Chua-1-IL-U-chunk-0038.smt2                                                                 |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|Chua-1-IL-U-chunk-0049.smt2                                                                 |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|Chua-1-IL-U-chunk-0063.smt2                                                                 |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|Chua-1-IL-U-chunk-0076.smt2                                                                 |   0.100s  |   0.100s  |   0.000s  | 0.0%|
|Chua-1-VC1-L-chunk-0019.smt2                                                                |   0.060s  |   0.060s  |   0.000s  | 0.0%|
|Chua-1-VC1-L-chunk-0035.smt2                                                                |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|Chua-1-VC1-L-chunk-0046.smt2                                                                |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|Chua-1-VC1-L-chunk-0057.smt2                                                                |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|Chua-1-VC1-L-chunk-0070.smt2                                                                |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|Chua-1-VC1-L-chunk-0081.smt2                                                                |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|Chua-1-VC1-L-chunk-0093.smt2                                                                |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|Chua-1-VC1-L-chunk-0107.smt2                                                                |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|Chua-1-VC1-L-chunk-0120.smt2                                                                |   0.041s  |   0.041s  |   0.000s  | 0.0%|
|Chua-1-VC1-L-chunk-0132.smt2                                                                |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|Chua-1-VC1-L-chunk-0146.smt2                                                                |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|Chua-1-VC1-L-chunk-0160.smt2                                                                |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|Chua-1-VC1-U-chunk-0032.smt2                                                                |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|Chua-1-VC1-U-chunk-0044.smt2                                                                |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|Chua-1-VC1-U-chunk-0056.smt2                                                                |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|Chua-1-VC1-U-chunk-0072.smt2                                                                |   0.062s  |   0.062s  |   0.000s  | 0.0%|
|Chua-1-VC1-U-chunk-0083.smt2                                                                |   0.084s  |   0.084s  |   0.000s  | 0.0%|
|Chua-1-VC2-L-chunk-0027.smt2                                                                |   0.026s  |   0.026s  |   0.000s  | 0.0%|
|Chua-1-VC2-L-chunk-0039.smt2                                                                |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|Chua-1-VC2-L-chunk-0050.smt2                                                                |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|Chua-1-VC2-L-chunk-0064.smt2                                                                |   0.023s  |   0.023s  |   0.000s  | 0.0%|
|Chua-1-VC2-L-chunk-0077.smt2                                                                |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|Chua-1-VC2-U-chunk-0024.smt2                                                                |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|Chua-1-VC2-U-chunk-0038.smt2                                                                |   0.085s  |   0.085s  |   0.000s  | 0.0%|
|Chua-1-VC2-U-chunk-0050.smt2                                                                |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|Chua-1-VC2-U-chunk-0061.smt2                                                                |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|Chua-1-VC2-U-chunk-0073.smt2                                                                |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|Chua-1-VC2-U-chunk-0086.smt2                                                                |   0.080s  |   0.080s  |   0.000s  | 0.0%|
|Chua-1-VC2-U-chunk-0097.smt2                                                                |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|Chua-1-VC2-U-chunk-0113.smt2                                                                |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|Chua-1-VC2-U-chunk-0123.smt2                                                                |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|Chua-1-VC2-U-chunk-0135.smt2                                                                |   0.075s  |   0.075s  |   0.000s  | 0.0%|
|Chua-1-VC2-U-chunk-0149.smt2                                                                |   0.092s  |   0.092s  |   0.000s  | 0.0%|
|Chua-2-IL-L-chunk-0005.smt2                                                                 |   0.062s  |   0.062s  |   0.000s  | 0.0%|
|Chua-2-IL-L-chunk-0021.smt2                                                                 |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|Chua-2-IL-L-chunk-0037.smt2                                                                 |   0.065s  |   0.065s  |   0.000s  | 0.0%|
|Chua-2-IL-L-chunk-0047.smt2                                                                 |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|Chua-2-IL-L-chunk-0058.smt2                                                                 |   0.094s  |   0.094s  |   0.000s  | 0.0%|
|Chua-2-IL-L-chunk-0072.smt2                                                                 |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|Chua-2-IL-L-chunk-0082.smt2                                                                 |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|Chua-2-IL-L-chunk-0093.smt2                                                                 |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|Chua-2-IL-L-chunk-0104.smt2                                                                 |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|Chua-2-IL-U-chunk-0009.smt2                                                                 |   0.027s  |   0.027s  |   0.000s  | 0.0%|
|Chua-2-IL-U-chunk-0021.smt2                                                                 |   0.076s  |   0.076s  |   0.000s  | 0.0%|
|Chua-2-IL-U-chunk-0032.smt2                                                                 |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|Chua-2-IL-U-chunk-0042.smt2                                                                 |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|Chua-2-IL-U-chunk-0053.smt2                                                                 |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|Chua-2-IL-U-chunk-0067.smt2                                                                 |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|Chua-2-IL-U-chunk-0083.smt2                                                                 |   0.074s  |   0.074s  |   0.000s  | 0.0%|
|Chua-2-IL-U-chunk-0094.smt2                                                                 |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|Chua-2-IL-U-chunk-0107.smt2                                                                 |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|Chua-2-IL-U-chunk-0123.smt2                                                                 |   1.672s  |   1.672s  |   0.000s  | 0.0%|
|Chua-2-VC1-L-chunk-0036.smt2                                                                |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|Chua-2-VC1-L-chunk-0052.smt2                                                                |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|Chua-2-VC1-L-chunk-0062.smt2                                                                |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|Chua-2-VC1-L-chunk-0073.smt2                                                                |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|Chua-2-VC1-L-chunk-0086.smt2                                                                |   0.073s  |   0.073s  |   0.000s  | 0.0%|
|Chua-2-VC1-L-chunk-0097.smt2                                                                |   0.062s  |   0.062s  |   0.000s  | 0.0%|
|Chua-2-VC1-L-chunk-0108.smt2                                                                |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|Chua-2-VC1-L-chunk-0119.smt2                                                                |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|Chua-2-VC1-U-chunk-0013.smt2                                                                |   0.091s  |   0.091s  |   0.000s  | 0.0%|
|Chua-2-VC1-U-chunk-0024.smt2                                                                |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|Chua-2-VC1-U-chunk-0035.smt2                                                                |   0.077s  |   0.077s  |   0.000s  | 0.0%|
|Chua-2-VC1-U-chunk-0045.smt2                                                                |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|Chua-2-VC1-U-chunk-0058.smt2                                                                |   0.076s  |   0.076s  |   0.000s  | 0.0%|
|Chua-2-VC1-U-chunk-0071.smt2                                                                |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|Chua-2-VC1-U-chunk-0087.smt2                                                                |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|Chua-2-VC1-U-chunk-0098.smt2                                                                |   0.075s  |   0.075s  |   0.000s  | 0.0%|
|Chua-2-VC1-U-chunk-0117.smt2                                                                |   0.097s  |   0.097s  |   0.000s  | 0.0%|
|Chua-2-VC2-L-chunk-0013.smt2                                                                |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|Chua-2-VC2-L-chunk-0029.smt2                                                                |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|Chua-2-VC2-L-chunk-0040.smt2                                                                |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|Chua-2-VC2-L-chunk-0052.smt2                                                                |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|Chua-2-VC2-L-chunk-0062.smt2                                                                |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|Chua-2-VC2-U-chunk-0018.smt2                                                                |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|Chua-2-VC2-U-chunk-0029.smt2                                                                |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|Chua-2-VC2-U-chunk-0039.smt2                                                                |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|Chua-2-VC2-U-chunk-0051.smt2                                                                |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|Chua-2-VC2-U-chunk-0066.smt2                                                                |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|Chua-2-VC2-U-chunk-0086.smt2                                                                |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|Chua-2-VC2-U-chunk-0097.smt2                                                                |   0.098s  |   0.098s  |   0.000s  | 0.0%|
|Chua-2-VC2-U-chunk-0111.smt2                                                                |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|Chua-2-VC2-U-chunk-0127.smt2                                                                |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|Collatz.bpl_Iteration1_Lasso_2-pieceTemplate.smt2                                           |  64.117s  |  64.117s  |   0.000s  | 0.0%|
|Collatz.bpl_Iteration1_Lasso_6-nestedTemplate.smt2                                          |  47.895s  |  47.895s  |   0.000s  | 0.0%|
|Collatz.bpl_Iteration1_Loop_3-nestedTemplate.smt2                                           |  44.661s  |  44.661s  |   0.000s  | 0.0%|
|Collatz.bpl_Iteration1_Loop_6-phaseTemplate.smt2                                            |  48.683s  |  48.683s  |   0.000s  | 0.0%|
|CookSeeZuleger-2013TACAS-Fig3_true-termination.c_Iteration1_Loop_5-phaseTemplate.smt2       |   0.557s  |   0.557s  |   0.000s  | 0.0%|
|CookSeeZuleger-2013TACAS-Fig7a_true-termination.c_Iteration1_Loop_5-phaseTemplate.smt2      |   0.759s  |   0.759s  |   0.000s  | 0.0%|
|CookSeeZuleger-2013TACAS-Fig7b.bpl_Iteration1_Loop_3-pieceTemplate.smt2                     |  53.449s  |  53.449s  |   0.000s  | 0.0%|
|Garmisch.bpl_Iteration1_Loop_4-pieceTemplate.smt2                                           |  21.826s  |  21.826s  |   0.000s  | 0.0%|
|Gulwani.bpl_Iteration1_Lasso_4-pieceTemplate.smt2                                           | 200.131s  | 200.131s  |   0.000s  | 0.0%|
|GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_3-lexTemplate.smt2    | 132.266s  | 132.266s  |   0.000s  | 0.0%|
|GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_6-nestedTemplate.smt2  | 112.713s  | 112.713s  |   0.000s  | 0.0%|
|InVarSynth_BugHoareAnnotationWithMinimiation.bpl_Iteration1_0.smt2                          | 200.016s  | 200.016s  |   0.000s  | 0.0%|
|InVarSynth_LabelEncodingWithUnrolling.bpl_Iteration2_0.smt2                                 |   0.080s  |   0.080s  |   0.000s  | 0.0%|
|InVarSynth_PostfixIncrementDecrement.c_Iteration3_0.smt2                                    |   0.073s  |   0.073s  |   0.000s  | 0.0%|
|InVarSynth_ShortCircuit-SideEffect-SwitchStatement-Safe.c_Iteration1_0.smt2                 |   0.125s  |   0.125s  |   0.000s  | 0.0%|
|InVarSynth_doubleLoopUniformIterations.bpl_Iteration2_0.smt2                                |   0.131s  |   0.131s  |   0.000s  | 0.0%|
|InVarSynth_threadpooling_out2.mover.bpl_Iteration2_0.smt2                                   | 200.019s  | 200.019s  |   0.000s  | 0.0%|
|KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-termination.c_Iteration1_Lasso_4-lexTemplate.smt2  |  70.285s  |  70.285s  |   0.000s  | 0.0%|
|KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-termination.c_Iteration1_Lasso_affineTemplate.smt2  |   4.922s  |   4.922s  |   0.000s  | 0.0%|
|LeeJonesBen-Amram-2001POPL-Ex1_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2      |  57.201s  |  57.201s  |   0.000s  | 0.0%|
|LeeJonesBen-Amram-2001POPL-Ex4_true-termination.c_Iteration2_Loop_3-pieceTemplate.smt2      |  53.182s  |  53.182s  |   0.000s  | 0.0%|
|LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_3-pieceTemplate.smt2     | 200.087s  | 200.087s  |   0.000s  | 0.0%|
|LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_7-phaseTemplate.smt2     | 200.065s  | 200.065s  |   0.000s  | 0.0%|
|Lobnya-Boolean-Reordered.bpl_Iteration1_Loop_4-pieceTemplate.smt2                           |  40.087s  |  40.087s  |   0.000s  | 0.0%|
|Lyapunov1a-chunk-0011.smt2                                                                  |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|Lyapunov1a-chunk-0021.smt2                                                                  |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|Lyapunov1a-chunk-0032.smt2                                                                  |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|Lyapunov1a-chunk-0042.smt2                                                                  |   0.055s  |   0.055s  |   0.000s  | 0.0%|
|Masse_true-termination.c_Iteration1_Loop_2-pieceTemplate.smt2                               |  58.619s  |  58.619s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0006a.smt2                                                            |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0013c.smt2                                                            |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0018e.smt2                                                            |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0024a.smt2                                                            |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0027c.smt2                                                            |   0.080s  |   0.080s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0030e.smt2                                                            |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0054a.smt2                                                            |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0057c.smt2                                                            |  18.613s  |  18.613s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0063e.smt2                                                            |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0067a.smt2                                                            |   0.099s  |   0.099s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0077c.smt2                                                            |   0.098s  |   0.098s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0080e.smt2                                                            |   0.076s  |   0.076s  |   0.000s  | 0.0%|
|MulliganEconomicsModel0085a.smt2                                                            |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|Mysore2.bpl_Iteration1_Loop_3-pieceTemplate.smt2                                            |  32.856s  |  32.856s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0024.smt2                                    |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0036.smt2                                    |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0054.smt2                                    |   0.073s  |   0.073s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0078.smt2                                    |   0.041s  |   0.041s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0098.smt2                                    |   0.099s  |   0.099s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0117.smt2                                    |   0.061s  |   0.061s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0137.smt2                                    |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0156.smt2                                    |   0.094s  |   0.094s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0173.smt2                                    |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0190.smt2                                    |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0205.smt2                                    |   0.083s  |   0.083s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0224.smt2                                    |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|Nichols-Plot-Inverted-Pendulum-Fails-1-6-chunk-0241.smt2                                    |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Lasso_4-pieceTemplate.smt2            | 200.117s  | 200.117s  |   0.000s  | 0.0%|
|NoriSharma-2013FSE-Fig8_true-termination.c_Iteration1_Loop_7-phaseTemplate.smt2             | 200.129s  | 200.129s  |   0.000s  | 0.0%|
|Nyala-TwoLex.bpl_Iteration1_Lasso_4-pieceTemplate.smt2                                      |  61.673s  |  61.673s  |   0.000s  | 0.0%|
|OpposedDisjuncts.bpl_Iteration1_Loop_4-pieceTemplate.smt2                                   | 106.257s  | 106.257s  |   0.000s  | 0.0%|
|RL-high-pass-circuit-gain-chunk-0010.smt2                                                   |   0.124s  |   0.124s  |   0.000s  | 0.0%|
|SantaBarbara01.bpl_Iteration1_Lasso_4-pieceTemplate.smt2                                    |  51.893s  |  51.893s  |   0.000s  | 0.0%|
|SyntaxSupportDisjunction1.bpl_Iteration1_Loop_4-pieceTemplate.smt2                          |   0.752s  |   0.752s  |   0.000s  | 0.0%|
|SyntaxSupportDivision1.bpl_Iteration1_Lasso_7-nestedTemplate.smt2                           |  39.100s  |  39.100s  |   0.000s  | 0.0%|
|TelAviv-Amir-Minimum_true-termination.c_Iteration1_Lasso_7-phaseTemplate.smt2               |   4.691s  |   4.691s  |   0.000s  | 0.0%|
|afagp-fail.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2                                       | 200.071s  | 200.071s  |   0.000s  | 0.0%|
|asin-8-chunk-0024.smt2                                                                      |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|asin-8-chunk-0039.smt2                                                                      |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|asin-8-chunk-0053.smt2                                                                      |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|asin-8-vars4-chunk-0019.smt2                                                                |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|asin-8-vars4-chunk-0034.smt2                                                                |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|asin-8-vars4-chunk-0046.smt2                                                                |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|atan-problem-1-chunk-0006.smt2                                                              |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|atan-problem-1-chunk-0022.smt2                                                              |   0.025s  |   0.025s  |   0.000s  | 0.0%|
|atan-problem-1-chunk-0035.smt2                                                              |   0.077s  |   0.077s  |   0.000s  | 0.0%|
|atan-problem-1-chunk-0047.smt2                                                              |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|atan-problem-1-chunk-0058.smt2                                                              |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|atan-problem-1-chunk-0071.smt2                                                              |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|atan-problem-1-chunk-0081.smt2                                                              |   0.060s  |   0.060s  |   0.000s  | 0.0%|
|atan-problem-1-chunk-0091.smt2                                                              |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|atan-problem-1-chunk-0102.smt2                                                              |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|atan-problem-1-weak-chunk-0020.smt2                                                         |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|atan-problem-1-weak-chunk-0035.smt2                                                         |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|atan-problem-2-chunk-0011.smt2                                                              |   0.041s  |   0.041s  |   0.000s  | 0.0%|
|atan-problem-2-chunk-0024.smt2                                                              |   0.071s  |   0.071s  |   0.000s  | 0.0%|
|atan-problem-2-chunk-0037.smt2                                                              |   0.055s  |   0.055s  |   0.000s  | 0.0%|
|atan-problem-2-chunk-0047.smt2                                                              |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|atan-problem-2-chunk-0059.smt2                                                              |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|atan-problem-2-chunk-0070.smt2                                                              |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|atan-problem-2-chunk-0080.smt2                                                              |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|atan-problem-2-chunk-0092.smt2                                                              |   0.076s  |   0.076s  |   0.000s  | 0.0%|
|atan-problem-2-chunk-0107.smt2                                                              |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|atan-problem-2-chunk-0117.smt2                                                              |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|atan-problem-2-sqrt-chunk-0019.smt2                                                         |   0.075s  |   0.075s  |   0.000s  | 0.0%|
|atan-problem-2-sqrt-chunk-0039.smt2                                                         |   0.073s  |   0.073s  |   0.000s  | 0.0%|
|atan-problem-2-sqrt-weak-chunk-0009.smt2                                                    |   0.093s  |   0.093s  |   0.000s  | 0.0%|
|atan-problem-2-sqrt-weak-chunk-0032.smt2                                                    |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|atan-problem-2-sqrt-weak-chunk-0050.smt2                                                    |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|atan-problem-2-sqrt-weak-chunk-0065.smt2                                                    |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|atan-problem-2-sqrt-weak-chunk-0075.smt2                                                    |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|atan-problem-2-sqrt-weak-chunk-0086.smt2                                                    |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0014.smt2                                                         |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0028.smt2                                                         |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0041.smt2                                                         |   0.060s  |   0.060s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0053.smt2                                                         |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0064.smt2                                                         |   0.090s  |   0.090s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0076.smt2                                                         |   0.084s  |   0.084s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0087.smt2                                                         |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0098.smt2                                                         |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0109.smt2                                                         |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0124.smt2                                                         |   0.055s  |   0.055s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0134.smt2                                                         |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0146.smt2                                                         |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0157.smt2                                                         |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0168.smt2                                                         |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0179.smt2                                                         |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0189.smt2                                                         |   0.055s  |   0.055s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0201.smt2                                                         |   0.308s  |   0.308s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0212.smt2                                                         |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|atan-problem-2-weak-chunk-0222.smt2                                                         |   0.041s  |   0.041s  |   0.000s  | 0.0%|
|atan-problem-2-weak2-chunk-0008.smt2                                                        |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|atan-problem-2-weak2-chunk-0022.smt2                                                        |   0.090s  |   0.090s  |   0.000s  | 0.0%|
|atan-problem-2-weak2-chunk-0043.smt2                                                        |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|atan-problem-2-weak2-chunk-0056.smt2                                                        |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|atan-problem-2-weak2-chunk-0070.smt2                                                        |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|atan-problem-2-weak2-chunk-0082.smt2                                                        |   0.087s  |   0.087s  |   0.000s  | 0.0%|
|atan-problem-2-weak2-chunk-0093.smt2                                                        |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|atan-problem-2-weak2-chunk-0103.smt2                                                        |   0.074s  |   0.074s  |   0.000s  | 0.0%|
|atan-problem-2-weak2-chunk-0120.smt2                                                        |   0.060s  |   0.060s  |   0.000s  | 0.0%|
|atan-problem-2-weak2-chunk-0136.smt2                                                        |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|atan-problem-2-weakT-chunk-0019.smt2                                                        |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|atan-problem-2-weakT-chunk-0030.smt2                                                        |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|atan-problem-2-weakT-chunk-0041.smt2                                                        |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|atan-problem-2-weakT-chunk-0054.smt2                                                        |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0011.smt2                                                                 |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0027.smt2                                                                 |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0045.smt2                                                                 |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0057.smt2                                                                 |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0067.smt2                                                                 |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0077.smt2                                                                 |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0089.smt2                                                                 |   0.061s  |   0.061s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0099.smt2                                                                 |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0109.smt2                                                                 |   0.083s  |   0.083s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0119.smt2                                                                 |   0.087s  |   0.087s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0129.smt2                                                                 |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0139.smt2                                                                 |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0149.smt2                                                                 |   0.083s  |   0.083s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0159.smt2                                                                 |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0169.smt2                                                                 |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0179.smt2                                                                 |   0.059s  |   0.059s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0189.smt2                                                                 |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0199.smt2                                                                 |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0210.smt2                                                                 |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0220.smt2                                                                 |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0230.smt2                                                                 |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0240.smt2                                                                 |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0250.smt2                                                                 |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0260.smt2                                                                 |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0270.smt2                                                                 |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0280.smt2                                                                 |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0290.smt2                                                                 |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0300.smt2                                                                 |   0.121s  |   0.121s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0310.smt2                                                                 |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0320.smt2                                                                 |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0330.smt2                                                                 |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0340.smt2                                                                 |   0.070s  |   0.070s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0350.smt2                                                                 |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0360.smt2                                                                 |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0370.smt2                                                                 |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0380.smt2                                                                 |   0.055s  |   0.055s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0390.smt2                                                                 |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0400.smt2                                                                 |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0413.smt2                                                                 |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0423.smt2                                                                 |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0433.smt2                                                                 |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0443.smt2                                                                 |   0.109s  |   0.109s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0453.smt2                                                                 |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0463.smt2                                                                 |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0473.smt2                                                                 |   0.069s  |   0.069s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0483.smt2                                                                 |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0493.smt2                                                                 |   0.095s  |   0.095s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0503.smt2                                                                 |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0513.smt2                                                                 |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0523.smt2                                                                 |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0533.smt2                                                                 |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0543.smt2                                                                 |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0553.smt2                                                                 |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0563.smt2                                                                 |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0573.smt2                                                                 |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0583.smt2                                                                 |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0593.smt2                                                                 |   0.064s  |   0.064s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0603.smt2                                                                 |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0613.smt2                                                                 |   0.098s  |   0.098s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0623.smt2                                                                 |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|atan-vega-3-chunk-0633.smt2                                                                 |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0019.smt2                                                            |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0074.smt2                                                            |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0102.smt2                                                            |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0113.smt2                                                            |   0.084s  |   0.084s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0126.smt2                                                            |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0136.smt2                                                            |   0.065s  |   0.065s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0147.smt2                                                            |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0159.smt2                                                            |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0170.smt2                                                            |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0183.smt2                                                            |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0193.smt2                                                            |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0204.smt2                                                            |   0.023s  |   0.023s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0218.smt2                                                            |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0231.smt2                                                            |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0241.smt2                                                            |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0255.smt2                                                            |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0267.smt2                                                            |   0.074s  |   0.074s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0277.smt2                                                            |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0290.smt2                                                            |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0301.smt2                                                            |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0312.smt2                                                            |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0323.smt2                                                            |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0334.smt2                                                            |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0344.smt2                                                            |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0363.smt2                                                            |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0374.smt2                                                            |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0385.smt2                                                            | 200.016s  | 200.016s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0398.smt2                                                            |   0.093s  |   0.093s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0409.smt2                                                            |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0421.smt2                                                            |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0433.smt2                                                            |   0.065s  |   0.065s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0444.smt2                                                            |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0457.smt2                                                            |   0.073s  |   0.073s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0469.smt2                                                            |   0.060s  |   0.060s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0480.smt2                                                            |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0490.smt2                                                            |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0500.smt2                                                            |   0.081s  |   0.081s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0510.smt2                                                            |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0522.smt2                                                            |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0534.smt2                                                            |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0545.smt2                                                            |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0555.smt2                                                            |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0566.smt2                                                            |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0576.smt2                                                            |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0586.smt2                                                            |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0596.smt2                                                            |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0606.smt2                                                            |   0.087s  |   0.087s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0619.smt2                                                            |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0629.smt2                                                            |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0639.smt2                                                            |   0.061s  |   0.061s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0651.smt2                                                            |   0.025s  |   0.025s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0661.smt2                                                            |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0671.smt2                                                            |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0681.smt2                                                            |   0.064s  |   0.064s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0691.smt2                                                            |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0701.smt2                                                            |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0711.smt2                                                            |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|atan-vega-3-weak-chunk-0721.smt2                                                            |   0.069s  |   0.069s  |   0.000s  | 0.0%|
|avg60.i_5_5_4.bpl_3.smt2                                                                    | 200.027s  | 200.027s  |   0.000s  | 0.0%|
|aviad_true-termination.c_Iteration1_Loop_3-lexTemplate.smt2                                 | 200.125s  | 200.125s  |   0.000s  | 0.0%|
|aviad_true-termination.c_Iteration1_Loop_6-phaseTemplate.smt2                               | 200.089s  | 200.089s  |   0.000s  | 0.0%|
|ball_count_1d_plain.01.qfree_global_1.smt2                                                  |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|ball_count_1d_plain.01.qfree_global_5.smt2                                                  |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|ball_count_1d_plain.01.redlog_global_13.smt2                                                |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|ball_count_1d_plain.01.redlog_global_9.smt2                                                 |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|ball_count_1d_plain.01.seq_lazy_global_3.smt2                                               |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|ball_count_1d_plain.01.seq_lazy_lemmas_global_11.smt2                                       |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|ball_count_1d_plain.01.seq_lazy_lemmas_global_7.smt2                                        |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|ball_count_1d_plain.01.seq_lazy_linear_enc_global_15.smt2                                   |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|ball_count_1d_plain.01.seq_lazy_linear_enc_lemmas_global_1.smt2                             |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|ball_count_1d_plain.01.seq_lazy_linear_enc_lemmas_global_5.smt2                             |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|ball_count_1d_plain.02.qfree_global_13.smt2                                                 |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|ball_count_1d_plain.02.qfree_global_9.smt2                                                  |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|ball_count_1d_plain.02.redlog_global_3.smt2                                                 |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|ball_count_1d_plain.02.seq_lazy_global_11.smt2                                              |   0.059s  |   0.059s  |   0.000s  | 0.0%|
|ball_count_1d_plain.02.seq_lazy_global_7.smt2                                               |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|ball_count_1d_plain.02.seq_lazy_lemmas_global_15.smt2                                       |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|ball_count_1d_plain.02.seq_lazy_linear_enc_global_1.smt2                                    |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|ball_count_1d_plain.02.seq_lazy_linear_enc_global_5.smt2                                    |   0.071s  |   0.071s  |   0.000s  | 0.0%|
|ball_count_1d_plain.02.seq_lazy_linear_enc_lemmas_global_13.smt2                            |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|ball_count_1d_plain.02.seq_lazy_linear_enc_lemmas_global_9.smt2                             |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|ball_count_1d_plain.03.qfree_global_3.smt2                                                  |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|ball_count_1d_plain.03.redlog_global_11.smt2                                                |   0.111s  |   0.111s  |   0.000s  | 0.0%|
|ball_count_1d_plain.03.redlog_global_7.smt2                                                 |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|ball_count_1d_plain.03.seq_lazy_global_15.smt2                                              |   0.173s  |   0.173s  |   0.000s  | 0.0%|
|ball_count_1d_plain.03.seq_lazy_lemmas_global_1.smt2                                        |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|ball_count_1d_plain.03.seq_lazy_lemmas_global_5.smt2                                        |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|ball_count_1d_plain.03.seq_lazy_linear_enc_global_13.smt2                                   |   0.089s  |   0.089s  |   0.000s  | 0.0%|
|ball_count_1d_plain.03.seq_lazy_linear_enc_global_9.smt2                                    |   0.153s  |   0.153s  |   0.000s  | 0.0%|
|ball_count_1d_plain.03.seq_lazy_linear_enc_lemmas_global_3.smt2                             |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|ball_count_1d_plain.04.qfree_global_11.smt2                                                 |   0.114s  |   0.114s  |   0.000s  | 0.0%|
|ball_count_1d_plain.04.qfree_global_7.smt2                                                  |   0.091s  |   0.091s  |   0.000s  | 0.0%|
|ball_count_1d_plain.04.redlog_global_15.smt2                                                |   0.276s  |   0.276s  |   0.000s  | 0.0%|
|ball_count_1d_plain.04.seq_lazy_global_1.smt2                                               |   0.061s  |   0.061s  |   0.000s  | 0.0%|
|ball_count_1d_plain.04.seq_lazy_global_5.smt2                                               |   0.097s  |   0.097s  |   0.000s  | 0.0%|
|ball_count_1d_plain.04.seq_lazy_lemmas_global_13.smt2                                       |   0.192s  |   0.192s  |   0.000s  | 0.0%|
|ball_count_1d_plain.04.seq_lazy_lemmas_global_9.smt2                                        |   0.121s  |   0.121s  |   0.000s  | 0.0%|
|ball_count_1d_plain.04.seq_lazy_linear_enc_global_3.smt2                                    |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|ball_count_1d_plain.04.seq_lazy_linear_enc_lemmas_global_11.smt2                            |   0.121s  |   0.121s  |   0.000s  | 0.0%|
|ball_count_1d_plain.04.seq_lazy_linear_enc_lemmas_global_7.smt2                             |   0.059s  |   0.059s  |   0.000s  | 0.0%|
|ball_count_1d_plain.05.qfree_global_15.smt2                                                 |   0.199s  |   0.199s  |   0.000s  | 0.0%|
|ball_count_1d_plain.05.redlog_global_1.smt2                                                 |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|ball_count_1d_plain.05.redlog_global_5.smt2                                                 |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|ball_count_1d_plain.05.seq_lazy_global_13.smt2                                              |   0.121s  |   0.121s  |   0.000s  | 0.0%|
|ball_count_1d_plain.05.seq_lazy_global_9.smt2                                               |   0.108s  |   0.108s  |   0.000s  | 0.0%|
|ball_count_1d_plain.05.seq_lazy_lemmas_global_3.smt2                                        |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|ball_count_1d_plain.05.seq_lazy_linear_enc_global_11.smt2                                   |   0.080s  |   0.080s  |   0.000s  | 0.0%|
|ball_count_1d_plain.05.seq_lazy_linear_enc_global_7.smt2                                    |   0.055s  |   0.055s  |   0.000s  | 0.0%|
|ball_count_1d_plain.05.seq_lazy_linear_enc_lemmas_global_15.smt2                            |   0.283s  |   0.283s  |   0.000s  | 0.0%|
|ball_count_1d_plain.10.qfree_global_1.smt2                                                  |   0.062s  |   0.062s  |   0.000s  | 0.0%|
|ball_count_1d_plain.10.qfree_global_5.smt2                                                  |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|ball_count_1d_plain.10.redlog_global_13.smt2                                                |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|ball_count_1d_plain.10.redlog_global_9.smt2                                                 |   0.075s  |   0.075s  |   0.000s  | 0.0%|
|ball_count_1d_plain.10.seq_lazy_global_3.smt2                                               |   0.055s  |   0.055s  |   0.000s  | 0.0%|
|ball_count_1d_plain.10.seq_lazy_lemmas_global_11.smt2                                       |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|ball_count_1d_plain.10.seq_lazy_lemmas_global_7.smt2                                        |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|ball_count_1d_plain.10.seq_lazy_linear_enc_global_15.smt2                                   |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|ball_count_1d_plain.10.seq_lazy_linear_enc_lemmas_global_1.smt2                             |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|ball_count_1d_plain.10.seq_lazy_linear_enc_lemmas_global_5.smt2                             |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|ball_count_2d_hill.01.redlog_global_13.smt2                                                 |   0.082s  |   0.082s  |   0.000s  | 0.0%|
|ball_count_2d_hill.01.redlog_global_9.smt2                                                  |   0.082s  |   0.082s  |   0.000s  | 0.0%|
|ball_count_2d_hill.01.seq_lazy_global_3.smt2                                                |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|ball_count_2d_hill.01.seq_lazy_lemmas_global_11.smt2                                        |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|ball_count_2d_hill.01.seq_lazy_lemmas_global_7.smt2                                         |   0.077s  |   0.077s  |   0.000s  | 0.0%|
|ball_count_2d_hill.01.seq_lazy_linear_enc_global_15.smt2                                    |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_1.smt2                              |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_5.smt2                              |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|ball_count_2d_hill.02.redlog_global_13.smt2                                                 |   0.082s  |   0.082s  |   0.000s  | 0.0%|
|ball_count_2d_hill.02.redlog_global_9.smt2                                                  |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|ball_count_2d_hill.02.seq_lazy_global_3.smt2                                                |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|ball_count_2d_hill.02.seq_lazy_lemmas_global_11.smt2                                        |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|ball_count_2d_hill.02.seq_lazy_lemmas_global_7.smt2                                         |   0.061s  |   0.061s  |   0.000s  | 0.0%|
|ball_count_2d_hill.02.seq_lazy_linear_enc_global_15.smt2                                    |   0.110s  |   0.110s  |   0.000s  | 0.0%|
|ball_count_2d_hill.02.seq_lazy_linear_enc_lemmas_global_1.smt2                              |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|ball_count_2d_hill.02.seq_lazy_linear_enc_lemmas_global_5.smt2                              |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|ball_count_2d_hill.03.redlog_global_13.smt2                                                 |   7.767s  |   7.767s  |   0.000s  | 0.0%|
|ball_count_2d_hill.03.redlog_global_9.smt2                                                  |   0.845s  |   0.845s  |   0.000s  | 0.0%|
|ball_count_2d_hill.03.seq_lazy_global_3.smt2                                                |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|ball_count_2d_hill.03.seq_lazy_lemmas_global_11.smt2                                        |   0.188s  |   0.188s  |   0.000s  | 0.0%|
|ball_count_2d_hill.03.seq_lazy_lemmas_global_7.smt2                                         |   0.090s  |   0.090s  |   0.000s  | 0.0%|
|ball_count_2d_hill.03.seq_lazy_linear_enc_global_15.smt2                                    |   0.220s  |   0.220s  |   0.000s  | 0.0%|
|ball_count_2d_hill.03.seq_lazy_linear_enc_lemmas_global_1.smt2                              |   0.055s  |   0.055s  |   0.000s  | 0.0%|
|ball_count_2d_hill.03.seq_lazy_linear_enc_lemmas_global_5.smt2                              |   0.138s  |   0.138s  |   0.000s  | 0.0%|
|ball_count_2d_hill.04.redlog_global_13.smt2                                                 |   7.850s  |   7.850s  |   0.000s  | 0.0%|
|ball_count_2d_hill.04.redlog_global_9.smt2                                                  |   0.808s  |   0.808s  |   0.000s  | 0.0%|
|ball_count_2d_hill.04.seq_lazy_global_3.smt2                                                |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|ball_count_2d_hill.04.seq_lazy_lemmas_global_11.smt2                                        |   0.178s  |   0.178s  |   0.000s  | 0.0%|
|ball_count_2d_hill.04.seq_lazy_lemmas_global_7.smt2                                         |   0.098s  |   0.098s  |   0.000s  | 0.0%|
|ball_count_2d_hill.04.seq_lazy_linear_enc_global_15.smt2                                    |   0.224s  |   0.224s  |   0.000s  | 0.0%|
|ball_count_2d_hill.04.seq_lazy_linear_enc_lemmas_global_1.smt2                              |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|ball_count_2d_hill.04.seq_lazy_linear_enc_lemmas_global_5.smt2                              |   0.071s  |   0.071s  |   0.000s  | 0.0%|
|ball_count_2d_hill.05.redlog_global_13.smt2                                                 |   6.635s  |   6.635s  |   0.000s  | 0.0%|
|ball_count_2d_hill.05.redlog_global_9.smt2                                                  |   0.839s  |   0.839s  |   0.000s  | 0.0%|
|ball_count_2d_hill.05.seq_lazy_global_3.smt2                                                |   0.081s  |   0.081s  |   0.000s  | 0.0%|
|ball_count_2d_hill.05.seq_lazy_lemmas_global_11.smt2                                        |   0.199s  |   0.199s  |   0.000s  | 0.0%|
|ball_count_2d_hill.05.seq_lazy_lemmas_global_7.smt2                                         |   0.091s  |   0.091s  |   0.000s  | 0.0%|
|ball_count_2d_hill.05.seq_lazy_linear_enc_global_15.smt2                                    |   0.219s  |   0.219s  |   0.000s  | 0.0%|
|ball_count_2d_hill.05.seq_lazy_linear_enc_lemmas_global_1.smt2                              |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|ball_count_2d_hill.05.seq_lazy_linear_enc_lemmas_global_5.smt2                              |   0.107s  |   0.107s  |   0.000s  | 0.0%|
|ball_count_2d_hill.10.redlog_global_13.smt2                                                 |   0.066s  |   0.066s  |   0.000s  | 0.0%|
|ball_count_2d_hill.10.redlog_global_9.smt2                                                  |   0.059s  |   0.059s  |   0.000s  | 0.0%|
|ball_count_2d_hill.10.seq_lazy_global_3.smt2                                                |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|ball_count_2d_hill.10.seq_lazy_lemmas_global_11.smt2                                        |   0.059s  |   0.059s  |   0.000s  | 0.0%|
|ball_count_2d_hill.10.seq_lazy_lemmas_global_7.smt2                                         |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|ball_count_2d_hill.10.seq_lazy_linear_enc_global_15.smt2                                    |   0.115s  |   0.115s  |   0.000s  | 0.0%|
|ball_count_2d_hill.10.seq_lazy_linear_enc_lemmas_global_1.smt2                              |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|ball_count_2d_hill.10.seq_lazy_linear_enc_lemmas_global_5.smt2                              |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.01.qfree_global_13.smt2                                           |   0.087s  |   0.087s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.01.qfree_global_9.smt2                                            |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.01.redlog_global_3.smt2                                           |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.01.seq_lazy_global_11.smt2                                        |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.01.seq_lazy_global_7.smt2                                         |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.01.seq_lazy_lemmas_global_15.smt2                                 |   0.066s  |   0.066s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.01.seq_lazy_linear_enc_global_1.smt2                              |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.01.seq_lazy_linear_enc_global_5.smt2                              |   0.084s  |   0.084s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.01.seq_lazy_linear_enc_lemmas_global_13.smt2                      |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.01.seq_lazy_linear_enc_lemmas_global_9.smt2                       |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.02.qfree_global_3.smt2                                            |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.02.redlog_global_11.smt2                                          |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.02.redlog_global_7.smt2                                           |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.02.seq_lazy_global_15.smt2                                        |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.02.seq_lazy_lemmas_global_1.smt2                                  |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.02.seq_lazy_lemmas_global_5.smt2                                  |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.02.seq_lazy_linear_enc_global_13.smt2                             |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.02.seq_lazy_linear_enc_global_9.smt2                              |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.02.seq_lazy_linear_enc_lemmas_global_3.smt2                       |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.03.qfree_global_11.smt2                                           |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.03.qfree_global_7.smt2                                            |   0.041s  |   0.041s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.03.redlog_global_15.smt2                                          |   0.090s  |   0.090s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.03.seq_lazy_global_1.smt2                                         |   0.026s  |   0.026s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.03.seq_lazy_global_5.smt2                                         |   0.091s  |   0.091s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.03.seq_lazy_lemmas_global_13.smt2                                 |   0.092s  |   0.092s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.03.seq_lazy_lemmas_global_9.smt2                                  |   0.072s  |   0.072s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.03.seq_lazy_linear_enc_global_3.smt2                              |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.03.seq_lazy_linear_enc_lemmas_global_11.smt2                      |   0.094s  |   0.094s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.03.seq_lazy_linear_enc_lemmas_global_7.smt2                       |   0.070s  |   0.070s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.04.qfree_global_15.smt2                                           |   0.073s  |   0.073s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.04.redlog_global_1.smt2                                           |   0.027s  |   0.027s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.04.redlog_global_5.smt2                                           |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.04.seq_lazy_global_13.smt2                                        |   0.066s  |   0.066s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.04.seq_lazy_global_9.smt2                                         |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.04.seq_lazy_lemmas_global_3.smt2                                  |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.04.seq_lazy_linear_enc_global_11.smt2                             |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.04.seq_lazy_linear_enc_global_7.smt2                              |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.04.seq_lazy_linear_enc_lemmas_global_15.smt2                      |   0.098s  |   0.098s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.05.qfree_global_1.smt2                                            |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.05.qfree_global_5.smt2                                            |   0.066s  |   0.066s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.05.redlog_global_13.smt2                                          |   0.106s  |   0.106s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.05.redlog_global_9.smt2                                           |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.05.seq_lazy_global_3.smt2                                         |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.05.seq_lazy_lemmas_global_11.smt2                                 |   0.125s  |   0.125s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.05.seq_lazy_lemmas_global_7.smt2                                  |   0.088s  |   0.088s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.05.seq_lazy_linear_enc_global_15.smt2                             |   0.118s  |   0.118s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.05.seq_lazy_linear_enc_lemmas_global_1.smt2                       |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.05.seq_lazy_linear_enc_lemmas_global_5.smt2                       |   0.114s  |   0.114s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.10.qfree_global_13.smt2                                           |   0.064s  |   0.064s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.10.qfree_global_9.smt2                                            |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.10.redlog_global_3.smt2                                           |   0.090s  |   0.090s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.10.seq_lazy_global_11.smt2                                        |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.10.seq_lazy_global_7.smt2                                         |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.10.seq_lazy_lemmas_global_15.smt2                                 |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.10.seq_lazy_linear_enc_global_1.smt2                              |   0.027s  |   0.027s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.10.seq_lazy_linear_enc_global_5.smt2                              |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.10.seq_lazy_linear_enc_lemmas_global_13.smt2                      |   0.065s  |   0.065s  |   0.000s  | 0.0%|
|ball_count_2d_hill_simple.10.seq_lazy_linear_enc_lemmas_global_9.smt2                       |   0.086s  |   0.086s  |   0.000s  | 0.0%|
|ball_count_2d_plain.01.qfree_global_3.smt2                                                  |   0.084s  |   0.084s  |   0.000s  | 0.0%|
|ball_count_2d_plain.01.redlog_global_11.smt2                                                |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|ball_count_2d_plain.01.redlog_global_7.smt2                                                 |   0.064s  |   0.064s  |   0.000s  | 0.0%|
|ball_count_2d_plain.01.seq_lazy_global_15.smt2                                              |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|ball_count_2d_plain.01.seq_lazy_lemmas_global_1.smt2                                        |   0.088s  |   0.088s  |   0.000s  | 0.0%|
|ball_count_2d_plain.01.seq_lazy_lemmas_global_5.smt2                                        |   0.069s  |   0.069s  |   0.000s  | 0.0%|
|ball_count_2d_plain.01.seq_lazy_linear_enc_global_13.smt2                                   |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|ball_count_2d_plain.01.seq_lazy_linear_enc_global_9.smt2                                    |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|ball_count_2d_plain.01.seq_lazy_linear_enc_lemmas_global_3.smt2                             |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|ball_count_2d_plain.02.qfree_global_11.smt2                                                 |   0.101s  |   0.101s  |   0.000s  | 0.0%|
|ball_count_2d_plain.02.qfree_global_7.smt2                                                  |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|ball_count_2d_plain.02.redlog_global_15.smt2                                                |   0.065s  |   0.065s  |   0.000s  | 0.0%|
|ball_count_2d_plain.02.seq_lazy_global_1.smt2                                               |   0.087s  |   0.087s  |   0.000s  | 0.0%|
|ball_count_2d_plain.02.seq_lazy_global_5.smt2                                               |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|ball_count_2d_plain.02.seq_lazy_lemmas_global_13.smt2                                       |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|ball_count_2d_plain.02.seq_lazy_lemmas_global_9.smt2                                        |   0.064s  |   0.064s  |   0.000s  | 0.0%|
|ball_count_2d_plain.02.seq_lazy_linear_enc_global_3.smt2                                    |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|ball_count_2d_plain.02.seq_lazy_linear_enc_lemmas_global_11.smt2                            |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|ball_count_2d_plain.02.seq_lazy_linear_enc_lemmas_global_7.smt2                             |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|ball_count_2d_plain.03.qfree_global_15.smt2                                                 |   0.086s  |   0.086s  |   0.000s  | 0.0%|
|ball_count_2d_plain.03.redlog_global_1.smt2                                                 |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|ball_count_2d_plain.03.redlog_global_5.smt2                                                 |   0.064s  |   0.064s  |   0.000s  | 0.0%|
|ball_count_2d_plain.03.seq_lazy_global_13.smt2                                              |   0.065s  |   0.065s  |   0.000s  | 0.0%|
|ball_count_2d_plain.03.seq_lazy_global_9.smt2                                               |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|ball_count_2d_plain.03.seq_lazy_lemmas_global_3.smt2                                        |   0.065s  |   0.065s  |   0.000s  | 0.0%|
|ball_count_2d_plain.03.seq_lazy_linear_enc_global_11.smt2                                   |   0.122s  |   0.122s  |   0.000s  | 0.0%|
|ball_count_2d_plain.03.seq_lazy_linear_enc_global_7.smt2                                    |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|ball_count_2d_plain.03.seq_lazy_linear_enc_lemmas_global_15.smt2                            |   0.145s  |   0.145s  |   0.000s  | 0.0%|
|ball_count_2d_plain.04.qfree_global_1.smt2                                                  |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|ball_count_2d_plain.04.qfree_global_5.smt2                                                  |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|ball_count_2d_plain.04.redlog_global_13.smt2                                                |   0.118s  |   0.118s  |   0.000s  | 0.0%|
|ball_count_2d_plain.04.redlog_global_9.smt2                                                 |   0.170s  |   0.170s  |   0.000s  | 0.0%|
|ball_count_2d_plain.04.seq_lazy_global_3.smt2                                               |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|ball_count_2d_plain.04.seq_lazy_lemmas_global_11.smt2                                       |   0.062s  |   0.062s  |   0.000s  | 0.0%|
|ball_count_2d_plain.04.seq_lazy_lemmas_global_7.smt2                                        |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|ball_count_2d_plain.04.seq_lazy_linear_enc_global_15.smt2                                   |   0.061s  |   0.061s  |   0.000s  | 0.0%|
|ball_count_2d_plain.04.seq_lazy_linear_enc_lemmas_global_1.smt2                             |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|ball_count_2d_plain.04.seq_lazy_linear_enc_lemmas_global_5.smt2                             |   0.136s  |   0.136s  |   0.000s  | 0.0%|
|ball_count_2d_plain.05.qfree_global_13.smt2                                                 |   0.079s  |   0.079s  |   0.000s  | 0.0%|
|ball_count_2d_plain.05.qfree_global_9.smt2                                                  |   0.061s  |   0.061s  |   0.000s  | 0.0%|
|ball_count_2d_plain.05.redlog_global_3.smt2                                                 |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|ball_count_2d_plain.05.seq_lazy_global_11.smt2                                              |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|ball_count_2d_plain.05.seq_lazy_global_7.smt2                                               |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|ball_count_2d_plain.05.seq_lazy_lemmas_global_15.smt2                                       |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|ball_count_2d_plain.05.seq_lazy_linear_enc_global_1.smt2                                    |   0.024s  |   0.024s  |   0.000s  | 0.0%|
|ball_count_2d_plain.05.seq_lazy_linear_enc_global_5.smt2                                    |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|ball_count_2d_plain.05.seq_lazy_linear_enc_lemmas_global_13.smt2                            |   0.078s  |   0.078s  |   0.000s  | 0.0%|
|ball_count_2d_plain.05.seq_lazy_linear_enc_lemmas_global_9.smt2                             |   0.100s  |   0.100s  |   0.000s  | 0.0%|
|ball_count_2d_plain.10.qfree_global_3.smt2                                                  |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|ball_count_2d_plain.10.redlog_global_11.smt2                                                |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|ball_count_2d_plain.10.redlog_global_7.smt2                                                 |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|ball_count_2d_plain.10.seq_lazy_global_15.smt2                                              |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|ball_count_2d_plain.10.seq_lazy_lemmas_global_1.smt2                                        |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|ball_count_2d_plain.10.seq_lazy_lemmas_global_5.smt2                                        |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|ball_count_2d_plain.10.seq_lazy_linear_enc_global_13.smt2                                   |   0.065s  |   0.065s  |   0.000s  | 0.0%|
|ball_count_2d_plain.10.seq_lazy_linear_enc_global_9.smt2                                    |   0.041s  |   0.041s  |   0.000s  | 0.0%|
|ball_count_2d_plain.10.seq_lazy_linear_enc_lemmas_global_3.smt2                             |   0.090s  |   0.090s  |   0.000s  | 0.0%|
|ball_count_2d_slope.01.seq_lazy_global_11.smt2                                              |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|ball_count_2d_slope.01.seq_lazy_global_7.smt2                                               |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|ball_count_2d_slope.01.seq_lazy_lemmas_global_15.smt2                                       |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|ball_count_2d_slope.01.seq_lazy_linear_enc_global_1.smt2                                    |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|ball_count_2d_slope.01.seq_lazy_linear_enc_global_5.smt2                                    |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|ball_count_2d_slope.01.seq_lazy_linear_enc_lemmas_global_13.smt2                            |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|ball_count_2d_slope.01.seq_lazy_linear_enc_lemmas_global_9.smt2                             |   0.110s  |   0.110s  |   0.000s  | 0.0%|
|ball_count_2d_slope.02.seq_lazy_global_3.smt2                                               |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|ball_count_2d_slope.02.seq_lazy_lemmas_global_11.smt2                                       |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|ball_count_2d_slope.02.seq_lazy_lemmas_global_7.smt2                                        |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|ball_count_2d_slope.02.seq_lazy_linear_enc_global_15.smt2                                   |   0.066s  |   0.066s  |   0.000s  | 0.0%|
|ball_count_2d_slope.02.seq_lazy_linear_enc_lemmas_global_1.smt2                             |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|ball_count_2d_slope.02.seq_lazy_linear_enc_lemmas_global_5.smt2                             |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|ball_count_2d_slope.03.seq_lazy_global_13.smt2                                              |  14.062s  |  14.062s  |   0.000s  | 0.0%|
|ball_count_2d_slope.03.seq_lazy_global_9.smt2                                               |   1.002s  |   1.002s  |   0.000s  | 0.0%|
|ball_count_2d_slope.03.seq_lazy_lemmas_global_3.smt2                                        |   0.099s  |   0.099s  |   0.000s  | 0.0%|
|ball_count_2d_slope.03.seq_lazy_linear_enc_global_11.smt2                                   |   2.622s  |   2.622s  |   0.000s  | 0.0%|
|ball_count_2d_slope.03.seq_lazy_linear_enc_global_7.smt2                                    |   0.242s  |   0.242s  |   0.000s  | 0.0%|
|ball_count_2d_slope.03.seq_lazy_linear_enc_lemmas_global_15.smt2                            |   0.098s  |   0.098s  |   0.000s  | 0.0%|
|ball_count_2d_slope.04.seq_lazy_global_1.smt2                                               |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|ball_count_2d_slope.04.seq_lazy_global_5.smt2                                               |   0.090s  |   0.090s  |   0.000s  | 0.0%|
|ball_count_2d_slope.04.seq_lazy_lemmas_global_13.smt2                                       |  14.083s  |  14.083s  |   0.000s  | 0.0%|
|ball_count_2d_slope.04.seq_lazy_lemmas_global_9.smt2                                        |   2.470s  |   2.470s  |   0.000s  | 0.0%|
|ball_count_2d_slope.04.seq_lazy_linear_enc_global_3.smt2                                    |   0.075s  |   0.075s  |   0.000s  | 0.0%|
|ball_count_2d_slope.04.seq_lazy_linear_enc_lemmas_global_11.smt2                            |   0.064s  |   0.064s  |   0.000s  | 0.0%|
|ball_count_2d_slope.04.seq_lazy_linear_enc_lemmas_global_7.smt2                             |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|ball_count_2d_slope.05.seq_lazy_global_15.smt2                                              |  10.071s  |  10.071s  |   0.000s  | 0.0%|
|ball_count_2d_slope.05.seq_lazy_lemmas_global_1.smt2                                        |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|ball_count_2d_slope.05.seq_lazy_lemmas_global_5.smt2                                        |   0.269s  |   0.269s  |   0.000s  | 0.0%|
|ball_count_2d_slope.05.seq_lazy_linear_enc_global_13.smt2                                   |  14.060s  |  14.060s  |   0.000s  | 0.0%|
|ball_count_2d_slope.05.seq_lazy_linear_enc_global_9.smt2                                    |   0.734s  |   0.734s  |   0.000s  | 0.0%|
|ball_count_2d_slope.05.seq_lazy_linear_enc_lemmas_global_3.smt2                             |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|ball_count_2d_slope.10.seq_lazy_global_11.smt2                                              |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|ball_count_2d_slope.10.seq_lazy_global_7.smt2                                               |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|ball_count_2d_slope.10.seq_lazy_lemmas_global_15.smt2                                       |   0.083s  |   0.083s  |   0.000s  | 0.0%|
|ball_count_2d_slope.10.seq_lazy_linear_enc_global_1.smt2                                    |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|ball_count_2d_slope.10.seq_lazy_linear_enc_global_5.smt2                                    |   0.094s  |   0.094s  |   0.000s  | 0.0%|
|ball_count_2d_slope.10.seq_lazy_linear_enc_lemmas_global_13.smt2                            |   0.084s  |   0.084s  |   0.000s  | 0.0%|
|ball_count_2d_slope.10.seq_lazy_linear_enc_lemmas_global_9.smt2                             |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|bf10.t2.c_Iteration1_Loop_4-pieceTemplate.smt2                                              |   0.617s  |   0.617s  |   0.000s  | 0.0%|
|bottom-plate-mixer-chunk-0039.smt2                                                          |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|bottom-plate-mixer-chunk-0050.smt2                                                          |   0.105s  |   0.105s  |   0.000s  | 0.0%|
|brp_withassume.t2.c_Iteration1_Loop_4-pieceTemplate.smt2                                    | 200.113s  | 200.113s  |   0.000s  | 0.0%|
|byron-1.t2.c_Iteration1_Loop_3-pieceTemplate.smt2                                           |  32.862s  |  32.862s  |   0.000s  | 0.0%|
|cbrt-problem-3-chunk-0028.smt2                                                              |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|cbrt-problem-3-chunk-0055.smt2                                                              |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|cbrt-problem-3-chunk-0070.smt2                                                              |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|cbrt-problem-3-weak-chunk-0023.smt2                                                         |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|cbrt-problem-3-weak-chunk-0040.smt2                                                         |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|cbrt-problem-3-weak-chunk-0069.smt2                                                         |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|cbrt-problem-3-weak-chunk-0084.smt2                                                         |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|cbrt-problem-3-weak-chunk-0094.smt2                                                         |   0.076s  |   0.076s  |   0.000s  | 0.0%|
|cbrt-problem-3-weak-chunk-0108.smt2                                                         |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|collatz.t2.c_Iteration3_Lasso_6-phaseTemplate.smt2                                          |  56.804s  |  56.804s  |   0.000s  | 0.0%|
|cos-3410-b-chunk-0015.smt2                                                                  |   0.114s  |   0.114s  |   0.000s  | 0.0%|
|cos-3410-b-chunk-0027.smt2                                                                  |   0.059s  |   0.059s  |   0.000s  | 0.0%|
|cos-problem-5-chunk-0023.smt2                                                               |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|cos-problem-5-chunk-0039.smt2                                                               |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|db3.t2.c_Iteration2_Loop_4-pieceTemplate.smt2                                               |  15.451s  |  15.451s  |   0.000s  | 0.0%|
|efegp.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2                                            | 200.077s  | 200.077s  |   0.000s  | 0.0%|
|eric.t2.c_Iteration1_Lasso_5-phaseTemplate.smt2                                             |   1.806s  |   1.806s  |   0.000s  | 0.0%|
|eric2.t2.c_Iteration1_Loop_4-pieceTemplate.smt2                                             |  52.327s  |  52.327s  |   0.000s  | 0.0%|
|eric2.t2.c_Iteration7_Loop_4-pieceTemplate.smt2                                             |  66.746s  |  66.746s  |   0.000s  | 0.0%|
|etcs_braking_2.01.qfree_global_3.smt2                                                       |   0.073s  |   0.073s  |   0.000s  | 0.0%|
|etcs_braking_2.01.redlog_global_11.smt2                                                     |  50.268s  |  50.268s  |   0.000s  | 0.0%|
|etcs_braking_2.01.redlog_global_7.smt2                                                      |  50.386s  |  50.386s  |   0.000s  | 0.0%|
|etcs_braking_2.01.seq_lazy_global_15.smt2                                                   |  14.356s  |  14.356s  |   0.000s  | 0.0%|
|etcs_braking_2.01.seq_lazy_lemmas_global_1.smt2                                             |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|etcs_braking_2.01.seq_lazy_lemmas_global_5.smt2                                             |   0.211s  |   0.211s  |   0.000s  | 0.0%|
|etcs_braking_2.01.seq_lazy_linear_enc_global_13.smt2                                        | 200.037s  | 200.037s  |   0.000s  | 0.0%|
|etcs_braking_2.01.seq_lazy_linear_enc_global_9.smt2                                         |   0.463s  |   0.463s  |   0.000s  | 0.0%|
|etcs_braking_2.01.seq_lazy_linear_enc_lemmas_global_3.smt2                                  |   0.100s  |   0.100s  |   0.000s  | 0.0%|
|ex11.t2.c_Iteration1_Lasso_5-phaseTemplate.smt2                                             |   1.149s  |   1.149s  |   0.000s  | 0.0%|
|ex4.t2.c_Iteration2_Loop_3-pieceTemplate.smt2                                               |  14.249s  |  14.249s  |   0.000s  | 0.0%|
|exp-361-neg-6-e-chunk-0216.smt2                                                             |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0016.smt2                                                            |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0028.smt2                                                            |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0038.smt2                                                            |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0048.smt2                                                            |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0059.smt2                                                            |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0069.smt2                                                            |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0079.smt2                                                            |   0.026s  |   0.026s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0090.smt2                                                            |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0102.smt2                                                            |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0112.smt2                                                            |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0124.smt2                                                            |   0.087s  |   0.087s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0134.smt2                                                            |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0144.smt2                                                            |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0154.smt2                                                            |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0164.smt2                                                            |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0174.smt2                                                            |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0184.smt2                                                            |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0194.smt2                                                            |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0204.smt2                                                            |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0214.smt2                                                            |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0224.smt2                                                            |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0234.smt2                                                            |   0.071s  |   0.071s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0245.smt2                                                            |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0255.smt2                                                            |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0265.smt2                                                            |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0275.smt2                                                            |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0285.smt2                                                            |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0295.smt2                                                            |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0305.smt2                                                            |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0315.smt2                                                            |   1.248s  |   1.248s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0325.smt2                                                            |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0335.smt2                                                            |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0346.smt2                                                            |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0358.smt2                                                            |   0.069s  |   0.069s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0375.smt2                                                            |   0.078s  |   0.078s  |   0.000s  | 0.0%|
|exp-problem-10-2-chunk-0385.smt2                                                            |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0010.smt2                                                            |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0021.smt2                                                            |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0032.smt2                                                            |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0042.smt2                                                            |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0052.smt2                                                            |   0.090s  |   0.090s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0063.smt2                                                            |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0073.smt2                                                            |   0.095s  |   0.095s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0084.smt2                                                            |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0096.smt2                                                            |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0106.smt2                                                            |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0118.smt2                                                            |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0128.smt2                                                            |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0138.smt2                                                            |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0148.smt2                                                            |   0.059s  |   0.059s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0158.smt2                                                            |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0168.smt2                                                            |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0178.smt2                                                            |   0.090s  |   0.090s  |   0.000s  | 0.0%|
|exp-problem-10-3-chunk-0188.smt2                                                            |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0015.smt2                                                       |   0.070s  |   0.070s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0025.smt2                                                       |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0035.smt2                                                       |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0048.smt2                                                       |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0059.smt2                                                       |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0070.smt2                                                       |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0080.smt2                                                       |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0091.smt2                                                       |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0101.smt2                                                       |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0111.smt2                                                       |   0.041s  |   0.041s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0121.smt2                                                       |   0.065s  |   0.065s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0131.smt2                                                       |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0141.smt2                                                       |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0151.smt2                                                       |   0.121s  |   0.121s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0161.smt2                                                       |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0171.smt2                                                       |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0181.smt2                                                       |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0191.smt2                                                       |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0202.smt2                                                       |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0218.smt2                                                       |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|exp-problem-10-3-weak-chunk-0230.smt2                                                       |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|firewire.t2.c_Iteration1_Lasso_7-nestedTemplate.smt2                                        |  87.065s  |  87.065s  |   0.000s  | 0.0%|
|fragtest_simple.i_4_5_4.bpl_3.smt2                                                          | 200.013s  | 200.013s  |   0.000s  | 0.0%|
|fuhs-inflasso.t2.c_Iteration2_Loop_4-pieceTemplate.smt2                                     |  26.219s  |  26.219s  |   0.000s  | 0.0%|
|fun9.t2.c_Iteration1_Loop_4-pieceTemplate.smt2                                              |  19.123s  |  19.123s  |   0.000s  | 0.0%|
|gen-09.smt2                                                                                 |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|heidy7-simple.t2.c_Iteration2_Lasso_4-pieceTemplate.smt2                                    | 200.064s  | 200.064s  |   0.000s  | 0.0%|
|hong_10.smt2                                                                                |  49.782s  |  49.782s  |   0.000s  | 0.0%|
|hong_2.smt2                                                                                 |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|iecs.t2.c_Iteration1_Loop_4-pieceTemplate.smt2                                              |  52.152s  |  52.152s  |   0.000s  | 0.0%|
|joey_false-termination.c_Iteration2_Loop_6-phaseTemplate.smt2                               |   3.576s  |   3.576s  |   0.000s  | 0.0%|
|kissing_3_11.smt2                                                                           | 200.043s  | 200.043s  |   0.000s  | 0.0%|
|kissing_3_9.smt2                                                                            | 200.028s  | 200.028s  |   0.000s  | 0.0%|
|kissing_4_18.smt2                                                                           | 200.013s  | 200.013s  |   0.000s  | 0.0%|
|kissing_4_4.smt2                                                                            |  50.718s  |  50.718s  |   0.000s  | 0.0%|
|linear_search.i_7_19_3.bpl_3.smt2                                                           | 200.017s  | 200.017s  |   0.000s  | 0.0%|
|log-fun-ineq-g-chunk-0036.smt2                                                              |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|loop_on_input.t2.c_Iteration1_Loop_4-pieceTemplate.smt2                                     |  15.775s  |  15.775s  |   0.000s  | 0.0%|
|matrix-1-all-10.smt2                                                                        |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|matrix-1-all-2.smt2                                                                         |   0.096s  |   0.096s  |   0.000s  | 0.0%|
|matrix-1-all-29.smt2                                                                        |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|matrix-1-all-38.smt2                                                                        |   0.595s  |   0.595s  |   0.000s  | 0.0%|
|matrix-1-all-47.smt2                                                                        |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|matrix-1-all-8.smt2                                                                         |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|matrix-2-all-17.smt2                                                                        | 200.033s  | 200.033s  |   0.000s  | 0.0%|
|matrix-2-all-4.smt2                                                                         |  14.421s  |  14.421s  |   0.000s  | 0.0%|
|matrix-3-all-13.smt2                                                                        | 200.022s  | 200.022s  |   0.000s  | 0.0%|
|matrix-3-all-4.smt2                                                                         |  32.586s  |  32.586s  |   0.000s  | 0.0%|
|matrix-4-all-13.smt2                                                                        | 200.052s  | 200.052s  |   0.000s  | 0.0%|
|matrix-4-all-22.smt2                                                                        | 200.014s  | 200.014s  |   0.000s  | 0.0%|
|matrix-4-all-4.smt2                                                                         | 200.036s  | 200.036s  |   0.000s  | 0.0%|
|matrix-5-all-13.smt2                                                                        |  94.639s  |  94.639s  |   0.000s  | 0.0%|
|matrix-5-all-23.smt2                                                                        |   0.070s  |   0.070s  |   0.000s  | 0.0%|
|mbo_E10E18.smt2                                                                             |  56.423s  |  56.423s  |   0.000s  | 0.0%|
|mbo_E10E28.smt2                                                                             | 200.030s  | 200.030s  |   0.000s  | 0.0%|
|mbo_E11E20.smt2                                                                             |  97.362s  |  97.362s  |   0.000s  | 0.0%|
|mbo_E12E13.smt2                                                                             |  56.611s  |  56.611s  |   0.000s  | 0.0%|
|mbo_E12E23.smt2                                                                             |  95.958s  |  95.958s  |   0.000s  | 0.0%|
|mbo_E13E17.smt2                                                                             |  14.207s  |  14.207s  |   0.000s  | 0.0%|
|mbo_E13E27.smt2                                                                             |  55.272s  |  55.272s  |   0.000s  | 0.0%|
|mbo_E14E22.smt2                                                                             |  45.559s  |  45.559s  |   0.000s  | 0.0%|
|mbo_E15E18.smt2                                                                             |  14.607s  |  14.607s  |   0.000s  | 0.0%|
|mbo_E15E28.smt2                                                                             |  78.694s  |  78.694s  |   0.000s  | 0.0%|
|mbo_E16E25.smt2                                                                             | 200.034s  | 200.034s  |   0.000s  | 0.0%|
|mbo_E17E23.smt2                                                                             |   0.069s  |   0.069s  |   0.000s  | 0.0%|
|mbo_E18E22.smt2                                                                             |  55.694s  |  55.694s  |   0.000s  | 0.0%|
|mbo_E19E22.smt2                                                                             |  78.231s  |  78.231s  |   0.000s  | 0.0%|
|mbo_E1E13.smt2                                                                              |  61.075s  |  61.075s  |   0.000s  | 0.0%|
|mbo_E1E22.smt2                                                                              |  14.256s  |  14.256s  |   0.000s  | 0.0%|
|mbo_E1E6.smt2                                                                               |  16.569s  |  16.569s  |   0.000s  | 0.0%|
|mbo_E20E25.smt2                                                                             |  59.116s  |  59.116s  |   0.000s  | 0.0%|
|mbo_E21E27.smt2                                                                             |   0.062s  |   0.062s  |   0.000s  | 0.0%|
|mbo_E23E24.smt2                                                                             |  52.846s  |  52.846s  |   0.000s  | 0.0%|
|mbo_E25.smt2                                                                                |  50.254s  |  50.254s  |   0.000s  | 0.0%|
|mbo_E2E10.smt2                                                                              |  58.938s  |  58.938s  |   0.000s  | 0.0%|
|mbo_E2E20.smt2                                                                              | 200.042s  | 200.042s  |   0.000s  | 0.0%|
|mbo_E2E4.smt2                                                                               |  58.281s  |  58.281s  |   0.000s  | 0.0%|
|mbo_E3E13.smt2                                                                              |  60.808s  |  60.808s  |   0.000s  | 0.0%|
|mbo_E3E23.smt2                                                                              |  78.862s  |  78.862s  |   0.000s  | 0.0%|
|mbo_E3E8.smt2                                                                               |  58.959s  |  58.959s  |   0.000s  | 0.0%|
|mbo_E4E17.smt2                                                                              |  15.103s  |  15.103s  |   0.000s  | 0.0%|
|mbo_E4E27.smt2                                                                              |  53.385s  |  53.385s  |   0.000s  | 0.0%|
|mbo_E5E12.smt2                                                                              |  16.347s  |  16.347s  |   0.000s  | 0.0%|
|mbo_E5E23.smt2                                                                              |   0.109s  |   0.109s  |   0.000s  | 0.0%|
|mbo_E6.smt2                                                                                 |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|mbo_E6E19.smt2                                                                              |  60.380s  |  60.380s  |   0.000s  | 0.0%|
|mbo_E6E7.smt2                                                                               |  14.123s  |  14.123s  |   0.000s  | 0.0%|
|mbo_E7E16.smt2                                                                              |  52.925s  |  52.925s  |   0.000s  | 0.0%|
|mbo_E7E26.smt2                                                                              |  25.625s  |  25.625s  |   0.000s  | 0.0%|
|mbo_E8E14.smt2                                                                              |  98.737s  |  98.737s  |   0.000s  | 0.0%|
|mbo_E8E24.smt2                                                                              |  56.844s  |  56.844s  |   0.000s  | 0.0%|
|mbo_E9E13.smt2                                                                              |  14.318s  |  14.318s  |   0.000s  | 0.0%|
|mbo_E9E23.smt2                                                                              |  60.823s  |  60.823s  |   0.000s  | 0.0%|
|mc91test.t2.c_Iteration5_Loop_3-pieceTemplate.smt2                                          |   0.189s  |   0.189s  |   0.000s  | 0.0%|
|mgc_06.smt2                                                                                 |   0.126s  |   0.126s  |   0.000s  | 0.0%|
|min_rf_true-termination.c_Iteration1_Loop_4-pieceTemplate.smt2                              | 200.072s  | 200.072s  |   0.000s  | 0.0%|
|nested.t2.c_Iteration3_Loop_3-pieceTemplate.smt2                                            |  32.185s  |  32.185s  |   0.000s  | 0.0%|
|p-42.t2.c_Iteration2_Loop_4-pieceTemplate.smt2                                              |   0.426s  |   0.426s  |   0.000s  | 0.0%|
|p-46.t2.c_Iteration2_Lasso_7-phaseTemplate.smt2                                             | 200.084s  | 200.084s  |   0.000s  | 0.0%|
|p-55.t2.c_Iteration3_Loop_4-pieceTemplate.smt2                                              |   4.373s  |   4.373s  |   0.000s  | 0.0%|
|pentagon.t2.c_Iteration9_Loop_3-pieceTemplate.smt2                                          |   0.322s  |   0.322s  |   0.000s  | 0.0%|
|polypaver-bench-exp-3d-chunk-0028.smt2                                                      |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|polypaver-bench-exp-3d-chunk-0072.smt2                                                      |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|polypaver-bench-exp-3d-chunk-0085.smt2                                                      |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|polypaver-bench-exp-3d-chunk-0109.smt2                                                      |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|polypaver-bench-exp-3d-chunk-0126.smt2                                                      |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|polypaver-bench-exp-3d-chunk-0138.smt2                                                      |   0.080s  |   0.080s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0020.smt2                                                     |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0069.smt2                                                     |   0.077s  |   0.077s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0087.smt2                                                     |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0100.smt2                                                     |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0144.smt2                                                     |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0162.smt2                                                     |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0183.smt2                                                     |   0.101s  |   0.101s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0196.smt2                                                     |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0206.smt2                                                     |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0217.smt2                                                     |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0227.smt2                                                     |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0237.smt2                                                     |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0250.smt2                                                     |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0265.smt2                                                     |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0278.smt2                                                     |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0288.smt2                                                     |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0299.smt2                                                     |   0.059s  |   0.059s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0310.smt2                                                     |   0.098s  |   0.098s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0320.smt2                                                     |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0330.smt2                                                     |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0342.smt2                                                     |   0.066s  |   0.066s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0352.smt2                                                     |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0369.smt2                                                     |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0379.smt2                                                     |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0390.smt2                                                     |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0405.smt2                                                     |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0415.smt2                                                     |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0425.smt2                                                     |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0435.smt2                                                     |   0.072s  |   0.072s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0446.smt2                                                     |   0.090s  |   0.090s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0456.smt2                                                     |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0469.smt2                                                     |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0481.smt2                                                     |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0493.smt2                                                     |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0504.smt2                                                     |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|polypaver-bench-sqrt-3d-chunk-0515.smt2                                                     |   0.087s  |   0.087s  |   0.000s  | 0.0%|
|polypaver-sqrt-circles-1a-chunk-0011.smt2                                                   |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|polypaver-sqrt43-int-3vars-chunk-0029.smt2                                                  |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|polypaver-sqrt43-int-3vars-chunk-0043.smt2                                                  |   0.103s  |   0.103s  |   0.000s  | 0.0%|
|polypaver-sqrt43-int-3vars-chunk-0075.smt2                                                  |   0.099s  |   0.099s  |   0.000s  | 0.0%|
|polypaver-sqrt43-int-3vars-chunk-0086.smt2                                                  |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|polypaver-sqrt43-int-3vars-chunk-0103.smt2                                                  |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|polypaver-sqrt43-int-3vars-chunk-0121.smt2                                                  |   0.077s  |   0.077s  |   0.000s  | 0.0%|
|polypaver-sqrt43-int-4vars-chunk-0026.smt2                                                  |   0.064s  |   0.064s  |   0.000s  | 0.0%|
|polypaver-sqrt43-int-chunk-0053.smt2                                                        |   0.080s  |   0.080s  |   0.000s  | 0.0%|
|polyrank3.t2.c_Iteration2_Loop_3-pieceTemplate.smt2                                         |  28.618s  |  28.618s  |   0.000s  | 0.0%|
|polyrank3.t2.c_Iteration8_Loop_4-pieceTemplate.smt2                                         |  55.861s  |  55.861s  |   0.000s  | 0.0%|
|polyrank4.t2.c_Iteration3_Loop_3-pieceTemplate.smt2                                         |  51.819s  |  51.819s  |   0.000s  | 0.0%|
|polyrank4.t2.c_Iteration8_Loop_2-pieceTemplate.smt2                                         |  50.450s  |  50.450s  |   0.000s  | 0.0%|
|polyrank5.t2.c_Iteration1_Loop_7-phaseTemplate.smt2                                         |  16.904s  |  16.904s  |   0.000s  | 0.0%|
|qrdcmp.t2.c_Iteration6_Loop_3-pieceTemplate.smt2                                            |   0.269s  |   0.269s  |   0.000s  | 0.0%|
|sas2.t2.c_Iteration1_Lasso_4-pieceTemplate.smt2                                             | 124.493s  | 124.493s  |   0.000s  | 0.0%|
|sas2.t2.c_Iteration6_Lasso_7-nestedTemplate.smt2                                            |  56.823s  |  56.823s  |   0.000s  | 0.0%|
|selectSort.t2.c_Iteration3_Loop_4-pieceTemplate.smt2                                        |  14.600s  |  14.600s  |   0.000s  | 0.0%|
|seq.i_5_5_5.bpl_3.smt2                                                                      | 200.013s  | 200.013s  |   0.000s  | 0.0%|
|simple-scaled200.bpl_Iteration1_Lasso_7-phaseTemplate.smt2                                  |  46.033s  |  46.033s  |   0.000s  | 0.0%|
|simple_ballistics_reach.01.seq_lazy_global_11.smt2                                          | 200.023s  | 200.023s  |   0.000s  | 0.0%|
|simple_ballistics_reach.01.seq_lazy_global_7.smt2                                           | 200.010s  | 200.010s  |   0.000s  | 0.0%|
|simple_ballistics_reach.01.seq_lazy_lemmas_global_15.smt2                                   | 200.013s  | 200.013s  |   0.000s  | 0.0%|
|simple_ballistics_reach.01.seq_lazy_linear_enc_global_1.smt2                                |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|simple_ballistics_reach.01.seq_lazy_linear_enc_global_5.smt2                                | 200.039s  | 200.039s  |   0.000s  | 0.0%|
|simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_13.smt2                        | 200.035s  | 200.035s  |   0.000s  | 0.0%|
|simple_ballistics_reach.01.seq_lazy_linear_enc_lemmas_global_9.smt2                         | 200.048s  | 200.048s  |   0.000s  | 0.0%|
|sin-344-3-chunk-0029.smt2                                                                   |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|sin-344-3-chunk-0046.smt2                                                                   |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|sin-344-3-chunk-0058.smt2                                                                   |   0.072s  |   0.072s  |   0.000s  | 0.0%|
|sin-344-3-weak-chunk-0017.smt2                                                              |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|sin-344-3-weak-chunk-0044.smt2                                                              |   0.092s  |   0.092s  |   0.000s  | 0.0%|
|sin-344-4-chunk-0032.smt2                                                                   |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|sin-344-4-chunk-0050.smt2                                                                   |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0018.smt2                                                               |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0030.smt2                                                               |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0044.smt2                                                               |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0054.smt2                                                               |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0068.smt2                                                               |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0078.smt2                                                               |   0.028s  |   0.028s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0092.smt2                                                               |   0.026s  |   0.026s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0102.smt2                                                               |   0.027s  |   0.027s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0114.smt2                                                               |   0.083s  |   0.083s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0126.smt2                                                               |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0139.smt2                                                               |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0158.smt2                                                               |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0168.smt2                                                               |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0186.smt2                                                               |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0198.smt2                                                               |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0209.smt2                                                               |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0221.smt2                                                               |   0.025s  |   0.025s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0232.smt2                                                               |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0242.smt2                                                               |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0252.smt2                                                               |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0262.smt2                                                               |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0272.smt2                                                               |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0285.smt2                                                               |   0.103s  |   0.103s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0296.smt2                                                               |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0306.smt2                                                               |   0.041s  |   0.041s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0316.smt2                                                               |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0326.smt2                                                               |   0.056s  |   0.056s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0338.smt2                                                               |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0348.smt2                                                               |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0358.smt2                                                               |   0.070s  |   0.070s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0368.smt2                                                               |   0.075s  |   0.075s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0378.smt2                                                               |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0391.smt2                                                               |   0.080s  |   0.080s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0401.smt2                                                               |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0414.smt2                                                               |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0424.smt2                                                               |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0434.smt2                                                               |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0444.smt2                                                               |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0454.smt2                                                               |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0464.smt2                                                               |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0474.smt2                                                               |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0484.smt2                                                               |   0.055s  |   0.055s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0494.smt2                                                               |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0504.smt2                                                               |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0514.smt2                                                               |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0524.smt2                                                               |   0.085s  |   0.085s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0536.smt2                                                               |   0.059s  |   0.059s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0549.smt2                                                               |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0560.smt2                                                               |   0.094s  |   0.094s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0572.smt2                                                               |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0584.smt2                                                               |   0.102s  |   0.102s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0597.smt2                                                               |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0607.smt2                                                               |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0620.smt2                                                               |   0.087s  |   0.087s  |   0.000s  | 0.0%|
|sin-cos-346-b-chunk-0631.smt2                                                               |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|sin-problem-10-2-chunk-0010.smt2                                                            |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|sin-problem-10-2-chunk-0024.smt2                                                            |   0.025s  |   0.025s  |   0.000s  | 0.0%|
|sin-problem-10-2-chunk-0034.smt2                                                            |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|sin-problem-10-3-chunk-0023.smt2                                                            |   0.061s  |   0.061s  |   0.000s  | 0.0%|
|sin-problem-10-3-chunk-0033.smt2                                                            |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0054.smt2                                                               |   0.070s  |   0.070s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0079.smt2                                                               |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0091.smt2                                                               |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0105.smt2                                                               |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0117.smt2                                                               |   0.086s  |   0.086s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0129.smt2                                                               |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0143.smt2                                                               |   0.039s  |   0.039s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0156.smt2                                                               |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0172.smt2                                                               |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0182.smt2                                                               |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0192.smt2                                                               |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0208.smt2                                                               |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0221.smt2                                                               |   0.038s  |   0.038s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0233.smt2                                                               |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0247.smt2                                                               |   0.081s  |   0.081s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0257.smt2                                                               |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0273.smt2                                                               |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0283.smt2                                                               |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0297.smt2                                                               | 200.022s  | 200.022s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0311.smt2                                                               |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0322.smt2                                                               |   0.093s  |   0.093s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0335.smt2                                                               |   0.074s  |   0.074s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0348.smt2                                                               |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|sin-problem-7-chunk-0361.smt2                                                               |   0.027s  |   0.027s  |   0.000s  | 0.0%|
|sin-problem-7-weak-chunk-0073.smt2                                                          |   0.041s  |   0.041s  |   0.000s  | 0.0%|
|sin-problem-7-weak-chunk-0085.smt2                                                          |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|sin-problem-7-weak-chunk-0101.smt2                                                          |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|sin-problem-7-weak-chunk-0115.smt2                                                          |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|sin-problem-7-weak-chunk-0126.smt2                                                          |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|sin-problem-7-weak-chunk-0138.smt2                                                          |   0.059s  |   0.059s  |   0.000s  | 0.0%|
|sin-problem-7-weak-chunk-0149.smt2                                                          |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|sin-problem-7-weak-chunk-0160.smt2                                                          |   0.072s  |   0.072s  |   0.000s  | 0.0%|
|sin-problem-7-weak-chunk-0171.smt2                                                          |   0.073s  |   0.073s  |   0.000s  | 0.0%|
|sin-problem-7-weak-chunk-0181.smt2                                                          |   3.687s  |   3.687s  |   0.000s  | 0.0%|
|sin-problem-7-weak2-chunk-0044.smt2                                                         |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|sin-problem-7-weak2-chunk-0057.smt2                                                         |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|sin-problem-7-weak2-chunk-0075.smt2                                                         |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|sin-problem-7-weak2-chunk-0088.smt2                                                         |   0.060s  |   0.060s  |   0.000s  | 0.0%|
|sin-problem-7-weak2-chunk-0100.smt2                                                         |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|sin-problem-7-weak2-chunk-0113.smt2                                                         |   2.960s  |   2.960s  |   0.000s  | 0.0%|
|sin-problem-7-weak2-chunk-0123.smt2                                                         |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|sin-problem-8-chunk-0026.smt2                                                               |   0.061s  |   0.061s  |   0.000s  | 0.0%|
|sin-problem-8-chunk-0043.smt2                                                               |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|sin-problem-8-chunk-0054.smt2                                                               |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|sin-problem-8-chunk-0067.smt2                                                               |   0.102s  |   0.102s  |   0.000s  | 0.0%|
|sin-problem-8-weak-chunk-0027.smt2                                                          |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|sin-problem-8-weak-chunk-0044.smt2                                                          |   0.095s  |   0.095s  |   0.000s  | 0.0%|
|sin-problem-8-weak-chunk-0056.smt2                                                          |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|sin-problem-8-weak-chunk-0068.smt2                                                          |   0.042s  |   0.042s  |   0.000s  | 0.0%|
|sin-problem-8-weak-chunk-0079.smt2                                                          |   0.156s  |   0.156s  |   0.000s  | 0.0%|
|sort.t2.c_Iteration5_Loop_3-pieceTemplate.smt2                                              |   0.439s  |   0.439s  |   0.000s  | 0.0%|
|spiral.t2.c_Iteration8_Loop_4-pieceTemplate.smt2                                            |   0.484s  |   0.484s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0027.smt2                                                               |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0039.smt2                                                               |   0.063s  |   0.063s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0053.smt2                                                               |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0077.smt2                                                               |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0093.smt2                                                               |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0116.smt2                                                               |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0130.smt2                                                               |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0143.smt2                                                               |   0.041s  |   0.041s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0155.smt2                                                               |   0.060s  |   0.060s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0167.smt2                                                               |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0177.smt2                                                               |   0.109s  |   0.109s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0191.smt2                                                               |   0.080s  |   0.080s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0206.smt2                                                               |   0.061s  |   0.061s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0216.smt2                                                               |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|sqrt-1mcosq-7-chunk-0230.smt2                                                               |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0026.smt2                                                               |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0043.smt2                                                               |   0.052s  |   0.052s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0054.smt2                                                               |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0064.smt2                                                               |   0.074s  |   0.074s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0075.smt2                                                               |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0085.smt2                                                               |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0100.smt2                                                               |   0.040s  |   0.040s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0110.smt2                                                               |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0121.smt2                                                               |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0132.smt2                                                               |   0.064s  |   0.064s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0142.smt2                                                               |   0.084s  |   0.084s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0155.smt2                                                               |   0.049s  |   0.049s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0166.smt2                                                               |   0.071s  |   0.071s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0176.smt2                                                               | 128.851s  | 128.851s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0189.smt2                                                               |   0.051s  |   0.051s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0199.smt2                                                               |   0.069s  |   0.069s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0209.smt2                                                               |   0.127s  |   0.127s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0223.smt2                                                               |   0.048s  |   0.048s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0233.smt2                                                               | 200.012s  | 200.012s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0243.smt2                                                               |   0.072s  |   0.072s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0254.smt2                                                               |   0.129s  |   0.129s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0265.smt2                                                               | 120.985s  | 120.985s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0276.smt2                                                               |   0.083s  |   0.083s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0286.smt2                                                               |   0.081s  |   0.081s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0296.smt2                                                               |   0.367s  |   0.367s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0307.smt2                                                               |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0318.smt2                                                               |   0.094s  |   0.094s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0328.smt2                                                               |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0339.smt2                                                               |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0349.smt2                                                               |   0.058s  |   0.058s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0359.smt2                                                               |   0.062s  |   0.062s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0370.smt2                                                               |   0.037s  |   0.037s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0380.smt2                                                               |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0391.smt2                                                               |   0.083s  |   0.083s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0402.smt2                                                               |   0.083s  |   0.083s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0412.smt2                                                               |   0.068s  |   0.068s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0426.smt2                                                               |   0.115s  |   0.115s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0436.smt2                                                               |   0.079s  |   0.079s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0446.smt2                                                               |   0.168s  |   0.168s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0457.smt2                                                               |   0.179s  |   0.179s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0467.smt2                                                               |   0.078s  |   0.078s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0479.smt2                                                               |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0496.smt2                                                               |   0.047s  |   0.047s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0508.smt2                                                               |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0519.smt2                                                               |   0.043s  |   0.043s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0530.smt2                                                               |   0.074s  |   0.074s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0541.smt2                                                               |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0556.smt2                                                               |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0567.smt2                                                               |   0.050s  |   0.050s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0577.smt2                                                               |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0589.smt2                                                               |   0.074s  |   0.074s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0600.smt2                                                               |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0610.smt2                                                               |   0.120s  |   0.120s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0621.smt2                                                               |   0.107s  |   0.107s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0633.smt2                                                               |   0.067s  |   0.067s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0643.smt2                                                               |   0.074s  |   0.074s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0657.smt2                                                               |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0668.smt2                                                               |   0.072s  |   0.072s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0679.smt2                                                               |   0.085s  |   0.085s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0690.smt2                                                               |   0.116s  |   0.116s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0700.smt2                                                               |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0714.smt2                                                               |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|sqrt-1mcosq-8-chunk-0728.smt2                                                               |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|sqrt-circles-2-chunk-0002.smt2                                                              |   0.070s  |   0.070s  |   0.000s  | 0.0%|
|sqrt-circles-2-chunk-0015.smt2                                                              |   0.104s  |   0.104s  |   0.000s  | 0.0%|
|sqrt-circles-3-chunk-0016.smt2                                                              |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|sqrt-problem-12vars3-chunk-0010.smt2                                                        |   0.046s  |   0.046s  |   0.000s  | 0.0%|
|sqrt-problem-12vars3-chunk-0025.smt2                                                        |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|sqrt-problem-12vars3-chunk-0039.smt2                                                        |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|sqrt-problem-12vars3-chunk-0055.smt2                                                        |   0.060s  |   0.060s  |   0.000s  | 0.0%|
|sqrt-problem-12vars3-chunk-0068.smt2                                                        |   0.033s  |   0.033s  |   0.000s  | 0.0%|
|sqrt-problem-12vars3-chunk-0081.smt2                                                        |   0.036s  |   0.036s  |   0.000s  | 0.0%|
|sqrt-problem-12vars3-chunk-0097.smt2                                                        |   0.057s  |   0.057s  |   0.000s  | 0.0%|
|sqrt-problem-13-chunk-0019.smt2                                                             |   0.030s  |   0.030s  |   0.000s  | 0.0%|
|sqrt-problem-13-sqrt1-chunk-0015.smt2                                                       |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|sqrt-problem-13-sqrt1-chunk-0034.smt2                                                       |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|sqrt-problem-13-sqrt1-chunk-0049.smt2                                                       |   0.029s  |   0.029s  |   0.000s  | 0.0%|
|sqrt-problem-13-sqrt1-chunk-0062.smt2                                                       |   0.079s  |   0.079s  |   0.000s  | 0.0%|
|sqrt-problem-13-sqrt1-chunk-0080.smt2                                                       |   0.064s  |   0.064s  |   0.000s  | 0.0%|
|sqrt-problem-13-vars5-chunk-0026.smt2                                                       |   0.032s  |   0.032s  |   0.000s  | 0.0%|
|sqrt-problem-Melquiond2-chunk-0010.smt2                                                     |   0.069s  |   0.069s  |   0.000s  | 0.0%|
|sqrt-problem-Melquiond2-chunk-0023.smt2                                                     |   0.044s  |   0.044s  |   0.000s  | 0.0%|
|sqrt-problem-Melquiond2-chunk-0034.smt2                                                     |   0.053s  |   0.053s  |   0.000s  | 0.0%|
|sqrt-problem-Melquiond2-chunk-0045.smt2                                                     |   0.034s  |   0.034s  |   0.000s  | 0.0%|
|sqrt-problem-Melquiond2-chunk-0059.smt2                                                     |   0.045s  |   0.045s  |   0.000s  | 0.0%|
|sqrt-problem-Melquiond2-chunk-0071.smt2                                                     |   0.089s  |   0.089s  |   0.000s  | 0.0%|
|sqrt-problem-Melquiond2-chunk-0081.smt2                                                     |   0.031s  |   0.031s  |   0.000s  | 0.0%|
|sqrt-problem-Melquiond2-chunk-0091.smt2                                                     |   0.054s  |   0.054s  |   0.000s  | 0.0%|
|sqrt-problem-Melquiond3-chunk-0018.smt2                                                     |   0.035s  |   0.035s  |   0.000s  | 0.0%|
|standard_copy5_ground.i_3_2_2.bpl_3.smt2                                                    |  32.273s  |  32.273s  |   0.000s  | 0.0%|
|standard_init9_ground.i_3_2_2.bpl_1.smt2                                                    |   0.237s  |   0.237s  |   0.000s  | 0.0%|
|standard_two_index_05.i_3_2_2.bpl_5.smt2                                                    | 200.020s  | 200.020s  |   0.000s  | 0.0%|
|toeplz.c.i.toeplz.pl.t2.fixed.t2.c_Iteration10_Loop_3-pieceTemplate.smt2                    |   0.172s  |   0.172s  |   0.000s  | 0.0%|
|toeplz.t2.c_Iteration7_Loop_4-pieceTemplate.smt2                                            |   0.614s  |   0.614s  |   0.000s  | 0.0%|
|yPositive-MixedIntReal.bpl_Iteration1_Loop_3-pieceTemplate.smt2                             |  51.967s  |  51.967s  |   0.000s  | 0.0%|
</details>