# .

* SAT 543
* UNSAT 760
* TIMEOUT 0
* UNKNOWN 0

* ERRORS 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/QF_AUFLIA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-QF_AUFLIA.tar.zst-
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 4a90d3105054796562079406e125b9480ac3472b
Z3 branch: master
Z3 options: "-T:20 model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_AUFLIA.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00030_009.cvc.smt2 |    0.022s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00040_002.cvc.smt2 |    0.022s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00020_001.cvc.smt2 |    0.023s | 20.352MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00060_009.cvc.smt2 |    0.023s | 20.088MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00010_001.cvc.smt2 |    0.023s | 20.104MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00020_009.cvc.smt2 |    0.024s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00030_007.cvc.smt2 |    0.024s | 20.096MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00020_003.cvc.smt2 |    0.024s | 20.068MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00040_005.cvc.smt2 |    0.024s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00030_007.cvc.smt2 |    0.025s | 20.608MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00020_005.cvc.smt2 |    0.025s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00030_009.cvc.smt2 |    0.025s | 20.344MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00060_007.cvc.smt2 |    0.025s | 20.352MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/array_benchmarks/misc/pipeline-invalid.smt2 |    0.026s | 20.756MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5410124224885464815.smt2 |    0.026s | 19.96MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00060_003.cvc.smt2 |    0.027s | 20.084MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00010_003.cvc.smt2 |    0.028s | 19.852MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00010_009.cvc.smt2 |    0.028s | 20.192MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00040_001.cvc.smt2 |    0.028s | 20.356MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00008_005.cvc.smt2 |    0.029s | 20.092MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00010_009.cvc.smt2 |    0.029s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00020_004.cvc.smt2 |    0.029s | 20.352MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4160855460817203141.smt2 |    0.029s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6985556550088020826.smt2 |    0.029s | 19.496MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00004_003.cvc.smt2 |    0.030s | 19.904MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00004_007.cvc.smt2 |    0.030s | 19.9MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00050_004.cvc.smt2 |    0.030s | 20.072MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00030_003.cvc.smt2 |    0.031s | 20.364MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7909578851601176589.smt2 |    0.031s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00030_008.cvc.smt2 |    0.032s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3502153459994386289.smt2 |    0.032s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00050_009.cvc.smt2 |    0.034s | 20.348MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00020_004.cvc.smt2 |    0.035s | 19.868MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00020_005.cvc.smt2 |    0.035s | 20.368MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00006_003.cvc.smt2 |    0.036s | 19.948MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00004_006.cvc.smt2 |    0.036s | 20.1MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00004_008.cvc.smt2 |    0.036s | 20.104MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00030_002.cvc.smt2 |    0.036s | 20.616MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1676069739265740399.smt2 |    0.036s | 19.896MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8908367221374111203.smt2 |    0.036s | 19.56MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/fb_var_6_12.smt2               |    0.037s | 20.14MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00060_005.cvc.smt2 |    0.037s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5192927862320386454.smt2 |    0.037s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00004_005.cvc.smt2 |    0.038s | 20.14MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00005_001.cvc.smt2 |    0.038s | 19.928MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/pp-invariant.smt2              |    0.038s | 20.128MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/fb_var_27_8.smt2               |    0.038s | 20.336MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00060_002.cvc.smt2 |    0.038s | 21.772MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt362130990708396776.smt2 |    0.038s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5963100064704668089.smt2 |    0.038s | 19.916MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00008_002.cvc.smt2 |    0.039s | 20.216MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/read8.smt2                     |    0.039s | 20.124MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/add6.smt2                      |    0.039s | 20.628MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00020_003.cvc.smt2 |    0.039s | 20.66MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00040_008.cvc.smt2 |    0.039s | 19.984MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5695631438254231329.smt2 |    0.039s | 19.836MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00002_009.cvc.smt2 |    0.040s | 19.836MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00008_003.cvc.smt2 |    0.040s | 20.156MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/add5.smt2                      |    0.040s | 20.4MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00040_007.cvc.smt2 |    0.040s | 20.184MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00050_008.cvc.smt2 |    0.040s | 20.52MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00003_002.cvc.smt2 |    0.041s | 20.152MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00006_009.cvc.smt2 |    0.041s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00002_008.cvc.smt2 |    0.041s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00050_003.cvc.smt2 |    0.041s | 21.352MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00030_002.cvc.smt2 |    0.041s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00020_008.cvc.smt2 |    0.041s | 19.892MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00050_005.cvc.smt2 |    0.041s | 20.372MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00060_009.cvc.smt2 |    0.041s | 20.468MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8778954223442726272.smt2 |    0.041s | 19.948MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt215465074793711162.smt2 |    0.041s | 20.096MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00004_001.cvc.smt2 |    0.042s | 20.252MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00010_004.cvc.smt2 |    0.042s | 20.484MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00004_008.cvc.smt2 |    0.042s | 20.14MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00006_001.cvc.smt2 |    0.042s | 20.3MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/dlx-pc.smt2                    |    0.042s | 20.908MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00050_007.cvc.smt2 |    0.042s | 21.96MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00020_003.cvc.smt2 |    0.042s | 20.056MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00008_001.cvc.smt2 |    0.043s | 20.2MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00007_004.cvc.smt2 |    0.043s | 20.156MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00007_004.cvc.smt2 |    0.043s | 20.136MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00020_004.cvc.smt2 |    0.043s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00060_003.cvc.smt2 |    0.043s | 19.94MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00060_007.cvc.smt2 |    0.043s | 19.96MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2922685147464036249.smt2 |    0.043s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00008_005.cvc.smt2 |    0.044s | 20.2MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00010_004.cvc.smt2 |    0.044s | 20.392MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00005_008.cvc.smt2 |    0.044s | 20.46MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00008_007.cvc.smt2 |    0.044s | 20.128MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00050_004.cvc.smt2 |    0.044s | 20.184MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00030_004.cvc.smt2 |    0.044s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00010_009.cvc.smt2 |    0.044s | 20.116MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6721808556525809116.smt2 |    0.044s | 19.484MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5369852344916049416.smt2 |    0.044s | 19.896MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1171825036458049994.smt2 |    0.044s | 19.432MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5385891397487700209.smt2 |    0.044s | 19.5MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4953135282161464900.smt2 |    0.044s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00008_009.cvc.smt2 |    0.045s | 20.372MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00007_008.cvc.smt2 |    0.045s | 20.348MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00002_008.cvc.smt2 |    0.045s | 19.872MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00004_003.cvc.smt2 |    0.045s | 19.96MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/dlx-regfile.smt2               |    0.045s | 20.536MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00010_009.cvc.smt2 |    0.045s | 19.368MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00020_008.cvc.smt2 |    0.045s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00010_008.cvc.smt2 |    0.045s | 20.244MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt9106017864656048635.smt2 |    0.045s | 19.912MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1042633846661310290.smt2 |    0.045s | 19.884MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3227222663221958379.smt2 |    0.045s | 19.976MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00007_006.cvc.smt2 |    0.046s | 20.132MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00003_007.cvc.smt2 |    0.046s | 20.164MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00004_002.cvc.smt2 |    0.046s | 19.976MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00010_008.cvc.smt2 |    0.046s | 19.488MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4037084432145914526.smt2 |    0.046s | 19.9MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8247715440196289156.smt2 |    0.046s | 20.068MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5103224205058501184.smt2 |    0.046s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2349554521575265533.smt2 |    0.046s | 19.836MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00005_005.cvc.smt2 |    0.047s | 20.144MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00006_008.cvc.smt2 |    0.047s | 20.26MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00005_008.cvc.smt2 |    0.047s | 20.096MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00003_003.cvc.smt2 |    0.047s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00002_001.cvc.smt2 |    0.047s | 19.376MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00010_008.cvc.smt2 |    0.047s | 20.156MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00010_002.cvc.smt2 |    0.047s | 19.976MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00060_006.cvc.smt2 |    0.047s | 20.428MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00060_008.cvc.smt2 |    0.047s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00030_009.cvc.smt2 |    0.047s | 20.068MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00020_003.cvc.smt2 |    0.047s | 20.38MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00010_004.cvc.smt2 |    0.047s | 20.58MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4697568481354341164.smt2 |    0.047s | 20.044MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7006792903852855302.smt2 |    0.047s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00005_006.cvc.smt2 |    0.048s | 19.976MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00009_007.cvc.smt2 |    0.048s | 20.364MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00009_003.cvc.smt2 |    0.048s | 20.296MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00009_005.cvc.smt2 |    0.048s | 20.548MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00006_008.cvc.smt2 |    0.048s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_nf_ni_00020_009.cvc.smt2 |    0.048s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00020_002.cvc.smt2 |    0.048s | 19.544MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt52509716184046872.smt2 |    0.048s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt498171090311845791.smt2 |    0.048s | 20.044MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1803124073673899816.smt2 |    0.048s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1441273869767862168.smt2 |    0.048s | 20.252MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00006_005.cvc.smt2 |    0.049s | 20.132MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00009_007.cvc.smt2 |    0.049s | 20.612MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00010_001.cvc.smt2 |    0.049s | 20.0MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00020_001.cvc.smt2 |    0.049s | 19.904MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00020_001.cvc.smt2 |    0.049s | 19.996MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2905633022829326820.smt2 |    0.049s | 19.904MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4238401262965072047.smt2 |    0.049s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2360244902319652454.smt2 |    0.049s | 20.284MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt672151100080778092.smt2 |    0.049s | 20.368MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00002_002.cvc.smt2 |    0.050s | 19.844MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00005_003.cvc.smt2 |    0.050s | 19.912MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00004_006.cvc.smt2 |    0.050s | 20.08MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00030_006.cvc.smt2 |    0.050s | 20.624MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00020_009.cvc.smt2 |    0.050s | 20.08MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00030_004.cvc.smt2 |    0.050s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6818634933433425749.smt2 |    0.050s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00006_002.cvc.smt2 |    0.051s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00007_005.cvc.smt2 |    0.051s | 20.22MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00007_007.cvc.smt2 |    0.051s | 20.144MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00010_008.cvc.smt2 |    0.051s | 20.452MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00009_005.cvc.smt2 |    0.051s | 20.36MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00040_005.cvc.smt2 |    0.051s | 20.232MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00040_007.cvc.smt2 |    0.051s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8139752062040253806.smt2 |    0.051s | 20.036MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4181015227210656643.smt2 |    0.051s | 19.572MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00010_006.cvc.smt2 |    0.052s | 20.324MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00004_005.cvc.smt2 |    0.052s | 20.104MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00002_005.cvc.smt2 |    0.052s | 19.976MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00007_005.cvc.smt2 |    0.052s | 20.048MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00010_002.cvc.smt2 |    0.052s | 20.596MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00030_009.cvc.smt2 |    0.052s | 20.564MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00010_005.cvc.smt2 |    0.052s | 20.116MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00010_004.cvc.smt2 |    0.052s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00020_007.cvc.smt2 |    0.052s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00030_001.cvc.smt2 |    0.052s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2187227346843288353.smt2 |    0.052s | 19.896MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3275743009640726251.smt2 |    0.052s | 19.564MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2897810692389626239.smt2 |    0.052s | 20.576MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8077224534801305670.smt2 |    0.052s | 19.904MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00007_003.cvc.smt2 |    0.053s | 20.276MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00007_006.cvc.smt2 |    0.053s | 20.248MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00007_001.cvc.smt2 |    0.053s | 20.244MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00020_004.cvc.smt2 |    0.053s | 20.432MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00050_005.cvc.smt2 |    0.053s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00060_005.cvc.smt2 |    0.053s | 20.356MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00050_009.cvc.smt2 |    0.053s | 20.612MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00040_004.cvc.smt2 |    0.053s | 20.88MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00050_005.cvc.smt2 |    0.053s | 20.252MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt770795137149803982.smt2 |    0.053s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7565714320681306474.smt2 |    0.053s | 19.928MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2384827473142460326.smt2 |    0.053s | 20.012MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00010_001.cvc.smt2 |    0.054s | 20.64MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00009_009.cvc.smt2 |    0.054s | 20.376MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00008_004.cvc.smt2 |    0.054s | 20.552MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00002_002.cvc.smt2 |    0.054s | 19.864MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00006_005.cvc.smt2 |    0.054s | 20.192MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00006_007.cvc.smt2 |    0.054s | 20.04MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00010_002.cvc.smt2 |    0.054s | 20.896MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00005_001.cvc.smt2 |    0.054s | 20.076MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00010_006.cvc.smt2 |    0.054s | 20.252MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00010_005.cvc.smt2 |    0.054s | 20.488MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/pp-pc-s2i.smt2                 |    0.054s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/add4.smt2                      |    0.054s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00060_009.cvc.smt2 |    0.054s | 20.624MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8135394236603703050.smt2 |    0.054s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1162898569824201421.smt2 |    0.054s | 19.832MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt9014840936023401544.smt2 |    0.054s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00004_004.cvc.smt2 |    0.055s | 19.968MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00050_009.cvc.smt2 |    0.055s | 20.384MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00040_006.cvc.smt2 |    0.055s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00020_001.cvc.smt2 |    0.055s | 20.336MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00040_008.cvc.smt2 |    0.055s | 20.9MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00040_005.cvc.smt2 |    0.055s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00030_005.cvc.smt2 |    0.055s | 20.612MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00010_005.cvc.smt2 |    0.055s | 19.436MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2438845199361275753.smt2 |    0.055s | 20.0MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00008_001.cvc.smt2 |    0.056s | 20.348MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00008_003.cvc.smt2 |    0.056s | 19.376MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/fb_var_5_12.smt2               |    0.056s | 20.16MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00050_004.cvc.smt2 |    0.056s | 20.576MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00040_004.cvc.smt2 |    0.056s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00060_002.cvc.smt2 |    0.056s | 20.352MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00030_005.cvc.smt2 |    0.056s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00060_002.cvc.smt2 |    0.056s | 22.084MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1656968675425225632.smt2 |    0.056s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3341546682240303433.smt2 |    0.056s | 20.072MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00004_002.cvc.smt2 |    0.057s | 20.244MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00008_002.cvc.smt2 |    0.057s | 20.1MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00008_008.cvc.smt2 |    0.057s | 20.376MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00050_003.cvc.smt2 |    0.057s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00040_004.cvc.smt2 |    0.057s | 20.012MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00060_002.cvc.smt2 |    0.057s | 20.048MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00030_002.cvc.smt2 |    0.057s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00050_002.cvc.smt2 |    0.057s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5562411513078936721.smt2 |    0.057s | 20.064MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8106154715414218129.smt2 |    0.057s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00007_004.cvc.smt2 |    0.058s | 19.94MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/check/array_incompleteness1.smt2   |    0.058s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00040_003.cvc.smt2 |    0.058s | 21.272MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00050_008.cvc.smt2 |    0.058s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00060_001.cvc.smt2 |    0.058s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00010_003.cvc.smt2 |    0.058s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00010_002.cvc.smt2 |    0.058s | 20.12MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3093696166632615469.smt2 |    0.058s | 19.884MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8228927933959930295.smt2 |    0.058s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6931994702471017916.smt2 |    0.058s | 20.024MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00005_009.cvc.smt2 |    0.059s | 20.148MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00006_002.cvc.smt2 |    0.059s | 20.516MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00030_008.cvc.smt2 |    0.059s | 20.044MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00010_005.cvc.smt2 |    0.059s | 20.044MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00050_008.cvc.smt2 |    0.059s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00040_006.cvc.smt2 |    0.059s | 20.904MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00040_003.cvc.smt2 |    0.059s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00010_007.cvc.smt2 |    0.059s | 20.092MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00060_002.cvc.smt2 |    0.059s | 20.328MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00030_004.cvc.smt2 |    0.059s | 19.86MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5994810375074922742.smt2 |    0.059s | 20.204MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6150185324016898914.smt2 |    0.059s | 20.0MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4601349962451502646.smt2 |    0.059s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5905287966985476080.smt2 |    0.059s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00006_004.cvc.smt2 |    0.060s | 20.232MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00010_006.cvc.smt2 |    0.060s | 20.28MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00050_007.cvc.smt2 |    0.060s | 21.212MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00040_004.cvc.smt2 |    0.060s | 21.18MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00060_004.cvc.smt2 |    0.060s | 20.732MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00040_004.cvc.smt2 |    0.060s | 20.896MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00020_002.cvc.smt2 |    0.060s | 19.572MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00020_006.cvc.smt2 |    0.060s | 19.428MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt182987599385075282.smt2 |    0.060s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5759472278662243112.smt2 |    0.060s | 20.216MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00003_007.cvc.smt2 |    0.061s | 20.36MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00050_006.cvc.smt2 |    0.061s | 20.252MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00020_005.cvc.smt2 |    0.061s | 20.188MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00030_003.cvc.smt2 |    0.061s | 20.768MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00050_009.cvc.smt2 |    0.061s | 20.22MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00040_002.cvc.smt2 |    0.061s | 19.916MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00030_008.cvc.smt2 |    0.061s | 19.572MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00060_004.cvc.smt2 |    0.061s | 22.22MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00060_002.cvc.smt2 |    0.061s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8579077759948482627.smt2 |    0.061s | 20.1MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00009_002.cvc.smt2 |    0.062s | 20.432MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00002_001.cvc.smt2 |    0.062s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00060_001.cvc.smt2 |    0.062s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00060_006.cvc.smt2 |    0.062s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00040_004.cvc.smt2 |    0.062s | 21.076MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00020_007.cvc.smt2 |    0.062s | 20.584MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00060_008.cvc.smt2 |    0.062s | 20.348MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00050_004.cvc.smt2 |    0.062s | 20.42MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1026703085055728276.smt2 |    0.062s | 20.004MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4134543687752878794.smt2 |    0.062s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00004_009.cvc.smt2 |    0.063s | 20.0MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/pp-TakenBranch-s2e.smt2        |    0.063s | 21.728MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00010_007.cvc.smt2 |    0.063s | 20.092MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00060_003.cvc.smt2 |    0.063s | 20.312MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00060_008.cvc.smt2 |    0.063s | 21.772MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/dlx-dmem.smt2                  |    0.064s | 20.604MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00060_009.cvc.smt2 |    0.064s | 22.496MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00010_001.cvc.smt2 |    0.064s | 20.332MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00010_008.cvc.smt2 |    0.064s | 19.464MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00060_002.cvc.smt2 |    0.064s | 20.416MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00010_005.cvc.smt2 |    0.064s | 19.424MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2445729392550066586.smt2 |    0.064s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00009_002.cvc.smt2 |    0.065s | 20.44MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00009_007.cvc.smt2 |    0.065s | 20.464MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00040_007.cvc.smt2 |    0.065s | 20.872MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00040_005.cvc.smt2 |    0.065s | 20.168MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00020_007.cvc.smt2 |    0.065s | 20.092MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8618877835758306362.smt2 |    0.065s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7358386960044497066.smt2 |    0.065s | 20.0MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00005_004.cvc.smt2 |    0.067s | 20.832MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00010_007.cvc.smt2 |    0.067s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00040_007.cvc.smt2 |    0.067s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00030_001.cvc.smt2 |    0.067s | 20.62MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt862348610184470396.smt2 |    0.067s | 19.936MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2190929513395224328.smt2 |    0.067s | 19.52MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5469619136922200125.smt2 |    0.067s | 20.036MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00009_007.cvc.smt2 |    0.068s | 20.464MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00010_002.cvc.smt2 |    0.068s | 19.944MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00010_004.cvc.smt2 |    0.068s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t1_pp_nf_ai_00002_001.cvc.smt2 |    0.068s | 20.348MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00020_005.cvc.smt2 |    0.069s | 19.86MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00060_002.cvc.smt2 |    0.069s | 20.184MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00050_009.cvc.smt2 |    0.069s | 21.104MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00060_003.cvc.smt2 |    0.069s | 22.392MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6683355899000363898.smt2 |    0.069s | 20.024MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00004_004.cvc.smt2 |    0.070s | 19.992MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00060_007.cvc.smt2 |    0.070s | 22.256MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00020_005.cvc.smt2 |    0.070s | 19.444MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00050_009.cvc.smt2 |    0.070s | 21.088MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t1_pp_nf_ai_00003_001.cvc.smt2 |    0.070s | 20.348MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00006_003.cvc.smt2 |    0.071s | 20.604MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00050_002.cvc.smt2 |    0.071s | 21.748MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00030_008.cvc.smt2 |    0.071s | 20.424MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00020_009.cvc.smt2 |    0.071s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00010_002.cvc.smt2 |    0.071s | 20.064MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1491157424836014881.smt2 |    0.071s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00060_009.cvc.smt2 |    0.072s | 21.72MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7092553497391582906.smt2 |    0.072s | 19.396MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2010137000504826137.smt2 |    0.072s | 20.348MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00007_005.cvc.smt2 |    0.073s | 20.168MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00060_007.cvc.smt2 |    0.073s | 20.168MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00050_003.cvc.smt2 |    0.073s | 20.076MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00050_007.cvc.smt2 |    0.073s | 20.304MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00010_004.cvc.smt2 |    0.073s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1816060575230669721.smt2 |    0.073s | 20.324MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1286129643722180277.smt2 |    0.073s | 19.468MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00040_003.cvc.smt2 |    0.074s | 19.952MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00050_005.cvc.smt2 |    0.074s | 19.78MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00010_006.cvc.smt2 |    0.074s | 20.1MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt377028722021915405.smt2 |    0.074s | 20.104MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3444773566975549937.smt2 |    0.074s | 19.408MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8755060589107111188.smt2 |    0.074s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3489543249285628273.smt2 |    0.074s | 20.02MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1495354633285877311.smt2 |    0.074s | 19.88MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00010_008.cvc.smt2 |    0.075s | 20.012MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00020_006.cvc.smt2 |    0.075s | 20.36MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00010_001.cvc.smt2 |    0.075s | 19.936MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3764635514138113797.smt2 |    0.075s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3405277169006856699.smt2 |    0.075s | 20.104MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2782844312644070087.smt2 |    0.075s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6161395833903900850.smt2 |    0.075s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00006_007.cvc.smt2 |    0.076s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00050_001.cvc.smt2 |    0.076s | 21.796MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00020_003.cvc.smt2 |    0.076s | 19.888MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1355996306873782731.smt2 |    0.076s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6557511902038258587.smt2 |    0.076s | 20.392MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1789157312273459318.smt2 |    0.076s | 20.592MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1782466548403316802.smt2 |    0.076s | 20.136MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00050_001.cvc.smt2 |    0.077s | 19.956MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00060_004.cvc.smt2 |    0.077s | 20.096MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1272323520518114421.smt2 |    0.077s | 20.092MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6513374120730325283.smt2 |    0.077s | 20.584MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt373337730591991193.smt2 |    0.077s | 20.036MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3758766264560852005.smt2 |    0.077s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00060_008.cvc.smt2 |    0.078s | 22.516MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00050_006.cvc.smt2 |    0.078s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7809753410478836385.smt2 |    0.078s | 19.856MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3440074116434092548.smt2 |    0.078s | 19.848MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00030_007.cvc.smt2 |    0.079s | 19.928MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00020_006.cvc.smt2 |    0.079s | 19.944MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5029315679561572039.smt2 |    0.079s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/fb_var_12_11.smt2              |    0.080s | 20.588MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00040_006.cvc.smt2 |    0.080s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00050_007.cvc.smt2 |    0.080s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00040_009.cvc.smt2 |    0.080s | 21.644MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7916933981353194815.smt2 |    0.080s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7618872707393860004.smt2 |    0.080s | 19.98MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7218190703470801014.smt2 |    0.080s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00010_003.cvc.smt2 |    0.081s | 20.168MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00020_001.cvc.smt2 |    0.081s | 20.26MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00020_002.cvc.smt2 |    0.081s | 20.304MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00030_004.cvc.smt2 |    0.081s | 20.516MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00010_002.cvc.smt2 |    0.081s | 20.296MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00008_008.cvc.smt2 |    0.082s | 20.436MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00004_007.cvc.smt2 |    0.082s | 20.352MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/read6.smt2                     |    0.082s | 20.112MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00060_004.cvc.smt2 |    0.082s | 21.552MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00050_006.cvc.smt2 |    0.082s | 20.12MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00030_005.cvc.smt2 |    0.082s | 19.5MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8855116929086333489.smt2 |    0.082s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3620633566921225648.smt2 |    0.082s | 19.4MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00020_006.cvc.smt2 |    0.083s | 20.304MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00040_005.cvc.smt2 |    0.083s | 21.276MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00050_009.cvc.smt2 |    0.083s | 20.212MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00030_002.cvc.smt2 |    0.083s | 19.928MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00060_005.cvc.smt2 |    0.083s | 20.156MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7092645672798492791.smt2 |    0.083s | 19.38MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8233570541221801360.smt2 |    0.083s | 20.348MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00020_006.cvc.smt2 |    0.084s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00030_006.cvc.smt2 |    0.084s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00050_005.cvc.smt2 |    0.084s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00020_006.cvc.smt2 |    0.084s | 19.98MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00060_009.cvc.smt2 |    0.084s | 20.216MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00050_008.cvc.smt2 |    0.084s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00040_009.cvc.smt2 |    0.084s | 20.88MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00060_003.cvc.smt2 |    0.084s | 21.82MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1048206973303286471.smt2 |    0.084s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt9111281160760624293.smt2 |    0.084s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt9116345646566616227.smt2 |    0.084s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4296070423334654308.smt2 |    0.084s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00004_007.cvc.smt2 |    0.085s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00010_003.cvc.smt2 |    0.085s | 19.972MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00010_005.cvc.smt2 |    0.085s | 20.204MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t1_pp_nf_ai_00006_001.cvc.smt2 |    0.085s | 20.396MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t3_pp_nf_ai_00007_001.cvc.smt2 |    0.085s | 20.36MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t1_pp_sf_ai_00001_001.cvc.smt2 |    0.085s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6900099572485246069.smt2 |    0.085s | 20.096MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt101358492275879472.smt2 |    0.085s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6231400525874152157.smt2 |    0.085s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7523130558871236757.smt2 |    0.085s | 19.488MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6493885507856928851.smt2 |    0.085s | 19.372MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7359050099439661129.smt2 |    0.085s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6281226815274613658.smt2 |    0.085s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00009_008.cvc.smt2 |    0.086s | 20.468MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00009_009.cvc.smt2 |    0.086s | 20.632MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00050_007.cvc.smt2 |    0.086s | 19.712MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00030_009.cvc.smt2 |    0.086s | 20.084MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00020_002.cvc.smt2 |    0.086s | 19.948MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00040_003.cvc.smt2 |    0.086s | 20.18MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00060_002.cvc.smt2 |    0.086s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8504464876204807071.smt2 |    0.086s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1523369924372993649.smt2 |    0.086s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5361404349484649674.smt2 |    0.086s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00009_002.cvc.smt2 |    0.087s | 20.584MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00010_007.cvc.smt2 |    0.087s | 20.548MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00030_005.cvc.smt2 |    0.087s | 20.772MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00030_005.cvc.smt2 |    0.087s | 20.7MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00030_008.cvc.smt2 |    0.087s | 20.524MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t3_pp_nf_ai_00009_001.cvc.smt2 |    0.087s | 20.12MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3580158146100843999.smt2 |    0.087s | 20.18MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6614798558121277247.smt2 |    0.087s | 20.356MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5491752019313122314.smt2 |    0.087s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00030_009.cvc.smt2 |    0.088s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7178509395836479705.smt2 |    0.088s | 19.496MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6456719111248078638.smt2 |    0.088s | 20.032MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3587125020666388275.smt2 |    0.088s | 20.032MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5066516013081219368.smt2 |    0.088s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6642385862663943481.smt2 |    0.088s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4315728387069939040.smt2 |    0.088s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5863666924611184171.smt2 |    0.088s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4277905976004114414.smt2 |    0.088s | 20.04MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2621433222940787538.smt2 |    0.088s | 20.036MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00003_005.cvc.smt2 |    0.089s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00030_005.cvc.smt2 |    0.089s | 20.336MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00050_001.cvc.smt2 |    0.089s | 20.008MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00040_007.cvc.smt2 |    0.089s | 20.132MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00050_008.cvc.smt2 |    0.089s | 21.148MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4909910871814089418.smt2 |    0.089s | 19.896MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1611612768507250801.smt2 |    0.089s | 19.94MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2367064203144307817.smt2 |    0.089s | 19.916MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt616279233519394183.smt2 |    0.089s | 20.036MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3136064081515784448.smt2 |    0.089s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6736572510318727716.smt2 |    0.089s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4507590573018277494.smt2 |    0.089s | 19.868MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3708937932107853478.smt2 |    0.089s | 19.896MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt676738985188385144.smt2 |    0.089s | 19.948MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1284056365933344272.smt2 |    0.089s | 19.84MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1076382332286802622.smt2 |    0.089s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4955949051970003181.smt2 |    0.089s | 19.916MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8987693239582237306.smt2 |    0.089s | 20.032MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5438568486190973361.smt2 |    0.089s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8974883641230246788.smt2 |    0.089s | 20.484MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6977760194528203096.smt2 |    0.089s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6876078461802558953.smt2 |    0.089s | 19.968MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7175394277113951989.smt2 |    0.089s | 20.06MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2427263037432339916.smt2 |    0.089s | 20.156MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00006_001.cvc.smt2 |    0.090s | 20.34MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00008_003.cvc.smt2 |    0.090s | 20.092MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00020_004.cvc.smt2 |    0.090s | 20.112MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00010_001.cvc.smt2 |    0.090s | 19.852MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00020_001.cvc.smt2 |    0.090s | 19.46MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00060_008.cvc.smt2 |    0.090s | 20.132MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2960554548505310231.smt2 |    0.090s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7960645538533115809.smt2 |    0.090s | 20.276MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2106860836086514151.smt2 |    0.090s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3523843011010396885.smt2 |    0.090s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt407122468318533822.smt2 |    0.090s | 19.904MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00010_008.cvc.smt2 |    0.091s | 20.72MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00006_001.cvc.smt2 |    0.091s | 20.116MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00008_006.cvc.smt2 |    0.091s | 20.612MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00050_004.cvc.smt2 |    0.091s | 21.74MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00030_004.cvc.smt2 |    0.091s | 20.352MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00010_009.cvc.smt2 |    0.091s | 20.068MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00020_006.cvc.smt2 |    0.091s | 20.296MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00020_007.cvc.smt2 |    0.091s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t1_pp_sf_ai_00010_001.cvc.smt2 |    0.091s | 20.388MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5657856502894956631.smt2 |    0.091s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8814225796421462573.smt2 |    0.091s | 19.468MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6433635961432197699.smt2 |    0.091s | 19.904MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4266255760697615431.smt2 |    0.091s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00050_003.cvc.smt2 |    0.092s | 19.712MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00010_004.cvc.smt2 |    0.092s | 20.076MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00010_001.cvc.smt2 |    0.092s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00040_005.cvc.smt2 |    0.092s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00010_006.cvc.smt2 |    0.092s | 19.544MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00010_003.cvc.smt2 |    0.093s | 20.604MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00003_004.cvc.smt2 |    0.093s | 20.344MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00008_001.cvc.smt2 |    0.093s | 20.256MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00060_002.cvc.smt2 |    0.093s | 22.392MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00040_008.cvc.smt2 |    0.093s | 19.94MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00040_002.cvc.smt2 |    0.093s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00040_002.cvc.smt2 |    0.093s | 20.956MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00050_001.cvc.smt2 |    0.093s | 21.768MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00020_007.cvc.smt2 |    0.093s | 20.572MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00040_002.cvc.smt2 |    0.093s | 20.052MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4514744799427321218.smt2 |    0.093s | 19.924MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5283357161187483598.smt2 |    0.093s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00005_005.cvc.smt2 |    0.094s | 20.592MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00030_007.cvc.smt2 |    0.094s | 20.644MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00050_006.cvc.smt2 |    0.094s | 21.736MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00030_002.cvc.smt2 |    0.094s | 20.004MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00020_004.cvc.smt2 |    0.094s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00060_001.cvc.smt2 |    0.094s | 19.864MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00040_002.cvc.smt2 |    0.094s | 21.128MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00040_001.cvc.smt2 |    0.094s | 20.88MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5563843641339295592.smt2 |    0.094s | 19.888MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4572245676070776514.smt2 |    0.094s | 20.02MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00008_008.cvc.smt2 |    0.095s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00050_001.cvc.smt2 |    0.095s | 20.048MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00020_009.cvc.smt2 |    0.095s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1364854746565558653.smt2 |    0.095s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2561940327326492283.smt2 |    0.095s | 20.004MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00004_006.cvc.smt2 |    0.096s | 20.132MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00007_006.cvc.smt2 |    0.096s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00050_003.cvc.smt2 |    0.096s | 20.196MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00020_003.cvc.smt2 |    0.096s | 20.312MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00010_004.cvc.smt2 |    0.096s | 20.272MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00020_002.cvc.smt2 |    0.096s | 20.38MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00010_008.cvc.smt2 |    0.096s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt436905341138176170.smt2 |    0.096s | 19.46MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00010_007.cvc.smt2 |    0.097s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00020_007.cvc.smt2 |    0.097s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00050_008.cvc.smt2 |    0.097s | 20.384MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00020_006.cvc.smt2 |    0.097s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t1_pp_sf_ai_00006_001.cvc.smt2 |    0.097s | 20.388MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3372199210070462891.smt2 |    0.097s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4504006725135742977.smt2 |    0.097s | 20.02MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3899959149727363456.smt2 |    0.097s | 19.58MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt166278749308099823.smt2 |    0.097s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00030_008.cvc.smt2 |    0.098s | 19.516MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00030_009.cvc.smt2 |    0.098s | 20.616MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00010_005.cvc.smt2 |    0.098s | 19.408MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00040_002.cvc.smt2 |    0.098s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00020_008.cvc.smt2 |    0.098s | 20.356MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00050_006.cvc.smt2 |    0.098s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00010_007.cvc.smt2 |    0.098s | 20.64MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00030_003.cvc.smt2 |    0.098s | 20.368MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6334367605951226396.smt2 |    0.098s | 20.352MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2843347168814075751.smt2 |    0.098s | 19.5MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7726411424237190229.smt2 |    0.098s | 20.204MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00005_009.cvc.smt2 |    0.099s | 20.352MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00010_006.cvc.smt2 |    0.099s | 20.628MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00040_003.cvc.smt2 |    0.099s | 20.872MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00050_003.cvc.smt2 |    0.099s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_nf_ni_00040_004.cvc.smt2 |    0.099s | 19.516MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00010_004.cvc.smt2 |    0.099s | 20.092MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00030_003.cvc.smt2 |    0.099s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00030_006.cvc.smt2 |    0.099s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt971450140125177067.smt2 |    0.099s | 19.488MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6608232286625221829.smt2 |    0.099s | 19.492MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt570363212685114932.smt2 |    0.099s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00006_003.cvc.smt2 |    0.100s | 20.584MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00003_006.cvc.smt2 |    0.100s | 20.144MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00004_009.cvc.smt2 |    0.100s | 20.14MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00060_005.cvc.smt2 |    0.100s | 20.152MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00060_007.cvc.smt2 |    0.100s | 20.12MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00040_008.cvc.smt2 |    0.100s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00020_005.cvc.smt2 |    0.100s | 20.444MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_nf_ni_00040_003.cvc.smt2 |    0.100s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00010_008.cvc.smt2 |    0.100s | 20.068MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00040_005.cvc.smt2 |    0.100s | 20.068MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00010_001.cvc.smt2 |    0.100s | 19.996MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00050_002.cvc.smt2 |    0.100s | 20.204MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00030_004.cvc.smt2 |    0.100s | 20.468MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00010_003.cvc.smt2 |    0.100s | 20.272MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00010_003.cvc.smt2 |    0.100s | 19.452MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00010_002.cvc.smt2 |    0.100s | 19.524MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00020_002.cvc.smt2 |    0.100s | 19.852MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00050_001.cvc.smt2 |    0.100s | 21.388MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2256856461941224445.smt2 |    0.100s | 20.092MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2931782982977550988.smt2 |    0.100s | 20.228MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6111014224437564259.smt2 |    0.100s | 20.0MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00003_002.cvc.smt2 |    0.101s | 20.128MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00006_008.cvc.smt2 |    0.101s | 20.376MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00006_005.cvc.smt2 |    0.101s | 20.124MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00050_006.cvc.smt2 |    0.101s | 20.14MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00020_004.cvc.smt2 |    0.101s | 19.856MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00050_005.cvc.smt2 |    0.101s | 21.732MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00040_006.cvc.smt2 |    0.101s | 20.424MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00030_001.cvc.smt2 |    0.101s | 20.16MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00050_001.cvc.smt2 |    0.101s | 20.428MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00060_002.cvc.smt2 |    0.101s | 20.828MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00060_003.cvc.smt2 |    0.101s | 20.38MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00050_004.cvc.smt2 |    0.101s | 20.172MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00020_005.cvc.smt2 |    0.101s | 20.176MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t1_pp_nf_ai_00010_001.cvc.smt2 |    0.101s | 20.38MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8792219215910766754.smt2 |    0.101s | 20.416MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4215517483378047775.smt2 |    0.101s | 19.388MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00002_006.cvc.smt2 |    0.102s | 19.916MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00010_006.cvc.smt2 |    0.102s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00030_004.cvc.smt2 |    0.102s | 20.76MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00060_006.cvc.smt2 |    0.102s | 20.08MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00060_003.cvc.smt2 |    0.102s | 20.116MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00040_006.cvc.smt2 |    0.102s | 20.372MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t3_pp_sf_ai_00002_001.cvc.smt2 |    0.102s | 20.1MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1823835542615668089.smt2 |    0.102s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00004_001.cvc.smt2 |    0.103s | 20.344MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00010_005.cvc.smt2 |    0.103s | 20.08MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00040_008.cvc.smt2 |    0.103s | 20.624MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00060_009.cvc.smt2 |    0.103s | 20.224MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00020_009.cvc.smt2 |    0.103s | 20.104MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00050_003.cvc.smt2 |    0.103s | 21.148MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00020_009.cvc.smt2 |    0.103s | 19.904MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00020_001.cvc.smt2 |    0.103s | 20.544MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00060_001.cvc.smt2 |    0.103s | 20.116MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00010_007.cvc.smt2 |    0.103s | 19.904MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00030_003.cvc.smt2 |    0.103s | 20.112MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t1_pp_nf_ai_00001_001.cvc.smt2 |    0.103s | 19.976MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2180380275580545420.smt2 |    0.103s | 19.856MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1630796854449618649.smt2 |    0.103s | 20.332MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8591958557635707797.smt2 |    0.103s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00009_004.cvc.smt2 |    0.104s | 20.888MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00002_005.cvc.smt2 |    0.104s | 19.848MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00020_007.cvc.smt2 |    0.104s | 20.164MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00020_005.cvc.smt2 |    0.104s | 20.144MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00040_007.cvc.smt2 |    0.104s | 21.356MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00040_008.cvc.smt2 |    0.104s | 21.364MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00050_004.cvc.smt2 |    0.104s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00020_001.cvc.smt2 |    0.104s | 20.248MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00050_007.cvc.smt2 |    0.104s | 20.176MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00040_001.cvc.smt2 |    0.104s | 19.92MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00010_009.cvc.smt2 |    0.104s | 20.128MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00040_008.cvc.smt2 |    0.104s | 20.788MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt793638039879708422.smt2 |    0.104s | 20.308MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4503191635050547935.smt2 |    0.104s | 20.104MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00040_008.cvc.smt2 |    0.105s | 20.576MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00010_006.cvc.smt2 |    0.105s | 19.86MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00010_002.cvc.smt2 |    0.105s | 20.068MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00030_001.cvc.smt2 |    0.105s | 20.724MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00020_008.cvc.smt2 |    0.105s | 19.468MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00010_009.cvc.smt2 |    0.105s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00050_009.cvc.smt2 |    0.105s | 21.728MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1269517447706381031.smt2 |    0.105s | 19.512MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt957085527369554317.smt2 |    0.105s | 20.128MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00004_004.cvc.smt2 |    0.106s | 20.352MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00006_009.cvc.smt2 |    0.106s | 20.452MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00060_008.cvc.smt2 |    0.106s | 20.324MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00060_008.cvc.smt2 |    0.106s | 20.836MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00010_005.cvc.smt2 |    0.106s | 19.836MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00040_005.cvc.smt2 |    0.106s | 19.96MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1766380371263919774.smt2 |    0.106s | 20.12MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5732050528631778495.smt2 |    0.106s | 19.4MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00007_009.cvc.smt2 |    0.107s | 20.52MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00010_006.cvc.smt2 |    0.107s | 19.496MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00010_004.cvc.smt2 |    0.107s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00060_009.cvc.smt2 |    0.107s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00020_007.cvc.smt2 |    0.107s | 20.06MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7585830350792253192.smt2 |    0.107s | 19.92MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00007_007.cvc.smt2 |    0.108s | 20.352MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00004_003.cvc.smt2 |    0.108s | 20.58MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00050_003.cvc.smt2 |    0.108s | 20.336MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_nf_ni_00050_009.cvc.smt2 |    0.108s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00050_002.cvc.smt2 |    0.108s | 19.912MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00020_007.cvc.smt2 |    0.108s | 20.684MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00020_002.cvc.smt2 |    0.108s | 20.44MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t1_pp_nf_ai_00007_001.cvc.smt2 |    0.108s | 20.124MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4625083610563501181.smt2 |    0.108s | 19.976MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2638042934975705528.smt2 |    0.108s | 20.3MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3796329264322518882.smt2 |    0.108s | 20.564MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8875471975092501873.smt2 |    0.108s | 19.54MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4735237723456590332.smt2 |    0.108s | 20.096MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00009_006.cvc.smt2 |    0.109s | 21.096MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00030_008.cvc.smt2 |    0.109s | 20.76MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00040_009.cvc.smt2 |    0.109s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00020_002.cvc.smt2 |    0.109s | 20.116MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00040_009.cvc.smt2 |    0.109s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_nf_ni_00050_004.cvc.smt2 |    0.109s | 19.836MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_nf_ni_00030_007.cvc.smt2 |    0.109s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00050_006.cvc.smt2 |    0.109s | 21.388MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00020_005.cvc.smt2 |    0.109s | 20.008MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00010_001.cvc.smt2 |    0.109s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00030_007.cvc.smt2 |    0.109s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1946805393457691034.smt2 |    0.109s | 20.008MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00008_009.cvc.smt2 |    0.110s | 20.764MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00030_005.cvc.smt2 |    0.110s | 20.552MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00010_006.cvc.smt2 |    0.110s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00010_006.cvc.smt2 |    0.110s | 20.376MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00030_004.cvc.smt2 |    0.110s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00060_009.cvc.smt2 |    0.110s | 20.592MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00040_006.cvc.smt2 |    0.110s | 20.844MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00030_009.cvc.smt2 |    0.110s | 20.62MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00010_002.cvc.smt2 |    0.110s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_nf_ni_00020_004.cvc.smt2 |    0.110s | 19.912MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4069305995038800906.smt2 |    0.110s | 19.924MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00003_001.cvc.smt2 |    0.111s | 20.1MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00003_007.cvc.smt2 |    0.111s | 20.076MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00010_007.cvc.smt2 |    0.111s | 20.22MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00040_005.cvc.smt2 |    0.111s | 20.88MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00060_007.cvc.smt2 |    0.111s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00050_006.cvc.smt2 |    0.111s | 20.58MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00050_001.cvc.smt2 |    0.111s | 20.148MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00030_001.cvc.smt2 |    0.111s | 20.12MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00030_007.cvc.smt2 |    0.111s | 20.02MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00060_007.cvc.smt2 |    0.111s | 20.62MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00010_008.cvc.smt2 |    0.111s | 20.644MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00050_008.cvc.smt2 |    0.111s | 22.128MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3698555390396458023.smt2 |    0.111s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8108887928342549384.smt2 |    0.111s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt615792926171406937.smt2 |    0.111s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4697298586713226690.smt2 |    0.111s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7725713132450845498.smt2 |    0.111s | 19.896MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3905221720212478447.smt2 |    0.111s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00007_007.cvc.smt2 |    0.112s | 20.62MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00010_003.cvc.smt2 |    0.112s | 20.092MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00030_005.cvc.smt2 |    0.112s | 20.124MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00040_008.cvc.smt2 |    0.112s | 19.992MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00040_003.cvc.smt2 |    0.112s | 21.232MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00030_007.cvc.smt2 |    0.112s | 20.68MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00010_008.cvc.smt2 |    0.112s | 19.904MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2016035095367711249.smt2 |    0.112s | 20.088MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt593896481169620861.smt2 |    0.112s | 19.828MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8289280324694207722.smt2 |    0.112s | 20.356MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6071472468091070475.smt2 |    0.112s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00050_006.cvc.smt2 |    0.113s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00040_009.cvc.smt2 |    0.113s | 19.9MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00020_001.cvc.smt2 |    0.113s | 19.532MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00040_002.cvc.smt2 |    0.113s | 21.74MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00030_008.cvc.smt2 |    0.113s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00010_001.cvc.smt2 |    0.113s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8644563128435345329.smt2 |    0.113s | 20.144MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4053218693677797575.smt2 |    0.113s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3439443866029601711.smt2 |    0.113s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt9065296178149417744.smt2 |    0.113s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00009_009.cvc.smt2 |    0.114s | 20.632MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00050_007.cvc.smt2 |    0.114s | 20.128MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00040_009.cvc.smt2 |    0.114s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00030_006.cvc.smt2 |    0.114s | 20.844MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00020_003.cvc.smt2 |    0.114s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00040_008.cvc.smt2 |    0.114s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00050_002.cvc.smt2 |    0.114s | 21.736MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4300906401518735495.smt2 |    0.114s | 19.856MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3728766622780732153.smt2 |    0.114s | 19.984MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8422912073068378811.smt2 |    0.114s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2677767669072326293.smt2 |    0.114s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5047342450357881159.smt2 |    0.114s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00003_004.cvc.smt2 |    0.115s | 20.352MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00060_004.cvc.smt2 |    0.115s | 19.932MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00020_007.cvc.smt2 |    0.115s | 20.096MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00060_004.cvc.smt2 |    0.115s | 21.82MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00050_004.cvc.smt2 |    0.115s | 22.012MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00040_006.cvc.smt2 |    0.115s | 20.18MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00050_008.cvc.smt2 |    0.115s | 21.768MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00030_003.cvc.smt2 |    0.115s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00010_006.cvc.smt2 |    0.115s | 20.072MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00010_008.cvc.smt2 |    0.115s | 20.06MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8654111885011073106.smt2 |    0.115s | 19.5MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3004264733300706548.smt2 |    0.115s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2561449432101481323.smt2 |    0.115s | 19.924MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2264998853780541334.smt2 |    0.115s | 20.024MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1880986003611271595.smt2 |    0.115s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00050_003.cvc.smt2 |    0.116s | 21.74MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7273354942600505220.smt2 |    0.116s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6481616554623030076.smt2 |    0.116s | 19.928MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3487051362416095263.smt2 |    0.116s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt194092121051256533.smt2 |    0.116s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7147939896033940408.smt2 |    0.116s | 20.304MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8701917448127671974.smt2 |    0.116s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00005_007.cvc.smt2 |    0.117s | 20.836MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00060_006.cvc.smt2 |    0.117s | 22.412MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00010_006.cvc.smt2 |    0.117s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00060_005.cvc.smt2 |    0.117s | 21.688MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00050_005.cvc.smt2 |    0.117s | 20.324MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00030_006.cvc.smt2 |    0.117s | 20.464MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t1_pp_nf_ai_00010_001.cvc.smt2 |    0.117s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t1_pp_nf_ai_00002_001.cvc.smt2 |    0.117s | 20.36MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8078846980698793773.smt2 |    0.117s | 19.56MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7033469606705066791.smt2 |    0.117s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00030_002.cvc.smt2 |    0.118s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00030_001.cvc.smt2 |    0.118s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00020_009.cvc.smt2 |    0.118s | 19.852MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00060_006.cvc.smt2 |    0.118s | 20.36MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00010_005.cvc.smt2 |    0.118s | 20.044MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3010346108910513369.smt2 |    0.118s | 20.188MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00009_003.cvc.smt2 |    0.119s | 20.388MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00006_009.cvc.smt2 |    0.119s | 20.332MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00020_002.cvc.smt2 |    0.119s | 19.888MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00050_004.cvc.smt2 |    0.119s | 21.52MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00050_006.cvc.smt2 |    0.119s | 21.728MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00050_007.cvc.smt2 |    0.119s | 21.14MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00010_007.cvc.smt2 |    0.119s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00010_002.cvc.smt2 |    0.119s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00060_004.cvc.smt2 |    0.119s | 20.104MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00050_003.cvc.smt2 |    0.119s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t3_pp_sf_ai_00003_001.cvc.smt2 |    0.119s | 19.908MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5641415969807714253.smt2 |    0.119s | 20.072MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00002_006.cvc.smt2 |    0.120s | 19.948MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00006_008.cvc.smt2 |    0.120s | 20.08MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00040_006.cvc.smt2 |    0.120s | 21.144MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00060_004.cvc.smt2 |    0.120s | 22.272MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00040_002.cvc.smt2 |    0.120s | 20.912MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00060_004.cvc.smt2 |    0.120s | 20.368MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00040_004.cvc.smt2 |    0.120s | 20.588MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt65467803538243106.smt2 |    0.120s | 20.08MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7811725335601850819.smt2 |    0.120s | 19.864MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00020_005.cvc.smt2 |    0.121s | 19.712MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00040_007.cvc.smt2 |    0.121s | 20.104MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00060_005.cvc.smt2 |    0.121s | 20.036MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00030_007.cvc.smt2 |    0.121s | 20.624MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00020_006.cvc.smt2 |    0.121s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00030_007.cvc.smt2 |    0.121s | 20.08MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8833779138211845249.smt2 |    0.121s | 19.344MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2033088614343642251.smt2 |    0.121s | 19.488MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7405460456682932921.smt2 |    0.121s | 20.316MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1656603882241727713.smt2 |    0.121s | 19.432MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt342752384921269204.smt2 |    0.121s | 19.54MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00050_003.cvc.smt2 |    0.122s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00020_009.cvc.smt2 |    0.122s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00010_003.cvc.smt2 |    0.122s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00020_006.cvc.smt2 |    0.122s | 20.36MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00020_007.cvc.smt2 |    0.122s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00010_002.cvc.smt2 |    0.122s | 20.336MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00040_001.cvc.smt2 |    0.122s | 20.168MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00010_001.cvc.smt2 |    0.122s | 20.348MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4537035296062250448.smt2 |    0.122s | 19.824MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7034109130135749243.smt2 |    0.122s | 19.42MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2468388263826893998.smt2 |    0.122s | 19.976MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7271452269704952934.smt2 |    0.122s | 19.956MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8129085571079473607.smt2 |    0.122s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1989795988797382439.smt2 |    0.122s | 19.948MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt599099718845180000.smt2 |    0.122s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4552940212595976610.smt2 |    0.122s | 19.908MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00003_008.cvc.smt2 |    0.123s | 20.0MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00010_005.cvc.smt2 |    0.123s | 20.104MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00020_004.cvc.smt2 |    0.123s | 20.116MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00050_009.cvc.smt2 |    0.123s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00030_003.cvc.smt2 |    0.123s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00050_005.cvc.smt2 |    0.123s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00040_008.cvc.smt2 |    0.123s | 20.068MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6416286979991758948.smt2 |    0.123s | 19.428MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt893324914284709225.smt2 |    0.123s | 19.492MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6879946163714078134.smt2 |    0.123s | 20.008MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2093842384271029720.smt2 |    0.123s | 19.904MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00008_009.cvc.smt2 |    0.124s | 20.4MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00010_004.cvc.smt2 |    0.124s | 20.836MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00010_009.cvc.smt2 |    0.124s | 20.096MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00020_008.cvc.smt2 |    0.124s | 20.08MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00030_009.cvc.smt2 |    0.124s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00040_002.cvc.smt2 |    0.124s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00030_008.cvc.smt2 |    0.124s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00010_009.cvc.smt2 |    0.124s | 20.332MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00060_007.cvc.smt2 |    0.124s | 22.072MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1525565934219293349.smt2 |    0.124s | 19.476MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3160966959479480483.smt2 |    0.124s | 19.468MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8513434858697749825.smt2 |    0.124s | 20.1MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00008_006.cvc.smt2 |    0.125s | 20.36MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00006_006.cvc.smt2 |    0.125s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00005_005.cvc.smt2 |    0.125s | 20.42MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00050_007.cvc.smt2 |    0.125s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00040_005.cvc.smt2 |    0.125s | 21.384MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00060_001.cvc.smt2 |    0.125s | 20.12MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00060_004.cvc.smt2 |    0.125s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00060_006.cvc.smt2 |    0.125s | 20.624MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00030_002.cvc.smt2 |    0.125s | 20.332MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1524375163231819094.smt2 |    0.125s | 19.572MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3038087770311212541.smt2 |    0.125s | 20.024MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00008_007.cvc.smt2 |    0.126s | 20.12MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00030_001.cvc.smt2 |    0.126s | 20.172MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00010_003.cvc.smt2 |    0.126s | 20.096MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t1_pp_sf_ai_00009_001.cvc.smt2 |    0.126s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2946635118515808081.smt2 |    0.126s | 20.044MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00010_006.cvc.smt2 |    0.127s | 19.988MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00040_005.cvc.smt2 |    0.127s | 20.924MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1829682051084319908.smt2 |    0.127s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00009_005.cvc.smt2 |    0.128s | 20.496MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00009_008.cvc.smt2 |    0.128s | 20.872MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00030_006.cvc.smt2 |    0.128s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00050_002.cvc.smt2 |    0.128s | 21.396MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00007_008.cvc.smt2 |    0.129s | 20.604MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00010_005.cvc.smt2 |    0.129s | 20.624MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00004_001.cvc.smt2 |    0.129s | 20.088MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00060_008.cvc.smt2 |    0.129s | 20.472MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t1_pp_nf_ai_00005_001.cvc.smt2 |    0.129s | 20.116MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00040_003.cvc.smt2 |    0.130s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00050_008.cvc.smt2 |    0.130s | 21.156MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00060_003.cvc.smt2 |    0.130s | 19.896MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_nf_ni_00030_002.cvc.smt2 |    0.130s | 19.488MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00040_007.cvc.smt2 |    0.130s | 21.132MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t3_pp_nf_ai_00003_001.cvc.smt2 |    0.130s | 20.604MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00004_007.cvc.smt2 |    0.131s | 19.852MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00008_009.cvc.smt2 |    0.131s | 20.436MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00050_002.cvc.smt2 |    0.131s | 20.06MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t1_pp_sf_ai_00007_001.cvc.smt2 |    0.131s | 20.34MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2748958072806976140.smt2 |    0.131s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4596042264305301650.smt2 |    0.131s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00050_005.cvc.smt2 |    0.132s | 21.168MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00020_008.cvc.smt2 |    0.132s | 20.148MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00030_003.cvc.smt2 |    0.132s | 19.904MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00020_002.cvc.smt2 |    0.132s | 19.904MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4132343230757244602.smt2 |    0.132s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00005_004.cvc.smt2 |    0.133s | 20.116MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00006_004.cvc.smt2 |    0.133s | 20.164MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00020_008.cvc.smt2 |    0.133s | 20.404MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00040_003.cvc.smt2 |    0.133s | 20.104MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00060_007.cvc.smt2 |    0.133s | 21.604MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00010_003.cvc.smt2 |    0.133s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6534511334474546878.smt2 |    0.133s | 20.016MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6395525940490892471.smt2 |    0.133s | 19.984MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4574461499410346282.smt2 |    0.133s | 20.16MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5743509124567723052.smt2 |    0.133s | 19.976MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00002_005.cvc.smt2 |    0.134s | 20.136MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00040_006.cvc.smt2 |    0.134s | 20.088MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1329906230419089873.smt2 |    0.134s | 19.86MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00003_001.cvc.smt2 |    0.135s | 19.948MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00020_004.cvc.smt2 |    0.135s | 20.092MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00050_002.cvc.smt2 |    0.135s | 21.136MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00020_003.cvc.smt2 |    0.135s | 19.424MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00040_001.cvc.smt2 |    0.135s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00060_006.cvc.smt2 |    0.135s | 20.2MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00050_008.cvc.smt2 |    0.135s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1232146482622696854.smt2 |    0.135s | 20.14MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt6946123632041025678.smt2 |    0.135s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3499861634082508558.smt2 |    0.135s | 19.896MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00010_009.cvc.smt2 |    0.136s | 20.356MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00009_008.cvc.smt2 |    0.136s | 20.4MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00005_001.cvc.smt2 |    0.136s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00007_002.cvc.smt2 |    0.136s | 20.62MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00004_002.cvc.smt2 |    0.136s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00030_007.cvc.smt2 |    0.136s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_nf_ni_00040_007.cvc.smt2 |    0.136s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00010_004.cvc.smt2 |    0.136s | 19.9MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00010_002.cvc.smt2 |    0.136s | 19.856MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00040_001.cvc.smt2 |    0.136s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00060_008.cvc.smt2 |    0.136s | 22.508MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00040_008.cvc.smt2 |    0.136s | 21.384MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8011955704126474321.smt2 |    0.136s | 19.928MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00009_001.cvc.smt2 |    0.137s | 20.624MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00008_006.cvc.smt2 |    0.137s | 20.516MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00030_007.cvc.smt2 |    0.137s | 20.652MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00050_001.cvc.smt2 |    0.137s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00010_007.cvc.smt2 |    0.137s | 19.944MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00030_006.cvc.smt2 |    0.137s | 20.624MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00040_007.cvc.smt2 |    0.137s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00010_003.cvc.smt2 |    0.137s | 19.856MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00020_008.cvc.smt2 |    0.137s | 19.956MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00020_003.cvc.smt2 |    0.137s | 19.916MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00002_003.cvc.smt2 |    0.138s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00003_008.cvc.smt2 |    0.138s | 20.14MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00040_009.cvc.smt2 |    0.138s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00040_001.cvc.smt2 |    0.138s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00060_006.cvc.smt2 |    0.138s | 21.656MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00040_004.cvc.smt2 |    0.138s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00060_009.cvc.smt2 |    0.138s | 21.708MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00040_006.cvc.smt2 |    0.138s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00050_006.cvc.smt2 |    0.138s | 20.004MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00040_007.cvc.smt2 |    0.138s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00005_006.cvc.smt2 |    0.139s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00020_009.cvc.smt2 |    0.139s | 20.24MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00010_008.cvc.smt2 |    0.139s | 19.42MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00020_004.cvc.smt2 |    0.139s | 19.456MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00040_001.cvc.smt2 |    0.139s | 20.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00010_008.cvc.smt2 |    0.139s | 19.896MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00010_004.cvc.smt2 |    0.139s | 20.144MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00010_004.cvc.smt2 |    0.139s | 19.848MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_nf_ni_00060_003.cvc.smt2 |    0.139s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00005_003.cvc.smt2 |    0.140s | 19.896MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00004_003.cvc.smt2 |    0.140s | 20.4MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00003_002.cvc.smt2 |    0.140s | 19.864MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00004_008.cvc.smt2 |    0.140s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00005_005.cvc.smt2 |    0.140s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00004_008.cvc.smt2 |    0.140s | 20.224MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00002_002.cvc.smt2 |    0.140s | 20.144MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00005_008.cvc.smt2 |    0.140s | 20.368MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00003_004.cvc.smt2 |    0.140s | 20.192MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00006_005.cvc.smt2 |    0.140s | 20.26MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00040_002.cvc.smt2 |    0.140s | 20.14MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00020_008.cvc.smt2 |    0.140s | 19.852MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00010_001.cvc.smt2 |    0.140s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00020_001.cvc.smt2 |    0.140s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_nf_ni_00020_005.cvc.smt2 |    0.140s | 19.428MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00040_009.cvc.smt2 |    0.140s | 20.876MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00003_005.cvc.smt2 |    0.141s | 19.892MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00004_009.cvc.smt2 |    0.141s | 19.928MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00004_006.cvc.smt2 |    0.141s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00060_001.cvc.smt2 |    0.141s | 21.708MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00020_008.cvc.smt2 |    0.141s | 19.576MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00030_001.cvc.smt2 |    0.141s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00050_002.cvc.smt2 |    0.141s | 20.292MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00006_001.cvc.smt2 |    0.142s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00010_006.cvc.smt2 |    0.142s | 20.176MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00008_006.cvc.smt2 |    0.142s | 20.364MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00005_009.cvc.smt2 |    0.142s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00005_002.cvc.smt2 |    0.142s | 20.148MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00007_005.cvc.smt2 |    0.142s | 20.376MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00020_006.cvc.smt2 |    0.142s | 19.856MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00040_007.cvc.smt2 |    0.142s | 21.488MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_nf_ni_00050_001.cvc.smt2 |    0.142s | 19.948MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00030_006.cvc.smt2 |    0.142s | 20.552MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00060_004.cvc.smt2 |    0.142s | 20.588MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t1_pp_nf_ai_00006_001.cvc.smt2 |    0.142s | 20.12MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00009_009.cvc.smt2 |    0.143s | 20.428MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00020_002.cvc.smt2 |    0.143s | 20.092MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00030_001.cvc.smt2 |    0.143s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00030_005.cvc.smt2 |    0.143s | 19.996MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00010_007.cvc.smt2 |    0.143s | 20.496MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00030_004.cvc.smt2 |    0.143s | 20.156MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00030_006.cvc.smt2 |    0.143s | 19.904MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00010_002.cvc.smt2 |    0.143s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00030_002.cvc.smt2 |    0.143s | 20.736MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00040_001.cvc.smt2 |    0.143s | 21.4MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00040_001.cvc.smt2 |    0.143s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00006_007.cvc.smt2 |    0.144s | 20.14MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00050_002.cvc.smt2 |    0.144s | 20.152MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00040_009.cvc.smt2 |    0.144s | 20.22MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00020_006.cvc.smt2 |    0.144s | 19.888MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00060_006.cvc.smt2 |    0.144s | 19.94MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00010_005.cvc.smt2 |    0.144s | 20.044MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ni_00050_009.cvc.smt2 |    0.144s | 19.92MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00030_008.cvc.smt2 |    0.144s | 19.844MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00030_006.cvc.smt2 |    0.144s | 20.14MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00008_004.cvc.smt2 |    0.145s | 20.132MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00060_006.cvc.smt2 |    0.145s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00020_004.cvc.smt2 |    0.145s | 20.476MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00030_004.cvc.smt2 |    0.145s | 20.624MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00030_005.cvc.smt2 |    0.145s | 19.852MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00030_009.cvc.smt2 |    0.145s | 19.956MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4885496405062058007.smt2 |    0.145s | 19.98MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/fb_var_33_6.smt2               |    0.146s | 20.66MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00040_004.cvc.smt2 |    0.146s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00060_009.cvc.smt2 |    0.146s | 20.212MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00040_006.cvc.smt2 |    0.146s | 21.14MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00020_005.cvc.smt2 |    0.146s | 19.86MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00030_001.cvc.smt2 |    0.146s | 20.66MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00020_001.cvc.smt2 |    0.146s | 20.392MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00040_006.cvc.smt2 |    0.146s | 20.16MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00030_004.cvc.smt2 |    0.146s | 20.652MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00010_006.cvc.smt2 |    0.146s | 19.832MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00050_001.cvc.smt2 |    0.146s | 20.156MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00060_007.cvc.smt2 |    0.146s | 20.316MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00050_007.cvc.smt2 |    0.146s | 20.168MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00030_008.cvc.smt2 |    0.146s | 20.972MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00020_009.cvc.smt2 |    0.146s | 20.436MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00050_007.cvc.smt2 |    0.147s | 19.904MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00060_001.cvc.smt2 |    0.147s | 20.292MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00030_002.cvc.smt2 |    0.147s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00020_003.cvc.smt2 |    0.147s | 20.092MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00060_001.cvc.smt2 |    0.147s | 20.616MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t1_pp_nf_ai_00009_001.cvc.smt2 |    0.147s | 20.588MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00003_006.cvc.smt2 |    0.148s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00040_009.cvc.smt2 |    0.148s | 20.04MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00050_001.cvc.smt2 |    0.148s | 21.408MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00050_002.cvc.smt2 |    0.148s | 20.084MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00002_002.cvc.smt2 |    0.149s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00040_009.cvc.smt2 |    0.149s | 21.168MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00060_001.cvc.smt2 |    0.149s | 20.148MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00060_005.cvc.smt2 |    0.149s | 22.6MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00060_004.cvc.smt2 |    0.149s | 20.164MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t3_pp_sf_ai_00005_001.cvc.smt2 |    0.149s | 20.428MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00040_003.cvc.smt2 |    0.150s | 20.936MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2282925904598514077.smt2 |    0.150s | 20.08MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00040_003.cvc.smt2 |    0.151s | 20.332MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00030_004.cvc.smt2 |    0.151s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00060_008.cvc.smt2 |    0.151s | 20.412MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00060_008.cvc.smt2 |    0.151s | 21.744MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00030_002.cvc.smt2 |    0.151s | 20.636MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4754789943944392049.smt2 |    0.151s | 20.104MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00060_001.cvc.smt2 |    0.152s | 21.796MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00050_004.cvc.smt2 |    0.152s | 21.344MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00060_005.cvc.smt2 |    0.152s | 19.908MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00060_003.cvc.smt2 |    0.152s | 21.824MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t1_pp_nf_ai_00005_001.cvc.smt2 |    0.152s | 20.128MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00060_005.cvc.smt2 |    0.153s | 21.816MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00010_007.cvc.smt2 |    0.154s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00030_003.cvc.smt2 |    0.154s | 20.628MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00009_001.cvc.smt2 |    0.155s | 20.456MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00060_008.cvc.smt2 |    0.155s | 19.896MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00060_003.cvc.smt2 |    0.155s | 22.516MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00020_002.cvc.smt2 |    0.155s | 20.08MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_np_sf_ni_00030_003.cvc.smt2 |    0.155s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00020_003.cvc.smt2 |    0.155s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00030_006.cvc.smt2 |    0.155s | 20.168MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00060_003.cvc.smt2 |    0.155s | 20.38MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00007_009.cvc.smt2 |    0.156s | 20.832MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ni_00040_004.cvc.smt2 |    0.156s | 20.144MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00010_003.cvc.smt2 |    0.156s | 20.168MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00020_009.cvc.smt2 |    0.156s | 20.592MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00010_004.cvc.smt2 |    0.157s | 20.584MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00020_008.cvc.smt2 |    0.157s | 19.96MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00050_005.cvc.smt2 |    0.157s | 21.78MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00030_006.cvc.smt2 |    0.157s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00007_006.cvc.smt2 |    0.158s | 20.608MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00050_003.cvc.smt2 |    0.158s | 21.64MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00020_003.cvc.smt2 |    0.158s | 20.076MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t1_pp_sf_ai_00006_001.cvc.smt2 |    0.158s | 20.132MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00003_002.cvc.smt2 |    0.159s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00040_001.cvc.smt2 |    0.159s | 20.128MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00040_004.cvc.smt2 |    0.159s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00050_008.cvc.smt2 |    0.159s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ni_00020_001.cvc.smt2 |    0.159s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00010_001.cvc.smt2 |    0.159s | 19.86MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00010_004.cvc.smt2 |    0.159s | 19.912MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t1_pp_sf_ai_00005_001.cvc.smt2 |    0.159s | 20.532MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t1_pp_sf_ai_00004_001.cvc.smt2 |    0.159s | 20.584MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t3_pp_sf_ai_00002_001.cvc.smt2 |    0.159s | 20.096MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt2524590214650541314.smt2 |    0.159s | 20.316MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00010_005.cvc.smt2 |    0.160s | 21.16MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00040_003.cvc.smt2 |    0.160s | 20.368MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00010_009.cvc.smt2 |    0.160s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00010_007.cvc.smt2 |    0.160s | 20.124MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00050_004.cvc.smt2 |    0.160s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t1_pp_sf_ai_00008_001.cvc.smt2 |    0.160s | 20.388MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t3_pp_nf_ai_00004_001.cvc.smt2 |    0.160s | 20.096MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t3_pp_nf_ai_00008_001.cvc.smt2 |    0.160s | 20.62MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/read7.smt2                     |    0.161s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00060_005.cvc.smt2 |    0.161s | 22.348MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00040_002.cvc.smt2 |    0.161s | 20.116MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00040_005.cvc.smt2 |    0.161s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00030_009.cvc.smt2 |    0.161s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ni_00010_009.cvc.smt2 |    0.161s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00010_005.cvc.smt2 |    0.161s | 20.156MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00020_008.cvc.smt2 |    0.161s | 20.392MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ni_00030_005.cvc.smt2 |    0.161s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00010_009.cvc.smt2 |    0.161s | 20.112MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ni_00050_005.cvc.smt2 |    0.162s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00060_007.cvc.smt2 |    0.162s | 20.156MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_nf_ni_00050_008.cvc.smt2 |    0.162s | 20.148MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t1_pp_nf_ai_00004_001.cvc.smt2 |    0.162s | 19.864MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_invalid_t3_pp_sf_ai_00004_001.cvc.smt2 |    0.162s | 19.924MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00009_004.cvc.smt2 |    0.163s | 20.828MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_np_sf_ni_00030_005.cvc.smt2 |    0.163s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00060_006.cvc.smt2 |    0.163s | 22.276MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ni_00020_007.cvc.smt2 |    0.163s | 19.9MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_sf_ni_00050_002.cvc.smt2 |    0.163s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_sf_ni_00060_005.cvc.smt2 |    0.163s | 20.6MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t3_pp_nf_ai_00008_001.cvc.smt2 |    0.163s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t1_pp_sf_ai_00007_001.cvc.smt2 |    0.163s | 20.12MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t3_pp_sf_ai_00003_001.cvc.smt2 |    0.163s | 19.94MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00003_006.cvc.smt2 |    0.164s | 19.856MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ni_00030_008.cvc.smt2 |    0.164s | 20.104MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00050_005.cvc.smt2 |    0.164s | 21.408MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00030_003.cvc.smt2 |    0.164s | 20.628MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00030_001.cvc.smt2 |    0.164s | 20.448MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t2_np_nf_ni_00060_005.cvc.smt2 |    0.164s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t3_pp_sf_ai_00009_001.cvc.smt2 |    0.164s | 20.376MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_sf_ai_00030_002.cvc.smt2 |    0.165s | 20.624MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00060_001.cvc.smt2 |    0.166s | 22.264MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_sf_ai_00050_006.cvc.smt2 |    0.166s | 21.268MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_np_sf_ni_00040_009.cvc.smt2 |    0.167s | 20.008MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00060_001.cvc.smt2 |    0.167s | 22.224MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00030_009.cvc.smt2 |    0.168s | 20.62MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4417655513178192608.smt2 |    0.168s | 20.084MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t3_pp_sf_ai_00010_001.cvc.smt2 |    0.169s | 20.372MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storeinv/storeinv_t3_pp_sf_ai_00008_001.cvc.smt2 |    0.169s | 20.396MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00006_004.cvc.smt2 |    0.170s | 20.076MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00009_006.cvc.smt2 |    0.170s | 20.66MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_sf_ai_00040_001.cvc.smt2 |    0.170s | 21.356MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_sf_ai_00060_009.cvc.smt2 |    0.170s | 22.496MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7534652473557877715.smt2 |    0.170s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00008_002.cvc.smt2 |    0.171s | 20.28MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00010_005.cvc.smt2 |    0.171s | 20.5MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00050_007.cvc.smt2 |    0.172s | 21.716MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00050_009.cvc.smt2 |    0.172s | 21.72MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00006_006.cvc.smt2 |    0.173s | 20.112MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t3_pp_nf_ai_00060_006.cvc.smt2 |    0.173s | 21.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00002_005.cvc.smt2 |    0.176s | 19.94MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00007_001.cvc.smt2 |    0.178s | 20.408MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00007_003.cvc.smt2 |    0.178s | 20.228MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_pp_nf_ai_00060_007.cvc.smt2 |    0.178s | 22.44MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00004_002.cvc.smt2 |    0.179s | 20.364MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t3_pp_nf_ai_00060_002.cvc.smt2 |    0.179s | 22.312MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00008_002.cvc.smt2 |    0.182s | 20.36MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00003_001.cvc.smt2 |    0.182s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00005_002.cvc.smt2 |    0.182s | 20.552MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00006_004.cvc.smt2 |    0.184s | 20.828MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3204289262029909600.smt2 |    0.185s | 20.044MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00003_001.cvc.smt2 |    0.186s | 20.16MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00005_004.cvc.smt2 |    0.187s | 20.72MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00002_006.cvc.smt2 |    0.188s | 20.04MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00003_004.cvc.smt2 |    0.189s | 19.852MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00002_006.cvc.smt2 |    0.189s | 20.352MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00007_003.cvc.smt2 |    0.190s | 20.748MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00007_001.cvc.smt2 |    0.191s | 20.776MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00004_005.cvc.smt2 |    0.192s | 20.284MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00008_005.cvc.smt2 |    0.193s | 20.392MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00005_007.cvc.smt2 |    0.195s | 20.64MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00005_001.cvc.smt2 |    0.195s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/pp-dmem.smt2                   |    0.195s | 22.264MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7788503754068870422.smt2 |    0.195s | 20.572MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00004_005.cvc.smt2 |    0.196s | 20.472MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00006_007.cvc.smt2 |    0.199s | 20.156MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00008_004.cvc.smt2 |    0.199s | 20.232MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5584401144276258491.smt2 |    0.200s | 20.1MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00004_001.cvc.smt2 |    0.202s | 20.58MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00003_003.cvc.smt2 |    0.202s | 19.376MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00010_007.cvc.smt2 |    0.203s | 21.06MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00009_008.cvc.smt2 |    0.204s | 20.776MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00007_008.cvc.smt2 |    0.205s | 20.348MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5901762799217475108.smt2 |    0.205s | 19.816MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00007_009.cvc.smt2 |    0.206s | 20.572MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00010_008.cvc.smt2 |    0.206s | 20.624MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00003_008.cvc.smt2 |    0.207s | 19.884MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00003_008.cvc.smt2 |    0.208s | 20.332MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00003_005.cvc.smt2 |    0.209s | 19.856MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00005_003.cvc.smt2 |    0.214s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt393108595912720571.smt2 |    0.214s | 19.844MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00004_004.cvc.smt2 |    0.215s | 20.32MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt1529145317830911829.smt2 |    0.215s | 20.124MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00008_007.cvc.smt2 |    0.216s | 20.332MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00005_007.cvc.smt2 |    0.219s | 20.356MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00005_006.cvc.smt2 |    0.219s | 20.14MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3150137541310906277.smt2 |    0.220s | 19.584MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00009_004.cvc.smt2 |    0.221s | 21.304MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7782311372861729448.smt2 |    0.221s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00008_001.cvc.smt2 |    0.225s | 20.284MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00005_002.cvc.smt2 |    0.226s | 20.232MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00009_001.cvc.smt2 |    0.226s | 20.368MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00005_006.cvc.smt2 |    0.226s | 19.888MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00007_003.cvc.smt2 |    0.226s | 20.264MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00006_002.cvc.smt2 |    0.226s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3411894737991763499.smt2 |    0.226s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00010_007.cvc.smt2 |    0.227s | 20.368MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00008_003.cvc.smt2 |    0.227s | 20.12MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt424770915908526889.smt2 |    0.227s | 20.176MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00010_001.cvc.smt2 |    0.228s | 20.712MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00005_009.cvc.smt2 |    0.228s | 19.92MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00009_002.cvc.smt2 |    0.228s | 20.372MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt275238204253440021.smt2 |    0.228s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt3809310795425240370.smt2 |    0.228s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00005_007.cvc.smt2 |    0.229s | 20.132MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00007_008.cvc.smt2 |    0.230s | 20.388MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00008_007.cvc.smt2 |    0.231s | 20.14MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00007_009.cvc.smt2 |    0.235s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00003_005.cvc.smt2 |    0.245s | 20.124MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00005_004.cvc.smt2 |    0.245s | 20.112MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00009_006.cvc.smt2 |    0.245s | 21.14MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt7740554476252106281.smt2 |    0.245s | 19.864MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5720223571793459860.smt2 |    0.245s | 20.156MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt5776021850984479403.smt2 |    0.245s | 20.452MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_sf_ai_00005_002.cvc.smt2 |    0.246s | 20.14MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00003_006.cvc.smt2 |    0.246s | 20.116MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00003_007.cvc.smt2 |    0.246s | 19.852MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00006_009.cvc.smt2 |    0.246s | 20.356MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00005_008.cvc.smt2 |    0.246s | 20.1MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00006_006.cvc.smt2 |    0.246s | 20.368MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00002_009.cvc.smt2 |    0.246s | 20.168MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00009_005.cvc.smt2 |    0.246s | 20.152MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00002_003.cvc.smt2 |    0.246s | 19.98MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt8706308851182253950.smt2 |    0.246s | 19.852MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/20170829-Rodin/smt4507059480007023557.smt2 |    0.246s | 19.888MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00007_007.cvc.smt2 |    0.247s | 20.148MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00007_002.cvc.smt2 |    0.247s | 20.364MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00008_004.cvc.smt2 |    0.247s | 20.36MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00005_003.cvc.smt2 |    0.247s | 20.108MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00007_001.cvc.smt2 |    0.247s | 20.424MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00008_005.cvc.smt2 |    0.247s | 20.24MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_sf_ai_00006_006.cvc.smt2 |    0.247s | 20.332MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00010_009.cvc.smt2 |    0.247s | 20.616MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t1_pp_nf_ai_00006_002.cvc.smt2 |    0.247s | 20.144MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_invalid_t3_pp_nf_ai_00010_003.cvc.smt2 |    0.247s | 20.4MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00004_009.cvc.smt2 |    0.247s | 20.116MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00007_004.cvc.smt2 |    0.247s | 20.112MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00006_003.cvc.smt2 |    0.247s | 20.164MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00007_002.cvc.smt2 |    0.249s | 20.4MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00009_006.cvc.smt2 |    0.249s | 20.884MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00010_003.cvc.smt2 |    0.249s | 21.128MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00009_004.cvc.smt2 |    0.250s | 21.384MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00007_002.cvc.smt2 |    0.250s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00009_003.cvc.smt2 |    0.253s | 20.72MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00010_007.cvc.smt2 |    0.253s | 21.12MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00009_001.cvc.smt2 |    0.264s | 20.632MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00010_001.cvc.smt2 |    0.271s | 21.632MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00010_008.cvc.smt2 |    0.276s | 20.872MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00008_008.cvc.smt2 |    0.277s | 20.7MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00009_003.cvc.smt2 |    0.279s | 20.664MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00010_003.cvc.smt2 |    0.287s | 21.172MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_t1_pp_nf_ai_00030_003.cvc.smt2 |    0.323s | 20.576MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/storecomm/storecomm_invalid_t1_np_nf_ni_00030_001.cvc.smt2 |    0.324s | 20.004MiB| sat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_sf_ai_00010_001.cvc.smt2 |    0.399s | 21.4MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/cvc/pp-regfile.smt2                |    0.516s | 23.78MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00010_009.cvc.smt2 |    0.563s | 21.644MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t3_pp_nf_ai_00010_009.cvc.smt2 |    0.570s | 21.632MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_nf_ai_00010_002.cvc.smt2 |    1.849s | 23.788MiB| unsat | 0 |  |  |
|non-incremental/QF_AUFLIA/swap/swap_t1_pp_sf_ai_00010_002.cvc.smt2 |    2.093s | 23.804MiB| unsat | 0 |  |  |