# .

* SAT 26
* UNSAT 0
* TIMEOUT 0
* UNKNOWN 33

* ERRORS 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/QF_FPLRA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-QF_FPLRA.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/QF_FPLRA.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/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0460_true-unreach-call.c_2.smt2 |    0.022s | 19.6MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0874_true-unreach-call.c_3.smt2 |    0.022s | 19.612MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0520_true-unreach-call.c_0.smt2 |    0.022s | 19.596MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0490a.c_4.smt2 |    0.022s | 19.6MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_21.smt2 |    0.023s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0260_true-unreach-call.c_3.smt2 |    0.023s | 19.852MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_11.smt2 |    0.023s | 19.812MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Newton_pseudoconstant_true-unreach-call.c_1.smt2 |    0.023s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/schanda/spark/zeros_consistent_1.smt2 |    0.023s | 20.092MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/lnLaw.smt2            |    0.024s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/propLnExp3.smt2       |    0.024s | 19.632MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0470_true-unreach-call.c_12.smt2 |    0.024s | 19.592MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_2.smt2 |    0.024s | 19.592MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c_3.smt2 |    0.024s | 19.624MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0490a_true-unreach-call.c_3.smt2 |    0.024s | 19.916MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0550b_true-unreach-call.c_9.smt2 |    0.024s | 19.82MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20170501-Heizmann-UltimateAutomizer/filter2_reinit_true-unreach-call.c_7.smt2 |    0.024s | 19.6MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/Rump_double_true-unreach-call_true-termination.c_0.smt2 |    0.025s | 19.544MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/propExpLn1.smt2       |    0.026s | 19.844MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0310_true-unreach-call.c_3.smt2 |    0.026s | 19.616MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/propLnExp0.smt2       |    0.027s | 19.832MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/propExpLn0.smt2       |    0.027s | 19.94MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c_3.smt2 |    0.028s | 19.9MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/cos_polynomial_true-unreach-call_true-termination.c_0.smt2 |    0.028s | 19.444MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0460_true-unreach-call.c_3.smt2 |    0.028s | 19.628MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0490a_true-unreach-call.c_10.smt2 |    0.028s | 19.86MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0240a_true-unreach-call.c_6.smt2 |    0.050s | 19.556MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/Double_div_bad_false-unreach-call.i_0.smt2 |    0.051s | 19.48MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c_2.smt2 |    0.051s | 19.556MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0330b_true-unreach-call.c_10.smt2 |    0.051s | 19.58MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0873a_true-unreach-call.c_3.smt2 |    0.052s | 19.808MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0320_true-unreach-call.c_6.smt2 |    0.052s | 19.628MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0260_true-unreach-call.c_1.smt2 |    0.052s | 19.656MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0490a_true-unreach-call.c_9.smt2 |    0.052s | 19.692MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0870b_true-unreach-call.c_3.smt2 |    0.052s | 19.848MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0870b.c_1.smt2 |    0.052s | 19.612MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c_4.smt2 |    0.053s | 19.884MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0490a_true-unreach-call.c_0.smt2 |    0.053s | 19.62MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0250b_true-unreach-call.c_4.smt2 |    0.053s | 19.912MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/propLnExp1.smt2       |    0.054s | 19.704MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/Double_div_bad_false-unreach-call.i_1.smt2 |    0.054s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_4.smt2 |    0.054s | 19.62MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0250a.c_1.smt2 |    0.054s | 19.892MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20170501-Heizmann-UltimateAutomizer/image_filter_true-unreach-call.c_2.smt2 |    0.054s | 19.512MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/propLnExp2.smt2       |    0.055s | 19.62MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/expLaw.smt2           |    0.055s | 19.88MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0490a_true-unreach-call.c_2.smt2 |    0.055s | 19.652MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c_1.smt2 |    0.055s | 19.624MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0330a_true-unreach-call.c_6.smt2 |    0.055s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0320_true-unreach-call.c_7.smt2 |    0.055s | 19.624MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20230321-UltimateAutomizerSvcomp2023/cos_polynomial.c_0.smt2 |    0.055s | 19.884MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20170501-Heizmann-UltimateAutomizer/cos_polynomial_true-unreach-call.c_9.smt2 |    0.055s | 19.848MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/expInUnit.smt2        |    0.056s | 19.648MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/propExpLn2.smt2       |    0.056s | 19.592MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/expInUnit2.smt2       |    0.056s | 19.964MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0320_true-unreach-call.c_5.smt2 |    0.056s | 19.868MiB| sat | 0 |  |  |
|non-incremental/QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_19.smt2 |    0.056s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/propExpLn3.smt2       |    0.057s | 19.688MiB| unknown | 0 |  |  |
|non-incremental/QF_FPLRA/2019-Gudemann/maxReward.smt2        |    0.057s | 19.852MiB| unknown | 0 |  |  |