# . * SAT 513 * UNSAT 8 * TIMEOUT 0 * UNKNOWN 30 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/QF_AX.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-QF_AX.tar.zst-down
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 459629c662eb7abf25a010b7383431a9f729d234
Z3 branch: master
Z3 options: "-T:20 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify sls-smt)" model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_AX.tar.zst?download=1
Z3 commit message: bugfixes to ho_matcher

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00003_005.cvc.smt2 | 0.022s | 19.848MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00002_001.cvc.smt2 | 0.022s | 20.1MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_sf_ai_00005_001.cvc.smt2 | 0.022s | 19.592MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00010_007.cvc.smt2 | 0.023s | 20.172MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00004_003.cvc.smt2 | 0.023s | 20.228MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00009_002.cvc.smt2 | 0.023s | 19.852MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00005_002.cvc.smt2 | 0.023s | 19.852MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00010_001.cvc.smt2 | 0.024s | 19.924MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00006_003.cvc.smt2 | 0.024s | 19.852MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00008_001.cvc.smt2 | 0.024s | 20.084MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00010_002.cvc.smt2 | 0.024s | 19.888MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00005_008.cvc.smt2 | 0.026s | 20.124MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00008_004.cvc.smt2 | 0.026s | 19.852MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00009_001.cvc.smt2 | 0.026s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00010_009.cvc.smt2 | 0.026s | 19.904MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00007_001.cvc.smt2 | 0.027s | 20.144MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00004_004.cvc.smt2 | 0.027s | 20.092MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00010_003.cvc.smt2 | 0.027s | 20.004MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00010_004.cvc.smt2 | 0.027s | 19.848MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00010_007.cvc.smt2 | 0.029s | 20.456MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00009_004.cvc.smt2 | 0.030s | 20.064MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00010_009.cvc.smt2 | 0.031s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00002_006.cvc.smt2 | 0.031s | 19.584MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00010_006.cvc.smt2 | 0.032s | 19.768MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00030_006.cvc.smt2 | 0.032s | 20.88MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00004_007.cvc.smt2 | 0.033s | 19.764MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00004_009.cvc.smt2 | 0.033s | 19.652MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_nf_ai_00010_001.cvc.smt2 | 0.033s | 19.856MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00010_008.cvc.smt2 | 0.034s | 19.908MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_sf_ai_00003_001.cvc.smt2 | 0.034s | 19.752MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00020_006.cvc.smt2 | 0.035s | 20.404MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00040_004.cvc.smt2 | 0.035s | 22.28MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00040_007.cvc.smt2 | 0.035s | 22.272MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t1_np_sf_ai_00006_001.cvc.smt2 | 0.035s | 19.848MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_sf_ai_00002_001.cvc.smt2 | 0.035s | 19.94MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_nf_ai_00006_001.cvc.smt2 | 0.037s | 19.596MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_nf_ai_00010_001.cvc.smt2 | 0.037s | 19.828MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_nf_ai_00007_001.cvc.smt2 | 0.037s | 19.608MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00005_004.cvc.smt2 | 0.038s | 19.748MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00010_009.cvc.smt2 | 0.038s | 19.856MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t1_np_sf_ai_00009_001.cvc.smt2 | 0.038s | 19.876MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_sf_ai_00007_001.cvc.smt2 | 0.038s | 19.664MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_nf_ai_00008_001.cvc.smt2 | 0.038s | 19.86MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00007_004.cvc.smt2 | 0.039s | 19.824MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00030_002.cvc.smt2 | 0.039s | 21.128MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00005_005.cvc.smt2 | 0.040s | 19.724MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00007_009.cvc.smt2 | 0.040s | 19.856MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00040_009.cvc.smt2 | 0.040s | 21.864MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00050_007.cvc.smt2 | 0.040s | 22.928MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00010_003.cvc.smt2 | 0.040s | 19.868MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_007.cvc.smt2 | 0.041s | 20.124MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00050_002.cvc.smt2 | 0.041s | 22.996MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00010_008.cvc.smt2 | 0.041s | 20.344MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00040_003.cvc.smt2 | 0.041s | 21.72MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00020_002.cvc.smt2 | 0.041s | 20.84MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00009_007.cvc.smt2 | 0.042s | 19.836MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00030_003.cvc.smt2 | 0.042s | 20.872MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00030_009.cvc.smt2 | 0.042s | 20.876MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00030_003.cvc.smt2 | 0.043s | 21.124MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00006_002.cvc.smt2 | 0.044s | 19.752MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00009_007.cvc.smt2 | 0.045s | 19.724MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00060_007.cvc.smt2 | 0.045s | 24.22MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00010_003.cvc.smt2 | 0.046s | 20.032MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_006.cvc.smt2 | 0.047s | 19.736MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00060_009.cvc.smt2 | 0.048s | 23.968MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00060_005.cvc.smt2 | 0.048s | 24.208MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00040_005.cvc.smt2 | 0.048s | 21.892MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00050_009.cvc.smt2 | 0.051s | 22.944MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t2_np_nf_ai_00001_001.cvc.smt2 | 0.051s | 19.72MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_sf_ai_00006_001.cvc.smt2 | 0.051s | 20.116MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00008_007.cvc.smt2 | 0.052s | 19.748MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_sf_ai_00010_001.cvc.smt2 | 0.052s | 19.924MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_nf_ai_00009_001.cvc.smt2 | 0.052s | 19.852MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00010_006.cvc.smt2 | 0.053s | 19.832MiB| sat | 1 | | | |non-incremental/QF_AX/cvc/read5.smt2 | 0.053s | 19.848MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00040_005.cvc.smt2 | 0.053s | 22.5MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00005_009.cvc.smt2 | 0.054s | 19.74MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00003_006.cvc.smt2 | 0.054s | 19.736MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00010_008.cvc.smt2 | 0.056s | 19.896MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00030_001.cvc.smt2 | 0.057s | 21.052MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t2_np_sf_ai_00001_001.cvc.smt2 | 0.057s | 19.844MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00006_008.cvc.smt2 | 0.058s | 19.904MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00004_005.cvc.smt2 | 0.058s | 19.808MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00002_002.cvc.smt2 | 0.058s | 19.592MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00030_005.cvc.smt2 | 0.058s | 21.404MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00010_007.cvc.smt2 | 0.059s | 19.788MiB| unknown | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00060_003.cvc.smt2 | 0.060s | 24.728MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00010_002.cvc.smt2 | 0.061s | 20.0MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_001.cvc.smt2 | 0.062s | 19.496MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_003.cvc.smt2 | 0.062s | 19.68MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00003_006.cvc.smt2 | 0.062s | 19.76MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00002_008.cvc.smt2 | 0.062s | 19.648MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00008_008.cvc.smt2 | 0.062s | 19.928MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00003_008.cvc.smt2 | 0.062s | 19.484MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00007_006.cvc.smt2 | 0.063s | 19.72MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00010_004.cvc.smt2 | 0.064s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00008_008.cvc.smt2 | 0.064s | 19.9MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00002_005.cvc.smt2 | 0.066s | 19.684MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00008_001.cvc.smt2 | 0.066s | 19.868MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00002_006.cvc.smt2 | 0.067s | 19.624MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00050_003.cvc.smt2 | 0.067s | 23.416MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00009_003.cvc.smt2 | 0.068s | 19.732MiB| unknown | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t2_np_nf_ai_00007_001.cvc.smt2 | 0.069s | 19.856MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00009_005.cvc.smt2 | 0.070s | 19.92MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_009.cvc.smt2 | 0.070s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00008_003.cvc.smt2 | 0.070s | 19.596MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00007_002.cvc.smt2 | 0.071s | 19.864MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00006_003.cvc.smt2 | 0.074s | 19.896MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_005.cvc.smt2 | 0.075s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_006.cvc.smt2 | 0.075s | 20.128MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00005_002.cvc.smt2 | 0.076s | 19.648MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00004_006.cvc.smt2 | 0.076s | 19.588MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00006_005.cvc.smt2 | 0.077s | 19.864MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00009_006.cvc.smt2 | 0.077s | 19.944MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00010_004.cvc.smt2 | 0.077s | 20.14MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00003_002.cvc.smt2 | 0.077s | 19.612MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00004_001.cvc.smt2 | 0.078s | 19.604MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00005_007.cvc.smt2 | 0.078s | 19.856MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00007_006.cvc.smt2 | 0.078s | 19.844MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00009_008.cvc.smt2 | 0.078s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00005_004.cvc.smt2 | 0.078s | 19.828MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00003_002.cvc.smt2 | 0.078s | 19.644MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00007_002.cvc.smt2 | 0.078s | 19.888MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00007_005.cvc.smt2 | 0.078s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00008_005.cvc.smt2 | 0.078s | 19.692MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00010_005.cvc.smt2 | 0.078s | 20.12MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00005_003.cvc.smt2 | 0.079s | 19.644MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00002_002.cvc.smt2 | 0.079s | 19.776MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_008.cvc.smt2 | 0.080s | 19.848MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00004_004.cvc.smt2 | 0.080s | 19.636MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00004_001.cvc.smt2 | 0.080s | 19.748MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00002_002.cvc.smt2 | 0.080s | 19.684MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00006_007.cvc.smt2 | 0.080s | 19.852MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00010_006.cvc.smt2 | 0.081s | 19.904MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00009_007.cvc.smt2 | 0.082s | 19.896MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00007_007.cvc.smt2 | 0.082s | 19.816MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00006_007.cvc.smt2 | 0.082s | 19.884MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00005_008.cvc.smt2 | 0.082s | 19.568MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_007.cvc.smt2 | 0.083s | 19.892MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00002_003.cvc.smt2 | 0.083s | 19.6MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00008_006.cvc.smt2 | 0.083s | 19.896MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00004_007.cvc.smt2 | 0.083s | 19.732MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00009_005.cvc.smt2 | 0.083s | 19.9MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00008_009.cvc.smt2 | 0.084s | 19.904MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00009_001.cvc.smt2 | 0.084s | 19.992MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00003_003.cvc.smt2 | 0.084s | 19.636MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_sf_ai_00008_001.cvc.smt2 | 0.084s | 19.796MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00007_008.cvc.smt2 | 0.085s | 19.884MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00008_008.cvc.smt2 | 0.085s | 19.756MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00010_002.cvc.smt2 | 0.085s | 19.916MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00010_001.cvc.smt2 | 0.085s | 19.896MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00010_009.cvc.smt2 | 0.085s | 19.884MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00030_006.cvc.smt2 | 0.085s | 20.884MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00006_009.cvc.smt2 | 0.086s | 19.896MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_008.cvc.smt2 | 0.086s | 19.792MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00005_008.cvc.smt2 | 0.086s | 19.728MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00002_008.cvc.smt2 | 0.086s | 19.604MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00050_009.cvc.smt2 | 0.086s | 22.84MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00008_009.cvc.smt2 | 0.087s | 19.904MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00010_004.cvc.smt2 | 0.087s | 19.852MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00006_005.cvc.smt2 | 0.088s | 19.86MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00005_005.cvc.smt2 | 0.088s | 19.764MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00010_005.cvc.smt2 | 0.088s | 20.076MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00003_001.cvc.smt2 | 0.089s | 19.6MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00006_002.cvc.smt2 | 0.089s | 19.888MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00010_001.cvc.smt2 | 0.089s | 20.12MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00005_005.cvc.smt2 | 0.090s | 19.868MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00010_005.cvc.smt2 | 0.090s | 20.076MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00008_001.cvc.smt2 | 0.090s | 19.952MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00010_002.cvc.smt2 | 0.090s | 19.848MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00010_001.cvc.smt2 | 0.090s | 20.192MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00040_002.cvc.smt2 | 0.090s | 21.784MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00020_003.cvc.smt2 | 0.090s | 20.352MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00030_002.cvc.smt2 | 0.090s | 20.896MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00050_004.cvc.smt2 | 0.091s | 22.916MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00010_009.cvc.smt2 | 0.091s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00030_002.cvc.smt2 | 0.091s | 20.876MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00020_004.cvc.smt2 | 0.091s | 20.564MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00003_005.cvc.smt2 | 0.092s | 19.644MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00010_009.cvc.smt2 | 0.092s | 19.864MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00009_009.cvc.smt2 | 0.092s | 20.316MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00006_001.cvc.smt2 | 0.093s | 19.592MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00010_006.cvc.smt2 | 0.093s | 20.324MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00020_009.cvc.smt2 | 0.093s | 20.616MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00040_005.cvc.smt2 | 0.093s | 21.716MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00004_003.cvc.smt2 | 0.094s | 19.824MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00007_009.cvc.smt2 | 0.094s | 19.876MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00030_007.cvc.smt2 | 0.094s | 21.084MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00030_007.cvc.smt2 | 0.094s | 20.876MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00007_006.cvc.smt2 | 0.095s | 19.712MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00004_009.cvc.smt2 | 0.095s | 19.6MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00005_003.cvc.smt2 | 0.096s | 19.736MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00040_008.cvc.smt2 | 0.096s | 22.04MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00030_009.cvc.smt2 | 0.096s | 21.304MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00005_009.cvc.smt2 | 0.097s | 19.98MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00040_007.cvc.smt2 | 0.097s | 22.38MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00030_007.cvc.smt2 | 0.097s | 21.108MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00006_009.cvc.smt2 | 0.098s | 20.328MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00030_009.cvc.smt2 | 0.098s | 20.956MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00040_006.cvc.smt2 | 0.098s | 21.804MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00020_003.cvc.smt2 | 0.098s | 20.364MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_006.cvc.smt2 | 0.098s | 20.672MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00009_003.cvc.smt2 | 0.099s | 20.04MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00010_005.cvc.smt2 | 0.099s | 19.844MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_sf_ai_00005_001.cvc.smt2 | 0.099s | 19.604MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_006.cvc.smt2 | 0.100s | 19.856MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00006_001.cvc.smt2 | 0.100s | 19.872MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00009_002.cvc.smt2 | 0.101s | 19.972MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00004_008.cvc.smt2 | 0.101s | 20.032MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00006_005.cvc.smt2 | 0.101s | 20.116MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_009.cvc.smt2 | 0.101s | 20.568MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00040_006.cvc.smt2 | 0.101s | 21.904MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00030_003.cvc.smt2 | 0.101s | 21.116MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00020_001.cvc.smt2 | 0.101s | 20.608MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00002_009.cvc.smt2 | 0.102s | 19.972MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00003_008.cvc.smt2 | 0.102s | 20.324MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00050_005.cvc.smt2 | 0.102s | 22.916MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00050_002.cvc.smt2 | 0.102s | 23.136MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00020_008.cvc.smt2 | 0.102s | 20.26MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00010_003.cvc.smt2 | 0.102s | 20.1MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00004_002.cvc.smt2 | 0.103s | 19.684MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00040_008.cvc.smt2 | 0.103s | 21.844MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00050_004.cvc.smt2 | 0.103s | 23.16MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00010_005.cvc.smt2 | 0.104s | 20.192MiB| unknown | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00040_006.cvc.smt2 | 0.104s | 21.944MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00040_004.cvc.smt2 | 0.104s | 21.824MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00003_001.cvc.smt2 | 0.105s | 20.324MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00040_002.cvc.smt2 | 0.105s | 21.928MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00050_004.cvc.smt2 | 0.105s | 23.276MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00040_002.cvc.smt2 | 0.105s | 22.064MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00005_001.cvc.smt2 | 0.106s | 19.528MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00020_008.cvc.smt2 | 0.106s | 20.412MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00040_007.cvc.smt2 | 0.106s | 22.164MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00040_007.cvc.smt2 | 0.106s | 21.796MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00050_008.cvc.smt2 | 0.106s | 22.936MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00003_004.cvc.smt2 | 0.107s | 19.788MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00007_001.cvc.smt2 | 0.107s | 19.892MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00003_006.cvc.smt2 | 0.107s | 20.08MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00040_009.cvc.smt2 | 0.107s | 21.832MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00030_004.cvc.smt2 | 0.107s | 21.056MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00007_005.cvc.smt2 | 0.108s | 20.12MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00009_005.cvc.smt2 | 0.108s | 20.188MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00030_008.cvc.smt2 | 0.108s | 21.272MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00050_006.cvc.smt2 | 0.108s | 22.948MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00030_006.cvc.smt2 | 0.108s | 21.356MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00020_002.cvc.smt2 | 0.108s | 20.624MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00010_005.cvc.smt2 | 0.109s | 20.156MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00050_008.cvc.smt2 | 0.109s | 22.908MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00005_007.cvc.smt2 | 0.110s | 20.084MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00004_005.cvc.smt2 | 0.110s | 20.124MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00009_001.cvc.smt2 | 0.110s | 19.784MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00050_008.cvc.smt2 | 0.110s | 23.1MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00040_009.cvc.smt2 | 0.110s | 21.876MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00050_002.cvc.smt2 | 0.110s | 23.18MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00003_004.cvc.smt2 | 0.111s | 20.412MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00005_007.cvc.smt2 | 0.111s | 19.828MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00003_005.cvc.smt2 | 0.111s | 19.596MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00010_003.cvc.smt2 | 0.111s | 19.98MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00050_001.cvc.smt2 | 0.111s | 22.924MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00010_003.cvc.smt2 | 0.111s | 20.184MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00010_002.cvc.smt2 | 0.111s | 19.724MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00040_009.cvc.smt2 | 0.111s | 22.204MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00020_004.cvc.smt2 | 0.111s | 20.172MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00050_003.cvc.smt2 | 0.111s | 22.916MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00007_004.cvc.smt2 | 0.112s | 20.14MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00007_001.cvc.smt2 | 0.112s | 20.136MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00060_004.cvc.smt2 | 0.112s | 24.224MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00040_004.cvc.smt2 | 0.112s | 22.176MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00040_002.cvc.smt2 | 0.112s | 21.772MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00020_006.cvc.smt2 | 0.112s | 20.376MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00040_003.cvc.smt2 | 0.112s | 21.884MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00060_005.cvc.smt2 | 0.112s | 24.512MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00007_007.cvc.smt2 | 0.113s | 19.916MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00009_006.cvc.smt2 | 0.113s | 19.968MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00050_009.cvc.smt2 | 0.113s | 22.808MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00030_004.cvc.smt2 | 0.113s | 20.92MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00030_005.cvc.smt2 | 0.113s | 21.06MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00020_005.cvc.smt2 | 0.113s | 20.904MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00006_007.cvc.smt2 | 0.114s | 19.748MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00060_003.cvc.smt2 | 0.114s | 24.22MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00030_005.cvc.smt2 | 0.114s | 21.176MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_sf_ai_00003_001.cvc.smt2 | 0.114s | 19.9MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00009_004.cvc.smt2 | 0.115s | 19.972MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00005_004.cvc.smt2 | 0.115s | 20.072MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00020_005.cvc.smt2 | 0.115s | 20.42MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00020_006.cvc.smt2 | 0.115s | 20.516MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00010_008.cvc.smt2 | 0.115s | 19.776MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00050_007.cvc.smt2 | 0.115s | 22.932MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00060_004.cvc.smt2 | 0.115s | 24.276MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00002_006.cvc.smt2 | 0.116s | 19.828MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00006_002.cvc.smt2 | 0.116s | 20.096MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00003_002.cvc.smt2 | 0.116s | 19.776MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00002_005.cvc.smt2 | 0.117s | 19.648MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00005_006.cvc.smt2 | 0.117s | 19.824MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00004_008.cvc.smt2 | 0.117s | 19.6MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00060_006.cvc.smt2 | 0.117s | 24.012MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00050_001.cvc.smt2 | 0.117s | 22.928MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00050_002.cvc.smt2 | 0.117s | 22.916MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t1_np_sf_ai_00002_001.cvc.smt2 | 0.117s | 20.216MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00003_004.cvc.smt2 | 0.118s | 19.724MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_001.cvc.smt2 | 0.118s | 19.9MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00008_003.cvc.smt2 | 0.118s | 19.864MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00005_002.cvc.smt2 | 0.118s | 20.1MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00010_001.cvc.smt2 | 0.118s | 19.948MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00003_005.cvc.smt2 | 0.119s | 19.616MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00009_001.cvc.smt2 | 0.119s | 19.888MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00010_009.cvc.smt2 | 0.119s | 20.1MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00003_001.cvc.smt2 | 0.119s | 19.744MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00050_006.cvc.smt2 | 0.119s | 22.868MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00010_002.cvc.smt2 | 0.119s | 20.236MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00040_001.cvc.smt2 | 0.119s | 21.844MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00060_001.cvc.smt2 | 0.119s | 23.968MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00020_008.cvc.smt2 | 0.119s | 20.356MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00009_002.cvc.smt2 | 0.120s | 19.88MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00007_005.cvc.smt2 | 0.120s | 20.016MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00008_002.cvc.smt2 | 0.120s | 19.8MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t2_np_nf_ai_00003_001.cvc.smt2 | 0.120s | 19.94MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00004_008.cvc.smt2 | 0.121s | 20.116MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00009_009.cvc.smt2 | 0.121s | 19.848MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00004_001.cvc.smt2 | 0.121s | 19.596MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00008_004.cvc.smt2 | 0.121s | 19.896MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00007_003.cvc.smt2 | 0.121s | 19.66MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00004_008.cvc.smt2 | 0.121s | 19.732MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00003_006.cvc.smt2 | 0.121s | 19.736MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00006_004.cvc.smt2 | 0.121s | 19.708MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00008_006.cvc.smt2 | 0.121s | 20.316MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00040_005.cvc.smt2 | 0.121s | 21.812MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_009.cvc.smt2 | 0.121s | 20.364MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00030_004.cvc.smt2 | 0.121s | 20.88MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t1_np_nf_ai_00002_001.cvc.smt2 | 0.121s | 19.596MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00005_001.cvc.smt2 | 0.122s | 19.884MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_003.cvc.smt2 | 0.122s | 19.592MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00007_006.cvc.smt2 | 0.122s | 19.856MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00010_008.cvc.smt2 | 0.122s | 19.936MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00006_004.cvc.smt2 | 0.122s | 20.1MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00006_006.cvc.smt2 | 0.122s | 19.876MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00009_004.cvc.smt2 | 0.122s | 19.852MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00009_008.cvc.smt2 | 0.122s | 20.108MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00008_007.cvc.smt2 | 0.122s | 19.856MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00030_001.cvc.smt2 | 0.122s | 21.436MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00060_001.cvc.smt2 | 0.122s | 24.236MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_001.cvc.smt2 | 0.122s | 20.372MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00006_009.cvc.smt2 | 0.123s | 19.832MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_004.cvc.smt2 | 0.123s | 19.644MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00010_004.cvc.smt2 | 0.123s | 19.848MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00003_007.cvc.smt2 | 0.123s | 19.836MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00020_003.cvc.smt2 | 0.123s | 20.62MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00020_009.cvc.smt2 | 0.123s | 20.296MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_sf_ai_00010_001.cvc.smt2 | 0.123s | 20.1MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00004_005.cvc.smt2 | 0.124s | 19.828MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00006_001.cvc.smt2 | 0.124s | 19.872MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00008_007.cvc.smt2 | 0.124s | 19.828MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00004_002.cvc.smt2 | 0.124s | 19.604MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00007_002.cvc.smt2 | 0.124s | 20.104MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00003_008.cvc.smt2 | 0.124s | 19.852MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00040_003.cvc.smt2 | 0.124s | 21.844MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_sf_ai_00008_001.cvc.smt2 | 0.124s | 20.224MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00004_001.cvc.smt2 | 0.125s | 19.62MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00003_007.cvc.smt2 | 0.125s | 19.696MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00010_006.cvc.smt2 | 0.125s | 20.052MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00010_004.cvc.smt2 | 0.125s | 19.892MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00006_009.cvc.smt2 | 0.126s | 20.336MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00007_008.cvc.smt2 | 0.126s | 20.112MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00009_008.cvc.smt2 | 0.126s | 19.864MiB| unknown | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00010_005.cvc.smt2 | 0.126s | 20.108MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00040_004.cvc.smt2 | 0.126s | 22.12MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00060_005.cvc.smt2 | 0.126s | 24.488MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_sf_ai_00004_001.cvc.smt2 | 0.126s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00006_006.cvc.smt2 | 0.127s | 19.608MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_003.cvc.smt2 | 0.127s | 20.328MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00004_002.cvc.smt2 | 0.127s | 19.668MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00005_001.cvc.smt2 | 0.127s | 20.052MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00040_006.cvc.smt2 | 0.127s | 22.168MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t2_np_nf_ai_00004_001.cvc.smt2 | 0.127s | 19.752MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_001.cvc.smt2 | 0.128s | 19.668MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00007_005.cvc.smt2 | 0.128s | 19.856MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00004_004.cvc.smt2 | 0.128s | 19.6MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_004.cvc.smt2 | 0.128s | 19.896MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00004_007.cvc.smt2 | 0.128s | 19.988MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00009_003.cvc.smt2 | 0.128s | 20.056MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00010_004.cvc.smt2 | 0.128s | 19.996MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00050_008.cvc.smt2 | 0.128s | 22.924MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00020_001.cvc.smt2 | 0.128s | 20.16MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00060_006.cvc.smt2 | 0.128s | 24.08MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00050_005.cvc.smt2 | 0.128s | 22.904MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t1_np_sf_ai_00007_001.cvc.smt2 | 0.128s | 20.104MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00004_007.cvc.smt2 | 0.129s | 19.636MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_009.cvc.smt2 | 0.129s | 19.836MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00003_008.cvc.smt2 | 0.129s | 19.492MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00010_003.cvc.smt2 | 0.129s | 20.336MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00010_007.cvc.smt2 | 0.129s | 20.12MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00010_003.cvc.smt2 | 0.130s | 20.332MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00040_008.cvc.smt2 | 0.130s | 21.796MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_005.cvc.smt2 | 0.130s | 20.416MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00030_003.cvc.smt2 | 0.131s | 20.908MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00050_001.cvc.smt2 | 0.131s | 23.152MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_005.cvc.smt2 | 0.132s | 19.736MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00009_009.cvc.smt2 | 0.132s | 19.86MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00003_003.cvc.smt2 | 0.132s | 19.828MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00030_006.cvc.smt2 | 0.132s | 20.832MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00004_005.cvc.smt2 | 0.133s | 19.656MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00010_008.cvc.smt2 | 0.133s | 19.868MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00010_007.cvc.smt2 | 0.133s | 20.344MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00030_001.cvc.smt2 | 0.133s | 20.88MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00040_001.cvc.smt2 | 0.133s | 22.028MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_nf_ai_00003_001.cvc.smt2 | 0.133s | 20.076MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00009_008.cvc.smt2 | 0.134s | 19.772MiB| unknown | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00010_001.cvc.smt2 | 0.134s | 19.86MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00004_006.cvc.smt2 | 0.135s | 19.82MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00004_004.cvc.smt2 | 0.135s | 19.7MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00004_009.cvc.smt2 | 0.135s | 19.832MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00020_003.cvc.smt2 | 0.135s | 20.576MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00060_008.cvc.smt2 | 0.135s | 24.228MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t1_np_sf_ai_00004_001.cvc.smt2 | 0.135s | 20.16MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00007_009.cvc.smt2 | 0.136s | 20.12MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00009_006.cvc.smt2 | 0.136s | 20.268MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_006.cvc.smt2 | 0.136s | 19.756MiB| unknown | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00020_009.cvc.smt2 | 0.136s | 20.632MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00010_006.cvc.smt2 | 0.136s | 19.908MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00002_002.cvc.smt2 | 0.137s | 19.748MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00003_001.cvc.smt2 | 0.137s | 19.948MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00030_008.cvc.smt2 | 0.137s | 21.056MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_005.cvc.smt2 | 0.138s | 19.752MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00005_003.cvc.smt2 | 0.138s | 19.6MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00008_008.cvc.smt2 | 0.138s | 20.004MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00002_009.cvc.smt2 | 0.138s | 19.948MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00050_007.cvc.smt2 | 0.138s | 22.82MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00010_008.cvc.smt2 | 0.138s | 20.152MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00010_002.cvc.smt2 | 0.139s | 20.14MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00010_008.cvc.smt2 | 0.140s | 19.892MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00010_001.cvc.smt2 | 0.140s | 19.884MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00002_006.cvc.smt2 | 0.140s | 19.7MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00030_004.cvc.smt2 | 0.140s | 21.04MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00050_007.cvc.smt2 | 0.140s | 23.044MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00020_002.cvc.smt2 | 0.140s | 20.612MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00030_009.cvc.smt2 | 0.140s | 21.096MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00010_001.cvc.smt2 | 0.140s | 19.848MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_nf_ai_00005_001.cvc.smt2 | 0.140s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00005_006.cvc.smt2 | 0.141s | 19.572MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00010_005.cvc.smt2 | 0.141s | 19.856MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00009_007.cvc.smt2 | 0.141s | 20.336MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00020_002.cvc.smt2 | 0.141s | 20.688MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_008.cvc.smt2 | 0.141s | 20.396MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_nf_ai_00004_001.cvc.smt2 | 0.141s | 20.268MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00009_002.cvc.smt2 | 0.142s | 19.856MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00007_003.cvc.smt2 | 0.142s | 19.912MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00006_002.cvc.smt2 | 0.142s | 19.84MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00040_001.cvc.smt2 | 0.142s | 22.004MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00060_008.cvc.smt2 | 0.142s | 23.972MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_sf_ai_00009_001.cvc.smt2 | 0.142s | 19.916MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00008_002.cvc.smt2 | 0.143s | 19.708MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00010_006.cvc.smt2 | 0.143s | 19.912MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00060_007.cvc.smt2 | 0.143s | 23.992MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00006_008.cvc.smt2 | 0.144s | 20.296MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_004.cvc.smt2 | 0.144s | 19.956MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00007_002.cvc.smt2 | 0.144s | 19.908MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00007_003.cvc.smt2 | 0.144s | 19.904MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00020_001.cvc.smt2 | 0.144s | 20.432MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00003_007.cvc.smt2 | 0.145s | 19.72MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00007_008.cvc.smt2 | 0.145s | 19.924MiB| unknown | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00060_002.cvc.smt2 | 0.145s | 24.24MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00030_007.cvc.smt2 | 0.145s | 21.068MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00005_009.cvc.smt2 | 0.146s | 19.736MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00004_003.cvc.smt2 | 0.146s | 19.824MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_004.cvc.smt2 | 0.147s | 19.9MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_003.cvc.smt2 | 0.147s | 19.864MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00009_004.cvc.smt2 | 0.147s | 20.072MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00050_004.cvc.smt2 | 0.147s | 22.816MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00010_004.cvc.smt2 | 0.147s | 19.864MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00050_003.cvc.smt2 | 0.148s | 22.924MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00003_002.cvc.smt2 | 0.149s | 19.608MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00004_002.cvc.smt2 | 0.150s | 19.632MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00006_008.cvc.smt2 | 0.150s | 19.868MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_002.cvc.smt2 | 0.150s | 20.04MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00050_003.cvc.smt2 | 0.150s | 22.94MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00040_008.cvc.smt2 | 0.150s | 21.808MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00003_007.cvc.smt2 | 0.152s | 19.616MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00004_006.cvc.smt2 | 0.152s | 19.628MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00030_005.cvc.smt2 | 0.153s | 20.9MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00010_009.cvc.smt2 | 0.153s | 19.94MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00060_001.cvc.smt2 | 0.154s | 24.228MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00060_004.cvc.smt2 | 0.154s | 24.348MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00040_003.cvc.smt2 | 0.157s | 21.84MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00010_007.cvc.smt2 | 0.159s | 20.1MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_nf_ai_00009_001.cvc.smt2 | 0.159s | 19.6MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00010_002.cvc.smt2 | 0.160s | 20.064MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00010_007.cvc.smt2 | 0.162s | 20.092MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00050_005.cvc.smt2 | 0.163s | 23.108MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00060_004.cvc.smt2 | 0.163s | 24.228MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_nf_ai_00006_001.cvc.smt2 | 0.163s | 20.036MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00050_006.cvc.smt2 | 0.164s | 22.968MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00050_001.cvc.smt2 | 0.164s | 22.88MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00020_005.cvc.smt2 | 0.164s | 20.4MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_004.cvc.smt2 | 0.164s | 20.4MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_nf_ai_00002_001.cvc.smt2 | 0.164s | 19.66MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00010_006.cvc.smt2 | 0.165s | 20.372MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00020_007.cvc.smt2 | 0.166s | 20.348MiB| sat | 1 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_nf_ai_00008_001.cvc.smt2 | 0.166s | 19.744MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00020_007.cvc.smt2 | 0.167s | 20.388MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00020_007.cvc.smt2 | 0.167s | 20.824MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_007.cvc.smt2 | 0.167s | 20.628MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_nf_ai_00005_001.cvc.smt2 | 0.167s | 20.056MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00020_004.cvc.smt2 | 0.168s | 20.388MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00060_003.cvc.smt2 | 0.168s | 24.004MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00030_002.cvc.smt2 | 0.168s | 20.912MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00030_008.cvc.smt2 | 0.169s | 20.872MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00005_006.cvc.smt2 | 0.171s | 19.596MiB| unknown | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00060_003.cvc.smt2 | 0.171s | 24.264MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00030_008.cvc.smt2 | 0.171s | 21.04MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00060_008.cvc.smt2 | 0.171s | 24.064MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00030_001.cvc.smt2 | 0.172s | 21.004MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00060_009.cvc.smt2 | 0.175s | 24.16MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00040_001.cvc.smt2 | 0.175s | 22.136MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00010_007.cvc.smt2 | 0.177s | 20.12MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00007_007.cvc.smt2 | 0.177s | 19.652MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00007_008.cvc.smt2 | 0.178s | 20.104MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_002.cvc.smt2 | 0.178s | 19.768MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00006_003.cvc.smt2 | 0.179s | 19.644MiB| unknown | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00050_009.cvc.smt2 | 0.179s | 22.972MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00009_006.cvc.smt2 | 0.180s | 20.112MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00002_009.cvc.smt2 | 0.180s | 19.6MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00050_005.cvc.smt2 | 0.180s | 22.732MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00005_007.cvc.smt2 | 0.182s | 19.896MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00002_001.cvc.smt2 | 0.182s | 19.876MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00007_001.cvc.smt2 | 0.183s | 19.888MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00003_004.cvc.smt2 | 0.183s | 19.744MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00050_006.cvc.smt2 | 0.183s | 23.188MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00009_005.cvc.smt2 | 0.184s | 20.064MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00007_004.cvc.smt2 | 0.184s | 19.86MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00060_002.cvc.smt2 | 0.184s | 23.976MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00060_009.cvc.smt2 | 0.184s | 24.228MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00004_006.cvc.smt2 | 0.185s | 19.628MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00002_005.cvc.smt2 | 0.186s | 19.556MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00060_008.cvc.smt2 | 0.186s | 24.276MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00002_005.cvc.smt2 | 0.187s | 20.02MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00004_009.cvc.smt2 | 0.187s | 20.104MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00007_007.cvc.smt2 | 0.187s | 19.908MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00060_005.cvc.smt2 | 0.187s | 24.632MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_002.cvc.smt2 | 0.188s | 19.904MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00004_003.cvc.smt2 | 0.188s | 19.624MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00007_009.cvc.smt2 | 0.188s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00009_009.cvc.smt2 | 0.188s | 20.164MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00060_001.cvc.smt2 | 0.188s | 24.5MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00009_003.cvc.smt2 | 0.189s | 20.024MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00007_003.cvc.smt2 | 0.189s | 20.076MiB| unknown | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_005.cvc.smt2 | 0.189s | 19.804MiB| sat | 1 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00060_009.cvc.smt2 | 0.189s | 24.252MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00006_004.cvc.smt2 | 0.190s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00006_006.cvc.smt2 | 0.190s | 19.76MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00007_004.cvc.smt2 | 0.190s | 20.1MiB| sat | 1 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00008_005.cvc.smt2 | 0.190s | 19.856MiB| sat | 1 | | |