# . * SAT 393 * UNSAT 398 * TIMEOUT 9 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-4-QF_LIA_hard-timeout10min-bb2
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: c383004968f5bf66a9668a7ae254c83d45ac3afe
Z3 branch: fmcad26_artifact
Z3 options: "-T:1200 -v:0 smt.threads=4 tactic.default_tactic=smt smt.auto_config=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.586s | 201.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1607.smt2 | 0.641s | 207.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1567.smt2 | 0.647s | 204.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1575.smt2 | 0.664s | 204.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1533.smt2 | 0.666s | 199.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1565.smt2 | 0.768s | 203.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1591.smt2 | 0.785s | 206.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1617.smt2 | 0.828s | 208.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-14.smt2 | 2.116s | 628.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-03.smt2 | 2.286s | 888.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-526410.smt2 | 2.320s | 490.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-10.smt2 | 2.372s | 1176.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-02.smt2 | 2.442s | 1396.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-09.smt2 | 2.458s | 1391.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-15.smt2 | 2.510s | 1391.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-01.smt2 | 2.653s | 1397.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-08.smt2 | 3.043s | 602.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-08.smt2 | 3.044s | 596.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-14.smt2 | 3.079s | 597.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-12.smt2 | 3.079s | 1349.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-14.smt2 | 3.115s | 1349.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-06.smt2 | 3.115s | 1360.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-13.smt2 | 3.160s | 1355.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-04.smt2 | 3.180s | 1352.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-15.smt2 | 3.212s | 1346.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-04.smt2 | 3.215s | 1353.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-05.smt2 | 3.275s | 1373.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-08.smt2 | 3.290s | 1361.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-15.smt2 | 3.563s | 921.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-11.smt2 | 3.571s | 1346.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-07.smt2 | 3.644s | 1366.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-11.smt2 | 3.678s | 941.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-03.smt2 | 3.727s | 2578.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-527358.smt2 | 3.764s | 577.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-06.smt2 | 3.767s | 1354.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-00.smt2 | 3.775s | 1359.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-10.smt2 | 4.036s | 2017.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-03.smt2 | 4.241s | 2836.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-10.smt2 | 4.259s | 2730.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-06.smt2 | 4.396s | 852.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-07.smt2 | 4.412s | 2894.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-01.smt2 | 4.419s | 858.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-12.smt2 | 4.465s | 2731.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-12.smt2 | 4.467s | 855.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-09.smt2 | 4.520s | 2900.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-10.smt2 | 4.551s | 852.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-00.smt2 | 4.552s | 2837.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-07.smt2 | 4.559s | 851.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-08.smt2 | 4.562s | 855.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-413904.smt2 | 4.585s | 616.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-11.smt2 | 4.614s | 852.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-14.smt2 | 4.635s | 856.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-00.smt2 | 4.654s | 852.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-13.smt2 | 4.672s | 2825.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-02.smt2 | 4.694s | 2960.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-05.smt2 | 4.725s | 852.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-09.smt2 | 4.728s | 2825.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-13.smt2 | 4.733s | 2931.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-00.smt2 | 4.774s | 3005.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-06.smt2 | 4.835s | 3049.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-343499.smt2 | 4.886s | 523.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-05.smt2 | 4.886s | 3030.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-14.smt2 | 4.945s | 2982.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-03.smt2 | 4.983s | 1600.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1007795.smt2 | 5.146s | 887.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r1000w0010/RC-08.smt2 | 5.232s | 1032.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1270163.smt2 | 5.707s | 1019.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-04.smt2 | 5.968s | 3481.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-03.smt2 | 6.467s | 4010.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-02.smt2 | 6.494s | 4441.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-13.smt2 | 6.510s | 4329.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-08.smt2 | 6.557s | 4326.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-10.smt2 | 6.585s | 4325.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-06.smt2 | 6.620s | 4329.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-01.smt2 | 6.628s | 4326.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-15.smt2 | 6.657s | 4328.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-14.smt2 | 6.704s | 4326.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-05.smt2 | 6.725s | 4328.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-916576.smt2 | 6.928s | 978.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-11.smt2 | 6.992s | 4328.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-00.smt2 | 7.005s | 4330.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-09.smt2 | 7.034s | 4297.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-13.smt2 | 7.045s | 4293.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-392137.smt2 | 7.093s | 626.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-928134.smt2 | 7.311s | 1077.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-02.smt2 | 7.526s | 4293.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-38.smt2 | 8.491s | 448.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-42.smt2 | 8.536s | 344.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-12.smt2 | 8.555s | 8569.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1148089.smt2 | 8.769s | 1155.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-04.smt2 | 8.772s | 6287.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-329386.smt2 | 8.809s | 554.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-916807.smt2 | 8.959s | 1194.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-01.smt2 | 8.970s | 4152.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-07.smt2 | 9.049s | 9048.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-415996.smt2 | 9.125s | 696.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-37.smt2 | 10.107s | 473.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-705295.smt2 | 10.706s | 1106.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-38.smt2 | 11.018s | 407.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1205831.smt2 | 11.052s | 1440.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-379665.smt2 | 11.108s | 700.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-38.smt2 | 11.439s | 428.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-39.smt2 | 12.718s | 451.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1015084.smt2 | 12.814s | 1445.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-758897.smt2 | 12.950s | 1217.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-901628.smt2 | 13.358s | 1284.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-917322.smt2 | 13.975s | 1314.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-50.smt2 | 14.254s | 572.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-38.smt2 | 14.311s | 541.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-864173.smt2 | 14.579s | 1513.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-47.smt2 | 14.693s | 198.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-47.smt2 | 14.696s | 198.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-09.smt2 | 14.734s | 5284.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-8-49.smt2 | 15.238s | 580.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-38.smt2 | 15.241s | 714.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-44.smt2 | 15.610s | 433.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-199.smt2 | 15.926s | 668.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-16-49.smt2 | 16.202s | 577.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-39.smt2 | 16.242s | 655.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-794687.smt2 | 16.367s | 1362.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-39.smt2 | 16.534s | 463.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-40.smt2 | 16.565s | 531.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-198.smt2 | 16.699s | 765.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-39.smt2 | 16.729s | 584.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-689472.smt2 | 16.787s | 1382.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-48.smt2 | 17.075s | 200.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-13-50.smt2 | 17.283s | 597.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-32-50.smt2 | 17.559s | 601.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-42.smt2 | 17.710s | 767.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-49.smt2 | 17.760s | 632.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-481231.smt2 | 17.793s | 936.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1185949.smt2 | 17.964s | 1674.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-39.smt2 | 18.365s | 558.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-49.smt2 | 18.637s | 637.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-50.smt2 | 18.768s | 608.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-24-49.smt2 | 18.839s | 639.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-42-50.smt2 | 18.855s | 644.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-196.smt2 | 18.958s | 980.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-47.smt2 | 19.099s | 541.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-48.smt2 | 19.442s | 578.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-23-50.smt2 | 19.537s | 707.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1360077.smt2 | 19.560s | 1951.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-37-50.smt2 | 19.730s | 669.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1192684.smt2 | 19.891s | 1669.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-197.smt2 | 19.905s | 811.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-49.smt2 | 19.910s | 595.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-48-50.smt2 | 20.505s | 616.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-19-50.smt2 | 20.629s | 618.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-49.smt2 | 20.714s | 613.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-43.smt2 | 20.826s | 495.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-40.smt2 | 20.862s | 452.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-50.smt2 | 20.961s | 663.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-48.smt2 | 21.010s | 633.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-41.smt2 | 21.273s | 588.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-50.smt2 | 21.572s | 670.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-46.smt2 | 21.921s | 644.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1275621.smt2 | 21.940s | 2183.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-49.smt2 | 21.940s | 592.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-42.smt2 | 21.999s | 554.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-49.smt2 | 22.000s | 628.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-47.smt2 | 22.094s | 507.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-60-50.smt2 | 22.285s | 619.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1361831.smt2 | 22.350s | 2055.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-45.smt2 | 22.420s | 631.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-49.smt2 | 22.664s | 612.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-57-49.smt2 | 22.697s | 702.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-50.smt2 | 22.774s | 685.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-49.smt2 | 22.797s | 611.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-40.smt2 | 22.815s | 651.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-77-50.smt2 | 22.905s | 614.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-19-49.smt2 | 22.907s | 665.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-40.smt2 | 22.925s | 873.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-49.smt2 | 22.977s | 588.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-49.smt2 | 22.996s | 670.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-44.smt2 | 23.186s | 595.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-67-50.smt2 | 23.312s | 627.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-46.smt2 | 23.428s | 644.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-41.smt2 | 23.435s | 597.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-199.smt2 | 23.624s | 905.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-64-50.smt2 | 23.792s | 651.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-59-50.smt2 | 23.903s | 609.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-46.smt2 | 24.153s | 637.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-198.smt2 | 24.241s | 808.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-50.smt2 | 24.392s | 728.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-47.smt2 | 24.406s | 657.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-41.smt2 | 24.617s | 440.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-65-50.smt2 | 24.697s | 689.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-41.smt2 | 24.738s | 466.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1317511.smt2 | 24.780s | 2199.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-46.smt2 | 24.949s | 778.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-41.smt2 | 24.962s | 745.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-69-50.smt2 | 25.148s | 641.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-48.smt2 | 25.154s | 775.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-58-50.smt2 | 25.166s | 615.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-49.smt2 | 25.285s | 765.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-76-50.smt2 | 25.307s | 626.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-49.smt2 | 25.670s | 653.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1121941.smt2 | 25.770s | 1970.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-68-50.smt2 | 25.874s | 656.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-57-50.smt2 | 25.917s | 637.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-46.smt2 | 26.045s | 760.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-41.smt2 | 26.055s | 526.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-48.smt2 | 26.256s | 585.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-48.smt2 | 26.273s | 600.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-50.smt2 | 26.361s | 703.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-48.smt2 | 26.433s | 597.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-41.smt2 | 26.532s | 858.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-47.smt2 | 26.654s | 811.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-48.smt2 | 27.092s | 618.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-196.smt2 | 27.102s | 1052.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-196.smt2 | 27.149s | 678.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-48.smt2 | 27.457s | 692.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-70-50.smt2 | 27.593s | 641.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-47.smt2 | 27.689s | 674.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-17-47.smt2 | 27.712s | 606.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-50.smt2 | 27.765s | 682.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-200.smt2 | 27.825s | 847.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-41.smt2 | 27.837s | 349.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-47.smt2 | 27.914s | 764.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-47.smt2 | 27.931s | 658.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-47.smt2 | 28.061s | 728.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-46.smt2 | 28.068s | 662.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-43.smt2 | 28.170s | 542.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-40-50.smt2 | 28.181s | 621.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-37-47.smt2 | 28.281s | 651.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-247831.smt2 | 28.388s | 491.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-45.smt2 | 28.431s | 964.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-48.smt2 | 28.933s | 670.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-50.smt2 | 29.216s | 657.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-50.smt2 | 29.588s | 731.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-50.smt2 | 29.604s | 620.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-45.smt2 | 29.803s | 1168.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-47.smt2 | 30.040s | 821.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-49.smt2 | 30.271s | 691.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-48.smt2 | 30.275s | 754.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-42.smt2 | 30.518s | 761.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-46.smt2 | 30.597s | 819.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-47.smt2 | 30.612s | 679.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-42.smt2 | 30.808s | 484.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-43.smt2 | 30.985s | 437.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-906586.smt2 | 30.995s | 1835.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-42.smt2 | 31.007s | 562.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-47.smt2 | 31.070s | 681.0MiB| sat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER10-13-fair.smt2 | 31.196s | 233.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-42.smt2 | 31.298s | 897.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-44.smt2 | 31.436s | 784.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-50.smt2 | 31.489s | 902.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-200.smt2 | 31.489s | 833.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-42.smt2 | 31.492s | 921.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-42.smt2 | 31.534s | 800.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-45.smt2 | 31.626s | 747.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-47.smt2 | 31.666s | 675.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-48.smt2 | 31.703s | 684.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-42.smt2 | 31.996s | 678.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-46.smt2 | 32.157s | 1025.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-44.smt2 | 32.164s | 572.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-46.smt2 | 32.169s | 1157.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-49.smt2 | 32.221s | 881.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-46.smt2 | 32.470s | 832.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1317230.smt2 | 32.550s | 2504.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-43.smt2 | 32.585s | 885.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-50.smt2 | 32.671s | 995.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-43.smt2 | 32.687s | 796.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-17-47.smt2 | 33.156s | 554.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-48.smt2 | 33.253s | 860.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-48.smt2 | 33.286s | 862.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-49.smt2 | 33.298s | 719.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-42.smt2 | 33.413s | 933.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-45.smt2 | 33.462s | 869.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-48.smt2 | 33.471s | 749.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-43.smt2 | 33.744s | 821.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-48.smt2 | 33.767s | 797.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-42.smt2 | 34.259s | 845.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-45.smt2 | 34.260s | 734.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-48.smt2 | 34.572s | 909.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-43.smt2 | 34.674s | 822.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1365816.smt2 | 34.697s | 2591.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-46.smt2 | 34.792s | 860.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-43.smt2 | 35.011s | 842.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-39-50.smt2 | 35.043s | 877.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-50.smt2 | 35.086s | 716.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-43.smt2 | 35.240s | 925.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-49.smt2 | 35.241s | 479.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-44.smt2 | 35.725s | 967.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-43.smt2 | 35.814s | 765.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-50.smt2 | 35.986s | 846.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-63-50.smt2 | 36.049s | 1059.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-44.smt2 | 36.216s | 1093.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-49.smt2 | 36.237s | 973.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-47.smt2 | 36.325s | 821.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-49.smt2 | 36.330s | 731.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-48.smt2 | 36.394s | 868.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-46.smt2 | 36.915s | 1233.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-47.smt2 | 36.916s | 993.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-49.smt2 | 37.061s | 894.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-44.smt2 | 37.123s | 875.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-45.smt2 | 37.128s | 1089.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-42.smt2 | 37.209s | 908.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-48.smt2 | 37.306s | 971.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-45.smt2 | 37.500s | 875.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-50.smt2 | 37.540s | 758.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-50.smt2 | 37.638s | 527.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-48.smt2 | 37.703s | 942.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-46.smt2 | 37.767s | 1337.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-45.smt2 | 38.065s | 557.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-50.smt2 | 38.220s | 750.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-48.smt2 | 38.255s | 415.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-45.smt2 | 38.268s | 708.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-49.smt2 | 38.349s | 1028.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-49.smt2 | 38.356s | 760.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-48.smt2 | 39.030s | 1152.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-45.smt2 | 39.194s | 1017.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-45.smt2 | 39.214s | 803.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-49.smt2 | 39.304s | 758.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-46.smt2 | 39.446s | 974.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-48.smt2 | 39.485s | 996.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-45.smt2 | 39.517s | 1155.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-43.smt2 | 39.542s | 738.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-49.smt2 | 39.632s | 879.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-200.smt2 | 39.667s | 589.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-46.smt2 | 39.741s | 645.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-44.smt2 | 39.820s | 841.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-44.smt2 | 39.949s | 1216.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-48.smt2 | 40.106s | 1060.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-48.smt2 | 40.411s | 730.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-49.smt2 | 40.749s | 895.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-48.smt2 | 40.813s | 1020.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-48.smt2 | 40.949s | 761.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-49.smt2 | 41.306s | 918.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-49.smt2 | 41.374s | 343.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-46.smt2 | 41.728s | 614.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-44.smt2 | 41.802s | 1178.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-44.smt2 | 41.843s | 1109.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-197.smt2 | 41.895s | 595.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-49.smt2 | 41.916s | 920.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-45.smt2 | 41.995s | 1533.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-50.smt2 | 42.270s | 822.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-45.smt2 | 42.681s | 1106.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-44.smt2 | 42.890s | 824.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-49.smt2 | 42.917s | 909.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-50.smt2 | 43.121s | 994.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-198.smt2 | 43.240s | 716.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-50.smt2 | 43.789s | 910.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-48.smt2 | 44.314s | 769.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-48.smt2 | 44.442s | 1252.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-50.smt2 | 44.545s | 995.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-48.smt2 | 44.607s | 611.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-50.smt2 | 45.102s | 911.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-13-50.smt2 | 45.389s | 848.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-48.smt2 | 45.541s | 953.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-47.smt2 | 45.673s | 1037.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-46.smt2 | 45.716s | 643.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-50.smt2 | 45.750s | 831.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-49.smt2 | 46.017s | 914.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-48.smt2 | 46.194s | 1120.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-43.smt2 | 46.484s | 1483.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-50.smt2 | 46.509s | 436.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-45.smt2 | 47.096s | 887.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-46.smt2 | 47.585s | 1052.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-49.smt2 | 47.589s | 1028.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-46.smt2 | 47.622s | 1340.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-44.smt2 | 47.733s | 967.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-48.smt2 | 47.766s | 1177.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-48.smt2 | 47.789s | 1075.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-50.smt2 | 47.978s | 807.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-46.smt2 | 47.989s | 1211.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-48.smt2 | 48.166s | 1029.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-50.smt2 | 48.212s | 802.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-199.smt2 | 48.408s | 861.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-41-50.smt2 | 48.830s | 915.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-46.smt2 | 48.849s | 960.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-46.smt2 | 48.910s | 1214.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-46.smt2 | 48.952s | 797.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-46.smt2 | 49.023s | 1449.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-48.smt2 | 49.035s | 1371.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-47.smt2 | 49.066s | 828.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-48.smt2 | 49.569s | 1213.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-45.smt2 | 49.915s | 573.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-46.smt2 | 50.207s | 1325.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-48.smt2 | 50.210s | 1155.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-48.smt2 | 50.546s | 624.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-48.smt2 | 50.639s | 1037.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-49.smt2 | 50.671s | 1357.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-48.smt2 | 50.984s | 1112.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-47.smt2 | 51.423s | 1208.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-47.smt2 | 51.524s | 1181.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-49.smt2 | 51.603s | 843.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-46.smt2 | 51.727s | 892.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-48.smt2 | 51.874s | 838.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-48.smt2 | 52.458s | 1029.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-49.smt2 | 52.587s | 1480.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-48.smt2 | 52.871s | 1063.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-46.smt2 | 52.961s | 1590.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-49.smt2 | 53.041s | 732.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-44.smt2 | 53.184s | 1301.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-48.smt2 | 53.379s | 1118.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-48.smt2 | 53.499s | 1056.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-50.smt2 | 53.511s | 1316.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-47.smt2 | 53.770s | 1216.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-48.smt2 | 53.787s | 1232.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-46.smt2 | 54.085s | 763.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-49.smt2 | 54.189s | 840.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-47.smt2 | 54.469s | 645.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-47.smt2 | 54.556s | 1387.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-47.smt2 | 54.923s | 1182.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-48.smt2 | 55.616s | 1542.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-48.smt2 | 55.712s | 1321.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-50.smt2 | 55.855s | 894.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-48.smt2 | 56.372s | 1377.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-48.smt2 | 56.426s | 1581.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-269353.smt2 | 56.659s | 545.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-47.smt2 | 58.099s | 1288.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-47.smt2 | 58.343s | 1004.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-46.smt2 | 58.508s | 1168.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-48.smt2 | 58.527s | 1023.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-47.smt2 | 58.542s | 1524.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-50.smt2 | 58.943s | 1220.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-48.smt2 | 58.986s | 1209.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-46.smt2 | 59.014s | 963.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-46.smt2 | 59.464s | 885.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-48.smt2 | 59.651s | 1305.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-47.smt2 | 59.752s | 1170.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-50.smt2 | 59.807s | 500.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-47.smt2 | 60.698s | 1089.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-47.smt2 | 61.459s | 1365.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-48.smt2 | 61.693s | 1202.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-47.smt2 | 61.716s | 1342.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-50.smt2 | 61.774s | 1449.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-49.smt2 | 62.128s | 735.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1268455.smt2 | 62.300s | 2499.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-46.smt2 | 62.344s | 1386.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-50.smt2 | 62.379s | 1240.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-50.smt2 | 62.426s | 1159.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-46.smt2 | 62.531s | 1733.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-49.smt2 | 62.843s | 1240.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-50.smt2 | 62.871s | 916.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-47.smt2 | 63.299s | 1399.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-45.smt2 | 63.351s | 2055.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-49.smt2 | 63.355s | 1388.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-47.smt2 | 63.675s | 1143.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-14-49.smt2 | 63.907s | 774.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-49.smt2 | 64.472s | 1624.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-48.smt2 | 64.521s | 1339.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-46.smt2 | 64.827s | 1040.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-49.smt2 | 65.147s | 923.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-48.smt2 | 65.170s | 1513.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-46.smt2 | 65.377s | 1458.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-46.smt2 | 65.688s | 1264.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-47.smt2 | 65.715s | 1017.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-50.smt2 | 66.124s | 1357.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-50.smt2 | 66.258s | 1241.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-47.smt2 | 66.886s | 1416.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-48.smt2 | 67.777s | 1354.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-50.smt2 | 67.843s | 1150.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1072007.smt2 | 67.954s | 2835.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-48.smt2 | 68.058s | 1375.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-48.smt2 | 68.136s | 924.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-46.smt2 | 68.515s | 1432.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-47.smt2 | 68.635s | 1689.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-50.smt2 | 69.123s | 1569.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-49.smt2 | 69.750s | 1932.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-49.smt2 | 70.126s | 1211.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-49.smt2 | 70.656s | 1343.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-49.smt2 | 70.782s | 1280.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-50.smt2 | 71.147s | 1130.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-50.smt2 | 71.598s | 830.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-48.smt2 | 72.148s | 1264.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-50.smt2 | 72.309s | 1429.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-46.smt2 | 72.337s | 798.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-48.smt2 | 72.633s | 1481.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-47.smt2 | 73.746s | 950.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-49.smt2 | 73.848s | 1354.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-21-40.smt2 | 73.911s | 2145.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-48.smt2 | 74.110s | 1293.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-50.smt2 | 74.120s | 1722.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-49.smt2 | 74.523s | 1898.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-50.smt2 | 74.920s | 1178.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-48.smt2 | 75.241s | 1202.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-46.smt2 | 76.355s | 1945.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-50.smt2 | 77.217s | 928.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-48.smt2 | 77.469s | 1301.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-63-50.smt2 | 78.143s | 1290.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-49.smt2 | 78.652s | 2000.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-49.smt2 | 79.113s | 1793.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-50.smt2 | 79.144s | 1500.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-48.smt2 | 79.214s | 1301.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-46.smt2 | 79.550s | 1161.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-49.smt2 | 80.076s | 1440.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER10-14-fair.smt2 | 80.134s | 255.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-49.smt2 | 80.179s | 1374.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-48.smt2 | 80.187s | 1548.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-46.smt2 | 80.491s | 1880.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-49.smt2 | 81.129s | 1663.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-50.smt2 | 81.174s | 1996.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-47.smt2 | 81.303s | 1584.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-49.smt2 | 81.343s | 1274.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-48.smt2 | 81.457s | 1051.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-47.smt2 | 81.564s | 1358.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-50.smt2 | 81.579s | 1953.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-50.smt2 | 81.736s | 1109.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-50.smt2 | 81.893s | 2176.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-48.smt2 | 82.094s | 1349.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-50.smt2 | 82.171s | 1427.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-47.smt2 | 82.582s | 1276.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-47.smt2 | 84.689s | 1310.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-49.smt2 | 85.281s | 1159.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-50.smt2 | 85.683s | 1409.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-50.smt2 | 87.096s | 2137.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-48.smt2 | 87.250s | 1142.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-50.smt2 | 87.461s | 1998.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-49.smt2 | 87.525s | 2024.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-48.smt2 | 87.935s | 1618.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-46.smt2 | 88.580s | 1034.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-46.smt2 | 88.719s | 1653.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-50.smt2 | 89.069s | 1895.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-48.smt2 | 89.800s | 1732.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-49.smt2 | 90.743s | 1826.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-50.smt2 | 91.525s | 1136.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-48.smt2 | 91.930s | 1970.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1265513.smt2 | 92.906s | 3366.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-48.smt2 | 93.102s | 1954.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-46.smt2 | 94.621s | 1050.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-48.smt2 | 94.666s | 2076.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-50.smt2 | 94.715s | 1281.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-48.smt2 | 95.132s | 1198.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-47.smt2 | 95.284s | 1658.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-50.smt2 | 95.460s | 776.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-50.smt2 | 95.475s | 1077.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-50.smt2 | 95.661s | 1538.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-31-42.smt2 | 96.042s | 760.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-49.smt2 | 96.159s | 1139.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-50.smt2 | 96.538s | 1554.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-49.smt2 | 97.760s | 1727.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-47.smt2 | 100.212s | 1488.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-46.smt2 | 100.834s | 894.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-23-41.smt2 | 102.049s | 755.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-49.smt2 | 102.765s | 1098.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-49.smt2 | 103.273s | 1535.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-50.smt2 | 103.415s | 1414.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-44.smt2 | 103.504s | 1042.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-47.smt2 | 104.268s | 2063.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-50.smt2 | 106.190s | 1935.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-47.smt2 | 107.360s | 1165.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-48.smt2 | 108.326s | 1321.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-50.smt2 | 109.735s | 2072.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-48.smt2 | 110.376s | 898.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-46.smt2 | 112.172s | 935.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-408585.smt2 | 112.178s | 1067.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-49.smt2 | 112.631s | 1181.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-46.smt2 | 112.765s | 1206.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-47.smt2 | 113.103s | 1076.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-47.smt2 | 114.736s | 2042.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-47.smt2 | 115.543s | 1201.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-50.smt2 | 118.470s | 922.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-47.smt2 | 121.205s | 1567.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-46.smt2 | 123.655s | 1746.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-46.smt2 | 125.369s | 1435.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-48.smt2 | 127.483s | 971.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-46.smt2 | 127.537s | 2200.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-26-43.smt2 | 129.803s | 1400.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER11-14-fair.smt2 | 129.943s | 280.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-46.smt2 | 130.666s | 1528.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-47.smt2 | 130.873s | 1344.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-50.smt2 | 131.755s | 1468.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-46.smt2 | 131.887s | 990.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-46.smt2 | 133.844s | 1220.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-46.smt2 | 134.200s | 1400.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-267105.smt2 | 134.763s | 630.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-50.smt2 | 135.246s | 1820.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-50.smt2 | 139.390s | 1220.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-46.smt2 | 139.500s | 1265.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-50.smt2 | 140.533s | 1504.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-48.smt2 | 141.173s | 1122.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-478122.smt2 | 142.327s | 1369.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-48.smt2 | 142.407s | 1201.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-50.smt2 | 144.159s | 2565.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-47.smt2 | 144.502s | 1065.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-48.smt2 | 144.928s | 1655.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-48.smt2 | 146.235s | 1687.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-618384.smt2 | 147.250s | 2006.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-50.smt2 | 148.768s | 1574.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-49.smt2 | 149.746s | 2051.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-46.smt2 | 151.018s | 1119.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-518109.smt2 | 152.119s | 1318.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-47.smt2 | 152.364s | 2101.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-46.smt2 | 153.303s | 929.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-49.smt2 | 154.080s | 1348.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-50.smt2 | 154.222s | 1172.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-48.smt2 | 156.822s | 2607.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-47.smt2 | 156.940s | 2119.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-48.smt2 | 156.994s | 1007.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-47.smt2 | 157.607s | 1443.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-47.smt2 | 158.948s | 2544.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-46.smt2 | 159.754s | 1374.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-46.smt2 | 162.134s | 1575.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-729964.smt2 | 162.552s | 2294.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-48.smt2 | 163.893s | 1573.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-50.smt2 | 164.112s | 942.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-49.smt2 | 164.542s | 1493.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-47.smt2 | 166.629s | 1141.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-47.smt2 | 167.423s | 1317.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-48.smt2 | 168.387s | 2045.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-46.smt2 | 169.505s | 2097.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-46.smt2 | 172.735s | 1160.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-50.smt2 | 173.943s | 1791.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-47.smt2 | 174.784s | 1882.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-49.smt2 | 175.491s | 1275.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-47.smt2 | 175.810s | 1288.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-50.smt2 | 176.066s | 1356.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-48.smt2 | 177.809s | 1210.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-49.smt2 | 181.335s | 1650.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-47.smt2 | 181.959s | 1649.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-762853.smt2 | 183.309s | 2549.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-47.smt2 | 183.742s | 1340.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-48.smt2 | 183.876s | 1294.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-47.smt2 | 184.047s | 2459.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-46.smt2 | 184.254s | 1443.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1262176.smt2 | 184.455s | 4591.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-49.smt2 | 185.002s | 2297.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-49.smt2 | 185.363s | 1691.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-278378.smt2 | 185.823s | 599.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-47.smt2 | 185.925s | 1176.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-46.smt2 | 186.296s | 1957.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-50.smt2 | 187.988s | 1490.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-48.smt2 | 192.276s | 2688.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-47.smt2 | 193.085s | 1279.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-46.smt2 | 193.928s | 1748.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-46.smt2 | 194.447s | 2211.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-46.smt2 | 195.043s | 1150.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-46.smt2 | 197.899s | 1594.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-46.smt2 | 198.490s | 1122.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-46.smt2 | 198.667s | 1411.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-46.smt2 | 199.815s | 1208.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-50.smt2 | 200.012s | 1518.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-46.smt2 | 201.480s | 2287.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-46.smt2 | 202.788s | 2111.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-50.smt2 | 203.481s | 1749.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-49.smt2 | 203.749s | 1378.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-48.smt2 | 205.797s | 1051.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-46.smt2 | 205.895s | 1192.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-50.smt2 | 205.914s | 1801.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-47.smt2 | 206.294s | 2171.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-47.smt2 | 209.323s | 892.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-47.smt2 | 209.764s | 1040.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-49.smt2 | 209.920s | 1282.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-49.smt2 | 209.945s | 1235.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-48.smt2 | 210.348s | 1677.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-49.smt2 | 214.464s | 1677.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-47.smt2 | 216.302s | 1252.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-47.smt2 | 217.391s | 1812.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-50.smt2 | 221.967s | 1186.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-49.smt2 | 224.083s | 1884.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1452366.smt2 | 224.593s | 5089.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-49.smt2 | 225.295s | 2763.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-46.smt2 | 227.310s | 1225.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-46.smt2 | 228.393s | 1322.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-47.smt2 | 228.625s | 2420.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-47.smt2 | 229.054s | 1339.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-47.smt2 | 230.316s | 2295.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-47.smt2 | 230.919s | 2260.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-47.smt2 | 231.757s | 1464.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-47.smt2 | 232.263s | 1131.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-48.smt2 | 233.564s | 1673.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-48.smt2 | 235.594s | 1359.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-46.smt2 | 236.893s | 1162.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-49.smt2 | 237.007s | 1279.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-48.smt2 | 239.262s | 1654.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-50.smt2 | 242.568s | 1165.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-48.smt2 | 244.309s | 1479.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-50.smt2 | 244.465s | 1616.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-46.smt2 | 244.843s | 1620.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-49.smt2 | 245.984s | 1996.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-48.smt2 | 246.323s | 1468.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-50.smt2 | 246.497s | 1214.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-49.smt2 | 252.207s | 1350.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-49.smt2 | 255.585s | 857.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-49.smt2 | 260.475s | 1464.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-47.smt2 | 260.589s | 1091.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER11-15-fair.smt2 | 264.052s | 311.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1472027.smt2 | 264.617s | 6284.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-49.smt2 | 266.456s | 1657.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-49.smt2 | 268.524s | 1668.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-47.smt2 | 270.180s | 1431.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-283008.smt2 | 272.954s | 613.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-49.smt2 | 274.107s | 1637.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-47.smt2 | 275.792s | 1357.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-47.smt2 | 277.726s | 1360.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-47.smt2 | 277.808s | 1380.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1400961.smt2 | 279.729s | 5876.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-49.smt2 | 279.930s | 3614.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-49.smt2 | 280.920s | 1470.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-47.smt2 | 282.064s | 1462.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-48.smt2 | 283.019s | 2708.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-285271.smt2 | 283.213s | 622.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-50.smt2 | 291.037s | 2674.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-46.smt2 | 294.391s | 2160.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-49.smt2 | 296.261s | 2421.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-46.smt2 | 296.528s | 2434.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-48.smt2 | 297.485s | 1869.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-46.smt2 | 297.780s | 1206.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-46.smt2 | 298.515s | 1435.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-47.smt2 | 302.009s | 1636.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-50.smt2 | 311.351s | 1131.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-49.smt2 | 312.090s | 2119.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-47.smt2 | 313.142s | 1339.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-50.smt2 | 319.976s | 2151.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-49.smt2 | 320.658s | 1999.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-49.smt2 | 322.671s | 1699.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-48.smt2 | 327.561s | 1452.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-46.smt2 | 328.099s | 1899.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-47.smt2 | 328.923s | 2039.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-49.smt2 | 332.521s | 2187.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-49.smt2 | 339.977s | 1624.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-49.smt2 | 341.595s | 1905.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-48.smt2 | 344.552s | 1522.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-48.smt2 | 344.930s | 1223.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-49.smt2 | 348.775s | 2201.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-48.smt2 | 349.669s | 2628.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-495717.smt2 | 353.381s | 1435.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-50.smt2 | 359.928s | 2776.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-46.smt2 | 363.267s | 2635.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-50.smt2 | 365.432s | 1983.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-50.smt2 | 365.748s | 1758.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-49.smt2 | 370.977s | 1172.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-50.smt2 | 372.363s | 1066.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-48.smt2 | 373.308s | 1654.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-49.smt2 | 375.776s | 2314.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-49.smt2 | 377.185s | 2743.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-50.smt2 | 381.177s | 2727.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-50.smt2 | 381.699s | 2254.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-49.smt2 | 387.219s | 2678.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-47.smt2 | 388.400s | 1250.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-50.smt2 | 388.899s | 1702.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-47.smt2 | 392.224s | 1156.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-658040.smt2 | 392.832s | 2098.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-928960.smt2 | 400.627s | 3056.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-49.smt2 | 402.459s | 1533.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-49.smt2 | 406.015s | 1898.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-50.smt2 | 406.138s | 1594.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-49.smt2 | 407.401s | 1852.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-49.smt2 | 408.746s | 3759.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-50.smt2 | 415.690s | 2953.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-50.smt2 | 417.044s | 2226.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-50.smt2 | 423.991s | 1876.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-48.smt2 | 432.914s | 1855.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-321761.smt2 | 449.132s | 794.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-48.smt2 | 455.066s | 2211.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-50.smt2 | 458.868s | 1851.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-50.smt2 | 461.107s | 1487.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-47.smt2 | 480.195s | 2385.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-49.smt2 | 482.944s | 1791.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-50.smt2 | 485.967s | 1925.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-49.smt2 | 497.130s | 3554.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-49.smt2 | 499.435s | 3441.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-50.smt2 | 507.710s | 3660.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-50.smt2 | 512.097s | 2341.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-49.smt2 | 512.807s | 1067.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-50.smt2 | 513.518s | 2595.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-50.smt2 | 514.782s | 2742.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-49.smt2 | 519.045s | 1478.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-50.smt2 | 549.948s | 1563.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-50.smt2 | 551.065s | 2124.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-49.smt2 | 552.248s | 2871.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-50.smt2 | 557.853s | 1859.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-368069.smt2 | 558.570s | 1005.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-49.smt2 | 559.874s | 2809.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-49.smt2 | 598.884s | 2180.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-49.smt2 | 605.022s | 1674.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-50.smt2 | 608.113s | 2888.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-50.smt2 | 622.642s | 2967.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-49.smt2 | 631.440s | 4584.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-49.smt2 | 634.924s | 1926.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-50.smt2 | 635.010s | 1421.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-47.smt2 | 643.614s | 3174.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-50.smt2 | 648.890s | 1655.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-50.smt2 | 663.866s | 1645.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-50.smt2 | 709.411s | 3289.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-50.smt2 | 738.843s | 1626.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-50.smt2 | 746.231s | 1724.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-50.smt2 | 774.793s | 2630.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-50.smt2 | 794.712s | 2016.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-48.smt2 | 803.755s | 3588.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-48.smt2 | 812.748s | 2552.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-46.smt2 | 817.383s | 2656.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1138192.smt2 | 819.834s | 5058.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-49.smt2 | 858.690s | 3251.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-49.smt2 | 932.317s | 1655.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-49.smt2 | 1000.174s | 2980.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-47.smt2 | 1009.537s | 2685.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-50.smt2 | 1011.520s | 1667.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-50.smt2 | 1144.778s | 1988.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/RWS/Example_7.txt.smt2 | 1200.063s | 308.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/RWS/Example_15.txt.smt2 | 1200.071s | 368.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-357303.smt2 | 1200.194s | 1010.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-49.smt2 | 1200.291s | 2868.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-50.smt2 | 1200.458s | 3752.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-985518.smt2 | 1200.526s | 4663.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1060546.smt2 | 1200.570s | 4816.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/20231117-c_inference/80_80_71_17_unsat.smt2 | 1200.579s | 2731.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1228327.smt2 | 1200.809s | 6818.0MiB| timeout | 0 | | |