# . * 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-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/ANIA.tar.zst?download=1
Z3 commit message: update tptp front-end
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_53.smt2 | 0.015s | 20.356MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_10.smt2 | 0.015s | 20.104MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/prefixsum_rec.c_11.smt2 | 0.015s | 20.272MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_20.smt2 | 0.015s | 20.312MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_55.smt2 | 0.016s | 20.296MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_5.smt2 | 0.016s | 20.208MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_11.smt2 | 0.016s | 20.444MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_16.smt2 | 0.016s | 20.288MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_9.smt2 | 0.017s | 20.384MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_57.smt2 | 0.018s | 20.304MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_8.smt2 | 0.018s | 20.244MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_9.smt2 | 0.018s | 20.128MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_8.smt2 | 0.018s | 20.064MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_5.smt2 | 0.018s | 20.308MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/cs_szymanski.i_3.smt2 | 0.018s | 20.308MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_8.smt2 | 0.019s | 20.312MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dancing.i_1.smt2 | 0.019s | 20.148MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_11.smt2 | 0.019s | 20.408MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/cs_szymanski.i_4.smt2 | 0.020s | 20.328MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_9.smt2 | 0.021s | 20.352MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_56.smt2 | 0.021s | 20.328MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_9.smt2 | 0.021s | 20.788MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_4.smt2 | 0.023s | 20.3MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_2.smt2 | 0.023s | 20.416MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_1.smt2 | 0.023s | 20.308MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_10.smt2 | 0.024s | 20.308MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_8.smt2 | 0.024s | 20.816MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_52.smt2 | 0.024s | 20.176MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_17.smt2 | 0.024s | 20.3MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_3.smt2 | 0.024s | 20.34MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_9.smt2 | 0.024s | 20.084MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_7.smt2 | 0.024s | 20.28MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/prefixsum_rec.c_12.smt2 | 0.025s | 20.248MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sll2n_insert_unequal.i_74.smt2 | 0.025s | 20.264MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_6.smt2 | 0.025s | 20.048MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_6.smt2 | 0.025s | 20.564MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_10.smt2 | 0.026s | 20.048MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/running_example.i_6.smt2 | 0.026s | 20.98MiB| unsat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sum_array-2-2.i_1.smt2 | 0.027s | 20.548MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_7.smt2 | 0.027s | 20.236MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_4.smt2 | 0.027s | 20.548MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_7.smt2 | 0.028s | 20.472MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sll2n_insert_unequal.i_76.smt2 | 0.028s | 20.024MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sum_array-2-2.i_2.smt2 | 0.028s | 20.596MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_6.smt2 | 0.028s | 20.232MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sll2n_insert_unequal.i_75.smt2 | 0.029s | 20.056MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_7.smt2 | 0.029s | 20.856MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_5.smt2 | 0.029s | 20.048MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_10.smt2 | 0.029s | 20.816MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_6.smt2 | 0.030s | 20.36MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_50.smt2 | 0.030s | 19.764MiB| unsat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_4.smt2 | 0.031s | 20.136MiB| sat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_5.smt2 | 0.036s | 20.604MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_1-2.c_AllErrorsAtOnce_Iteration3_0.smt2 | 0.050s | 21.224MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/mcmillan2006.i_AllErrorsAtOnce_Iteration5_0.smt2 | 0.076s | 22.032MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/condm.c_AllErrorsAtOnce_Iteration9_0.smt2 | 0.128s | 23.584MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_doub_access_init_const.c_AllErrorsAtOnce_Iteration3_0.smt2 | 0.184s | 24.936MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_shadowinit.i_AllErrorsAtOnce_Iteration5_0.smt2 | 0.257s | 23.86MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/benchmark52_polynomial.i_AllErrorsAtOnce_Iteration3_0.smt2 | 0.977s | 21.624MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sum_array-2-2.i_0.smt2 | 1.012s | 102.0MiB| sat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/rew.c_AllErrorsAtOnce_Iteration5_0.smt2 | 1.303s | 25.64MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/sep20-1.i_AllErrorsAtOnce_Iteration23_0.smt2 | 2.717s | 41.504MiB| unsat | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/skipped.c_AllErrorsAtOnce_Iteration5_0.smt2 | 4.988s | 38.124MiB| unsat | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/prefixsum_rec.c_25.smt2 | 20.007s | 40.052MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/sorting_selectionsort_ground-2.i_AllErrorsAtOnce_Iteration8_0.smt2 | 20.007s | 51.68MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/linear_sea.ch.c_AllErrorsAtOnce_Iteration8_0.smt2 | 20.007s | 43.264MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_4.c.v+lh-reducer.c_AllErrorsAtOnce_Iteration3_0.smt2 | 20.008s | 70.4MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_3.c_AllErrorsAtOnce_Iteration3_0.smt2 | 20.008s | 62.648MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_4.c.v+cfa-reducer.c_AllErrorsAtOnce_Iteration4_0.smt2 | 20.009s | 60.656MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_of_struct_break.i_AllErrorsAtOnce_Iteration5_0.smt2 | 20.009s | 64.472MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/partial_lesser_bound-1.i_AllErrorsAtOnce_Iteration3_0.smt2 | 20.010s | 73.936MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/flag_loopdep_simple.i_AllErrorsAtOnce_Iteration8_0.smt2 | 20.010s | 96.876MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_4.i_AllErrorsAtOnce_Iteration5_0.smt2 | 20.010s | 79.128MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_2.c_AllErrorsAtOnce_Iteration3_0.smt2 | 20.011s | 115.0MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/nr2.c_AllErrorsAtOnce_Iteration8_0.smt2 | 20.015s | 126.0MiB| timeout | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/tree_max.c_0.smt2 | 20.017s | 36.424MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/rewnifrev2.c_AllErrorsAtOnce_Iteration5_0.smt2 | 20.020s | 347.0MiB| timeout | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_4.c_AllErrorsAtOnce_Iteration3_0.smt2 | 20.030s | 433.0MiB| timeout | 0 | | |