# . * SAT 201 * UNSAT 12 * TIMEOUT 52 * UNKNOWN 1 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/BVFPLRA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-BVFPLRA.tar.zst-do
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/BVFPLRA.tar.zst?download=1
Z3 commit message: update tptp front-end
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0620a_true-unreach-call.c_5.smt2 | 0.017s | 20.068MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0931_true-unreach-call.c_4.smt2 | 0.018s | 19.756MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0470_true-unreach-call.c_4.smt2 | 0.018s | 20.552MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_9.smt2 | 0.018s | 20.048MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0490a_true-unreach-call.c_12.smt2 | 0.019s | 20.612MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0832a_true-unreach-call.c_0.smt2 | 0.019s | 20.264MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0686a_true-unreach-call.c_6.smt2 | 0.019s | 20.604MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_10.smt2 | 0.019s | 20.016MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0883_true-unreach-call.c_8.smt2 | 0.019s | 19.796MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_4.smt2 | 0.020s | 20.796MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1092a_true-unreach-call.c_5.smt2 | 0.020s | 20.656MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_3.smt2 | 0.020s | 20.556MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0920b_true-unreach-call.c_2.smt2 | 0.020s | 20.484MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_6.smt2 | 0.020s | 20.424MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_4.smt2 | 0.020s | 20.396MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0686a_true-unreach-call.c_3.smt2 | 0.020s | 20.224MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_7.smt2 | 0.021s | 20.516MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_2.smt2 | 0.021s | 20.22MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0920b_true-unreach-call.c_3.smt2 | 0.021s | 20.632MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_18.smt2 | 0.021s | 20.608MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0910a_true-unreach-call.c_4.smt2 | 0.021s | 20.56MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_6.smt2 | 0.021s | 20.408MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_12.smt2 | 0.021s | 20.444MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_16.smt2 | 0.021s | 20.516MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_16.smt2 | 0.021s | 20.488MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_10.smt2 | 0.021s | 20.552MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0910a_true-unreach-call.c_6.smt2 | 0.021s | 20.704MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0530a_true-unreach-call.c_8.smt2 | 0.021s | 21.164MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0930_true-unreach-call.c_2.smt2 | 0.022s | 20.212MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_12.smt2 | 0.022s | 20.752MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0883_true-unreach-call.c_8.smt2 | 0.022s | 20.3MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0470_true-unreach-call.c_14.smt2 | 0.022s | 20.432MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0920b_true-unreach-call.c_2.smt2 | 0.022s | 20.46MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0960a_true-unreach-call.c_4.smt2 | 0.023s | 21.064MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_6.smt2 | 0.023s | 20.384MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_8.smt2 | 0.023s | 20.592MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0832_true-unreach-call.c_8.smt2 | 0.023s | 21.188MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_17.smt2 | 0.024s | 20.692MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_1.smt2 | 0.024s | 20.36MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0910a_true-unreach-call.c_2.smt2 | 0.025s | 20.808MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_7.smt2 | 0.025s | 20.868MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0832b_true-unreach-call.c_0.smt2 | 0.025s | 20.568MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_9.smt2 | 0.025s | 20.676MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0470_true-unreach-call.c_3.smt2 | 0.025s | 20.352MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_14.smt2 | 0.027s | 20.816MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_11.smt2 | 0.028s | 20.568MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0960a_true-unreach-call.c_7.smt2 | 0.029s | 20.436MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_21.smt2 | 0.030s | 21.032MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1092a_true-unreach-call.c_4.smt2 | 0.032s | 20.148MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0931_true-unreach-call.c_1.smt2 | 0.034s | 22.14MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0920b_true-unreach-call.c_4.smt2 | 0.034s | 20.624MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0910a_true-unreach-call.c_11.smt2 | 0.034s | 19.856MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0883_true-unreach-call.c_3.smt2 | 0.035s | 19.784MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_11.smt2 | 0.035s | 20.66MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_2.smt2 | 0.036s | 19.8MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0685a_true-unreach-call.c_2.smt2 | 0.037s | 20.516MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_9.smt2 | 0.038s | 20.592MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_4.smt2 | 0.038s | 19.996MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0960a_true-unreach-call.c_3.smt2 | 0.038s | 20.768MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0490a_true-unreach-call.c_2.smt2 | 0.039s | 20.228MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0250a_true-unreach-call.c_5.smt2 | 0.039s | 19.912MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0920b_true-unreach-call.c_4.smt2 | 0.039s | 20.112MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0490a_true-unreach-call.c_7.smt2 | 0.039s | 20.22MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1092a_true-unreach-call.c_1.smt2 | 0.039s | 20.528MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_2.smt2 | 0.039s | 20.16MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_7.smt2 | 0.040s | 20.332MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0460_true-unreach-call.c_7.smt2 | 0.040s | 19.72MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_6.smt2 | 0.040s | 20.34MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_5.smt2 | 0.040s | 20.844MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0910a_true-unreach-call.c_8.smt2 | 0.040s | 20.556MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_18.smt2 | 0.040s | 20.552MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0250a_true-unreach-call.c_4.smt2 | 0.040s | 20.048MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_3.smt2 | 0.040s | 20.08MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0883_true-unreach-call.c_6.smt2 | 0.040s | 20.584MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_11.smt2 | 0.040s | 21.304MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_4.smt2 | 0.040s | 20.448MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_5.smt2 | 0.041s | 20.256MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_17.smt2 | 0.041s | 20.6MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_21.smt2 | 0.041s | 20.04MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_0.smt2 | 0.042s | 20.576MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_17.smt2 | 0.042s | 21.068MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_8.smt2 | 0.042s | 21.276MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_8.smt2 | 0.043s | 20.784MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0910a_true-unreach-call.c_3.smt2 | 0.043s | 20.38MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0682a_true-unreach-call.c_2.smt2 | 0.043s | 20.524MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1270b_true-unreach-call.c_10.smt2 | 0.043s | 23.368MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0686a_true-unreach-call.c_2.smt2 | 0.043s | 20.512MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0490a_true-unreach-call.c_5.smt2 | 0.043s | 20.108MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_24.smt2 | 0.043s | 20.552MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_18.smt2 | 0.044s | 20.812MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0910a_true-unreach-call.c_1.smt2 | 0.044s | 20.064MiB| unsat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0910a_true-unreach-call.c_5.smt2 | 0.044s | 20.392MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float-rounding1_true-unreach-call.i_0.smt2 | 0.044s | 20.824MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0910a_true-unreach-call.c_7.smt2 | 0.044s | 20.072MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0260_true-unreach-call.c_6.smt2 | 0.045s | 20.352MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_20.smt2 | 0.045s | 20.56MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_20.smt2 | 0.045s | 20.852MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_5.smt2 | 0.045s | 20.012MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1092a_true-unreach-call.c_6.smt2 | 0.045s | 20.348MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float-rounding1_true-unreach-call.i_1.smt2 | 0.045s | 21.124MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0870b_true-unreach-call.c_2.smt2 | 0.045s | 20.3MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_8.smt2 | 0.045s | 21.024MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0960a_true-unreach-call.c_6.smt2 | 0.045s | 20.504MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_16.smt2 | 0.045s | 20.808MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_5.smt2 | 0.046s | 20.356MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0960a_true-unreach-call.c_2.smt2 | 0.046s | 20.304MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_5.smt2 | 0.046s | 20.736MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0685a_true-unreach-call.c_10.smt2 | 0.046s | 20.3MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1092a_true-unreach-call.c_7.smt2 | 0.046s | 20.444MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1092a_true-unreach-call.c_3.smt2 | 0.047s | 20.56MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_6.smt2 | 0.047s | 20.66MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_2.smt2 | 0.047s | 20.528MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0920b_true-unreach-call.c_5.smt2 | 0.047s | 21.0MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_2.smt2 | 0.048s | 20.312MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0883_true-unreach-call.c_7.smt2 | 0.048s | 20.288MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0621b_true-unreach-call.c_5.smt2 | 0.048s | 20.712MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0460_true-unreach-call.c_5.smt2 | 0.048s | 19.828MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1092a_true-unreach-call.c_2.smt2 | 0.048s | 20.268MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_10.smt2 | 0.049s | 20.816MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_20.smt2 | 0.049s | 21.348MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_8.smt2 | 0.050s | 20.624MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1092a_true-unreach-call.c_0.smt2 | 0.050s | 20.564MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_19.smt2 | 0.050s | 20.776MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0960a_true-unreach-call.c_1.smt2 | 0.051s | 20.612MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_10.smt2 | 0.051s | 20.664MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_26.smt2 | 0.052s | 20.812MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0876_true-unreach-call.c_19.smt2 | 0.052s | 21.036MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_16.smt2 | 0.052s | 21.324MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0910a_true-unreach-call.c_10.smt2 | 0.052s | 20.872MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_12.smt2 | 0.053s | 20.892MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0875_true-unreach-call.c_20.smt2 | 0.054s | 21.288MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0880_true-unreach-call.c_9.smt2 | 0.055s | 20.824MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_27.smt2 | 0.055s | 20.532MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_20.smt2 | 0.055s | 21.064MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_3.smt2 | 0.055s | 20.568MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0960a_true-unreach-call.c_5.smt2 | 0.058s | 20.564MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_25.smt2 | 0.058s | 20.044MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0877_true-unreach-call.c_10.smt2 | 0.063s | 20.808MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0910a_true-unreach-call.c_9.smt2 | 0.069s | 20.908MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/filter1_true-unreach-call.c_348.smt2 | 0.070s | 26.6MiB| unsat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0931_true-unreach-call.c_2.smt2 | 0.075s | 23.528MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_7.smt2 | 0.076s | 23.064MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_15.smt2 | 0.077s | 20.804MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/filter1_true-unreach-call.c_344.smt2 | 0.079s | 26.536MiB| unsat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1052b_true-unreach-call.c_0.smt2 | 0.111s | 24.656MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1052b_true-unreach-call.c_1.smt2 | 0.124s | 24.74MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float-rounding1_true-unreach-call.i_3.smt2 | 0.151s | 27.368MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0931_true-unreach-call.c_3.smt2 | 0.170s | 26.788MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1091_true-unreach-call.c_0.smt2 | 0.251s | 27.728MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float-rounding1_true-unreach-call.i_2.smt2 | 0.271s | 29.22MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_960.smt2 | 0.288s | 26.484MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1051_true-unreach-call.c_0.smt2 | 0.325s | 27.644MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0270a_true-unreach-call.c_13.smt2 | 0.336s | 29.628MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0670_true-unreach-call.c_7.smt2 | 0.345s | 27.376MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/inv_square_true-unreach-call.c_87.smt2 | 0.709s | 27.284MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/inv_square_true-unreach-call.c_79.smt2 | 0.712s | 27.264MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1063.smt2 | 0.732s | 28.576MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1699.smt2 | 0.848s | 27.088MiB| unsat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1466.smt2 | 0.946s | 29.564MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1081.smt2 | 1.514s | 38.232MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1000.smt2 | 1.531s | 28.644MiB| unsat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1098.smt2 | 1.541s | 31.3MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1100.smt2 | 1.570s | 31.336MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/float20_true-unreach-call.i_54.smt2 | 1.621s | 42.32MiB| sat | 0 | | | |non-incremental/BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter1.c.p+cfa-reducer.c_3.smt2 | 1.730s | 31.108MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1457.smt2 | 1.731s | 29.828MiB| sat | 0 | | | |non-incremental/BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter1.c_7.smt2 | 1.768s | 30.972MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_877.smt2 | 1.902s | 29.868MiB| unsat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0530b_true-unreach-call.c_4.smt2 | 2.161s | 36.74MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1104.smt2 | 2.232s | 36.524MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/filter1_true-unreach-call.c_281.smt2 | 2.242s | 31.188MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_875.smt2 | 2.437s | 29.936MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1012a_true-unreach-call.c_5.smt2 | 2.758s | 37.176MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1768.smt2 | 2.759s | 31.268MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1012b_true-unreach-call.c_5.smt2 | 2.790s | 36.888MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1012a_true-unreach-call.c_4.smt2 | 2.795s | 37.096MiB| sat | 0 | | | |non-incremental/BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter1.c.p+cfa-reducer.c_5.smt2 | 2.815s | 31.192MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1012a_true-unreach-call.c_0.smt2 | 2.823s | 36.572MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_1012a_true-unreach-call.c_20.smt2 | 3.041s | 37.064MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_tight_true-unreach-call.c_113.smt2 | 3.125s | 66.224MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1067.smt2 | 3.692s | 37.808MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_159.smt2 | 4.232s | 152.0MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/float-div1_true-unreach-call.i_366.smt2 | 4.498s | 96.876MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_2065.smt2 | 4.677s | 36.564MiB| unsat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_964.smt2 | 5.039s | 33.676MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_2067.smt2 | 5.269s | 36.952MiB| unsat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_tight_true-unreach-call.c_38.smt2 | 5.986s | 98.0MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_1264.smt2 | 6.531s | 39.284MiB| unsat | 0 | | | |non-incremental/BVFPLRA/20230321-UltimateAutomizerSvcomp2023/loop3.c_9.smt2 | 6.559s | 68.708MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/float_req_bl_0930_true-unreach-call.c_8.smt2 | 7.938s | 41.148MiB| sat | 0 | | | |non-incremental/BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter1.c.p+cfa-reducer.c_4.smt2 | 8.205s | 38.02MiB| sat | 0 | | | |non-incremental/BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter1.c_8.smt2 | 8.609s | 52.792MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1697.smt2 | 8.794s | 46.092MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/filter1_true-unreach-call.c_342.smt2 | 9.268s | 52.124MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sin_interpolated_smallrange_true-unreach-call.c_0.smt2 | 9.521s | 67.948MiB| unknown | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/rlim_invariant_true-unreach-call.c_1073.smt2 | 9.606s | 60.084MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/bary_diverge_true-unreach-call_true-termination.c_2.smt2 | 9.967s | 38.004MiB| unsat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_158.smt2 | 10.651s | 101.0MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_2063.smt2 | 11.054s | 44.176MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/filter1_true-unreach-call.c_352.smt2 | 11.114s | 55.352MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/float-div1_true-unreach-call.i_365.smt2 | 11.687s | 77.324MiB| sat | 0 | | | |non-incremental/BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter1.c_9.smt2 | 11.913s | 53.364MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_3021.smt2 | 13.083s | 62.784MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_tight_true-unreach-call.c_37.smt2 | 13.911s | 101.0MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_3038.smt2 | 14.341s | 61.552MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_40.smt2 | 14.471s | 99.0MiB| unsat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_3026.smt2 | 15.640s | 79.0MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_3028.smt2 | 17.469s | 60.804MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_3029.smt2 | 17.979s | 70.272MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_tight_true-unreach-call.c_39.smt2 | 18.565s | 102.0MiB| unsat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_38.smt2 | 18.569s | 105.0MiB| sat | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/bary_diverge_true-unreach-call_true-termination.c_0.smt2 | 18.911s | 88.596MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_3022.smt2 | 19.093s | 71.808MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/float-div1_true-unreach-call.i_563.smt2 | 19.844s | 77.192MiB| sat | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_tight_true-unreach-call.c_135.smt2 | 20.009s | 66.224MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+nlh-reducer.c_5.smt2 | 20.010s | 95.344MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+nlh-reducer.c_3.smt2 | 20.010s | 90.5MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/bary_diverge_true-unreach-call_true-termination.c_1.smt2 | 20.010s | 64.58MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_10.smt2 | 20.010s | 51.336MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_3024.smt2 | 20.010s | 65.472MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_115.smt2 | 20.010s | 71.008MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_117.smt2 | 20.010s | 71.304MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sin_interpolated_smallrange_true-unreach-call.c_5.smt2 | 20.011s | 84.512MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/filter1_true-unreach-call.c_182.smt2 | 20.011s | 54.088MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_tight_true-unreach-call.c_117.smt2 | 20.011s | 73.216MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_112.smt2 | 20.011s | 73.528MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_tight_true-unreach-call.c_115.smt2 | 20.013s | 70.708MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_160.smt2 | 20.013s | 101.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_tight_true-unreach-call.c_116.smt2 | 20.013s | 70.048MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_41.smt2 | 20.013s | 100.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_3027.smt2 | 20.015s | 56.02MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_36.smt2 | 20.015s | 102.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_157.smt2 | 20.016s | 137.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_114.smt2 | 20.016s | 71.892MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_tight_true-unreach-call.c_114.smt2 | 20.017s | 71.236MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+nlh-reducer.c_6.smt2 | 20.018s | 147.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_156.smt2 | 20.018s | 101.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_tight_true-unreach-call.c_41.smt2 | 20.019s | 101.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter1.c_6.smt2 | 20.020s | 55.06MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_3023.smt2 | 20.020s | 75.68MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/bary_diverge_true-unreach-call.c_3025.smt2 | 20.020s | 89.276MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0620a_true-unreach-call.c_4.smt2 | 20.022s | 294.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/filter1_true-unreach-call.c_175.smt2 | 20.023s | 55.876MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+nlh-reducer.c_2.smt2 | 20.024s | 108.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/float-div1_true-unreach-call.i_367.smt2 | 20.024s | 75.72MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_6.smt2 | 20.027s | 46.968MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_39.smt2 | 20.027s | 104.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+nlh-reducer.c_4.smt2 | 20.031s | 116.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call_true-termination.c_5.smt2 | 20.031s | 84.456MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call_true-termination.c_0.smt2 | 20.031s | 89.712MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sin_interpolated_smallrange_true-unreach-call.c_1.smt2 | 20.031s | 64.572MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter1.c.p+cfa-reducer.c_2.smt2 | 20.031s | 54.848MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter1.c_2.smt2 | 20.032s | 57.324MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sin_interpolated_smallrange_true-unreach-call.c_2.smt2 | 20.033s | 64.648MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sin_interpolated_smallrange_true-unreach-call.c_4.smt2 | 20.034s | 84.712MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_5.smt2 | 20.035s | 51.408MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20230321-UltimateAutomizerSvcomp2023/filter1.c.p+cfa-reducer.c_1.smt2 | 20.035s | 55.736MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_3.smt2 | 20.036s | 44.928MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/sin_interpolated_smallrange_true-unreach-call.c_3.smt2 | 20.036s | 69.508MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/filter1_true-unreach-call.c.v+lhb-reducer.c_0.smt2 | 20.037s | 84.736MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/trunc_nondet_2_true-unreach-call.i_12.smt2 | 20.037s | 51.112MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20170501-Heizmann-UltimateAutomizer/zonotope_loose_true-unreach-call.c_161.smt2 | 20.042s | 71.6MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_0620a_true-unreach-call.c_6.smt2 | 20.044s | 298.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_26.smt2 | 20.307s | 4537.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_22.smt2 | 20.322s | 4341.0MiB| timeout | 0 | | | |non-incremental/BVFPLRA/20190429-UltimateAutomizerSvcomp2019/double_req_bl_1052d_true-unreach-call.c_23.smt2 | 20.447s | 6680.0MiB| timeout | 0 | | |