# . * 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-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/ABVFPLRA.tar.zst?download=1
Z3 commit message: update tptp front-end
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_9.smt2 | 0.013s | 20.148MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_15.smt2 | 0.013s | 19.736MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_7.smt2 | 0.014s | 20.16MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_7.smt2 | 0.014s | 20.048MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_8.smt2 | 0.014s | 20.456MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_15.smt2 | 0.015s | 20.724MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_5.smt2 | 0.015s | 20.276MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_10.smt2 | 0.015s | 20.488MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_12.smt2 | 0.016s | 20.436MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_15.smt2 | 0.016s | 20.208MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_11.smt2 | 0.017s | 20.68MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_17.smt2 | 0.017s | 20.172MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_3.smt2 | 0.017s | 20.568MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_11.smt2 | 0.017s | 20.308MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_22.smt2 | 0.018s | 20.636MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_5.smt2 | 0.018s | 20.492MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_15.smt2 | 0.018s | 20.364MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_8.smt2 | 0.019s | 20.772MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_28.smt2 | 0.019s | 20.312MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_8.smt2 | 0.019s | 21.492MiB| unsat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_9.smt2 | 0.020s | 20.172MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_23.smt2 | 0.020s | 20.356MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_24.smt2 | 0.020s | 20.324MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_14.smt2 | 0.021s | 20.728MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_10.smt2 | 0.021s | 20.224MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_6.smt2 | 0.021s | 20.076MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_9.smt2 | 0.021s | 20.092MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_18.smt2 | 0.022s | 20.592MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_4.smt2 | 0.022s | 20.056MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_13.smt2 | 0.022s | 20.3MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_6.smt2 | 0.023s | 20.196MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_12.smt2 | 0.023s | 20.348MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_12.smt2 | 0.024s | 20.044MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1032d_true-unreach-call.c_0.smt2 | 0.024s | 19.792MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_7.smt2 | 0.024s | 20.032MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_13.smt2 | 0.024s | 20.352MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_18.smt2 | 0.024s | 20.436MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_14.smt2 | 0.025s | 20.96MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_19.smt2 | 0.025s | 20.44MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0682a_true-unreach-call.c_1.smt2 | 0.025s | 20.312MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_8.smt2 | 0.025s | 20.36MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_13.smt2 | 0.026s | 20.128MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_16.smt2 | 0.026s | 20.148MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0883_true-unreach-call.c_5.smt2 | 0.026s | 20.052MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_23.smt2 | 0.026s | 21.112MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_9.smt2 | 0.027s | 20.0MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_15.smt2 | 0.027s | 20.168MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_14.smt2 | 0.027s | 20.196MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_4.smt2 | 0.028s | 21.06MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_25.smt2 | 0.029s | 21.004MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_18.smt2 | 0.029s | 20.704MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_5.smt2 | 0.029s | 20.048MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_10.smt2 | 0.029s | 20.876MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_6.smt2 | 0.029s | 20.336MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_11.smt2 | 0.030s | 20.188MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_12.smt2 | 0.030s | 20.816MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20230321-UltimateAutomizerSvcomp2023/float_req_bl_0683a.c_5.smt2 | 0.030s | 20.14MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20230321-UltimateAutomizerSvcomp2023/float_req_bl_0683a.c_7.smt2 | 0.030s | 19.992MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_27.smt2 | 0.031s | 20.632MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_21.smt2 | 0.032s | 21.132MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_12.smt2 | 0.032s | 20.816MiB| unknown | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_21.smt2 | 0.032s | 20.964MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_22.smt2 | 0.032s | 21.016MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_29.smt2 | 0.032s | 20.568MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_11.smt2 | 0.034s | 21.016MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_24.smt2 | 0.041s | 21.148MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_13.smt2 | 0.046s | 23.06MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_16.smt2 | 0.047s | 22.868MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_18.smt2 | 0.078s | 24.348MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_17.smt2 | 0.157s | 26.856MiB| unsat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_19.smt2 | 0.173s | 30.216MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_20.smt2 | 0.331s | 30.98MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_13.smt2 | 0.427s | 31.688MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_16.smt2 | 0.468s | 33.416MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_11.smt2 | 0.640s | 33.264MiB| sat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_14.smt2 | 2.699s | 52.328MiB| unsat | 0 | | | |non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_17.smt2 | 4.951s | 125.0MiB| unsat | 0 | | |