# . * 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-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/ABVFP.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_5.smt2 | 0.024s | 20.364MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_7.smt2 | 0.026s | 20.564MiB| unsat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_4.smt2 | 0.027s | 21.892MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0620b_true-unreach-call.c_6.smt2 | 0.027s | 20.324MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/test_mutex_unbounded-1.i_53.smt2 | 0.027s | 21.344MiB| unknown | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0620a_true-unreach-call.c_1.smt2 | 0.028s | 20.588MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_13.smt2 | 0.028s | 20.872MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/test_mutex_unbounded-2.i_63.smt2 | 0.028s | 21.388MiB| unknown | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0320_true-unreach-call.c_4.smt2 | 0.029s | 21.04MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/test_mutex_unbounded-2.i_64.smt2 | 0.029s | 21.276MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0663b.c_7.smt2 | 0.030s | 21.24MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_2.smt2 | 0.031s | 21.164MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_0.smt2 | 0.032s | 20.896MiB| unknown | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_7.smt2 | 0.034s | 21.156MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_1.smt2 | 0.038s | 22.588MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_2.smt2 | 0.040s | 22.928MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_16.smt2 | 0.049s | 21.148MiB| unknown | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_2.smt2 | 0.050s | 20.348MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_1.smt2 | 0.050s | 20.128MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_8.smt2 | 0.050s | 20.352MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/list_search-2.i_34.smt2 | 0.050s | 21.028MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/test_mutex_unbounded-1.i_52.smt2 | 0.050s | 21.68MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_14.smt2 | 0.050s | 20.864MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_4.smt2 | 0.050s | 20.88MiB| unknown | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0682a_true-unreach-call.c_13.smt2 | 0.052s | 21.0MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1210_false-unreach-call.c_0.smt2 | 0.052s | 20.88MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_4.smt2 | 0.053s | 20.132MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/sll2n_append_unequal.i_49.smt2 | 0.053s | 20.832MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0620a_true-unreach-call.c_3.smt2 | 0.054s | 20.348MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_3.smt2 | 0.054s | 20.992MiB| unsat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_15.smt2 | 0.054s | 20.944MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_17.smt2 | 0.054s | 21.016MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_6.smt2 | 0.054s | 21.18MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0663b.c_8.smt2 | 0.054s | 21.136MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_1.smt2 | 0.055s | 21.5MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_3.smt2 | 0.056s | 21.536MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0530a_true-unreach-call.c_4.smt2 | 0.057s | 20.752MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0663b.c_9.smt2 | 0.058s | 21.668MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_0.smt2 | 0.065s | 22.544MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_10.smt2 | 0.065s | 23.972MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_8.smt2 | 0.095s | 24.604MiB| sat | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float_req_bl_1130a.c_1.smt2 | 0.121s | 23.452MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_9.smt2 | 0.136s | 25.064MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_6.smt2 | 0.159s | 25.288MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0670_true-unreach-call.c_5.smt2 | 0.237s | 27.888MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0670_true-unreach-call.c_8.smt2 | 0.378s | 28.208MiB| sat | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_12.smt2 | 0.501s | 35.076MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_1300.c_2.smt2 | 2.763s | 49.208MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_1300.c_3.smt2 | 3.217s | 49.504MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_1300.c_1.smt2 | 4.082s | 50.724MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_1300.c_4.smt2 | 4.398s | 52.804MiB| unknown | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float_req_bl_1130a.c_0.smt2 | 20.022s | 64.036MiB| timeout | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_11.smt2 | 20.039s | 47.428MiB| timeout | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_10.smt2 | 20.041s | 47.648MiB| timeout | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_12.smt2 | 20.042s | 47.168MiB| timeout | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_13.smt2 | 20.043s | 47.76MiB| timeout | 0 | | | |non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_5.smt2 | 20.044s | 81.696MiB| timeout | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_11.smt2 | 20.048s | 98.968MiB| timeout | 0 | | | |non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_5.smt2 | 20.054s | 178.0MiB| timeout | 0 | | | |non-incremental/ABVFP/20170501-Heizmann-UltimateAutomizer/filter_iir_true-unreach-call.c_35.smt2 | 20.054s | 146.0MiB| timeout | 0 | | |