# .

* SAT 24
* UNSAT 0
* TIMEOUT 17
* UNKNOWN 0

* ERRORS 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/FPLRA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-FPLRA.tar.zst-down
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/FPLRA.tar.zst?download=1
Z3 commit message: update tptp front-end

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_6.smt2 |    0.015s | 20.056MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_14.smt2 |    0.017s | 20.336MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0683a_true-unreach-call.c_7.smt2 |    0.019s | 20.308MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_5.smt2 |    0.020s | 20.952MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_7.smt2 |    0.023s | 20.74MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0683a_true-unreach-call.c_3.smt2 |    0.071s | 23.132MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0683a_true-unreach-call.c_4.smt2 |    0.082s | 23.236MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_219.smt2 |    0.095s | 25.284MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/float-div1_true-unreach-call.i_574.smt2 |    0.134s | 36.556MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_1289.smt2 |    0.245s | 29.412MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_677.smt2 |    0.275s | 29.188MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_12.smt2 |    0.280s | 29.468MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_679.smt2 |    0.284s | 29.348MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_1310.smt2 |    0.299s | 29.7MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_1294.smt2 |    0.346s | 29.604MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0683a_true-unreach-call.c_6.smt2 |    0.413s | 28.384MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_1288.smt2 |    0.455s | 34.596MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/inv_square_true-unreach-call.c_139.smt2 |    0.475s | 33.152MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0683a_true-unreach-call.c_5.smt2 |    0.581s | 28.188MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_850.smt2 |    0.606s | 32.356MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0832a_true-unreach-call.c_2.smt2 |    2.270s | 43.804MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0832a_true-unreach-call.c_1.smt2 |    3.080s | 48.248MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1122a_true-unreach-call.c_3.smt2 |    4.320s | 131.0MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/water_pid_true-unreach-call_true-termination.c_2.smt2 |   11.086s | 84.896MiB| sat | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/inv_square_true-unreach-call.c_72.smt2 |   20.007s | 48.328MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call_true-termination.c_2.smt2 |   20.010s | 91.44MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/water_pid_true-unreach-call_true-termination.c_4.smt2 |   20.011s | 112.0MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/water_pid_true-unreach-call_true-termination.c_1.smt2 |   20.012s | 134.0MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/water_pid_true-unreach-call_true-termination.c_6.smt2 |   20.013s | 149.0MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/inv_square_true-unreach-call.c_70.smt2 |   20.013s | 45.864MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/inv_square_true-unreach-call.c_154.smt2 |   20.013s | 46.292MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+nlh-reducer.c_0.smt2 |   20.015s | 87.332MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call_true-termination.c_1.smt2 |   20.016s | 91.348MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/inv_square_true-unreach-call.c_110.smt2 |   20.016s | 54.564MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+nlh-reducer.c_1.smt2 |   20.020s | 94.844MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call_true-termination.c_3.smt2 |   20.020s | 99.0MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+lhb-reducer.c_1.smt2 |   20.020s | 97.652MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call_true-termination.c_4.smt2 |   20.020s | 101.0MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/water_pid_true-unreach-call_true-termination.c_5.smt2 |   20.023s | 143.0MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/water_pid_true-unreach-call_true-termination.c_3.smt2 |   20.025s | 174.0MiB| timeout | 0 |  |  |
|non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1122a_true-unreach-call.c_0.smt2 |   20.028s | 292.0MiB| timeout | 0 |  |  |
