# . * SAT 389 * UNSAT 372 * TIMEOUT 39 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-QF_LIA_hard-timeout10min-ablate_backtracking-bb2
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: c383004968f5bf66a9668a7ae254c83d45ac3afe
Z3 branch: fmcad26_artifact
Z3 options: "-T:600 -v:0 smt.threads=8 tactic.default_tactic=smt smt.auto_config=false smt_parallel.ablate_backtracking=true smt_parallel.core_minimize=false smt_parallel.num_global_bb_batch_threads=2"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_LIA.tar.zst?download=1
Z3 commit message: add ablate_backtracking experiment
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1550.smt2 | 0.835s | 283.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1567.smt2 | 0.865s | 286.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1607.smt2 | 0.868s | 290.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1533.smt2 | 0.878s | 280.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1575.smt2 | 0.914s | 285.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1591.smt2 | 0.988s | 288.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1565.smt2 | 1.032s | 286.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1617.smt2 | 1.048s | 293.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-14.smt2 | 3.319s | 897.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-526410.smt2 | 3.458s | 753.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-03.smt2 | 3.502s | 1362.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-10.smt2 | 3.713s | 1819.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-15.smt2 | 3.789s | 2199.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-09.smt2 | 3.887s | 2200.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-02.smt2 | 4.060s | 2212.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-01.smt2 | 4.116s | 2204.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-343499.smt2 | 4.134s | 738.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-13.smt2 | 4.303s | 2126.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-08.smt2 | 4.368s | 2136.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-08.smt2 | 4.464s | 819.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-14.smt2 | 4.477s | 833.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-04.smt2 | 4.580s | 2135.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-06.smt2 | 4.582s | 2130.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-527358.smt2 | 4.626s | 895.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-08.smt2 | 4.643s | 825.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-15.smt2 | 4.716s | 2126.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-12.smt2 | 4.759s | 2127.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-05.smt2 | 4.762s | 2143.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-11.smt2 | 4.980s | 1315.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-15.smt2 | 4.988s | 1159.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-03.smt2 | 5.025s | 4202.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-04.smt2 | 5.080s | 2142.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-07.smt2 | 5.083s | 2154.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-14.smt2 | 5.156s | 2126.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-413904.smt2 | 5.284s | 960.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-11.smt2 | 5.327s | 2126.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-06.smt2 | 5.391s | 2134.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-10.smt2 | 5.464s | 3219.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-00.smt2 | 5.504s | 2131.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-12.smt2 | 5.788s | 4410.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-10.smt2 | 5.850s | 4409.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-14.smt2 | 5.974s | 1210.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-03.smt2 | 6.048s | 4583.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-07.smt2 | 6.061s | 4657.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-07.smt2 | 6.081s | 1204.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-00.smt2 | 6.110s | 4583.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-09.smt2 | 6.340s | 4468.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-08.smt2 | 6.373s | 1210.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-11.smt2 | 6.374s | 1205.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-06.smt2 | 6.399s | 1204.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-13.smt2 | 6.405s | 4789.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-09.smt2 | 6.486s | 4565.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-06.smt2 | 6.517s | 4698.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-00.smt2 | 6.531s | 4685.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-13.smt2 | 6.536s | 4567.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-12.smt2 | 6.595s | 1213.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-01.smt2 | 6.599s | 1212.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-14.smt2 | 6.663s | 4810.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-05.smt2 | 6.693s | 4752.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-05.smt2 | 6.747s | 1203.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-00.smt2 | 6.750s | 1206.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-02.smt2 | 6.941s | 4647.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-03.smt2 | 7.279s | 2451.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1007795.smt2 | 7.315s | 1331.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r1000w0010/RC-08.smt2 | 7.638s | 1342.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-10.smt2 | 7.693s | 1203.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-392137.smt2 | 8.041s | 948.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-916576.smt2 | 8.047s | 1320.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1270163.smt2 | 8.116s | 1465.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-04.smt2 | 8.198s | 5583.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-03.smt2 | 8.289s | 6465.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-05.smt2 | 8.538s | 6995.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-02.smt2 | 8.547s | 7186.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-01.smt2 | 8.812s | 6993.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-14.smt2 | 8.853s | 6993.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-13.smt2 | 8.883s | 6998.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-08.smt2 | 8.913s | 6992.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-10.smt2 | 8.936s | 6995.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-06.smt2 | 8.976s | 6998.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-09.smt2 | 8.984s | 7002.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-00.smt2 | 9.099s | 6999.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-15.smt2 | 9.314s | 6995.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-11.smt2 | 9.337s | 6993.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-13.smt2 | 9.663s | 6937.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-928134.smt2 | 9.806s | 1596.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1015084.smt2 | 9.833s | 1613.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-38.smt2 | 9.952s | 543.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-415996.smt2 | 10.073s | 1070.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-09.smt2 | 10.131s | 6941.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-379665.smt2 | 10.175s | 1011.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-02.smt2 | 10.440s | 6939.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-267105.smt2 | 10.472s | 802.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-689472.smt2 | 10.578s | 1587.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-01.smt2 | 10.829s | 6832.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-916807.smt2 | 11.068s | 1856.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-794687.smt2 | 11.075s | 1745.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-39.smt2 | 11.284s | 514.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-04.smt2 | 11.482s | 11.105GiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-12.smt2 | 11.499s | 14.072GiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-42.smt2 | 11.506s | 474.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-38.smt2 | 11.560s | 495.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1148089.smt2 | 11.625s | 1747.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-07.smt2 | 11.776s | 14.856GiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-37.smt2 | 11.982s | 586.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-705295.smt2 | 12.186s | 1717.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-38.smt2 | 13.132s | 509.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-38.smt2 | 13.500s | 520.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1205831.smt2 | 14.107s | 2233.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-758897.smt2 | 14.299s | 1869.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-38.smt2 | 14.476s | 555.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-41.smt2 | 14.799s | 553.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-47.smt2 | 14.985s | 248.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-901628.smt2 | 15.033s | 1923.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-40.smt2 | 15.035s | 543.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-39.smt2 | 15.054s | 672.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-47.smt2 | 15.554s | 248.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-917322.smt2 | 16.315s | 2013.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-200.smt2 | 16.505s | 1398.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-198.smt2 | 16.552s | 1375.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-39.smt2 | 16.935s | 458.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-864173.smt2 | 17.171s | 2302.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-196.smt2 | 17.369s | 1209.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-197.smt2 | 17.566s | 1236.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-39.smt2 | 17.971s | 532.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-48.smt2 | 18.098s | 250.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-45.smt2 | 18.419s | 733.0MiB| sat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER10-13-fair.smt2 | 18.851s | 317.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-16-49.smt2 | 18.947s | 893.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-618384.smt2 | 18.954s | 1727.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-40.smt2 | 19.043s | 696.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-199.smt2 | 19.117s | 1369.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-41.smt2 | 19.538s | 716.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-48.smt2 | 19.629s | 798.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-481231.smt2 | 19.648s | 1482.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-43.smt2 | 20.304s | 611.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-8-49.smt2 | 20.313s | 898.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-24-49.smt2 | 20.317s | 844.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-48.smt2 | 20.398s | 729.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-41.smt2 | 20.423s | 874.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-39.smt2 | 20.431s | 826.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-49.smt2 | 20.705s | 905.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-49.smt2 | 20.840s | 813.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-42.smt2 | 20.904s | 663.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-41.smt2 | 21.187s | 767.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-48.smt2 | 21.418s | 743.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-40.smt2 | 21.485s | 726.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-23-50.smt2 | 21.623s | 885.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-37-50.smt2 | 21.661s | 889.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-50.smt2 | 21.710s | 910.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-50.smt2 | 21.720s | 872.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-40.smt2 | 21.924s | 770.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-32-50.smt2 | 22.031s | 804.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-13-50.smt2 | 22.139s | 893.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1185949.smt2 | 22.203s | 2667.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-41.smt2 | 22.714s | 599.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-41.smt2 | 23.041s | 778.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-41.smt2 | 23.418s | 773.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1360077.smt2 | 23.639s | 3134.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1317230.smt2 | 23.798s | 3247.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1192684.smt2 | 23.942s | 2728.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-198.smt2 | 23.961s | 1178.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-329386.smt2 | 23.975s | 1021.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-49.smt2 | 24.020s | 880.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-47.smt2 | 24.115s | 758.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-49.smt2 | 24.200s | 801.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-19-50.smt2 | 24.234s | 929.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-49.smt2 | 24.281s | 792.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-50.smt2 | 24.342s | 922.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-199.smt2 | 24.352s | 777.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-48.smt2 | 24.554s | 505.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-42.smt2 | 24.628s | 769.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-37-47.smt2 | 24.642s | 762.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-41.smt2 | 24.707s | 887.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-49.smt2 | 24.863s | 812.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-17-47.smt2 | 24.901s | 741.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-48.smt2 | 25.061s | 836.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1275621.smt2 | 25.074s | 3405.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-42-50.smt2 | 25.080s | 837.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-49.smt2 | 25.177s | 839.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-50.smt2 | 25.282s | 919.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-46.smt2 | 25.383s | 1047.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-42.smt2 | 25.498s | 932.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-59-50.smt2 | 25.544s | 947.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-57-49.smt2 | 25.763s | 944.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-198.smt2 | 25.880s | 892.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-49.smt2 | 25.913s | 833.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-42.smt2 | 26.150s | 810.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-196.smt2 | 26.419s | 843.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-49.smt2 | 26.446s | 918.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-48.smt2 | 26.458s | 1013.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-48.smt2 | 26.474s | 862.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-42.smt2 | 26.654s | 873.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-42.smt2 | 27.080s | 704.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1317511.smt2 | 27.082s | 3404.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-40-50.smt2 | 27.093s | 844.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-197.smt2 | 27.252s | 988.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1361831.smt2 | 27.325s | 3282.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-76-50.smt2 | 27.452s | 932.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-44.smt2 | 27.549s | 922.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-46.smt2 | 27.787s | 812.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-49.smt2 | 27.791s | 830.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-200.smt2 | 27.810s | 1346.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-60-50.smt2 | 28.080s | 846.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-46.smt2 | 28.178s | 971.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-48.smt2 | 28.269s | 862.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-67-50.smt2 | 28.302s | 861.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-64-50.smt2 | 28.391s | 897.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-69-50.smt2 | 28.414s | 921.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-49.smt2 | 28.574s | 897.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-45.smt2 | 28.608s | 855.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-70-50.smt2 | 28.794s | 854.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-44.smt2 | 28.813s | 873.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-43.smt2 | 29.005s | 717.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-14-49.smt2 | 29.161s | 865.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-48-50.smt2 | 29.320s | 872.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-50.smt2 | 29.350s | 926.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-77-50.smt2 | 29.497s | 878.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-408585.smt2 | 29.597s | 1466.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-49.smt2 | 29.694s | 999.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-65-50.smt2 | 29.721s | 879.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-50.smt2 | 29.969s | 850.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-48.smt2 | 29.974s | 839.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-57-50.smt2 | 30.013s | 884.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-44.smt2 | 30.019s | 1086.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-50.smt2 | 30.227s | 898.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-46.smt2 | 30.320s | 885.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-47.smt2 | 30.496s | 940.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-42.smt2 | 30.576s | 720.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-43.smt2 | 30.761s | 988.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1121941.smt2 | 30.793s | 3171.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-45.smt2 | 30.894s | 1039.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-19-49.smt2 | 30.895s | 965.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-199.smt2 | 31.112s | 1520.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-50.smt2 | 31.207s | 1023.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-46.smt2 | 31.287s | 975.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-43.smt2 | 31.289s | 1103.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-42.smt2 | 31.481s | 936.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-47.smt2 | 31.523s | 838.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-46.smt2 | 31.601s | 907.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-50.smt2 | 31.828s | 1115.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-47.smt2 | 31.866s | 910.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-47.smt2 | 31.906s | 915.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-42.smt2 | 31.956s | 1075.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-46.smt2 | 32.023s | 1066.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-44.smt2 | 32.137s | 1061.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-46.smt2 | 32.231s | 903.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-50.smt2 | 32.289s | 929.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-43.smt2 | 32.300s | 550.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-58-50.smt2 | 32.650s | 1098.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-49.smt2 | 32.663s | 827.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-42.smt2 | 32.685s | 729.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-68-50.smt2 | 32.865s | 880.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-50.smt2 | 32.886s | 863.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-42.smt2 | 33.044s | 970.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-47.smt2 | 33.132s | 970.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-48.smt2 | 33.396s | 841.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-47.smt2 | 33.485s | 1021.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-48.smt2 | 33.507s | 1058.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-44.smt2 | 33.546s | 1051.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-50.smt2 | 33.847s | 978.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-42.smt2 | 34.522s | 1036.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-47.smt2 | 34.822s | 855.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-45.smt2 | 35.020s | 1024.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-50.smt2 | 35.083s | 854.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-43.smt2 | 35.113s | 863.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-45.smt2 | 35.395s | 1076.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-49.smt2 | 35.539s | 887.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-43.smt2 | 35.730s | 1087.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-49.smt2 | 35.738s | 1024.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-50.smt2 | 35.832s | 866.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-50.smt2 | 35.862s | 998.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-48.smt2 | 35.862s | 757.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-200.smt2 | 35.888s | 790.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-43.smt2 | 36.022s | 1102.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-47.smt2 | 36.087s | 1066.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-63-50.smt2 | 36.179s | 1317.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-45.smt2 | 36.210s | 1128.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-47.smt2 | 36.228s | 941.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-39-50.smt2 | 36.437s | 944.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-43.smt2 | 36.484s | 1160.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-43.smt2 | 36.522s | 1033.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-46.smt2 | 36.678s | 1390.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-44.smt2 | 36.678s | 1040.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-49.smt2 | 36.741s | 795.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-48.smt2 | 36.765s | 925.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-46.smt2 | 36.969s | 1062.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-47.smt2 | 37.189s | 968.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-43.smt2 | 37.528s | 1167.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-45.smt2 | 37.615s | 1146.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-46.smt2 | 37.647s | 861.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-45.smt2 | 37.702s | 1265.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-47.smt2 | 37.725s | 946.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-906586.smt2 | 38.015s | 3270.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-48.smt2 | 38.387s | 1090.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-45.smt2 | 38.403s | 746.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-44.smt2 | 38.406s | 1613.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-50.smt2 | 38.455s | 1090.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-43.smt2 | 38.582s | 1036.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-13-50.smt2 | 38.595s | 846.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-45.smt2 | 38.622s | 1327.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-49.smt2 | 38.650s | 928.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-48.smt2 | 39.340s | 1146.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-46.smt2 | 39.351s | 1464.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-48.smt2 | 39.364s | 1130.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1365816.smt2 | 39.407s | 4070.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-47.smt2 | 39.625s | 1145.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-44.smt2 | 39.804s | 1282.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-45.smt2 | 39.943s | 1109.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-44.smt2 | 39.972s | 1344.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-45.smt2 | 40.163s | 1243.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-45.smt2 | 40.176s | 1055.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-50.smt2 | 40.315s | 964.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-44.smt2 | 40.319s | 1066.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-48.smt2 | 40.329s | 1105.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-49.smt2 | 40.731s | 1046.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-48.smt2 | 40.850s | 921.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-48.smt2 | 40.890s | 1247.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-44.smt2 | 40.916s | 840.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-48.smt2 | 40.925s | 1116.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-50.smt2 | 40.947s | 721.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-45.smt2 | 41.221s | 1314.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-44.smt2 | 41.276s | 1114.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-48.smt2 | 41.608s | 1113.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-44.smt2 | 41.708s | 1384.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-50.smt2 | 41.930s | 1015.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-47.smt2 | 41.954s | 1050.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-50.smt2 | 42.179s | 1199.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-21-40.smt2 | 42.186s | 1074.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-49.smt2 | 42.199s | 561.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-49.smt2 | 42.409s | 1134.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-48.smt2 | 42.556s | 1419.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-41-50.smt2 | 42.595s | 1071.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-50.smt2 | 42.999s | 1208.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-49.smt2 | 43.334s | 1034.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-44.smt2 | 43.357s | 1085.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-50.smt2 | 43.445s | 599.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-47.smt2 | 43.509s | 1043.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-50.smt2 | 43.611s | 1177.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-45.smt2 | 43.785s | 1031.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-48.smt2 | 43.858s | 908.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-49.smt2 | 43.959s | 885.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-50.smt2 | 44.045s | 938.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-48.smt2 | 44.083s | 619.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-49.smt2 | 44.258s | 1042.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-46.smt2 | 44.340s | 1301.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-47.smt2 | 44.497s | 1296.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-48.smt2 | 44.750s | 1063.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-49.smt2 | 44.771s | 991.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-48.smt2 | 45.029s | 1281.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-46.smt2 | 45.416s | 1405.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-46.smt2 | 45.483s | 1304.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-46.smt2 | 45.637s | 1381.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-48.smt2 | 45.866s | 1147.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-45.smt2 | 45.896s | 1793.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-46.smt2 | 46.897s | 1029.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-48.smt2 | 47.065s | 1491.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-46.smt2 | 47.228s | 1332.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-17-47.smt2 | 47.348s | 757.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-50.smt2 | 47.462s | 932.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-48.smt2 | 47.629s | 1372.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-47.smt2 | 47.895s | 1145.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-48.smt2 | 47.930s | 1382.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-47.smt2 | 48.289s | 1228.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-46.smt2 | 48.354s | 1380.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-49.smt2 | 48.359s | 1153.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-48.smt2 | 48.446s | 1890.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-46.smt2 | 48.827s | 1659.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-50.smt2 | 49.142s | 1091.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-49.smt2 | 49.598s | 1207.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-49.smt2 | 49.975s | 1466.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-49.smt2 | 50.098s | 1076.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-47.smt2 | 50.273s | 1336.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-49.smt2 | 50.282s | 1553.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-50.smt2 | 50.286s | 1428.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-45.smt2 | 50.520s | 1409.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-47.smt2 | 50.732s | 1763.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-48.smt2 | 50.806s | 1443.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-50.smt2 | 50.969s | 1106.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-47.smt2 | 51.266s | 1489.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-49.smt2 | 51.285s | 1534.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-49.smt2 | 51.337s | 1414.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-47.smt2 | 51.686s | 1419.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-49.smt2 | 51.892s | 1229.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-196.smt2 | 52.737s | 775.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-50.smt2 | 52.949s | 1129.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-48.smt2 | 52.986s | 1073.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-50.smt2 | 53.347s | 1497.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-47.smt2 | 53.760s | 1376.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-46.smt2 | 53.885s | 1603.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-50.smt2 | 54.097s | 1242.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-47.smt2 | 54.548s | 1452.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-46.smt2 | 54.765s | 1438.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-50.smt2 | 54.906s | 1227.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-47.smt2 | 55.290s | 1258.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-46.smt2 | 55.435s | 1799.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-47.smt2 | 55.778s | 1780.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-46.smt2 | 55.867s | 1428.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-47.smt2 | 55.973s | 1576.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-49.smt2 | 56.154s | 999.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-49.smt2 | 56.175s | 1109.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-46.smt2 | 56.376s | 1384.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-46.smt2 | 56.912s | 1356.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-46.smt2 | 57.132s | 1913.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-48.smt2 | 57.270s | 1656.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-48.smt2 | 57.283s | 1437.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-46.smt2 | 57.449s | 1697.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-46.smt2 | 58.264s | 1933.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-48.smt2 | 58.289s | 1459.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-47.smt2 | 58.396s | 1403.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-46.smt2 | 58.475s | 1496.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-48.smt2 | 58.720s | 1213.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER10-14-fair.smt2 | 59.133s | 349.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-48.smt2 | 59.477s | 1463.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-48.smt2 | 59.680s | 1591.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-48.smt2 | 59.682s | 1580.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-48.smt2 | 59.955s | 1475.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-46.smt2 | 60.278s | 1073.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-50.smt2 | 60.466s | 1630.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-49.smt2 | 60.624s | 1120.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-47.smt2 | 60.642s | 1506.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-48.smt2 | 60.754s | 1460.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-48.smt2 | 60.774s | 1701.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-48.smt2 | 61.433s | 1347.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-47.smt2 | 61.592s | 1124.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-48.smt2 | 61.658s | 970.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-48.smt2 | 61.975s | 1562.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-48.smt2 | 62.051s | 1868.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-48.smt2 | 62.162s | 1239.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-48.smt2 | 62.337s | 1486.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-50.smt2 | 62.407s | 1452.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-321761.smt2 | 62.542s | 1078.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-46.smt2 | 62.551s | 1253.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-49.smt2 | 62.580s | 1381.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-50.smt2 | 62.594s | 1471.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-50.smt2 | 63.102s | 1159.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-50.smt2 | 63.144s | 1484.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-49.smt2 | 63.153s | 754.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-48.smt2 | 63.939s | 1061.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-50.smt2 | 64.062s | 1298.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-48.smt2 | 64.233s | 1925.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-49.smt2 | 64.335s | 1862.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1268455.smt2 | 64.499s | 4059.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-50.smt2 | 64.518s | 1630.0MiB| sat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER11-14-fair.smt2 | 65.345s | 371.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-48.smt2 | 65.411s | 1654.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-49.smt2 | 65.695s | 1450.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-49.smt2 | 66.440s | 1995.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-50.smt2 | 66.484s | 1087.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-46.smt2 | 66.507s | 1279.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-49.smt2 | 66.526s | 1262.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-48.smt2 | 66.693s | 1327.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-47.smt2 | 66.751s | 1419.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-47.smt2 | 66.784s | 1650.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-49.smt2 | 66.887s | 963.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-48.smt2 | 67.507s | 1885.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-46.smt2 | 68.706s | 1910.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-50.smt2 | 68.948s | 1547.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-49.smt2 | 69.530s | 1031.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-49.smt2 | 69.716s | 1491.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-48.smt2 | 70.041s | 1616.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-48.smt2 | 70.236s | 1428.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-50.smt2 | 70.453s | 1149.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-48.smt2 | 70.919s | 2131.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-49.smt2 | 70.989s | 1757.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-48.smt2 | 71.419s | 1378.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-49.smt2 | 71.804s | 1404.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-49.smt2 | 72.260s | 1720.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-48.smt2 | 72.807s | 1656.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-46.smt2 | 72.854s | 1299.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-49.smt2 | 72.965s | 2152.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-49.smt2 | 73.144s | 2342.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-50.smt2 | 73.484s | 1622.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-48.smt2 | 73.708s | 1989.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-247831.smt2 | 73.771s | 785.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-48.smt2 | 74.697s | 1299.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-46.smt2 | 74.779s | 1304.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-50.smt2 | 74.806s | 1703.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-48.smt2 | 75.659s | 1595.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-50.smt2 | 76.045s | 1259.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-48.smt2 | 76.151s | 1644.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-46.smt2 | 76.497s | 1400.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-48.smt2 | 76.535s | 1573.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-49.smt2 | 76.615s | 1394.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-49.smt2 | 76.770s | 1608.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-50.smt2 | 77.255s | 942.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-48.smt2 | 78.050s | 2302.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-46.smt2 | 78.347s | 1539.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-50.smt2 | 78.909s | 1928.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-44.smt2 | 78.938s | 1653.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-46.smt2 | 78.953s | 1791.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-46.smt2 | 79.167s | 1335.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-518109.smt2 | 79.338s | 1799.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1452366.smt2 | 79.746s | 5459.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-50.smt2 | 79.826s | 1650.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-47.smt2 | 79.909s | 1613.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-50.smt2 | 80.571s | 2249.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-48.smt2 | 80.677s | 1639.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-48.smt2 | 80.821s | 1958.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-47.smt2 | 81.003s | 1246.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-46.smt2 | 81.866s | 1680.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-50.smt2 | 82.365s | 1728.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-47.smt2 | 82.516s | 1645.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-50.smt2 | 83.160s | 1460.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-47.smt2 | 83.465s | 1747.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-48.smt2 | 85.281s | 1215.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-47.smt2 | 85.295s | 1908.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-48.smt2 | 85.378s | 1587.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-49.smt2 | 85.712s | 2236.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-50.smt2 | 86.167s | 2251.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-50.smt2 | 86.198s | 2036.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-48.smt2 | 86.388s | 1736.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-50.smt2 | 86.878s | 1295.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-49.smt2 | 87.258s | 2125.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-48.smt2 | 87.903s | 1378.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-50.smt2 | 88.095s | 1791.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-46.smt2 | 88.233s | 1544.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-50.smt2 | 88.345s | 1161.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-47.smt2 | 88.913s | 1880.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-48.smt2 | 89.085s | 1941.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-49.smt2 | 89.139s | 1855.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-50.smt2 | 89.965s | 1409.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-48.smt2 | 89.991s | 1501.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-48.smt2 | 90.181s | 2390.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-46.smt2 | 90.352s | 1602.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-46.smt2 | 90.358s | 1088.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-50.smt2 | 90.981s | 1959.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-49.smt2 | 91.100s | 1645.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-46.smt2 | 91.667s | 1176.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1262176.smt2 | 93.555s | 5606.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-46.smt2 | 94.630s | 1184.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-49.smt2 | 94.670s | 1619.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-50.smt2 | 95.020s | 2227.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1265513.smt2 | 95.094s | 5461.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-63-50.smt2 | 95.828s | 2019.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-49.smt2 | 96.316s | 2425.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-48.smt2 | 96.942s | 1383.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-50.smt2 | 97.208s | 2349.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-47.smt2 | 98.270s | 1386.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-48.smt2 | 98.343s | 2006.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-48.smt2 | 98.425s | 1960.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-48.smt2 | 100.701s | 1060.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-49.smt2 | 100.971s | 1699.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-50.smt2 | 101.471s | 1807.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-46.smt2 | 102.407s | 1670.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-48.smt2 | 102.495s | 2231.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-50.smt2 | 105.302s | 1619.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-50.smt2 | 105.595s | 1259.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-50.smt2 | 107.543s | 2376.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-46.smt2 | 108.230s | 1409.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-31-42.smt2 | 108.609s | 2422.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-49.smt2 | 109.435s | 1426.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-23-41.smt2 | 110.387s | 1796.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-50.smt2 | 111.511s | 2398.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-50.smt2 | 111.606s | 1262.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-46.smt2 | 115.414s | 1361.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-47.smt2 | 117.300s | 2303.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-46.smt2 | 119.693s | 1398.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-47.smt2 | 119.949s | 1130.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-49.smt2 | 121.092s | 1750.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-47.smt2 | 121.740s | 1534.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-45.smt2 | 122.595s | 2614.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-50.smt2 | 122.770s | 1200.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-47.smt2 | 123.692s | 1360.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-50.smt2 | 124.334s | 2255.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-47.smt2 | 125.785s | 1137.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-48.smt2 | 126.867s | 1887.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-49.smt2 | 127.677s | 1745.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-47.smt2 | 130.656s | 2436.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-50.smt2 | 131.219s | 1684.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-47.smt2 | 131.730s | 1309.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-26-43.smt2 | 133.020s | 2465.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-47.smt2 | 134.800s | 1466.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-47.smt2 | 135.903s | 1857.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-269353.smt2 | 136.879s | 890.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-47.smt2 | 136.911s | 2409.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-46.smt2 | 137.786s | 2155.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-48.smt2 | 139.014s | 1661.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-49.smt2 | 140.664s | 1875.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-46.smt2 | 142.135s | 1093.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-46.smt2 | 142.308s | 2568.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-46.smt2 | 143.777s | 2016.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-47.smt2 | 144.644s | 1780.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-47.smt2 | 145.948s | 1668.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1072007.smt2 | 147.404s | 5855.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-48.smt2 | 147.811s | 1587.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-47.smt2 | 149.041s | 2223.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-47.smt2 | 150.311s | 2030.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-49.smt2 | 150.573s | 2302.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-50.smt2 | 154.227s | 2312.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-49.smt2 | 154.472s | 1370.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-46.smt2 | 154.561s | 1925.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-46.smt2 | 155.187s | 1873.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-47.smt2 | 156.048s | 1897.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-50.smt2 | 157.527s | 1587.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-47.smt2 | 157.756s | 1265.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-49.smt2 | 157.886s | 1610.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-495717.smt2 | 159.835s | 2213.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-46.smt2 | 162.366s | 1489.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-47.smt2 | 162.587s | 1477.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-278378.smt2 | 162.846s | 936.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-47.smt2 | 163.373s | 1786.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-46.smt2 | 165.570s | 2804.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-47.smt2 | 165.678s | 1556.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-49.smt2 | 167.976s | 2307.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-46.smt2 | 169.171s | 3169.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-50.smt2 | 175.414s | 1905.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-46.smt2 | 175.822s | 1711.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-46.smt2 | 176.806s | 1344.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-47.smt2 | 177.069s | 2104.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-46.smt2 | 177.273s | 2647.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-49.smt2 | 177.317s | 1726.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-48.smt2 | 177.463s | 2163.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-48.smt2 | 179.892s | 3075.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-50.smt2 | 183.681s | 1638.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-46.smt2 | 183.785s | 2099.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-46.smt2 | 185.428s | 3141.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-46.smt2 | 186.900s | 1676.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-47.smt2 | 187.666s | 3689.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-49.smt2 | 188.624s | 2357.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-50.smt2 | 191.156s | 1880.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-50.smt2 | 192.099s | 1903.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-47.smt2 | 194.105s | 1669.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-47.smt2 | 194.251s | 1934.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-46.smt2 | 195.730s | 1960.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-46.smt2 | 196.420s | 1930.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-46.smt2 | 198.091s | 1408.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-50.smt2 | 198.206s | 1866.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-48.smt2 | 198.818s | 1671.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-47.smt2 | 203.983s | 2228.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-48.smt2 | 206.032s | 1369.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-47.smt2 | 209.021s | 3328.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1138192.smt2 | 211.993s | 6053.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-46.smt2 | 212.917s | 1795.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-48.smt2 | 216.885s | 2703.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-49.smt2 | 217.197s | 2064.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-47.smt2 | 217.767s | 1970.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-46.smt2 | 217.963s | 2820.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-49.smt2 | 218.622s | 1457.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-46.smt2 | 220.157s | 2059.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-50.smt2 | 221.987s | 2170.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-47.smt2 | 224.602s | 1745.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-48.smt2 | 225.142s | 1878.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-49.smt2 | 225.153s | 2676.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-46.smt2 | 225.375s | 4452.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-46.smt2 | 226.807s | 2083.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-47.smt2 | 227.117s | 2590.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-47.smt2 | 228.577s | 1963.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-49.smt2 | 229.448s | 2062.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-50.smt2 | 229.508s | 2196.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-48.smt2 | 231.542s | 2110.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-46.smt2 | 237.118s | 2045.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-50.smt2 | 237.372s | 3264.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-47.smt2 | 238.263s | 3017.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-48.smt2 | 238.606s | 1479.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-46.smt2 | 240.664s | 2506.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-49.smt2 | 240.771s | 2370.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-50.smt2 | 240.891s | 3967.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-50.smt2 | 242.415s | 2495.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-47.smt2 | 242.961s | 2409.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-47.smt2 | 244.360s | 2898.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-48.smt2 | 244.433s | 1900.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-49.smt2 | 245.463s | 3854.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-47.smt2 | 246.897s | 2260.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-46.smt2 | 247.739s | 1831.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-50.smt2 | 249.976s | 2175.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-48.smt2 | 251.941s | 1951.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-46.smt2 | 253.116s | 2026.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-47.smt2 | 254.205s | 2914.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-48.smt2 | 254.417s | 3950.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-47.smt2 | 254.781s | 2077.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-47.smt2 | 258.638s | 2322.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-47.smt2 | 262.798s | 3201.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-46.smt2 | 265.227s | 1622.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-50.smt2 | 265.625s | 1574.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-46.smt2 | 267.086s | 1974.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-50.smt2 | 270.133s | 1709.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-50.smt2 | 271.565s | 1893.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-50.smt2 | 273.899s | 3559.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-729964.smt2 | 277.156s | 4008.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-49.smt2 | 279.045s | 2351.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-48.smt2 | 285.269s | 2888.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-50.smt2 | 289.087s | 1953.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-49.smt2 | 295.935s | 3002.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER11-15-fair.smt2 | 297.810s | 486.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-658040.smt2 | 299.097s | 3325.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-47.smt2 | 299.323s | 3378.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-49.smt2 | 301.960s | 2826.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-50.smt2 | 304.678s | 2522.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-49.smt2 | 305.277s | 1390.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-49.smt2 | 309.170s | 3148.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-46.smt2 | 316.634s | 2026.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-47.smt2 | 317.275s | 2304.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-48.smt2 | 323.657s | 2976.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-46.smt2 | 326.252s | 2232.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-47.smt2 | 328.710s | 1774.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-49.smt2 | 331.470s | 2999.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-47.smt2 | 332.577s | 1429.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-49.smt2 | 333.248s | 2646.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-50.smt2 | 335.813s | 2527.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-48.smt2 | 338.144s | 2278.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-46.smt2 | 338.330s | 2226.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-49.smt2 | 339.642s | 2219.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-285271.smt2 | 340.022s | 961.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-49.smt2 | 343.343s | 1602.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-47.smt2 | 347.424s | 3228.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-49.smt2 | 354.734s | 2042.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-50.smt2 | 356.670s | 2113.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-47.smt2 | 360.886s | 2257.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-48.smt2 | 361.889s | 3343.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-46.smt2 | 362.482s | 3785.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-50.smt2 | 363.445s | 1984.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-49.smt2 | 373.917s | 2824.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-48.smt2 | 378.490s | 2076.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-49.smt2 | 389.419s | 2372.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-50.smt2 | 390.065s | 2100.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-47.smt2 | 395.626s | 1612.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-283008.smt2 | 401.925s | 975.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-46.smt2 | 405.783s | 2332.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-48.smt2 | 406.548s | 2437.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-48.smt2 | 407.663s | 2068.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-49.smt2 | 409.132s | 3209.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-50.smt2 | 420.243s | 4111.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-49.smt2 | 420.657s | 2148.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-49.smt2 | 420.873s | 2066.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-50.smt2 | 425.355s | 3442.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-49.smt2 | 434.331s | 1944.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-928960.smt2 | 437.571s | 4811.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-368069.smt2 | 439.623s | 1606.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-50.smt2 | 441.233s | 1926.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-49.smt2 | 443.097s | 3888.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-48.smt2 | 446.211s | 2243.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-49.smt2 | 449.385s | 2910.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-49.smt2 | 450.417s | 2849.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-49.smt2 | 457.031s | 2587.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-48.smt2 | 464.146s | 1830.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-50.smt2 | 464.311s | 2036.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-47.smt2 | 466.269s | 2090.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-50.smt2 | 472.206s | 2924.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-49.smt2 | 477.441s | 1954.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-49.smt2 | 483.985s | 2601.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-48.smt2 | 492.511s | 4855.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-48.smt2 | 505.622s | 3235.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-49.smt2 | 515.000s | 2934.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-49.smt2 | 520.005s | 2947.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-47.smt2 | 524.174s | 2605.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-50.smt2 | 532.910s | 2488.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-49.smt2 | 536.000s | 3493.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-49.smt2 | 542.276s | 2649.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-50.smt2 | 542.542s | 1806.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-49.smt2 | 542.899s | 1866.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-47.smt2 | 544.600s | 2555.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-478122.smt2 | 546.155s | 2372.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-48.smt2 | 547.303s | 3603.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-49.smt2 | 566.431s | 4013.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-50.smt2 | 567.115s | 3608.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-50.smt2 | 569.143s | 2485.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-50.smt2 | 571.998s | 2558.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-50.smt2 | 572.258s | 3268.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-50.smt2 | 575.895s | 2866.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-762853.smt2 | 591.653s | 4657.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-50.smt2 | 593.922s | 3550.0MiB| sat | 0 | | | |non-incremental/QF_LIA/RWS/Example_7.txt.smt2 | 600.092s | 482.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/RWS/Example_15.txt.smt2 | 600.118s | 504.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-49.smt2 | 600.197s | 1649.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-49.smt2 | 600.228s | 1792.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-48.smt2 | 600.251s | 2166.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-49.smt2 | 600.262s | 2145.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-50.smt2 | 600.262s | 2013.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-49.smt2 | 600.274s | 2274.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-49.smt2 | 600.279s | 2098.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-48.smt2 | 600.283s | 1977.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-50.smt2 | 600.289s | 2383.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-50.smt2 | 600.293s | 2369.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-49.smt2 | 600.301s | 2572.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-49.smt2 | 600.304s | 2622.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-50.smt2 | 600.310s | 2116.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-50.smt2 | 600.314s | 2565.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-50.smt2 | 600.321s | 2633.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-50.smt2 | 600.324s | 2522.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-357303.smt2 | 600.335s | 1603.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-49.smt2 | 600.337s | 2785.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-47.smt2 | 600.352s | 2973.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-49.smt2 | 600.374s | 3127.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-50.smt2 | 600.391s | 2845.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-50.smt2 | 600.432s | 3869.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-50.smt2 | 600.434s | 2720.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-49.smt2 | 600.445s | 3662.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-49.smt2 | 600.450s | 3900.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-49.smt2 | 600.455s | 3934.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-50.smt2 | 600.492s | 4117.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-50.smt2 | 600.493s | 4115.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-50.smt2 | 600.503s | 3996.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/20231117-c_inference/80_80_71_17_unsat.smt2 | 600.586s | 3376.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-50.smt2 | 600.596s | 4987.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-50.smt2 | 600.664s | 3617.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-985518.smt2 | 600.781s | 7069.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1228327.smt2 | 601.041s | 9852.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1400961.smt2 | 601.226s | 11.453GiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1060546.smt2 | 601.237s | 7430.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1472027.smt2 | 601.519s | 12.494GiB| timeout | 0 | | |