# . * SAT 23 * UNSAT 10 * TIMEOUT 15 * UNKNOWN 30 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/ANIA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-ANIA.tar.zst-downl
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/ANIA.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_5.smt2 | 0.025s | 20.86MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_50.smt2 | 0.025s | 20.36MiB| unsat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_20.smt2 | 0.025s | 20.876MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_8.smt2 | 0.026s | 20.684MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sll2n_insert_unequal.i_75.smt2 | 0.026s | 20.612MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_16.smt2 | 0.026s | 20.82MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_4.smt2 | 0.027s | 20.92MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_6.smt2 | 0.027s | 21.104MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_11.smt2 | 0.027s | 20.616MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_3.smt2 | 0.027s | 20.944MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_9.smt2 | 0.027s | 21.132MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_8.smt2 | 0.027s | 20.872MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_7.smt2 | 0.028s | 21.132MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_7.smt2 | 0.030s | 21.392MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_10.smt2 | 0.031s | 20.876MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_10.smt2 | 0.033s | 21.632MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_5.smt2 | 0.033s | 21.128MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_10.smt2 | 0.040s | 21.172MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_57.smt2 | 0.040s | 20.78MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_5.smt2 | 0.041s | 21.156MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_55.smt2 | 0.042s | 20.848MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_8.smt2 | 0.042s | 20.996MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sll2n_insert_unequal.i_76.smt2 | 0.042s | 21.124MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_17.smt2 | 0.044s | 20.88MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_9.smt2 | 0.046s | 20.676MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_4.smt2 | 0.046s | 20.784MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_6.smt2 | 0.048s | 20.728MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sll2n_insert_unequal.i_74.smt2 | 0.052s | 20.656MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_11.smt2 | 0.052s | 20.82MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_2.smt2 | 0.053s | 20.896MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sum_array-2-2.i_2.smt2 | 0.054s | 21.068MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_7.smt2 | 0.054s | 20.824MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_53.smt2 | 0.056s | 20.932MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sum_array-2-2.i_1.smt2 | 0.056s | 21.256MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/prefixsum_rec.c_12.smt2 | 0.056s | 20.808MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_9.smt2 | 0.056s | 21.012MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_7.smt2 | 0.056s | 20.808MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/cs_szymanski.i_3.smt2 | 0.056s | 20.92MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_6.smt2 | 0.057s | 20.68MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_5.smt2 | 0.058s | 20.928MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_52.smt2 | 0.059s | 20.832MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/cs_szymanski.i_4.smt2 | 0.059s | 20.92MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dancing.i_1.smt2 | 0.060s | 21.128MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_4.smt2 | 0.060s | 20.648MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_10.smt2 | 0.060s | 20.664MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_56.smt2 | 0.061s | 20.908MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_6.smt2 | 0.061s | 21.288MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_1.smt2 | 0.061s | 20.888MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_8.smt2 | 0.062s | 21.272MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/prefixsum_rec.c_11.smt2 | 0.062s | 20.964MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_9.smt2 | 0.063s | 21.16MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_9.smt2 | 0.064s | 21.404MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/running_example.i_6.smt2 | 0.071s | 21.428MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_1-2.c_AllErrorsAtOnce_Iteration3_0.smt2 | 0.084s | 21.964MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/mcmillan2006.i_AllErrorsAtOnce_Iteration5_0.smt2 | 0.103s | 22.708MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/condm.c_AllErrorsAtOnce_Iteration9_0.smt2 | 0.151s | 24.108MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_doub_access_init_const.c_AllErrorsAtOnce_Iteration3_0.smt2 | 0.211s | 25.748MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_shadowinit.i_AllErrorsAtOnce_Iteration5_0.smt2 | 0.272s | 24.44MiB| unsat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sum_array-2-2.i_0.smt2 | 1.014s | 103.0MiB| sat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/benchmark52_polynomial.i_AllErrorsAtOnce_Iteration3_0.smt2 | 1.052s | 22.208MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/rew.c_AllErrorsAtOnce_Iteration5_0.smt2 | 1.314s | 26.148MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/sep20-1.i_AllErrorsAtOnce_Iteration23_0.smt2 | 2.526s | 41.828MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/skipped.c_AllErrorsAtOnce_Iteration5_0.smt2 | 4.997s | 38.78MiB| unsat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/prefixsum_rec.c_25.smt2 | 20.017s | 41.696MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/flag_loopdep_simple.i_AllErrorsAtOnce_Iteration8_0.smt2 | 20.020s | 97.568MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/linear_sea.ch.c_AllErrorsAtOnce_Iteration8_0.smt2 | 20.028s | 45.1MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/sorting_selectionsort_ground-2.i_AllErrorsAtOnce_Iteration8_0.smt2 | 20.029s | 52.992MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_3.c_AllErrorsAtOnce_Iteration3_0.smt2 | 20.031s | 68.64MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_4.c.v+lh-reducer.c_AllErrorsAtOnce_Iteration3_0.smt2 | 20.032s | 71.156MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_4.i_AllErrorsAtOnce_Iteration5_0.smt2 | 20.033s | 80.028MiB| timeout | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/tree_max.c_0.smt2 | 20.045s | 37.088MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_of_struct_break.i_AllErrorsAtOnce_Iteration5_0.smt2 | 20.046s | 65.06MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_4.c.v+cfa-reducer.c_AllErrorsAtOnce_Iteration4_0.smt2 | 20.048s | 61.244MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/partial_lesser_bound-1.i_AllErrorsAtOnce_Iteration3_0.smt2 | 20.049s | 75.148MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_2.c_AllErrorsAtOnce_Iteration3_0.smt2 | 20.056s | 119.0MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/nr2.c_AllErrorsAtOnce_Iteration8_0.smt2 | 20.056s | 195.0MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/rewnifrev2.c_AllErrorsAtOnce_Iteration5_0.smt2 | 20.060s | 348.0MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_4.c_AllErrorsAtOnce_Iteration3_0.smt2 | 20.067s | 433.0MiB| timeout | 0 | | |