# . * SAT 30 * UNSAT 2 * TIMEOUT 9 * UNKNOWN 19 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/ABVFP.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-ABVFP.tar.zst-down
Runner: rise-runner-1
Z3 repo: Z3Prover/z3
Z3 commit: 8c989f8840e2c5789cd31aa9465dd2527852d453
Z3 branch: master
Z3 options: "-T:20 model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/ABVFP.tar.zst?download=1
Z3 commit message: update tptp front-end
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_4.smt2 | 0.016s | 19.58MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_16.smt2 | 0.017s | 20.52MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/test_mutex_unbounded-2.i_64.smt2 | 0.017s | 20.772MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_3.smt2 | 0.017s | 20.832MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_0.smt2 | 0.018s | 20.276MiB| unknown | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0682a_true-unreach-call.c_13.smt2 | 0.019s | 20.344MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0530a_true-unreach-call.c_4.smt2 | 0.019s | 19.7MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_1.smt2 | 0.019s | 19.692MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_3.smt2 | 0.019s | 20.056MiB| unsat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_14.smt2 | 0.019s | 20.104MiB| unknown | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0620b_true-unreach-call.c_6.smt2 | 0.020s | 19.584MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_7.smt2 | 0.020s | 20.344MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_5.smt2 | 0.020s | 19.724MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0620a_true-unreach-call.c_1.smt2 | 0.020s | 19.752MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0320_true-unreach-call.c_4.smt2 | 0.020s | 20.532MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_13.smt2 | 0.020s | 20.432MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_7.smt2 | 0.020s | 19.836MiB| unsat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_8.smt2 | 0.020s | 19.64MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_17.smt2 | 0.020s | 20.34MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/test_mutex_unbounded-2.i_63.smt2 | 0.020s | 20.98MiB| unknown | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_4.smt2 | 0.021s | 20.824MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/sll2n_append_unequal.i_49.smt2 | 0.021s | 20.288MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_2.smt2 | 0.024s | 19.512MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/list_search-2.i_34.smt2 | 0.024s | 20.22MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0663b.c_7.smt2 | 0.025s | 20.72MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/test_mutex_unbounded-1.i_53.smt2 | 0.026s | 20.756MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0663b.c_8.smt2 | 0.027s | 20.468MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0620a_true-unreach-call.c_3.smt2 | 0.028s | 19.928MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_2.smt2 | 0.028s | 20.312MiB| unknown | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1210_false-unreach-call.c_0.smt2 | 0.029s | 20.468MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_1.smt2 | 0.030s | 20.412MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_15.smt2 | 0.030s | 20.5MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_6.smt2 | 0.031s | 20.664MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_4.smt2 | 0.031s | 20.368MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/test_mutex_unbounded-1.i_52.smt2 | 0.033s | 20.836MiB| unknown | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_0.smt2 | 0.035s | 22.044MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_2.smt2 | 0.037s | 22.32MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_1.smt2 | 0.038s | 21.728MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0663b.c_9.smt2 | 0.040s | 21.104MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_10.smt2 | 0.048s | 23.256MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_8.smt2 | 0.075s | 24.016MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float_req_bl_1130a.c_1.smt2 | 0.128s | 22.76MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_9.smt2 | 0.142s | 24.532MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_6.smt2 | 0.144s | 24.672MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0670_true-unreach-call.c_5.smt2 | 0.237s | 27.332MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0670_true-unreach-call.c_8.smt2 | 0.341s | 27.584MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_12.smt2 | 0.496s | 34.456MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_1300.c_2.smt2 | 2.629s | 48.76MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_1300.c_3.smt2 | 3.149s | 48.84MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_1300.c_1.smt2 | 4.008s | 50.252MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_1300.c_4.smt2 | 4.313s | 52.204MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_13.smt2 | 20.007s | 45.108MiB| timeout | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_5.smt2 | 20.009s | 60.54MiB| timeout | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_11.smt2 | 20.009s | 45.748MiB| timeout | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float_req_bl_1130a.c_0.smt2 | 20.010s | 59.856MiB| timeout | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_10.smt2 | 20.012s | 45.844MiB| timeout | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_12.smt2 | 20.012s | 44.872MiB| timeout | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_11.smt2 | 20.018s | 98.284MiB| timeout | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_5.smt2 | 20.022s | 169.0MiB| timeout | 0 | | | |non-incremental/ABVFP/20170501-Heizmann-UltimateAutomizer/filter_iir_true-unreach-call.c_35.smt2 | 20.026s | 146.0MiB| timeout | 0 | | |