# . * SAT 64 * UNSAT 14 * TIMEOUT 0 * UNKNOWN 99 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/QF_BVFPLRA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-QF_BVFPLRA.tar.zst
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_BVFPLRA.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/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float-div1_true-unreach-call.i_0.smt2 | 0.023s | 19.6MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Muller_Kahan_true-unreach-call_true-termination.c_1.smt2 | 0.023s | 19.904MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Muller_Kahan_true-unreach-call_true-termination.c_4.smt2 | 0.023s | 19.864MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Double_div_bad_false-unreach-call.i_AllErrorsAtOnce_Iteration2_TraceCheck_0.smt2 | 0.023s | 19.508MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_1_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.024s | 20.196MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_430.smt2 | 0.025s | 19.596MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0661a_true-unreach-call.c_0.smt2 | 0.032s | 20.1MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_446.smt2 | 0.032s | 19.948MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Muller_Kahan_true-unreach-call_true-termination.c_2.smt2 | 0.033s | 20.088MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0530a_true-unreach-call.c_7.smt2 | 0.033s | 19.592MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter2_set_true-unreach-call_true-termination.c_0.smt2 | 0.034s | 19.728MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float21_true-unreach-call.i_1.smt2 | 0.034s | 19.596MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/Rump_double.c_0.smt2 | 0.034s | 19.68MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0330a_true-unreach-call.c_8.smt2 | 0.035s | 19.64MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0490b.c_2.smt2 | 0.035s | 19.472MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0490a.c_2.smt2 | 0.035s | 19.704MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0250a.c_4.smt2 | 0.035s | 19.86MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/sqrt_Householder_constant_true-unreach-call.c_274.smt2 | 0.035s | 19.604MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_414.smt2 | 0.035s | 19.844MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/water_pid_true-unreach-call.c_372.smt2 | 0.037s | 19.632MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_7.smt2 | 0.042s | 20.068MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_5_true-unreach-call_true-termination.i_0.smt2 | 0.051s | 19.596MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0684a_true-unreach-call.c_0.smt2 | 0.051s | 19.648MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0260_true-unreach-call.c_2.smt2 | 0.051s | 19.5MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_interval_true-unreach-call.c_1.smt2 | 0.051s | 19.616MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_3.smt2 | 0.051s | 19.584MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0882_true-unreach-call.c_1.smt2 | 0.052s | 19.616MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_true-unreach-call.i_0.smt2 | 0.052s | 19.464MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0240a_true-unreach-call.c_0.smt2 | 0.053s | 19.632MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0550b_true-unreach-call.c_4.smt2 | 0.053s | 19.48MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_1.smt2 | 0.055s | 19.636MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_3_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.055s | 19.604MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c_1.smt2 | 0.056s | 19.936MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0684a_true-unreach-call.c_1.smt2 | 0.057s | 19.5MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_AllErrorsAtOnce_Iteration2_TraceCheck_0.smt2 | 0.057s | 19.632MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_6_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.058s | 19.844MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Newton_pseudoconstant_true-unreach-call.c_2.smt2 | 0.058s | 19.468MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter2.c_0.smt2 | 0.058s | 19.704MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_interval_true-unreach-call.c_0.smt2 | 0.059s | 19.596MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/inv_Newton_false-unreach-call.c.p+cfa-reducer.c_1.smt2 | 0.059s | 19.676MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/sqrt_Householder_constant.c.p+cfa-reducer.c_2.smt2 | 0.059s | 19.916MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter2_reinit.c_0.smt2 | 0.059s | 20.148MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/schanda/spark/zeros_consistent_3.smt2 | 0.059s | 19.66MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/2019-Gudemann/refPred1.smt2 | 0.060s | 19.744MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0970a_true-unreach-call.c_0.smt2 | 0.060s | 19.604MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_while_true-unreach-call.i_2.smt2 | 0.060s | 19.676MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_while_true-unreach-call.i_1.smt2 | 0.060s | 19.576MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_7.smt2 | 0.060s | 19.604MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_bad_for_false-unreach-call.i_3.smt2 | 0.060s | 19.628MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Muller_Kahan_true-unreach-call_true-termination.c_3.smt2 | 0.060s | 19.668MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/sqrt_Newton_pseudoconstant_true-unreach-call.c_188.smt2 | 0.060s | 19.848MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_bad_while_false-unreach-call.i_3.smt2 | 0.061s | 19.7MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_bad_while_false-unreach-call.i_AllErrorsAtOnce_Iteration3_TraceCheck_0.smt2 | 0.061s | 19.984MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_5_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.061s | 19.652MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_7_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.061s | 19.596MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_4_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.061s | 19.728MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_4_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.061s | 19.6MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_2_false-unreach-call_true-termination.i_0.smt2 | 0.061s | 19.628MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_8_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.061s | 19.828MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0470_true-unreach-call.c_2.smt2 | 0.062s | 19.624MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0686b_true-unreach-call.c_0.smt2 | 0.062s | 19.592MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_4_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.062s | 19.688MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_0.smt2 | 0.062s | 19.684MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0920b_true-unreach-call.c_0.smt2 | 0.063s | 19.708MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_2_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.071s | 19.84MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_3_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.072s | 20.388MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0490b_true-unreach-call.c_1.smt2 | 0.074s | 19.596MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_true-unreach-call.i_3.smt2 | 0.075s | 20.076MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_6_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.079s | 19.864MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_1.smt2 | 0.080s | 20.096MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_6_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.083s | 20.076MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0931_true-unreach-call.c_0.smt2 | 0.084s | 20.092MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_5.smt2 | 0.084s | 19.836MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_1_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.088s | 19.824MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0931_true-unreach-call.c_0.smt2 | 0.090s | 19.84MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_315.smt2 | 0.090s | 19.816MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_3_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.092s | 19.56MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/cos_polynomial_true-unreach-call_true-termination.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.095s | 20.076MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0920b_true-unreach-call.c_0.smt2 | 0.095s | 19.984MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_8_true-unreach-call_true-termination.i_0.smt2 | 0.096s | 19.616MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_6_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.099s | 19.712MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_4_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.103s | 19.592MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c_5.smt2 | 0.104s | 20.08MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0971_true-unreach-call.c_1.smt2 | 0.105s | 20.068MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_179.smt2 | 0.108s | 19.856MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_1_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.110s | 19.86MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/filter2_true-unreach-call.c_11.smt2 | 0.110s | 19.956MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_0.smt2 | 0.114s | 19.676MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0490a_true-unreach-call.c_1.smt2 | 0.115s | 19.876MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_0.smt2 | 0.115s | 20.052MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/sqrt_Householder_interval_true-unreach-call.c_4.smt2 | 0.118s | 20.1MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_biNewton_pseudoconstant_true-unreach-call.c_2.smt2 | 0.119s | 19.744MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0872a_true-unreach-call.c_4.smt2 | 0.121s | 19.844MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Rump_double_true-unreach-call_true-termination.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.121s | 20.096MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0550b_true-unreach-call.c_8.smt2 | 0.122s | 19.924MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_4.smt2 | 0.123s | 19.604MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_2.smt2 | 0.124s | 19.892MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0883_true-unreach-call.c_1.smt2 | 0.124s | 19.596MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Newton_pseudoconstant_true-unreach-call.c_0.smt2 | 0.125s | 19.888MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_3.smt2 | 0.125s | 19.86MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_4.smt2 | 0.125s | 19.836MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_3.smt2 | 0.125s | 19.628MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0530a_true-unreach-call.c_1.smt2 | 0.126s | 19.728MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_interval_true-unreach-call.c_4.smt2 | 0.126s | 19.612MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c_0.smt2 | 0.127s | 20.16MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_biNewton_pseudoconstant_true-unreach-call.c_4.smt2 | 0.127s | 19.84MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_true-unreach-call.i_2.smt2 | 0.129s | 19.864MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_3.smt2 | 0.129s | 19.92MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Muller_Kahan_true-unreach-call_true-termination.c_0.smt2 | 0.130s | 19.868MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_bad_while_false-unreach-call.i_0.smt2 | 0.130s | 19.876MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_7_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.130s | 19.82MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_while_true-unreach-call.i_AllErrorsAtOnce_Iteration3_TraceCheck_0.smt2 | 0.131s | 19.64MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0920b_true-unreach-call.c_1.smt2 | 0.131s | 19.852MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0310_true-unreach-call.c_0.smt2 | 0.133s | 19.6MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_422.smt2 | 0.134s | 19.82MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_5_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.135s | 20.124MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_8_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.137s | 19.824MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/sqrt_biNewton_pseudoconstant_true-unreach-call.c_4.smt2 | 0.138s | 19.604MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_2_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.139s | 19.596MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_7_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.140s | 19.604MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_interval_true-unreach-call.c_2.smt2 | 0.141s | 19.828MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_3_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.142s | 19.604MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0970b_true-unreach-call.c_1.smt2 | 0.143s | 19.892MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float21_true-unreach-call.i_0.smt2 | 0.143s | 20.072MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_true-unreach-call.i_4.smt2 | 0.143s | 19.608MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0530a_true-unreach-call.c_3.smt2 | 0.144s | 19.82MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_interval_true-unreach-call.c_3.smt2 | 0.144s | 19.516MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_8_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.145s | 19.6MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_true-unreach-call.i_1.smt2 | 0.147s | 20.076MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/filter2_set_true-unreach-call.c_11.smt2 | 0.147s | 19.68MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/inv_Newton_false-unreach-call.c.p+cfa-reducer.c_0.smt2 | 0.152s | 19.88MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_true-unreach-call.i_5.smt2 | 0.154s | 19.604MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.154s | 19.572MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_6.smt2 | 0.165s | 19.6MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_9.smt2 | 0.166s | 20.1MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0470_true-unreach-call.c_8.smt2 | 0.166s | 19.652MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_2_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.166s | 19.6MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_biNewton_pseudoconstant_true-unreach-call.c_0.smt2 | 0.166s | 19.664MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/inv_Newton_false-unreach-call.c_0.smt2 | 0.166s | 20.436MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+lhb-reducer.c_3.smt2 | 0.166s | 20.38MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_1_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.166s | 19.6MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_interval_true-unreach-call.c_5.smt2 | 0.166s | 19.964MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float-div1_true-unreach-call.i_1.smt2 | 0.166s | 20.196MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c_2.smt2 | 0.166s | 19.716MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_5_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.166s | 19.628MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_11.smt2 | 0.166s | 19.64MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_7_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.167s | 19.888MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter2_set_true-unreach-call_true-termination.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.167s | 19.6MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.167s | 20.112MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_2.smt2 | 0.167s | 19.86MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0920b_true-unreach-call.c_3.smt2 | 0.167s | 19.856MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_bad_for_false-unreach-call.i_0.smt2 | 0.167s | 19.592MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0310_true-unreach-call.c_2.smt2 | 0.167s | 19.6MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_17.smt2 | 0.167s | 19.64MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0550b_true-unreach-call.c_0.smt2 | 0.167s | 20.104MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0320_true-unreach-call.c_8.smt2 | 0.167s | 19.988MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Double_div_true-unreach-call.i_AllErrorsAtOnce_Iteration2_TraceCheck_0.smt2 | 0.167s | 19.652MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_2.smt2 | 0.167s | 19.52MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.p+cfa-reducer.c_0.smt2 | 0.167s | 19.74MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/sqrt_Householder_constant_true-unreach-call.c_4.smt2 | 0.167s | 19.6MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_poly_true-unreach-call_true-termination.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.168s | 19.9MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_9.smt2 | 0.168s | 19.756MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_8.smt2 | 0.170s | 20.052MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_for_true-unreach-call.i_4.smt2 | 0.171s | 19.864MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_10.smt2 | 0.172s | 19.848MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_biNewton_pseudoconstant_true-unreach-call.c_1.smt2 | 0.172s | 19.856MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0960a_true-unreach-call.c_0.smt2 | 0.172s | 19.612MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_8_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.172s | 19.836MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_68.smt2 | 0.172s | 20.06MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/sqrt_Newton_pseudoconstant_true-unreach-call.c_4.smt2 | 0.172s | 19.7MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0960b_true-unreach-call.c_1.smt2 | 0.173s | 19.6MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_bad_for_false-unreach-call.i_4.smt2 | 0.173s | 19.892MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_5_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.173s | 19.608MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0520_true-unreach-call.c_6.smt2 | 0.173s | 19.84MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_2_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.173s | 19.636MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_for_true-unreach-call.i_1.smt2 | 0.174s | 19.816MiB| unknown | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/arctan_Pade_true-unreach-call_true-termination.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.176s | 19.88MiB| unknown | 0 | | |