# .

* SAT 0
* UNSAT 0
* TIMEOUT 0
* UNKNOWN 60

* ERRORS 0

# Meta data

<pre>
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: 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/ABVFP.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/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_14.smt2 |    0.021s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_13.smt2 |    0.022s | 19.648MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/test_mutex_unbounded-2.i_63.smt2 |    0.022s | 19.752MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0620b_true-unreach-call.c_6.smt2 |    0.023s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_9.smt2 |    0.023s | 19.96MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_1.smt2 |    0.023s | 19.592MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0620a_true-unreach-call.c_1.smt2 |    0.023s | 19.928MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_0.smt2 |    0.023s | 19.752MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_6.smt2 |    0.023s | 19.84MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float_req_bl_1130a.c_1.smt2 |    0.023s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0684a_true-unreach-call.c_4.smt2 |    0.024s | 19.888MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_4.smt2 |    0.025s | 20.016MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0682a_true-unreach-call.c_13.smt2 |    0.025s | 19.64MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_3.smt2 |    0.025s | 19.88MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_1300.c_1.smt2 |    0.025s | 19.88MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0663b.c_8.smt2 |    0.025s | 19.84MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_1300.c_3.smt2 |    0.025s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_11.smt2 |    0.026s | 19.728MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_13.smt2 |    0.026s | 19.968MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_12.smt2 |    0.027s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0530a_true-unreach-call.c_4.smt2 |    0.027s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_6.smt2 |    0.027s | 19.988MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0670_true-unreach-call.c_5.smt2 |    0.028s | 19.64MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_2.smt2 |    0.028s | 19.864MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_10.smt2 |    0.029s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_0.smt2 |    0.029s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_1300.c_4.smt2 |    0.031s | 19.892MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_4.smt2 |    0.031s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float_req_bl_1130a.c_0.smt2 |    0.032s | 19.584MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/test_mutex_unbounded-2.i_64.smt2 |    0.032s | 20.148MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1210_false-unreach-call.c_0.smt2 |    0.046s | 19.924MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_17.smt2 |    0.046s | 19.604MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/sll2n_append_unequal.i_49.smt2 |    0.046s | 19.648MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0320_true-unreach-call.c_4.smt2 |    0.047s | 19.632MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0670_true-unreach-call.c_8.smt2 |    0.047s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_8.smt2 |    0.047s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20170501-Heizmann-UltimateAutomizer/filter_iir_true-unreach-call.c_35.smt2 |    0.047s | 19.86MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_2.smt2 |    0.048s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_2.smt2 |    0.048s | 20.108MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_1.smt2 |    0.048s | 19.604MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_7.smt2 |    0.048s | 19.648MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_7.smt2 |    0.049s | 19.644MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_5.smt2 |    0.049s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0620a_true-unreach-call.c_3.smt2 |    0.049s | 19.632MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0663b.c_7.smt2 |    0.049s | 19.588MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_12.smt2 |    0.049s | 19.644MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_15.smt2 |    0.049s | 19.892MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_8.smt2 |    0.050s | 19.74MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_10.smt2 |    0.050s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20190429-UltimateAutomizerSvcomp2019/float22_true-unreach-call_true-termination.i_5.smt2 |    0.050s | 19.636MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_1.smt2 |    0.050s | 19.904MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_1300.c_2.smt2 |    0.050s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_5.smt2 |    0.050s | 19.628MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_3.smt2 |    0.050s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/test_mutex_unbounded-1.i_53.smt2 |    0.051s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_16.smt2 |    0.055s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/list_search-2.i_34.smt2 |    0.055s | 20.084MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/float22.i_11.smt2 |    0.055s | 19.732MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0663b.c_9.smt2 |    0.056s | 19.592MiB| unknown | 0 |  |  |
|non-incremental/ABVFP/20230321-UltimateAutomizerSvcomp2023/test_mutex_unbounded-1.i_52.smt2 |    0.056s | 19.884MiB| unknown | 0 |  |  |