# . * SAT 0 * UNSAT 0 * TIMEOUT 0 * UNKNOWN 41 * ERRORS 0 # Meta data 
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-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/FPLRA.tar.zst?download=1
Z3 commit message: bugfixes to ho_matcher

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_5.smt2 | 0.021s | 19.676MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_12.smt2 | 0.023s | 19.604MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0683a_true-unreach-call.c_5.smt2 | 0.023s | 19.672MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1122a_true-unreach-call.c_3.smt2 | 0.023s | 19.64MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call_true-termination.c_3.smt2 | 0.023s | 19.748MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_1289.smt2 | 0.023s | 19.652MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1122a_true-unreach-call.c_0.smt2 | 0.024s | 19.988MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/water_pid_true-unreach-call_true-termination.c_5.smt2 | 0.024s | 19.844MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+lhb-reducer.c_1.smt2 | 0.024s | 19.596MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/inv_square_true-unreach-call.c_154.smt2 | 0.024s | 19.836MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0683a_true-unreach-call.c_7.smt2 | 0.026s | 20.092MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/water_pid_true-unreach-call_true-termination.c_1.smt2 | 0.026s | 19.6MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_679.smt2 | 0.028s | 20.088MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_1294.smt2 | 0.028s | 19.6MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/water_pid_true-unreach-call_true-termination.c_6.smt2 | 0.029s | 19.844MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/inv_square_true-unreach-call.c_72.smt2 | 0.029s | 19.596MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_1288.smt2 | 0.029s | 19.896MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_850.smt2 | 0.029s | 19.596MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_1310.smt2 | 0.029s | 20.008MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0832a_true-unreach-call.c_1.smt2 | 0.045s | 19.592MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call_true-termination.c_1.smt2 | 0.045s | 19.776MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0683a_true-unreach-call.c_6.smt2 | 0.045s | 19.608MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_6.smt2 | 0.046s | 19.556MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0683a_true-unreach-call.c_3.smt2 | 0.046s | 19.752MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/water_pid_true-unreach-call_true-termination.c_4.smt2 | 0.047s | 19.712MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0683a_true-unreach-call.c_4.smt2 | 0.047s | 19.86MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/water_pid_true-unreach-call_true-termination.c_3.smt2 | 0.047s | 19.512MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+nlh-reducer.c_0.smt2 | 0.047s | 19.732MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_7.smt2 | 0.047s | 19.608MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+nlh-reducer.c_1.smt2 | 0.047s | 19.596MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call_true-termination.c_2.smt2 | 0.047s | 19.824MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call_true-termination.c_4.smt2 | 0.047s | 19.62MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0832a_true-unreach-call.c_2.smt2 | 0.047s | 19.804MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_219.smt2 | 0.047s | 19.884MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/water_pid_true-unreach-call_true-termination.c_2.smt2 | 0.048s | 19.708MiB| unknown | 0 | | | |non-incremental/FPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_14.smt2 | 0.048s | 19.672MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/inv_square_true-unreach-call.c_139.smt2 | 0.048s | 19.852MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/inv_square_true-unreach-call.c_110.smt2 | 0.048s | 19.852MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/float-div1_true-unreach-call.i_574.smt2 | 0.049s | 19.64MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/inv_square_true-unreach-call.c_70.smt2 | 0.049s | 20.128MiB| unknown | 0 | | | |non-incremental/FPLRA/20170501-Heizmann-UltimateAutomizer/exp_loop_true-unreach-call.c_677.smt2 | 0.049s | 20.352MiB| unknown | 0 | | |