# . * SAT 165 * UNSAT 265 * TIMEOUT 105 * 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/LIA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-LIA.tar.zst-downlo
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/LIA.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_557.smt2 | 0.021s | 19.616MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1371.smt2 | 0.023s | 20.52MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM917=1.smt2 | 0.023s | 19.848MiB| unsat | 0 | | | |non-incremental/LIA/psyco/161.smt2 | 0.025s | 21.196MiB| sat | 0 | | | |non-incremental/LIA/psyco/009.smt2 | 0.026s | 21.084MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1878.smt2 | 0.027s | 20.624MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_2746.smt2 | 0.028s | 20.668MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_10.smt2 | 0.029s | 21.348MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_6.smt2 | 0.029s | 20.804MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_1.smt2 | 0.030s | 21.124MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_6_true-unreach-call_true-no-overflow_false-termination.i_2.smt2 | 0.031s | 20.892MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_7_true-unreach-call_true-no-overflow_false-termination.i_4.smt2 | 0.031s | 20.88MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_8.smt2 | 0.032s | 20.876MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI079=1.smt2 | 0.032s | 19.868MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1752.smt2 | 0.033s | 19.592MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_751.smt2 | 0.033s | 19.84MiB| unsat | 0 | | | |non-incremental/LIA/psyco/031.smt2 | 0.034s | 22.396MiB| sat | 0 | | | |non-incremental/LIA/tptp/NUM899=1.smt2 | 0.035s | 19.852MiB| sat | 0 | | | |non-incremental/LIA/tptp/ARI011=1.smt2 | 0.035s | 20.636MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1357.smt2 | 0.036s | 20.62MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM893=1.smt2 | 0.036s | 20.632MiB| unsat | 0 | | | |non-incremental/LIA/psyco/123.smt2 | 0.036s | 21.392MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_12.smt2 | 0.037s | 20.884MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_6_true-unreach-call_true-no-overflow_false-termination.i_12.smt2 | 0.037s | 20.796MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI056=1.smt2 | 0.037s | 19.868MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM916=1.smt2 | 0.037s | 19.852MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM874=1.smt2 | 0.038s | 20.092MiB| sat | 0 | | | |non-incremental/LIA/psyco/050.smt2 | 0.038s | 22.096MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1887.smt2 | 0.039s | 21.04MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM889=1.smt2 | 0.039s | 19.6MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI038=1.smt2 | 0.039s | 19.824MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM871=1.smt2 | 0.039s | 19.532MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1578.smt2 | 0.040s | 19.824MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI031=1.smt2 | 0.040s | 19.852MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI572=1.smt2 | 0.040s | 20.612MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI052=1.smt2 | 0.040s | 19.852MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM875=1.smt2 | 0.040s | 19.576MiB| sat | 0 | | | |non-incremental/LIA/tptp/ARI591=1.smt2 | 0.040s | 19.848MiB| unknown | 0 | | | |non-incremental/LIA/psyco/141.smt2 | 0.040s | 20.76MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1874.smt2 | 0.041s | 20.864MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM868=1.smt2 | 0.041s | 19.944MiB| sat | 0 | | | |non-incremental/LIA/tptp/ARI032=1.smt2 | 0.041s | 20.832MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_2317.smt2 | 0.042s | 20.828MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI018=1.smt2 | 0.042s | 20.852MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM869=1.smt2 | 0.042s | 20.12MiB| sat | 0 | | | |non-incremental/LIA/tptp/ARI004=1.smt2 | 0.042s | 20.936MiB| unsat | 0 | | | |non-incremental/LIA/psyco/010.smt2 | 0.042s | 20.832MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM897=1.smt2 | 0.044s | 19.9MiB| sat | 0 | | | |non-incremental/LIA/psyco/127.smt2 | 0.044s | 21.52MiB| sat | 0 | | | |non-incremental/LIA/psyco/125.smt2 | 0.044s | 21.908MiB| sat | 0 | | | |non-incremental/LIA/psyco/072.smt2 | 0.045s | 21.648MiB| sat | 0 | | | |non-incremental/LIA/tptp/NUM918=1.smt2 | 0.046s | 19.86MiB| unsat | 0 | | | |non-incremental/LIA/psyco/066.smt2 | 0.046s | 21.132MiB| unsat | 0 | | | |non-incremental/LIA/psyco/173.smt2 | 0.046s | 21.672MiB| sat | 0 | | | |non-incremental/LIA/psyco/011.smt2 | 0.047s | 20.892MiB| sat | 0 | | | |non-incremental/LIA/psyco/138.smt2 | 0.047s | 22.88MiB| unsat | 0 | | | |non-incremental/LIA/psyco/143.smt2 | 0.047s | 21.192MiB| sat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_7_true-unreach-call_true-no-overflow_false-termination.i_3.smt2 | 0.048s | 21.084MiB| unsat | 0 | | | |non-incremental/LIA/psyco/061.smt2 | 0.048s | 21.092MiB| sat | 0 | | | |non-incremental/LIA/psyco/052.smt2 | 0.050s | 22.336MiB| sat | 0 | | | |non-incremental/LIA/psyco/158.smt2 | 0.051s | 21.356MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1767.smt2 | 0.053s | 19.896MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1726.smt2 | 0.053s | 19.624MiB| unsat | 0 | | | |non-incremental/LIA/psyco/159.smt2 | 0.053s | 21.124MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1786.smt2 | 0.054s | 20.56MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1761.smt2 | 0.055s | 19.512MiB| unsat | 0 | | | |non-incremental/LIA/psyco/113.smt2 | 0.055s | 21.38MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_17.smt2 | 0.056s | 21.192MiB| unsat | 0 | | | |non-incremental/LIA/psyco/134.smt2 | 0.056s | 21.676MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_874.smt2 | 0.058s | 19.768MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_187.smt2 | 0.059s | 20.672MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_3227.smt2 | 0.059s | 19.548MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM864=1.smt2 | 0.059s | 19.616MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_7_true-unreach-call_true-no-overflow_false-termination.i_9.smt2 | 0.060s | 20.98MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_527.smt2 | 0.060s | 19.608MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_4.smt2 | 0.061s | 20.648MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_5.smt2 | 0.061s | 20.944MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_6_true-unreach-call_true-no-overflow_false-termination.i_14.smt2 | 0.061s | 21.212MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI026=1.smt2 | 0.061s | 20.08MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI044=1.smt2 | 0.061s | 20.344MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_497.smt2 | 0.062s | 19.76MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1597.smt2 | 0.062s | 20.344MiB| unsat | 0 | | | |non-incremental/LIA/psyco/018.smt2 | 0.062s | 20.916MiB| unsat | 0 | | | |non-incremental/LIA/psyco/180.smt2 | 0.062s | 20.892MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1379.smt2 | 0.063s | 20.0MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1703.smt2 | 0.063s | 20.66MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_766.smt2 | 0.063s | 20.78MiB| unsat | 0 | | | |non-incremental/LIA/psyco/074.smt2 | 0.063s | 21.892MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1707.smt2 | 0.064s | 20.944MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM895=1.smt2 | 0.064s | 19.652MiB| unsat | 0 | | | |non-incremental/LIA/psyco/166.smt2 | 0.064s | 20.932MiB| sat | 0 | | | |non-incremental/LIA/psyco/024.smt2 | 0.064s | 21.272MiB| sat | 0 | | | |non-incremental/LIA/psyco/156.smt2 | 0.064s | 21.52MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_7.smt2 | 0.065s | 20.992MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1317.smt2 | 0.065s | 20.872MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_817.smt2 | 0.066s | 20.88MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1437.smt2 | 0.066s | 20.66MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_798.smt2 | 0.066s | 19.612MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_575.smt2 | 0.066s | 20.676MiB| unsat | 0 | | | |non-incremental/LIA/psyco/131.smt2 | 0.066s | 21.216MiB| sat | 0 | | | |non-incremental/LIA/psyco/013.smt2 | 0.066s | 21.0MiB| sat | 0 | | | |non-incremental/LIA/tptp/ARI045=1.smt2 | 0.067s | 20.944MiB| unsat | 0 | | | |non-incremental/LIA/psyco/187.smt2 | 0.067s | 21.164MiB| sat | 0 | | | |non-incremental/LIA/psyco/037.smt2 | 0.067s | 21.976MiB| sat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_14.smt2 | 0.068s | 20.844MiB| unsat | 0 | | | |non-incremental/LIA/psyco/110.smt2 | 0.068s | 21.904MiB| sat | 0 | | | |non-incremental/LIA/psyco/102.smt2 | 0.068s | 22.268MiB| unsat | 0 | | | |non-incremental/LIA/psyco/146.smt2 | 0.068s | 21.132MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_780.smt2 | 0.069s | 20.616MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_127.smt2 | 0.069s | 19.64MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_713.smt2 | 0.069s | 20.836MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1758.smt2 | 0.069s | 19.716MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1170.smt2 | 0.069s | 19.604MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1575.smt2 | 0.069s | 19.844MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM865=1.smt2 | 0.069s | 19.596MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI027=1.smt2 | 0.069s | 20.624MiB| unsat | 0 | | | |non-incremental/LIA/psyco/028.smt2 | 0.069s | 21.688MiB| sat | 0 | | | |non-incremental/LIA/psyco/003.smt2 | 0.069s | 21.104MiB| sat | 0 | | | |non-incremental/LIA/psyco/048.smt2 | 0.069s | 22.2MiB| sat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_7_true-unreach-call_true-no-overflow_false-termination.i_8.smt2 | 0.070s | 21.02MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1879.smt2 | 0.070s | 19.6MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_173.smt2 | 0.071s | 20.752MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1172.smt2 | 0.071s | 19.524MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1847.smt2 | 0.071s | 20.68MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1777.smt2 | 0.071s | 20.512MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1741.smt2 | 0.071s | 19.92MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1792.smt2 | 0.071s | 19.596MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1778.smt2 | 0.072s | 20.872MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_671.smt2 | 0.072s | 19.644MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1781.smt2 | 0.072s | 20.324MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1375.smt2 | 0.072s | 20.656MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_367.smt2 | 0.072s | 20.856MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_637.smt2 | 0.072s | 20.672MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1370.smt2 | 0.072s | 20.512MiB| unsat | 0 | | | |non-incremental/LIA/psyco/023.smt2 | 0.072s | 21.312MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1679.smt2 | 0.073s | 19.648MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_179.smt2 | 0.073s | 19.632MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1723.smt2 | 0.073s | 20.64MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_357.smt2 | 0.073s | 20.612MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1728.smt2 | 0.073s | 20.836MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_670.smt2 | 0.073s | 20.66MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1789.smt2 | 0.073s | 19.648MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI025=1.smt2 | 0.073s | 20.12MiB| unsat | 0 | | | |non-incremental/LIA/psyco/168.smt2 | 0.073s | 20.884MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1897.smt2 | 0.074s | 20.844MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1770.smt2 | 0.074s | 21.108MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_7.smt2 | 0.074s | 20.728MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1475.smt2 | 0.074s | 20.68MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_2147.smt2 | 0.074s | 21.156MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_73.smt2 | 0.074s | 20.664MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1479.smt2 | 0.074s | 20.8MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI017=1.smt2 | 0.074s | 20.088MiB| unsat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_2_3.smt2 | 0.074s | 21.008MiB| sat | 0 | | | |non-incremental/LIA/psyco/077.smt2 | 0.074s | 21.92MiB| sat | 0 | | | |non-incremental/LIA/psyco/029.smt2 | 0.074s | 22.144MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_574.smt2 | 0.075s | 20.368MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI012=1.smt2 | 0.075s | 20.62MiB| unsat | 0 | | | |non-incremental/LIA/psyco/119.smt2 | 0.075s | 21.388MiB| unsat | 0 | | | |non-incremental/LIA/psyco/150.smt2 | 0.075s | 21.556MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_847.smt2 | 0.076s | 19.592MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI083=1.smt2 | 0.076s | 19.872MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_657.smt2 | 0.077s | 20.9MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_744.smt2 | 0.077s | 20.624MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_537.smt2 | 0.077s | 19.624MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI039=1.smt2 | 0.077s | 20.1MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1737.smt2 | 0.078s | 20.62MiB| unsat | 0 | | | |non-incremental/LIA/psyco/014.smt2 | 0.078s | 21.656MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_277.smt2 | 0.079s | 20.668MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI005=1.smt2 | 0.079s | 20.348MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI590=1.smt2 | 0.079s | 20.584MiB| unsat | 0 | | | |non-incremental/LIA/psyco/081.smt2 | 0.079s | 21.912MiB| sat | 0 | | | |non-incremental/LIA/psyco/145.smt2 | 0.079s | 21.068MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_725.smt2 | 0.080s | 20.648MiB| unsat | 0 | | | |non-incremental/LIA/psyco/190.smt2 | 0.080s | 21.644MiB| sat | 0 | | | |non-incremental/LIA/psyco/093.smt2 | 0.080s | 22.188MiB| sat | 0 | | | |non-incremental/LIA/psyco/026.smt2 | 0.080s | 21.868MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_1757.smt2 | 0.081s | 20.844MiB| unsat | 0 | | | |non-incremental/LIA/psyco/056.smt2 | 0.081s | 22.44MiB| sat | 0 | | | |non-incremental/LIA/psyco/049.smt2 | 0.081s | 22.156MiB| sat | 0 | | | |non-incremental/LIA/psyco/140.smt2 | 0.081s | 20.872MiB| unsat | 0 | | | |non-incremental/LIA/psyco/118.smt2 | 0.082s | 21.416MiB| sat | 0 | | | |non-incremental/LIA/psyco/062.smt2 | 0.082s | 20.896MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_728.smt2 | 0.083s | 20.656MiB| unsat | 0 | | | |non-incremental/LIA/psyco/129.smt2 | 0.083s | 21.148MiB| sat | 0 | | | |non-incremental/LIA/psyco/025.smt2 | 0.083s | 21.288MiB| sat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_6_true-unreach-call_true-no-overflow_false-termination.i_15.smt2 | 0.084s | 21.148MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI053=1.smt2 | 0.084s | 20.136MiB| unsat | 0 | | | |non-incremental/LIA/psyco/097.smt2 | 0.084s | 22.168MiB| sat | 0 | | | |non-incremental/LIA/psyco/124.smt2 | 0.084s | 21.672MiB| sat | 0 | | | |non-incremental/LIA/psyco/160.smt2 | 0.084s | 21.416MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_2207.smt2 | 0.085s | 20.728MiB| unsat | 0 | | | |non-incremental/LIA/psyco/091.smt2 | 0.085s | 21.9MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_378.smt2 | 0.086s | 20.652MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_3.smt2 | 0.087s | 20.808MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI054=1.smt2 | 0.087s | 20.924MiB| unsat | 0 | | | |non-incremental/LIA/psyco/179.smt2 | 0.087s | 20.916MiB| unsat | 0 | | | |non-incremental/LIA/psyco/152.smt2 | 0.087s | 21.28MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM915=1.smt2 | 0.088s | 19.988MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI592=1.smt2 | 0.088s | 20.844MiB| unsat | 0 | | | |non-incremental/LIA/psyco/164.smt2 | 0.089s | 21.224MiB| sat | 0 | | | |non-incremental/LIA/psyco/155.smt2 | 0.089s | 21.852MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_7_true-unreach-call_true-no-overflow_false-termination.i_5.smt2 | 0.090s | 20.884MiB| unsat | 0 | | | |non-incremental/LIA/psyco/171.smt2 | 0.090s | 21.132MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_73.smt2 | 0.091s | 19.628MiB| unsat | 0 | | | |non-incremental/LIA/psyco/099.smt2 | 0.091s | 22.148MiB| sat | 0 | | | |non-incremental/LIA/psyco/083.smt2 | 0.091s | 22.248MiB| sat | 0 | | | |non-incremental/LIA/psyco/103.smt2 | 0.091s | 20.928MiB| sat | 0 | | | |non-incremental/LIA/psyco/122.smt2 | 0.091s | 21.388MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1739.smt2 | 0.092s | 19.484MiB| unsat | 0 | | | |non-incremental/LIA/psyco/188.smt2 | 0.092s | 21.328MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_775.smt2 | 0.093s | 19.864MiB| unsat | 0 | | | |non-incremental/LIA/psyco/007.smt2 | 0.093s | 21.34MiB| sat | 0 | | | |non-incremental/LIA/psyco/170.smt2 | 0.093s | 21.084MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1784.smt2 | 0.094s | 19.64MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM896=1.smt2 | 0.094s | 19.86MiB| sat | 0 | | | |non-incremental/LIA/psyco/035.smt2 | 0.094s | 22.552MiB| sat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_7_true-unreach-call_true-no-overflow_false-termination.i_7.smt2 | 0.095s | 20.924MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1785.smt2 | 0.096s | 20.388MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1107.smt2 | 0.097s | 20.44MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_3872.smt2 | 0.097s | 20.804MiB| unsat | 0 | | | |non-incremental/LIA/psyco/096.smt2 | 0.097s | 22.372MiB| sat | 0 | | | |non-incremental/LIA/psyco/079.smt2 | 0.097s | 22.16MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_379.smt2 | 0.098s | 20.808MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_673.smt2 | 0.098s | 19.592MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_763.smt2 | 0.099s | 21.208MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_473.smt2 | 0.099s | 20.748MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1749.smt2 | 0.099s | 20.664MiB| unsat | 0 | | | |non-incremental/LIA/psyco/112.smt2 | 0.099s | 21.552MiB| sat | 0 | | | |non-incremental/LIA/psyco/075.smt2 | 0.099s | 21.932MiB| sat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_11.smt2 | 0.100s | 20.964MiB| unsat | 0 | | | |non-incremental/LIA/psyco/051.smt2 | 0.100s | 22.328MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1729.smt2 | 0.101s | 20.692MiB| unsat | 0 | | | |non-incremental/LIA/psyco/174.smt2 | 0.101s | 21.384MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c_0.smt2 | 0.102s | 20.552MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_2715.smt2 | 0.102s | 21.076MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_703.smt2 | 0.102s | 19.7MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_597.smt2 | 0.102s | 19.484MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1337.smt2 | 0.102s | 19.856MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/MADWiFi-encode_ie_ok_true-unreach-call.i_17.smt2 | 0.103s | 20.74MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/MADWiFi-encode_ie_ok_true-unreach-call.i_7.smt2 | 0.103s | 20.668MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_755.smt2 | 0.103s | 20.888MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1755.smt2 | 0.103s | 20.028MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1677.smt2 | 0.103s | 20.56MiB| unsat | 0 | | | |non-incremental/LIA/psyco/043.smt2 | 0.103s | 22.196MiB| sat | 0 | | | |non-incremental/LIA/psyco/045.smt2 | 0.103s | 22.152MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_720.smt2 | 0.104s | 19.86MiB| unsat | 0 | | | |non-incremental/LIA/psyco/092.smt2 | 0.104s | 22.184MiB| sat | 0 | | | |non-incremental/LIA/psyco/121.smt2 | 0.104s | 21.68MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1117.smt2 | 0.105s | 21.116MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_297.smt2 | 0.105s | 19.832MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1738.smt2 | 0.106s | 20.852MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_1478.smt2 | 0.106s | 21.152MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1070.smt2 | 0.106s | 20.64MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_71.smt2 | 0.107s | 20.724MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1720.smt2 | 0.107s | 20.624MiB| unsat | 0 | | | |non-incremental/LIA/psyco/189.smt2 | 0.107s | 21.296MiB| sat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_13.smt2 | 0.108s | 20.972MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1722.smt2 | 0.108s | 20.824MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_7_true-unreach-call_true-no-overflow_false-termination.i_6.smt2 | 0.109s | 21.008MiB| unsat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_7_true-unreach-call_true-no-overflow_false-termination.i_10.smt2 | 0.110s | 21.376MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_470.smt2 | 0.110s | 21.068MiB| unsat | 0 | | | |non-incremental/LIA/tptp/NUM870=1.smt2 | 0.110s | 19.848MiB| sat | 0 | | | |non-incremental/LIA/tptp/NUM898=1.smt2 | 0.110s | 19.848MiB| sat | 0 | | | |non-incremental/LIA/psyco/033.smt2 | 0.110s | 22.192MiB| sat | 0 | | | |non-incremental/LIA/tptp/ARI040=1.smt2 | 0.111s | 20.644MiB| unsat | 0 | | | |non-incremental/LIA/tptp/ARI013=1.smt2 | 0.111s | 20.104MiB| unsat | 0 | | | |non-incremental/LIA/psyco/098.smt2 | 0.111s | 22.168MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1875.smt2 | 0.112s | 19.596MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_678.smt2 | 0.113s | 19.628MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1748.smt2 | 0.113s | 19.612MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_927.smt2 | 0.113s | 20.656MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1307.smt2 | 0.113s | 19.632MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_753.smt2 | 0.114s | 19.704MiB| unsat | 0 | | | |non-incremental/LIA/psyco/106.smt2 | 0.114s | 21.476MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_187.smt2 | 0.115s | 19.592MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1817.smt2 | 0.115s | 20.616MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_762.smt2 | 0.115s | 19.604MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_1735.smt2 | 0.116s | 20.656MiB| unsat | 0 | | | |non-incremental/LIA/psyco/063.smt2 | 0.116s | 20.84MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_2_3_5.smt2 | 0.117s | 21.14MiB| sat | 0 | | | |non-incremental/LIA/psyco/181.smt2 | 0.117s | 20.628MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_707.smt2 | 0.118s | 20.672MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1676.smt2 | 0.119s | 19.536MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_1657.smt2 | 0.119s | 19.848MiB| unsat | 0 | | | |non-incremental/LIA/psyco/151.smt2 | 0.119s | 20.904MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_947.smt2 | 0.121s | 20.98MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_887.smt2 | 0.121s | 19.86MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1877.smt2 | 0.121s | 20.628MiB| unsat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_3_5.smt2 | 0.121s | 21.176MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_287.smt2 | 0.122s | 19.528MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_237.smt2 | 0.122s | 19.64MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_2175.smt2 | 0.123s | 19.676MiB| unsat | 0 | | | |non-incremental/LIA/psyco/167.smt2 | 0.123s | 21.48MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_627.smt2 | 0.124s | 20.66MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_788.smt2 | 0.125s | 19.572MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1471.smt2 | 0.125s | 20.628MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_447.smt2 | 0.125s | 20.616MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1736.smt2 | 0.125s | 19.484MiB| unsat | 0 | | | |non-incremental/LIA/psyco/195.smt2 | 0.125s | 21.596MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_870.smt2 | 0.127s | 20.456MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1795.smt2 | 0.127s | 20.852MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_507.smt2 | 0.127s | 20.336MiB| unsat | 0 | | | |non-incremental/LIA/psyco/193.smt2 | 0.127s | 21.136MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1764.smt2 | 0.128s | 20.664MiB| unsat | 0 | | | |non-incremental/LIA/psyco/109.smt2 | 0.128s | 21.132MiB| unsat | 0 | | | |non-incremental/LIA/psyco/177.smt2 | 0.128s | 20.828MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_597.smt2 | 0.129s | 20.768MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_175.smt2 | 0.129s | 20.672MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested6_true-unreach-call.i_7.smt2 | 0.129s | 20.68MiB| unsat | 0 | | | |non-incremental/LIA/psyco/153.smt2 | 0.129s | 20.916MiB| sat | 0 | | | |non-incremental/LIA/psyco/004.smt2 | 0.129s | 20.78MiB| unsat | 0 | | | |non-incremental/LIA/psyco/133.smt2 | 0.130s | 21.632MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_573.smt2 | 0.131s | 19.716MiB| unsat | 0 | | | |non-incremental/LIA/psyco/178.smt2 | 0.131s | 21.084MiB| sat | 0 | | | |non-incremental/LIA/psyco/019.smt2 | 0.131s | 21.092MiB| sat | 0 | | | |non-incremental/LIA/psyco/172.smt2 | 0.131s | 21.136MiB| sat | 0 | | | |non-incremental/LIA/psyco/058.smt2 | 0.131s | 22.472MiB| unsat | 0 | | | |non-incremental/LIA/psyco/107.smt2 | 0.131s | 21.132MiB| unsat | 0 | | | |non-incremental/LIA/psyco/105.smt2 | 0.131s | 20.84MiB| unsat | 0 | | | |non-incremental/LIA/psyco/067.smt2 | 0.131s | 20.96MiB| sat | 0 | | | |non-incremental/LIA/psyco/154.smt2 | 0.132s | 21.12MiB| sat | 0 | | | |non-incremental/LIA/psyco/090.smt2 | 0.132s | 22.14MiB| unsat | 0 | | | |non-incremental/LIA/psyco/005.smt2 | 0.132s | 21.124MiB| sat | 0 | | | |non-incremental/LIA/psyco/108.smt2 | 0.132s | 20.864MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_746.smt2 | 0.133s | 20.772MiB| unsat | 0 | | | |non-incremental/LIA/psyco/162.smt2 | 0.133s | 20.82MiB| unsat | 0 | | | |non-incremental/LIA/psyco/100.smt2 | 0.133s | 22.452MiB| sat | 0 | | | |non-incremental/LIA/psyco/002.smt2 | 0.133s | 20.856MiB| unsat | 0 | | | |non-incremental/LIA/psyco/021.smt2 | 0.133s | 21.128MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_278.smt2 | 0.134s | 20.712MiB| unsat | 0 | | | |non-incremental/LIA/psyco/047.smt2 | 0.134s | 21.9MiB| sat | 0 | | | |non-incremental/LIA/psyco/157.smt2 | 0.134s | 20.892MiB| sat | 0 | | | |non-incremental/LIA/psyco/114.smt2 | 0.134s | 21.456MiB| sat | 0 | | | |non-incremental/LIA/psyco/137.smt2 | 0.134s | 22.572MiB| sat | 0 | | | |non-incremental/LIA/psyco/001.smt2 | 0.134s | 20.752MiB| sat | 0 | | | |non-incremental/LIA/psyco/186.smt2 | 0.134s | 20.68MiB| unsat | 0 | | | |non-incremental/LIA/psyco/095.smt2 | 0.134s | 22.376MiB| sat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_7_true-unreach-call_true-no-overflow_false-termination.i_2.smt2 | 0.135s | 20.912MiB| unsat | 0 | | | |non-incremental/LIA/psyco/142.smt2 | 0.135s | 21.256MiB| sat | 0 | | | |non-incremental/LIA/psyco/175.smt2 | 0.135s | 20.688MiB| sat | 0 | | | |non-incremental/LIA/psyco/163.smt2 | 0.135s | 20.932MiB| unsat | 0 | | | |non-incremental/LIA/psyco/176.smt2 | 0.135s | 20.8MiB| unsat | 0 | | | |non-incremental/LIA/psyco/017.smt2 | 0.135s | 20.616MiB| sat | 0 | | | |non-incremental/LIA/psyco/147.smt2 | 0.135s | 21.132MiB| sat | 0 | | | |non-incremental/LIA/psyco/115.smt2 | 0.135s | 21.348MiB| sat | 0 | | | |non-incremental/LIA/psyco/104.smt2 | 0.135s | 20.756MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1732.smt2 | 0.136s | 20.736MiB| unsat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_3_5_7.smt2 | 0.136s | 21.384MiB| sat | 0 | | | |non-incremental/LIA/psyco/065.smt2 | 0.136s | 20.876MiB| sat | 0 | | | |non-incremental/LIA/psyco/012.smt2 | 0.136s | 21.172MiB| unsat | 0 | | | |non-incremental/LIA/psyco/132.smt2 | 0.136s | 21.308MiB| unsat | 0 | | | |non-incremental/LIA/psyco/120.smt2 | 0.136s | 21.312MiB| sat | 0 | | | |non-incremental/LIA/psyco/068.smt2 | 0.136s | 21.22MiB| sat | 0 | | | |non-incremental/LIA/psyco/139.smt2 | 0.136s | 20.74MiB| sat | 0 | | | |non-incremental/LIA/psyco/069.smt2 | 0.136s | 21.132MiB| sat | 0 | | | |non-incremental/LIA/psyco/130.smt2 | 0.137s | 21.348MiB| sat | 0 | | | |non-incremental/LIA/psyco/022.smt2 | 0.137s | 21.432MiB| unsat | 0 | | | |non-incremental/LIA/psyco/030.smt2 | 0.137s | 21.8MiB| sat | 0 | | | |non-incremental/LIA/psyco/185.smt2 | 0.137s | 21.688MiB| sat | 0 | | | |non-incremental/LIA/psyco/064.smt2 | 0.137s | 21.024MiB| unsat | 0 | | | |non-incremental/LIA/psyco/111.smt2 | 0.137s | 21.488MiB| sat | 0 | | | |non-incremental/LIA/psyco/071.smt2 | 0.138s | 21.66MiB| sat | 0 | | | |non-incremental/LIA/psyco/149.smt2 | 0.138s | 21.148MiB| sat | 0 | | | |non-incremental/LIA/psyco/144.smt2 | 0.138s | 21.128MiB| unsat | 0 | | | |non-incremental/LIA/psyco/136.smt2 | 0.138s | 23.54MiB| sat | 0 | | | |non-incremental/LIA/psyco/116.smt2 | 0.138s | 21.536MiB| sat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_2_true-unreach-call_true-no-overflow_false-termination.i_9.smt2 | 0.139s | 20.704MiB| unsat | 0 | | | |non-incremental/LIA/psyco/020.smt2 | 0.139s | 21.124MiB| unsat | 0 | | | |non-incremental/LIA/psyco/015.smt2 | 0.139s | 21.388MiB| sat | 0 | | | |non-incremental/LIA/psyco/034.smt2 | 0.139s | 21.96MiB| sat | 0 | | | |non-incremental/LIA/psyco/027.smt2 | 0.139s | 21.804MiB| sat | 0 | | | |non-incremental/LIA/psyco/135.smt2 | 0.139s | 21.58MiB| unsat | 0 | | | |non-incremental/LIA/psyco/073.smt2 | 0.140s | 21.952MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1798.smt2 | 0.141s | 19.652MiB| unsat | 0 | | | |non-incremental/LIA/psyco/194.smt2 | 0.141s | 21.568MiB| sat | 0 | | | |non-incremental/LIA/psyco/016.smt2 | 0.141s | 21.776MiB| unsat | 0 | | | |non-incremental/LIA/psyco/169.smt2 | 0.141s | 21.428MiB| unsat | 0 | | | |non-incremental/LIA/psyco/008.smt2 | 0.142s | 21.836MiB| unsat | 0 | | | |non-incremental/LIA/psyco/094.smt2 | 0.142s | 21.98MiB| sat | 0 | | | |non-incremental/LIA/psyco/076.smt2 | 0.142s | 21.928MiB| sat | 0 | | | |non-incremental/LIA/psyco/148.smt2 | 0.142s | 21.488MiB| unsat | 0 | | | |non-incremental/LIA/psyco/126.smt2 | 0.142s | 21.944MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_670.smt2 | 0.143s | 19.632MiB| unsat | 0 | | | |non-incremental/LIA/psyco/054.smt2 | 0.143s | 22.252MiB| sat | 0 | | | |non-incremental/LIA/psyco/128.smt2 | 0.144s | 21.388MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1427.smt2 | 0.146s | 20.632MiB| unsat | 0 | | | |non-incremental/LIA/psyco/165.smt2 | 0.146s | 21.484MiB| unsat | 0 | | | |non-incremental/LIA/psyco/036.smt2 | 0.146s | 21.964MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_5_7.smt2 | 0.147s | 21.632MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1072.smt2 | 0.148s | 21.08MiB| unsat | 0 | | | |non-incremental/LIA/psyco/042.smt2 | 0.150s | 22.18MiB| sat | 0 | | | |non-incremental/LIA/20190429-UltimateAutomizerSvcomp2019/jain_7_true-unreach-call_true-no-overflow_false-termination.i_0.smt2 | 0.151s | 20.884MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/Primes_true-unreach-call.c_276.smt2 | 0.151s | 20.896MiB| unsat | 0 | | | |non-incremental/LIA/psyco/070.smt2 | 0.153s | 21.5MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/recHanoi03_true-unreach-call_true-termination.c_876.smt2 | 0.155s | 21.108MiB| unsat | 0 | | | |non-incremental/LIA/psyco/006.smt2 | 0.157s | 21.36MiB| unsat | 0 | | | |non-incremental/LIA/psyco/032.smt2 | 0.160s | 22.152MiB| sat | 0 | | | |non-incremental/LIA/psyco/046.smt2 | 0.160s | 22.152MiB| unsat | 0 | | | |non-incremental/LIA/psyco/086.smt2 | 0.161s | 22.072MiB| sat | 0 | | | |non-incremental/LIA/psyco/078.smt2 | 0.162s | 22.244MiB| sat | 0 | | | |non-incremental/LIA/psyco/082.smt2 | 0.164s | 22.404MiB| sat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_1477.smt2 | 0.167s | 20.616MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_785.smt2 | 0.173s | 20.844MiB| unsat | 0 | | | |non-incremental/LIA/UltimateAutomizer/nested9_true-unreach-call.i_807.smt2 | 0.174s | 20.668MiB| unsat | 0 | | | |non-incremental/LIA/psyco/117.smt2 | 0.174s | 21.792MiB| unsat | 0 | | | |non-incremental/LIA/psyco/044.smt2 | 0.176s | 22.152MiB| sat | 0 | | | |non-incremental/LIA/psyco/196.smt2 | 0.177s | 21.624MiB| sat | 0 | | | |non-incremental/LIA/psyco/087.smt2 | 0.177s | 22.236MiB| sat | 0 | | | |non-incremental/LIA/psyco/057.smt2 | 0.177s | 22.436MiB| sat | 0 | | | |non-incremental/LIA/psyco/040.smt2 | 0.178s | 22.392MiB| sat | 0 | | | |non-incremental/LIA/psyco/085.smt2 | 0.179s | 22.284MiB| sat | 0 | | | |non-incremental/LIA/psyco/055.smt2 | 0.180s | 22.496MiB| sat | 0 | | | |non-incremental/LIA/psyco/039.smt2 | 0.182s | 22.396MiB| sat | 0 | | | |non-incremental/LIA/psyco/080.smt2 | 0.183s | 22.156MiB| sat | 0 | | | |non-incremental/LIA/psyco/084.smt2 | 0.185s | 22.192MiB| sat | 0 | | | |non-incremental/LIA/psyco/038.smt2 | 0.185s | 22.084MiB| sat | 0 | | | |non-incremental/LIA/psyco/088.smt2 | 0.186s | 22.188MiB| sat | 0 | | | |non-incremental/LIA/psyco/053.smt2 | 0.190s | 22.336MiB| sat | 0 | | | |non-incremental/LIA/psyco/089.smt2 | 0.192s | 22.212MiB| sat | 0 | | | |non-incremental/LIA/psyco/041.smt2 | 0.196s | 22.192MiB| sat | 0 | | | |non-incremental/LIA/psyco/101.smt2 | 0.201s | 22.404MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_5_7_11.smt2 | 0.221s | 21.548MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_7_11_13.smt2 | 0.228s | 22.16MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_7_11.smt2 | 0.380s | 22.4MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_11_13.smt2 | 0.865s | 23.236MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_11_13_17.smt2 | 2.173s | 24.744MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_13_17_19.smt2 | 4.232s | 25.172MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_13_17.smt2 | 7.363s | 26.504MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_17_19_23.smt2 | 9.168s | 27.076MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_17_19.smt2 | 16.219s | 30.308MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_19_23_29.smt2 | 16.515s | 29.62MiB| sat | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_41_43_47.smt2 | 20.015s | 33.136MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_241_251_257.smt2 | 20.016s | 38.436MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_199_211_223.smt2 | 20.016s | 32.888MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_139_149.smt2 | 20.016s | 37.172MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_53_59.smt2 | 20.021s | 33.32MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_137_139_149.smt2 | 20.022s | 35.776MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_173_179_181.smt2 | 20.024s | 31.672MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_67_71.smt2 | 20.029s | 33.196MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_191_193.smt2 | 20.036s | 36.616MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_43_47_53.smt2 | 20.039s | 32.676MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_73_79_83.smt2 | 20.042s | 36.952MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_109_113_127.smt2 | 20.044s | 33.288MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_277_281_283.smt2 | 20.046s | 28.772MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_149_151.smt2 | 20.046s | 33.78MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_277_281.smt2 | 20.046s | 29.408MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_19_23.smt2 | 20.047s | 31.532MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_149_151_157.smt2 | 20.048s | 37.636MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_281_283.smt2 | 20.048s | 39.428MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_127_131_137.smt2 | 20.048s | 36.632MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_23_29.smt2 | 20.049s | 30.364MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_29_31_37.smt2 | 20.049s | 32.632MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_233_239.smt2 | 20.050s | 32.356MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_109_113.smt2 | 20.052s | 27.348MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_23_29_31.smt2 | 20.052s | 31.08MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_179_181_191.smt2 | 20.052s | 30.944MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_263_269.smt2 | 20.053s | 33.852MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_179_181.smt2 | 20.054s | 35.82MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_53_59_61.smt2 | 20.054s | 31.736MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_227_229_233.smt2 | 20.054s | 33.26MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_113_127.smt2 | 20.055s | 35.444MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_197_199.smt2 | 20.055s | 35.876MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_233_239_241.smt2 | 20.057s | 33.356MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_101_103_107.smt2 | 20.058s | 35.196MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_89_97_101.smt2 | 20.058s | 38.5MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_239_241.smt2 | 20.058s | 39.092MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_83_89.smt2 | 20.059s | 35.284MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_229_233.smt2 | 20.059s | 29.832MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_229_233_239.smt2 | 20.059s | 34.744MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_193_197.smt2 | 20.060s | 32.444MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_113_127_131.smt2 | 20.061s | 38.352MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_239_241_251.smt2 | 20.061s | 33.988MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_211_223_227.smt2 | 20.062s | 33.56MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_223_227.smt2 | 20.064s | 36.48MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_211_223.smt2 | 20.065s | 32.536MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_101_103.smt2 | 20.066s | 34.36MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_59_61_67.smt2 | 20.067s | 36.232MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_197_199_211.smt2 | 20.067s | 31.656MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_29_31.smt2 | 20.070s | 32.016MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_97_101.smt2 | 20.071s | 32.496MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_131_137_139.smt2 | 20.075s | 35.292MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_191_193_197.smt2 | 20.075s | 34.764MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_97_101_103.smt2 | 20.081s | 35.628MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_269_271_277.smt2 | 20.082s | 32.992MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_157_163.smt2 | 20.083s | 28.812MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_251_257.smt2 | 20.088s | 38.684MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_71_73_79.smt2 | 20.089s | 33.552MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_173_179.smt2 | 20.090s | 35.32MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_271_277.smt2 | 20.091s | 30.212MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_127_131.smt2 | 20.091s | 30.208MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_37_41_43.smt2 | 20.091s | 33.24MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_163_167.smt2 | 20.092s | 30.516MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_251_257_263.smt2 | 20.092s | 32.892MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_223_227_229.smt2 | 20.092s | 30.336MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_83_89_97.smt2 | 20.092s | 34.236MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_73_79.smt2 | 20.092s | 30.572MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_37_41.smt2 | 20.093s | 29.196MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_103_107_109.smt2 | 20.093s | 34.04MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_43_47.smt2 | 20.093s | 32.612MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_193_197_199.smt2 | 20.093s | 34.552MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_139_149_151.smt2 | 20.094s | 35.196MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_281_283_293.smt2 | 20.095s | 32.14MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_79_83_89.smt2 | 20.095s | 34.176MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_31_37.smt2 | 20.096s | 31.784MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_59_61.smt2 | 20.096s | 33.26MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_41_43.smt2 | 20.096s | 32.208MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_61_67.smt2 | 20.096s | 30.144MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_151_157.smt2 | 20.097s | 29.656MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_31_37_41.smt2 | 20.098s | 30.504MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_271_277_281.smt2 | 20.099s | 38.804MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_79_83.smt2 | 20.099s | 29.796MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_241_251.smt2 | 20.100s | 47.924MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_163_167_173.smt2 | 20.101s | 32.932MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_181_191.smt2 | 20.102s | 31.532MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_227_229.smt2 | 20.102s | 36.988MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_199_211.smt2 | 20.104s | 36.884MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_157_163_167.smt2 | 20.104s | 39.988MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_257_263_269.smt2 | 20.105s | 29.976MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_257_263.smt2 | 20.106s | 36.944MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_269_271.smt2 | 20.106s | 38.728MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_89_97.smt2 | 20.111s | 30.336MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_47_53_59.smt2 | 20.113s | 33.848MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_67_71_73.smt2 | 20.128s | 30.556MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_151_157_163.smt2 | 20.135s | 37.116MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_47_53.smt2 | 20.135s | 33.74MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_167_173_179.smt2 | 20.136s | 31.472MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_103_107.smt2 | 20.137s | 34.416MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_71_73.smt2 | 20.137s | 32.704MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_131_137.smt2 | 20.160s | 33.808MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_137_139.smt2 | 20.160s | 37.116MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_107_109.smt2 | 20.161s | 35.836MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_181_191_193.smt2 | 20.161s | 40.012MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_61_67_71.smt2 | 20.162s | 33.156MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_107_109_113.smt2 | 20.163s | 32.372MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_263_269_271.smt2 | 20.163s | 32.652MiB| timeout | 0 | | | |non-incremental/LIA/20250213-Frobenius/fcp_167_173.smt2 | 20.163s | 40.828MiB| timeout | 0 | | |