# . * SAT 78 * UNSAT 33 * TIMEOUT 66 * UNKNOWN 0 * 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: 4a90d3105054796562079406e125b9480ac3472b
Z3 branch: master
Z3 options: "-T:20 model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_BVFPLRA.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_AllErrorsAtOnce_Iteration2_TraceCheck_0.smt2 | 0.033s | 19.636MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/schanda/spark/zeros_consistent_3.smt2 | 0.042s | 19.784MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_6.smt2 | 0.043s | 19.844MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_0.smt2 | 0.054s | 19.852MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_7.smt2 | 0.055s | 19.592MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_5.smt2 | 0.058s | 19.852MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Rump_double_true-unreach-call_true-termination.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.084s | 19.604MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Double_div_bad_false-unreach-call.i_AllErrorsAtOnce_Iteration2_TraceCheck_0.smt2 | 0.087s | 19.732MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_true-unreach-call.i_4.smt2 | 0.096s | 19.632MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_bad_while_false-unreach-call.i_AllErrorsAtOnce_Iteration3_TraceCheck_0.smt2 | 0.100s | 19.84MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_while_true-unreach-call.i_AllErrorsAtOnce_Iteration3_TraceCheck_0.smt2 | 0.100s | 19.656MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_2.smt2 | 0.103s | 19.852MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_1.smt2 | 0.105s | 19.808MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 0.111s | 19.54MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_biNewton_pseudoconstant_true-unreach-call.c_2.smt2 | 0.117s | 29.716MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_true-unreach-call.i_5.smt2 | 0.174s | 40.06MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_true-unreach-call.i_3.smt2 | 0.205s | 40.024MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_true-unreach-call.i_0.smt2 | 0.252s | 39.976MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float21_true-unreach-call.i_1.smt2 | 0.416s | 33.096MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float21_true-unreach-call.i_0.smt2 | 0.441s | 32.324MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Double_div_true-unreach-call.i_AllErrorsAtOnce_Iteration2_TraceCheck_0.smt2 | 0.474s | 63.064MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_4.smt2 | 0.645s | 44.984MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_interval_true-unreach-call.c_4.smt2 | 0.719s | 108.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_interval_true-unreach-call.c_5.smt2 | 0.723s | 108.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_for_true-unreach-call.i_4.smt2 | 0.776s | 36.492MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_true-unreach-call.i_1.smt2 | 0.820s | 59.356MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_interval_true-unreach-call.c_2.smt2 | 0.873s | 108.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_interval_true-unreach-call.c_3.smt2 | 1.008s | 108.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_10.smt2 | 1.020s | 72.788MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_bad_while_false-unreach-call.i_3.smt2 | 1.069s | 51.732MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_3.smt2 | 1.073s | 73.108MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_true-unreach-call.i_2.smt2 | 1.077s | 59.316MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_bad_for_false-unreach-call.i_4.smt2 | 1.139s | 37.2MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_bad_for_false-unreach-call.i_3.smt2 | 1.174s | 44.944MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0920b_true-unreach-call.c_3.smt2 | 1.255s | 82.128MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_bad_for_false-unreach-call.i_0.smt2 | 1.318s | 80.324MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_for_true-unreach-call.i_1.smt2 | 1.364s | 65.416MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_bad_while_false-unreach-call.i_0.smt2 | 1.375s | 64.9MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_while_true-unreach-call.i_2.smt2 | 1.506s | 51.776MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.p+cfa-reducer.c_0.smt2 | 1.608s | 114.0MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_5_true-unreach-call_true-termination.i_0.smt2 | 1.629s | 126.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+lhb-reducer.c_3.smt2 | 1.636s | 113.0MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c_5.smt2 | 1.744s | 110.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_9.smt2 | 1.909s | 73.368MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_biNewton_pseudoconstant_true-unreach-call.c_1.smt2 | 1.922s | 338.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_interval_true-unreach-call.c_1.smt2 | 1.951s | 132.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Float_div_bad_false-unreach-call.i_8.smt2 | 2.042s | 73.164MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/inv_Newton_false-unreach-call.c.p+cfa-reducer.c_1.smt2 | 2.046s | 148.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float-div1_true-unreach-call.i_1.smt2 | 2.268s | 111.0MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0684a_true-unreach-call.c_1.smt2 | 2.339s | 338.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 2.349s | 28.696MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0661a_true-unreach-call.c_0.smt2 | 2.440s | 338.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_2.smt2 | 2.531s | 37.396MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/inv_Newton_false-unreach-call.c_0.smt2 | 2.622s | 148.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_11.smt2 | 2.708s | 37.396MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float-div1_true-unreach-call.i_0.smt2 | 2.761s | 111.0MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_4.smt2 | 2.831s | 36.144MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_0.smt2 | 2.972s | 37.408MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0470_true-unreach-call.c_2.smt2 | 3.011s | 198.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_7.smt2 | 3.198s | 38.088MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_6_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 3.292s | 198.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_2_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 3.347s | 105.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_9.smt2 | 3.423s | 37.9MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0320_true-unreach-call.c_8.smt2 | 3.861s | 276.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0310_true-unreach-call.c_0.smt2 | 4.127s | 190.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/sqrt_Newton_pseudoconstant_true-unreach-call.c_188.smt2 | 4.187s | 279.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0960a_true-unreach-call.c_0.smt2 | 4.205s | 240.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0550b_true-unreach-call.c_0.smt2 | 4.227s | 190.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/inv_Newton_false-unreach-call.c.p+cfa-reducer.c_0.smt2 | 4.434s | 148.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0240a_true-unreach-call.c_0.smt2 | 4.889s | 207.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_0.smt2 | 5.240s | 240.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_1.smt2 | 5.445s | 241.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter2_set_true-unreach-call_true-termination.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 5.725s | 112.0MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_1_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 5.759s | 81.464MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0920b_true-unreach-call.c_1.smt2 | 6.032s | 246.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0470_true-unreach-call.c_8.smt2 | 6.474s | 200.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0931_true-unreach-call.c_0.smt2 | 6.586s | 237.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0872a_true-unreach-call.c_4.smt2 | 6.812s | 358.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c_1.smt2 | 7.324s | 480.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c_2.smt2 | 7.517s | 416.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_biNewton_pseudoconstant_true-unreach-call.c_4.smt2 | 7.570s | 410.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0920b_true-unreach-call.c_0.smt2 | 7.720s | 247.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0310_true-unreach-call.c_2.smt2 | 7.984s | 158.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_8_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 8.082s | 393.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c_0.smt2 | 8.125s | 559.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_1_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 8.151s | 109.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_7_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 9.035s | 202.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Newton_pseudoconstant_true-unreach-call.c_2.smt2 | 9.066s | 410.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0684a_true-unreach-call.c_0.smt2 | 9.342s | 602.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_5_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 9.411s | 203.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_8_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 9.411s | 202.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_8_true-unreach-call_true-termination.i_0.smt2 | 10.110s | 480.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_2.smt2 | 10.577s | 710.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_2_false-unreach-call_true-termination.i_0.smt2 | 10.589s | 479.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_17.smt2 | 12.109s | 689.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0550b_true-unreach-call.c_8.smt2 | 12.126s | 798.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0550b_true-unreach-call.c_4.smt2 | 12.517s | 797.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_poly_true-unreach-call_true-termination.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 13.846s | 98.548MiB| unsat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Muller_Kahan_true-unreach-call_true-termination.c_1.smt2 | 14.428s | 955.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/digits_while_true-unreach-call.i_1.smt2 | 14.533s | 244.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Muller_Kahan_true-unreach-call_true-termination.c_2.smt2 | 14.647s | 959.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_3.smt2 | 14.670s | 491.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0530a_true-unreach-call.c_7.smt2 | 15.136s | 801.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0971_true-unreach-call.c_1.smt2 | 15.223s | 174.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_3_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 15.346s | 108.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_179.smt2 | 15.567s | 976.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0882_true-unreach-call.c_1.smt2 | 16.278s | 400.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0330a_true-unreach-call.c_8.smt2 | 16.623s | 176.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/Rump_double.c_0.smt2 | 19.074s | 2696.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_7_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 19.878s | 392.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0530a_true-unreach-call.c_3.smt2 | 19.960s | 797.0MiB| sat | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/filter2_set_true-unreach-call.c_11.smt2 | 20.052s | 305.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_5_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.053s | 84.812MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter2.c_0.smt2 | 20.055s | 238.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter2_reinit.c_0.smt2 | 20.055s | 239.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_1_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.068s | 202.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0883_true-unreach-call.c_1.smt2 | 20.070s | 333.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_8_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.070s | 84.836MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/sqrt_Householder_constant_true-unreach-call.c_274.smt2 | 20.070s | 475.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_1_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.072s | 388.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0490a_true-unreach-call.c_1.smt2 | 20.072s | 640.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_4_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.072s | 109.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/sqrt_Householder_constant.c.p+cfa-reducer.c_2.smt2 | 20.072s | 553.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_7_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.074s | 82.568MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_3_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.074s | 204.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/sqrt_Householder_interval_true-unreach-call.c_4.smt2 | 20.074s | 473.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_6_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.076s | 83.568MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_3.smt2 | 20.077s | 676.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_6_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.077s | 111.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0490b.c_2.smt2 | 20.080s | 641.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/filter2_true-unreach-call.c_11.smt2 | 20.080s | 172.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_2_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.081s | 83.72MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0520_true-unreach-call.c_6.smt2 | 20.082s | 764.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_5_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.086s | 112.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0250a.c_4.smt2 | 20.086s | 646.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_6_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.094s | 391.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20230321-UltimateAutomizerSvcomp2023/double_req_bl_0490a.c_2.smt2 | 20.096s | 641.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_4_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.099s | 84.784MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_8_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.101s | 111.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sine_7_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.103s | 109.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/arctan_Pade_true-unreach-call_true-termination.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.106s | 540.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/square_3_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.107s | 82.76MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_315.smt2 | 20.109s | 947.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_430.smt2 | 20.109s | 943.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_3_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.111s | 389.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/cos_polynomial_true-unreach-call_true-termination.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.115s | 602.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_4_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.116s | 203.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_414.smt2 | 20.116s | 943.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_1_2_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.117s | 205.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/sqrt_Newton_pseudoconstant_true-unreach-call.c_4.smt2 | 20.122s | 291.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter2_set_true-unreach-call_true-termination.c_0.smt2 | 20.123s | 340.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_biNewton_pseudoconstant_true-unreach-call.c_0.smt2 | 20.132s | 769.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0686b_true-unreach-call.c_0.smt2 | 20.134s | 417.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_2_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.136s | 388.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0260_true-unreach-call.c_2.smt2 | 20.140s | 472.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/sqrt_Householder_constant_true-unreach-call.c_4.smt2 | 20.145s | 473.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0490b_true-unreach-call.c_1.smt2 | 20.149s | 637.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Householder_interval_true-unreach-call.c_0.smt2 | 20.153s | 523.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_4_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.160s | 386.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sqrt_Newton_pseudoconstant_true-unreach-call.c_0.smt2 | 20.161s | 344.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0920b_true-unreach-call.c_0.smt2 | 20.162s | 866.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Muller_Kahan_true-unreach-call_true-termination.c_0.smt2 | 20.163s | 939.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0833_true-unreach-call.c_3.smt2 | 20.164s | 676.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_446.smt2 | 20.164s | 947.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/newton_2_5_true-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.smt2 | 20.165s | 391.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/water_pid_true-unreach-call.c_372.smt2 | 20.165s | 939.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0970b_true-unreach-call.c_1.smt2 | 20.167s | 859.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0960b_true-unreach-call.c_1.smt2 | 20.169s | 864.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0530a_true-unreach-call.c_1.smt2 | 20.169s | 762.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/2019-Gudemann/refPred1.smt2 | 20.172s | 1886.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0931_true-unreach-call.c_0.smt2 | 20.173s | 859.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Muller_Kahan_true-unreach-call_true-termination.c_4.smt2 | 20.173s | 943.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/sqrt_biNewton_pseudoconstant_true-unreach-call.c_4.smt2 | 20.175s | 483.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/Muller_Kahan_true-unreach-call_true-termination.c_3.smt2 | 20.198s | 932.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0970a_true-unreach-call.c_0.smt2 | 20.202s | 863.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_68.smt2 | 20.212s | 943.0MiB| timeout | 0 | | | |non-incremental/QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/Muller_Kahan_true-unreach-call.c_422.smt2 | 20.223s | 976.0MiB| timeout | 0 | | |