# .

* SAT 0
* UNSAT 0
* TIMEOUT 0
* UNKNOWN 77

* ERRORS 0

# Meta data

<pre>
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: 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/ABVFPLRA.tar.zst?download=1
Z3 commit message: bugfixes to ho_matcher

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_27.smt2 |    0.021s | 19.716MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_3.smt2 |    0.022s | 19.612MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_4.smt2 |    0.022s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_16.smt2 |    0.022s | 19.836MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_9.smt2 |    0.022s | 19.7MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_18.smt2 |    0.023s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_10.smt2 |    0.023s | 19.604MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_23.smt2 |    0.023s | 19.816MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_4.smt2 |    0.024s | 19.624MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_5.smt2 |    0.024s | 19.616MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_15.smt2 |    0.024s | 19.812MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_9.smt2 |    0.024s | 19.68MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_18.smt2 |    0.024s | 19.592MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_25.smt2 |    0.025s | 19.872MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_14.smt2 |    0.025s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_5.smt2 |    0.025s | 20.096MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_6.smt2 |    0.025s | 19.56MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_11.smt2 |    0.026s | 19.616MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_8.smt2 |    0.026s | 19.672MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_11.smt2 |    0.027s | 19.748MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_21.smt2 |    0.030s | 19.828MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_12.smt2 |    0.031s | 19.72MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_15.smt2 |    0.031s | 19.992MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_18.smt2 |    0.031s | 19.632MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_5.smt2 |    0.032s | 19.536MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_21.smt2 |    0.032s | 19.592MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_13.smt2 |    0.032s | 19.592MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_13.smt2 |    0.033s | 19.84MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_13.smt2 |    0.033s | 19.62MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_10.smt2 |    0.034s | 19.64MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_10.smt2 |    0.034s | 19.648MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_6.smt2 |    0.034s | 19.788MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_12.smt2 |    0.034s | 19.592MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_17.smt2 |    0.034s | 20.072MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_15.smt2 |    0.034s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_14.smt2 |    0.034s | 19.628MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_23.smt2 |    0.034s | 19.836MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_17.smt2 |    0.035s | 19.648MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_12.smt2 |    0.035s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0682a_true-unreach-call.c_1.smt2 |    0.035s | 19.972MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_13.smt2 |    0.036s | 19.64MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_22.smt2 |    0.036s | 19.588MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_20.smt2 |    0.036s | 19.612MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_15.smt2 |    0.036s | 19.588MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_12.smt2 |    0.037s | 19.62MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_11.smt2 |    0.037s | 20.092MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_9.smt2 |    0.038s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_7.smt2 |    0.038s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_8.smt2 |    0.038s | 19.684MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_16.smt2 |    0.039s | 19.552MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_11.smt2 |    0.040s | 19.864MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_14.smt2 |    0.040s | 19.796MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_7.smt2 |    0.041s | 20.028MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_6.smt2 |    0.042s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_19.smt2 |    0.042s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_13.smt2 |    0.044s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_7.smt2 |    0.044s | 19.776MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1032d_true-unreach-call.c_0.smt2 |    0.045s | 19.988MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_8.smt2 |    0.046s | 19.62MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_24.smt2 |    0.046s | 19.608MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_18.smt2 |    0.046s | 19.964MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_15.smt2 |    0.047s | 20.228MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0883_true-unreach-call.c_5.smt2 |    0.047s | 19.644MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_9.smt2 |    0.048s | 20.188MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_11.smt2 |    0.048s | 19.944MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_8.smt2 |    0.048s | 20.076MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_19.smt2 |    0.048s | 19.636MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_12.smt2 |    0.048s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20230321-UltimateAutomizerSvcomp2023/float_req_bl_0683a.c_7.smt2 |    0.048s | 19.788MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_22.smt2 |    0.049s | 20.464MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_29.smt2 |    0.049s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_28.smt2 |    0.049s | 19.824MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20230321-UltimateAutomizerSvcomp2023/float_req_bl_0683a.c_5.smt2 |    0.050s | 19.888MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_24.smt2 |    0.051s | 19.62MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_17.smt2 |    0.052s | 20.188MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621a_true-unreach-call.c_14.smt2 |    0.053s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_16.smt2 |    0.056s | 19.848MiB| unknown | 0 |  |  |