# . * SAT 59 * UNSAT 4 * TIMEOUT 0 * UNKNOWN 14 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/ABVFPLRA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-ABVFPLRA.tar.zst-d
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/ABVFPLRA.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0883_true-unreach-call.c_5.smt2 | 0.026s | 21.024MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20230321-UltimateAutomizerSvcomp2023/float_req_bl_0683a.c_5.smt2 | 0.028s | 20.624MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_17.smt2 | 0.029s | 20.744MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_7.smt2 | 0.031s | 21.408MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_8.smt2 | 0.031s | 20.624MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_14.smt2 | 0.031s | 21.392MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_29.smt2 | 0.033s | 21.276MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_15.smt2 | 0.043s | 20.876MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_24.smt2 | 0.047s | 21.128MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_11.smt2 | 0.049s | 20.88MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20230321-UltimateAutomizerSvcomp2023/float_req_bl_0683a.c_7.smt2 | 0.049s | 20.608MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_23.smt2 | 0.051s | 21.172MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_9.smt2 | 0.054s | 20.264MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_9.smt2 | 0.054s | 20.552MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_12.smt2 | 0.054s | 21.26MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_10.smt2 | 0.057s | 21.116MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_14.smt2 | 0.057s | 20.908MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_12.smt2 | 0.058s | 20.6MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_13.smt2 | 0.060s | 20.88MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_14.smt2 | 0.061s | 21.44MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_15.smt2 | 0.062s | 20.34MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_11.smt2 | 0.062s | 20.64MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_18.smt2 | 0.062s | 21.436MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_16.smt2 | 0.062s | 20.916MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_28.smt2 | 0.062s | 21.124MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_8.smt2 | 0.062s | 20.924MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_4.smt2 | 0.063s | 20.604MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_13.smt2 | 0.064s | 20.892MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_5.smt2 | 0.064s | 21.104MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_7.smt2 | 0.064s | 20.672MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_12.smt2 | 0.064s | 20.904MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_21.smt2 | 0.064s | 21.704MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_5.smt2 | 0.065s | 20.876MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_9.smt2 | 0.065s | 21.38MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_15.smt2 | 0.065s | 21.036MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_6.smt2 | 0.065s | 20.88MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_10.smt2 | 0.066s | 20.664MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_6.smt2 | 0.066s | 20.808MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_3.smt2 | 0.066s | 21.172MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_4.smt2 | 0.067s | 21.628MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0682a_true-unreach-call.c_1.smt2 | 0.067s | 20.908MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_22.smt2 | 0.068s | 21.132MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_24.smt2 | 0.068s | 21.676MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_12.smt2 | 0.068s | 21.144MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_25.smt2 | 0.069s | 21.668MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_22.smt2 | 0.069s | 21.656MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_27.smt2 | 0.070s | 21.216MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_11.smt2 | 0.072s | 21.712MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_9.smt2 | 0.075s | 20.796MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_18.smt2 | 0.076s | 21.372MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1032d_true-unreach-call.c_0.smt2 | 0.078s | 20.368MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_6.smt2 | 0.079s | 20.876MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_7.smt2 | 0.080s | 20.756MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_18.smt2 | 0.080s | 21.308MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_15.smt2 | 0.080s | 20.96MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_16.smt2 | 0.081s | 23.68MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_13.smt2 | 0.081s | 20.996MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_11.smt2 | 0.082s | 21.864MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_15.smt2 | 0.082s | 20.892MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_12.smt2 | 0.083s | 21.616MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_23.smt2 | 0.083s | 21.612MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_10.smt2 | 0.084s | 21.424MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_21.smt2 | 0.084s | 21.636MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_19.smt2 | 0.084s | 21.18MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_13.smt2 | 0.084s | 23.624MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_5.smt2 | 0.085s | 21.128MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_8.smt2 | 0.086s | 21.328MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_8.smt2 | 0.087s | 21.888MiB| unsat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_18.smt2 | 0.110s | 24.948MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_17.smt2 | 0.190s | 27.252MiB| unsat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_19.smt2 | 0.210s | 30.712MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_20.smt2 | 0.376s | 31.616MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_13.smt2 | 0.467s | 32.28MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_16.smt2 | 0.499s | 33.884MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_11.smt2 | 0.662s | 33.82MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_14.smt2 | 2.541s | 52.792MiB| unsat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_17.smt2 | 4.525s | 126.0MiB| unsat | 0 | | |