# . * SAT 0 * UNSAT 0 * TIMEOUT 0 * UNKNOWN 78 * 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: 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/ANIA.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/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_10.smt2 | 0.021s | 19.876MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_9.smt2 | 0.022s | 19.652MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_6.smt2 | 0.022s | 19.884MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_10.smt2 | 0.023s | 19.872MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_7.smt2 | 0.023s | 19.804MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_9.smt2 | 0.023s | 19.724MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_9.smt2 | 0.023s | 19.6MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/flag_loopdep_simple.i_AllErrorsAtOnce_Iteration8_0.smt2 | 0.023s | 19.664MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sum_array-2-2.i_1.smt2 | 0.025s | 19.716MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/cs_szymanski.i_4.smt2 | 0.025s | 19.68MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/prefixsum_rec.c_11.smt2 | 0.025s | 19.6MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_10.smt2 | 0.025s | 19.884MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/sep20-1.i_AllErrorsAtOnce_Iteration23_0.smt2 | 0.027s | 20.136MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/prefixsum_rec.c_25.smt2 | 0.028s | 19.628MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_16.smt2 | 0.032s | 19.88MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/prefixsum_rec.c_12.smt2 | 0.033s | 20.116MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sll2n_insert_unequal.i_74.smt2 | 0.033s | 20.016MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_55.smt2 | 0.034s | 19.692MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dancing.i_1.smt2 | 0.034s | 19.884MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_2.smt2 | 0.034s | 19.796MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sum_array-2-2.i_2.smt2 | 0.034s | 19.748MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_11.smt2 | 0.034s | 19.892MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_7.smt2 | 0.034s | 19.772MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_8.smt2 | 0.034s | 19.672MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/cs_szymanski.i_3.smt2 | 0.035s | 19.56MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/partial_lesser_bound-1.i_AllErrorsAtOnce_Iteration3_0.smt2 | 0.035s | 20.132MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_8.smt2 | 0.036s | 19.632MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_6.smt2 | 0.036s | 19.632MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/mcmillan2006.i_AllErrorsAtOnce_Iteration5_0.smt2 | 0.037s | 19.9MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/linear_sea.ch.c_AllErrorsAtOnce_Iteration8_0.smt2 | 0.038s | 20.24MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_doub_access_init_const.c_AllErrorsAtOnce_Iteration3_0.smt2 | 0.042s | 19.972MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/rewnifrev2.c_AllErrorsAtOnce_Iteration5_0.smt2 | 0.042s | 20.112MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_4.c_AllErrorsAtOnce_Iteration3_0.smt2 | 0.045s | 21.192MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_3.c_AllErrorsAtOnce_Iteration3_0.smt2 | 0.045s | 21.176MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_4.c.v+lh-reducer.c_AllErrorsAtOnce_Iteration3_0.smt2 | 0.047s | 21.208MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_1-2.c_AllErrorsAtOnce_Iteration3_0.smt2 | 0.052s | 19.856MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_of_struct_break.i_AllErrorsAtOnce_Iteration5_0.smt2 | 0.052s | 19.82MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_57.smt2 | 0.053s | 19.804MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_17.smt2 | 0.053s | 19.824MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/condm.c_AllErrorsAtOnce_Iteration9_0.smt2 | 0.053s | 19.9MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_53.smt2 | 0.054s | 20.02MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_8.smt2 | 0.054s | 19.848MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_3.smt2 | 0.054s | 19.604MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_4.smt2 | 0.055s | 19.872MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_10.smt2 | 0.055s | 20.024MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sll2n_insert_unequal.i_76.smt2 | 0.055s | 19.612MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sum_array-2-2.i_0.smt2 | 0.055s | 19.868MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_7.smt2 | 0.056s | 19.656MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/rew.c_AllErrorsAtOnce_Iteration5_0.smt2 | 0.056s | 20.036MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/nr2.c_AllErrorsAtOnce_Iteration8_0.smt2 | 0.056s | 20.108MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_8.smt2 | 0.057s | 19.632MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_5.smt2 | 0.057s | 19.872MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_52.smt2 | 0.057s | 20.064MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_6.smt2 | 0.057s | 19.876MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/sll2n_insert_unequal.i_75.smt2 | 0.057s | 19.6MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_11.smt2 | 0.057s | 19.856MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_4.smt2 | 0.057s | 19.844MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_9.smt2 | 0.057s | 20.064MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/tree_max.c_0.smt2 | 0.057s | 19.82MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_50.smt2 | 0.057s | 19.852MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0234-1.i_56.smt2 | 0.057s | 19.6MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_9.smt2 | 0.057s | 19.64MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_7.smt2 | 0.057s | 19.696MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_4.smt2 | 0.057s | 19.608MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_5.smt2 | 0.057s | 19.592MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/test-0237.i_20.smt2 | 0.057s | 19.636MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/vogal-2.i_1.smt2 | 0.057s | 19.816MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/benchmark52_polynomial.i_AllErrorsAtOnce_Iteration3_0.smt2 | 0.057s | 19.864MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/packet_filter.i_5.smt2 | 0.058s | 20.12MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_5.smt2 | 0.058s | 20.336MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/dll2n_insert_unequal.i_6.smt2 | 0.058s | 20.132MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/sorting_selectionsort_ground-2.i_AllErrorsAtOnce_Iteration8_0.smt2 | 0.058s | 19.672MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_shadowinit.i_AllErrorsAtOnce_Iteration5_0.smt2 | 0.058s | 19.856MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/skipped.c_AllErrorsAtOnce_Iteration5_0.smt2 | 0.059s | 20.056MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/array_4.i_AllErrorsAtOnce_Iteration5_0.smt2 | 0.060s | 19.86MiB| unknown | 0 | | | |non-incremental/ANIA/20230321-UltimateAutomizerSvcomp2023/running_example.i_6.smt2 | 0.063s | 19.812MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_2.c_AllErrorsAtOnce_Iteration3_0.smt2 | 0.064s | 21.14MiB| unknown | 0 | | | |non-incremental/ANIA/20240413-AutomizerLoopAcceleration/aiob_4.c.v+cfa-reducer.c_AllErrorsAtOnce_Iteration4_0.smt2 | 0.073s | 21.228MiB| unknown | 0 | | |