# . * SAT 386 * UNSAT 369 * TIMEOUT 45 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-QF_LIA_hard-timeout10min-no_core_min-bb2
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: f880fdccee614547c38c19beb7af5a027961646b
Z3 branch: core_min
Z3 options: "-T:600 -v:0 smt.threads=8 tactic.default_tactic=smt smt.auto_config=false 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: Merge branch 'master' of github.com:Z3Prover/z3 into core_min
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1550.smt2 | 0.751s | 282.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1567.smt2 | 0.831s | 285.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1575.smt2 | 0.847s | 286.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1607.smt2 | 0.867s | 290.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1533.smt2 | 0.904s | 279.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1565.smt2 | 1.003s | 286.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1591.smt2 | 1.015s | 289.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1617.smt2 | 1.082s | 293.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-14.smt2 | 3.292s | 907.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-526410.smt2 | 3.396s | 745.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-03.smt2 | 3.535s | 1362.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-09.smt2 | 3.595s | 2200.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-10.smt2 | 3.627s | 1819.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-15.smt2 | 3.790s | 2199.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-02.smt2 | 3.866s | 2200.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-01.smt2 | 4.030s | 2206.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-343499.smt2 | 4.111s | 736.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-06.smt2 | 4.229s | 2143.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-14.smt2 | 4.301s | 825.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-14.smt2 | 4.304s | 2131.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-15.smt2 | 4.354s | 2126.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-08.smt2 | 4.378s | 829.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-12.smt2 | 4.434s | 2133.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-05.smt2 | 4.505s | 2170.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-04.smt2 | 4.518s | 2135.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-13.smt2 | 4.559s | 2132.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-04.smt2 | 4.607s | 2134.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-527358.smt2 | 4.616s | 889.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-08.smt2 | 4.648s | 851.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-08.smt2 | 4.707s | 2140.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-15.smt2 | 4.771s | 1389.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-07.smt2 | 4.790s | 2136.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-06.smt2 | 4.814s | 2129.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-11.smt2 | 4.829s | 2133.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-03.smt2 | 4.960s | 4134.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-00.smt2 | 5.064s | 2129.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-11.smt2 | 5.065s | 1441.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-413904.smt2 | 5.118s | 960.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-10.smt2 | 5.557s | 3220.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-12.smt2 | 5.725s | 4409.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-10.smt2 | 5.801s | 4408.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-03.smt2 | 5.986s | 4583.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-00.smt2 | 6.006s | 4584.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-07.smt2 | 6.100s | 4657.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-12.smt2 | 6.141s | 1210.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-14.smt2 | 6.182s | 1213.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-10.smt2 | 6.232s | 1207.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-07.smt2 | 6.245s | 1205.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-00.smt2 | 6.311s | 1206.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-13.smt2 | 6.380s | 4810.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-14.smt2 | 6.400s | 4603.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-09.smt2 | 6.416s | 4470.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-13.smt2 | 6.459s | 4567.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-00.smt2 | 6.475s | 4663.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-05.smt2 | 6.489s | 4702.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-01.smt2 | 6.530s | 1209.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-09.smt2 | 6.533s | 4566.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-08.smt2 | 6.612s | 1208.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-06.smt2 | 6.626s | 1204.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-05.smt2 | 6.645s | 1206.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-11.smt2 | 6.725s | 1206.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-03.smt2 | 6.757s | 2448.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-02.smt2 | 6.790s | 4773.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1270163.smt2 | 6.924s | 1293.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1007795.smt2 | 7.019s | 1341.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-06.smt2 | 7.163s | 4814.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r1000w0010/RC-08.smt2 | 7.397s | 1449.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-916576.smt2 | 7.543s | 1350.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-392137.smt2 | 7.889s | 946.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-04.smt2 | 8.353s | 5584.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-11.smt2 | 8.548s | 6994.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-03.smt2 | 8.647s | 6466.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-02.smt2 | 8.650s | 7151.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-06.smt2 | 8.682s | 6999.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-01.smt2 | 8.755s | 6992.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-14.smt2 | 8.765s | 6993.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-13.smt2 | 8.853s | 6998.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-09.smt2 | 8.872s | 7003.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-00.smt2 | 8.918s | 6999.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-02.smt2 | 9.028s | 6939.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-05.smt2 | 9.049s | 6995.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-10.smt2 | 9.088s | 6993.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-15.smt2 | 9.235s | 6995.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-09.smt2 | 9.405s | 6939.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-38.smt2 | 9.475s | 465.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-01.smt2 | 9.553s | 6860.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-08.smt2 | 9.630s | 6994.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-928134.smt2 | 9.671s | 1620.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-13.smt2 | 9.827s | 6938.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-689472.smt2 | 9.977s | 1576.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-379665.smt2 | 10.171s | 1024.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-415996.smt2 | 10.246s | 1080.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1015084.smt2 | 10.804s | 1577.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-267105.smt2 | 11.097s | 804.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1148089.smt2 | 11.220s | 1697.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-916807.smt2 | 11.355s | 1864.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-37.smt2 | 11.668s | 459.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-705295.smt2 | 11.670s | 1722.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-38.smt2 | 11.702s | 626.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-12.smt2 | 11.757s | 14.073GiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-04.smt2 | 11.773s | 10.937GiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-07.smt2 | 12.096s | 14.846GiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-794687.smt2 | 12.138s | 1773.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-39.smt2 | 12.223s | 552.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1205831.smt2 | 13.222s | 2196.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-38.smt2 | 13.297s | 624.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-38.smt2 | 14.037s | 505.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-758897.smt2 | 14.397s | 1870.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-47.smt2 | 14.477s | 248.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-39.smt2 | 14.625s | 529.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-917322.smt2 | 14.946s | 1991.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-47.smt2 | 15.070s | 248.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-40.smt2 | 15.164s | 635.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-200.smt2 | 15.569s | 1321.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-901628.smt2 | 15.614s | 1912.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-44.smt2 | 15.726s | 629.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-200.smt2 | 16.267s | 1270.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-39.smt2 | 16.364s | 703.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-38.smt2 | 16.503s | 718.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-41.smt2 | 16.530s | 621.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-16-49.smt2 | 17.090s | 761.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-42.smt2 | 17.217s | 565.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-42.smt2 | 17.279s | 588.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-197.smt2 | 17.349s | 974.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-618384.smt2 | 17.653s | 1683.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-39.smt2 | 18.024s | 831.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-39.smt2 | 18.137s | 845.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-864173.smt2 | 18.205s | 2359.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-43.smt2 | 18.283s | 672.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-48.smt2 | 18.288s | 250.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-50.smt2 | 18.671s | 781.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-49.smt2 | 18.839s | 891.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-8-49.smt2 | 18.903s | 889.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-41.smt2 | 19.120s | 658.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-41.smt2 | 19.437s | 567.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-13-50.smt2 | 19.475s | 732.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-24-49.smt2 | 19.475s | 857.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-198.smt2 | 19.653s | 1444.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-40.smt2 | 19.677s | 654.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER10-13-fair.smt2 | 19.782s | 316.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-196.smt2 | 19.963s | 1441.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-41.smt2 | 20.396s | 699.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1185949.smt2 | 20.733s | 2633.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-481231.smt2 | 20.823s | 1500.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-199.smt2 | 21.363s | 1308.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-19-50.smt2 | 21.404s | 840.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-49.smt2 | 21.521s | 855.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-32-50.smt2 | 21.648s | 875.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-199.smt2 | 21.662s | 1154.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-40.smt2 | 21.717s | 727.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-13-50.smt2 | 21.729s | 834.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1192684.smt2 | 21.732s | 2692.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-37-50.smt2 | 22.027s | 917.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-50.smt2 | 22.129s | 953.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-23-50.smt2 | 22.264s | 1032.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-198.smt2 | 22.613s | 901.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-49.smt2 | 22.616s | 885.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-40.smt2 | 22.702s | 889.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-47.smt2 | 22.917s | 738.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-49.smt2 | 23.206s | 798.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-196.smt2 | 23.284s | 1282.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-50.smt2 | 23.285s | 871.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-48.smt2 | 23.321s | 800.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-41.smt2 | 23.407s | 583.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1360077.smt2 | 23.433s | 3131.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1317230.smt2 | 23.622s | 3251.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-49.smt2 | 23.835s | 820.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-50.smt2 | 23.869s | 919.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-57-49.smt2 | 24.004s | 1038.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-48.smt2 | 24.038s | 836.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-59-50.smt2 | 24.165s | 838.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-49.smt2 | 24.308s | 805.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-41.smt2 | 24.319s | 891.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-48.smt2 | 24.529s | 769.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-42-50.smt2 | 24.564s | 929.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-41.smt2 | 24.565s | 937.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-50.smt2 | 24.625s | 1008.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-196.smt2 | 24.660s | 928.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-46.smt2 | 24.766s | 914.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-46.smt2 | 24.881s | 824.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-14-49.smt2 | 24.899s | 812.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-40-50.smt2 | 24.973s | 840.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-48-50.smt2 | 25.288s | 932.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-70-50.smt2 | 25.426s | 838.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-50.smt2 | 25.566s | 703.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-49.smt2 | 25.607s | 712.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-45.smt2 | 25.771s | 791.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-64-50.smt2 | 25.807s | 826.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1275621.smt2 | 25.962s | 3407.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-42.smt2 | 26.013s | 686.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-67-50.smt2 | 26.087s | 851.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-45.smt2 | 26.099s | 966.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-50.smt2 | 26.127s | 781.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-41.smt2 | 26.173s | 1023.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-46.smt2 | 26.191s | 879.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-197.smt2 | 26.194s | 902.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-247831.smt2 | 26.522s | 743.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-49.smt2 | 26.551s | 762.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-45.smt2 | 26.626s | 924.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-50.smt2 | 26.660s | 849.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-37-47.smt2 | 26.720s | 694.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1361831.smt2 | 26.731s | 3283.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-42.smt2 | 26.791s | 972.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-200.smt2 | 27.055s | 906.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-49.smt2 | 27.077s | 855.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-49.smt2 | 27.130s | 890.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-49.smt2 | 27.192s | 833.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-42.smt2 | 27.221s | 618.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-42.smt2 | 27.310s | 934.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-60-50.smt2 | 27.726s | 875.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-198.smt2 | 27.845s | 1432.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-48.smt2 | 27.853s | 533.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-47.smt2 | 28.106s | 882.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-49.smt2 | 28.234s | 935.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-65-50.smt2 | 28.238s | 988.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-50.smt2 | 28.266s | 579.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1317511.smt2 | 28.306s | 3436.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-48.smt2 | 28.456s | 849.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-44.smt2 | 28.501s | 903.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-57-50.smt2 | 28.515s | 849.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-76-50.smt2 | 28.566s | 906.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-50.smt2 | 28.707s | 1066.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-42.smt2 | 28.781s | 1000.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-48.smt2 | 28.792s | 867.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-48.smt2 | 28.809s | 1035.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-45.smt2 | 28.826s | 769.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-42.smt2 | 28.925s | 944.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1121941.smt2 | 28.970s | 3056.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-69-50.smt2 | 29.478s | 833.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-43.smt2 | 29.896s | 886.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-68-50.smt2 | 29.953s | 849.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-42.smt2 | 30.002s | 625.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-43.smt2 | 30.366s | 983.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-77-50.smt2 | 30.456s | 890.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-19-49.smt2 | 30.762s | 959.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-42.smt2 | 30.871s | 600.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-50.smt2 | 31.137s | 814.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-58-50.smt2 | 31.373s | 1024.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-42.smt2 | 31.403s | 1173.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-45.smt2 | 31.419s | 1000.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-46.smt2 | 31.507s | 986.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-50.smt2 | 31.894s | 915.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-42.smt2 | 31.937s | 684.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-42.smt2 | 32.145s | 1345.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-39-50.smt2 | 32.666s | 1102.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-47.smt2 | 32.799s | 838.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-46.smt2 | 32.940s | 1171.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-47.smt2 | 33.090s | 1043.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-46.smt2 | 33.199s | 902.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-48.smt2 | 33.230s | 979.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-45.smt2 | 33.258s | 1223.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-43.smt2 | 33.279s | 980.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-199.smt2 | 33.304s | 889.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-46.smt2 | 33.633s | 936.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-48.smt2 | 33.663s | 846.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-45.smt2 | 33.745s | 1001.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-43.smt2 | 33.878s | 1058.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-47.smt2 | 33.896s | 923.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-43.smt2 | 34.030s | 957.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-49.smt2 | 34.146s | 1314.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-43.smt2 | 34.286s | 1272.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-47.smt2 | 34.484s | 911.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-50.smt2 | 34.557s | 858.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-17-47.smt2 | 34.622s | 781.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-49.smt2 | 34.720s | 830.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-44.smt2 | 34.878s | 1159.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-44.smt2 | 34.924s | 1021.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-329386.smt2 | 34.994s | 1059.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-906586.smt2 | 35.033s | 3181.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-46.smt2 | 35.063s | 813.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-44.smt2 | 35.090s | 942.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-63-50.smt2 | 35.210s | 922.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-49.smt2 | 35.270s | 954.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-46.smt2 | 35.398s | 1331.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-44.smt2 | 35.498s | 1128.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-43.smt2 | 35.519s | 1036.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-50.smt2 | 35.544s | 889.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-43.smt2 | 35.622s | 821.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-47.smt2 | 35.653s | 970.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-47.smt2 | 35.762s | 1005.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-48.smt2 | 35.883s | 927.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-47.smt2 | 36.031s | 936.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-49.smt2 | 36.129s | 983.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-48.smt2 | 36.294s | 1217.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-47.smt2 | 36.301s | 911.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-45.smt2 | 36.466s | 973.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-44.smt2 | 36.671s | 1014.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-48.smt2 | 36.689s | 915.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-46.smt2 | 36.888s | 946.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-50.smt2 | 37.181s | 971.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-43.smt2 | 37.251s | 1045.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-48.smt2 | 37.378s | 626.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-47.smt2 | 37.428s | 1066.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-47.smt2 | 37.444s | 816.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1365816.smt2 | 37.494s | 4022.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-44.smt2 | 37.514s | 1224.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-17-47.smt2 | 38.007s | 914.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-50.smt2 | 38.117s | 894.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-50.smt2 | 38.310s | 1085.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-45.smt2 | 38.401s | 850.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-43.smt2 | 38.413s | 974.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-45.smt2 | 38.466s | 1280.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-49.smt2 | 38.684s | 916.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-43.smt2 | 38.766s | 1358.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-48.smt2 | 38.814s | 971.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-46.smt2 | 38.864s | 1187.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-46.smt2 | 39.003s | 1199.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-45.smt2 | 39.230s | 1005.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-45.smt2 | 39.357s | 1551.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-46.smt2 | 39.391s | 1243.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-48.smt2 | 39.484s | 1132.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-47.smt2 | 39.512s | 994.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-48.smt2 | 39.514s | 1073.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-48.smt2 | 39.640s | 1018.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-44.smt2 | 39.733s | 1089.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-46.smt2 | 39.952s | 1010.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-46.smt2 | 40.089s | 1286.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-47.smt2 | 40.280s | 1062.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-47.smt2 | 40.407s | 1359.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-46.smt2 | 40.539s | 1479.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-48.smt2 | 40.879s | 1114.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-48.smt2 | 41.039s | 1140.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-50.smt2 | 41.181s | 958.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-44.smt2 | 41.235s | 1476.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-45.smt2 | 41.844s | 999.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-50.smt2 | 41.869s | 1083.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-49.smt2 | 42.513s | 562.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-48.smt2 | 42.652s | 990.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-48.smt2 | 43.361s | 1162.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-49.smt2 | 43.578s | 1267.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-48.smt2 | 43.753s | 1093.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-44.smt2 | 43.762s | 1247.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-46.smt2 | 43.964s | 1280.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-48.smt2 | 44.459s | 1142.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-46.smt2 | 44.479s | 1270.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-46.smt2 | 44.536s | 1382.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-46.smt2 | 44.543s | 1593.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-46.smt2 | 44.617s | 1147.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-49.smt2 | 44.856s | 1048.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-49.smt2 | 44.914s | 746.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-49.smt2 | 44.964s | 1030.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-44.smt2 | 45.182s | 1291.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-48.smt2 | 45.648s | 1384.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-45.smt2 | 45.650s | 1022.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-47.smt2 | 45.781s | 892.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-48.smt2 | 46.285s | 1404.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-48.smt2 | 46.331s | 1481.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-47.smt2 | 46.422s | 1317.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-48.smt2 | 46.505s | 1061.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-46.smt2 | 46.643s | 1498.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-49.smt2 | 46.751s | 1238.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-44.smt2 | 46.828s | 1065.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-45.smt2 | 47.048s | 1022.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-49.smt2 | 47.450s | 1506.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-49.smt2 | 47.829s | 1348.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-48.smt2 | 47.847s | 823.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-46.smt2 | 47.858s | 1217.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-45.smt2 | 47.950s | 1229.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-44.smt2 | 48.039s | 1368.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-49.smt2 | 48.072s | 1190.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-49.smt2 | 48.307s | 1153.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-50.smt2 | 48.345s | 1115.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-50.smt2 | 48.394s | 1134.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-48.smt2 | 48.922s | 1092.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-48.smt2 | 48.958s | 1417.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-50.smt2 | 49.066s | 1102.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-50.smt2 | 49.390s | 1049.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-21-40.smt2 | 49.491s | 1049.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-50.smt2 | 49.776s | 1109.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-50.smt2 | 50.607s | 1056.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-46.smt2 | 50.681s | 862.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-47.smt2 | 50.881s | 1495.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-49.smt2 | 51.080s | 1179.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-50.smt2 | 51.185s | 1202.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-48.smt2 | 51.633s | 1087.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-50.smt2 | 51.787s | 1090.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-50.smt2 | 52.419s | 1125.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-47.smt2 | 52.447s | 1001.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-48.smt2 | 53.004s | 1798.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-49.smt2 | 53.064s | 1296.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-49.smt2 | 53.177s | 1142.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-48.smt2 | 53.221s | 1166.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-50.smt2 | 53.274s | 1136.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-49.smt2 | 53.475s | 1354.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-48.smt2 | 53.713s | 1464.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-50.smt2 | 53.742s | 1140.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-46.smt2 | 53.913s | 1007.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-48.smt2 | 53.987s | 1441.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-46.smt2 | 54.073s | 1456.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-47.smt2 | 54.098s | 1456.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-46.smt2 | 54.363s | 799.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-48.smt2 | 54.410s | 1034.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-48.smt2 | 54.454s | 1419.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-49.smt2 | 54.948s | 1117.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-47.smt2 | 54.990s | 1440.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-48.smt2 | 55.066s | 1563.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-48.smt2 | 55.222s | 1269.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-48.smt2 | 55.426s | 1484.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-48.smt2 | 55.806s | 1123.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-50.smt2 | 55.854s | 1512.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-47.smt2 | 56.309s | 1407.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-50.smt2 | 56.805s | 1147.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-50.smt2 | 56.960s | 1171.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-46.smt2 | 57.359s | 1409.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-48.smt2 | 57.850s | 1352.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-47.smt2 | 58.071s | 1177.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-49.smt2 | 58.083s | 1109.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-50.smt2 | 58.186s | 806.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-46.smt2 | 58.466s | 1462.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-48.smt2 | 58.557s | 1599.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-47.smt2 | 58.558s | 1382.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-47.smt2 | 58.614s | 1105.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-50.smt2 | 58.710s | 1601.0MiB| sat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER11-14-fair.smt2 | 59.057s | 369.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-50.smt2 | 59.182s | 1440.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-47.smt2 | 59.253s | 1397.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-47.smt2 | 59.359s | 1828.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-45.smt2 | 59.512s | 1397.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-47.smt2 | 59.738s | 1339.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-49.smt2 | 60.030s | 1463.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-46.smt2 | 60.109s | 1483.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-49.smt2 | 60.507s | 1243.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-47.smt2 | 60.635s | 1176.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-46.smt2 | 60.703s | 1343.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-48.smt2 | 60.739s | 1365.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-47.smt2 | 60.922s | 1544.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-48.smt2 | 61.030s | 1454.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-48.smt2 | 61.247s | 1756.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-49.smt2 | 61.571s | 1735.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-48.smt2 | 62.216s | 1934.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-48.smt2 | 62.224s | 1569.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-49.smt2 | 62.546s | 1416.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-41-50.smt2 | 62.613s | 1100.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-49.smt2 | 62.713s | 1251.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-48.smt2 | 62.857s | 1551.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-46.smt2 | 62.988s | 1794.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-50.smt2 | 63.009s | 1246.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-47.smt2 | 63.186s | 1819.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-49.smt2 | 63.375s | 1290.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-48.smt2 | 63.524s | 1437.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-408585.smt2 | 63.581s | 1604.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-49.smt2 | 63.826s | 920.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-48.smt2 | 63.992s | 1140.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-48.smt2 | 64.325s | 1820.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1268455.smt2 | 64.866s | 4064.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-48.smt2 | 64.866s | 1562.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER10-14-fair.smt2 | 64.920s | 359.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-49.smt2 | 65.269s | 978.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-48.smt2 | 65.551s | 1457.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-48.smt2 | 65.733s | 1785.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-47.smt2 | 65.908s | 1150.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-48.smt2 | 66.587s | 1738.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-49.smt2 | 66.593s | 1808.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-48.smt2 | 66.705s | 1703.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-47.smt2 | 67.117s | 1774.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-48.smt2 | 67.148s | 1321.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-50.smt2 | 67.366s | 1553.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-46.smt2 | 68.041s | 2174.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-47.smt2 | 68.264s | 1541.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-48.smt2 | 68.287s | 1588.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-49.smt2 | 68.436s | 1459.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-49.smt2 | 68.643s | 1745.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-48.smt2 | 69.374s | 1593.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-49.smt2 | 69.532s | 1887.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-46.smt2 | 69.862s | 1651.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-49.smt2 | 69.892s | 1633.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-49.smt2 | 71.886s | 1576.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1452366.smt2 | 71.978s | 5411.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-49.smt2 | 72.404s | 1141.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-48.smt2 | 72.429s | 1460.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-49.smt2 | 72.749s | 1655.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-50.smt2 | 74.003s | 1883.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-50.smt2 | 74.084s | 1177.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-50.smt2 | 75.013s | 1264.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-46.smt2 | 75.028s | 1517.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-50.smt2 | 75.214s | 2064.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-50.smt2 | 75.446s | 2046.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-50.smt2 | 75.524s | 1659.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-46.smt2 | 75.763s | 1478.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-48.smt2 | 76.316s | 1713.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-50.smt2 | 76.383s | 1589.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-49.smt2 | 77.036s | 1793.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-50.smt2 | 77.087s | 1612.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-518109.smt2 | 77.291s | 1793.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-49.smt2 | 77.669s | 1709.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-50.smt2 | 77.708s | 1713.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-48.smt2 | 79.137s | 1699.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-50.smt2 | 79.256s | 1520.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-48.smt2 | 79.339s | 2008.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-48.smt2 | 79.453s | 1765.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-46.smt2 | 79.957s | 1290.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-50.smt2 | 80.197s | 1631.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-49.smt2 | 80.209s | 2002.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-49.smt2 | 80.632s | 1495.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-46.smt2 | 80.639s | 1541.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-50.smt2 | 80.924s | 1380.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-49.smt2 | 81.141s | 1679.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-47.smt2 | 81.486s | 1634.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-50.smt2 | 81.597s | 1534.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-47.smt2 | 82.138s | 1605.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-47.smt2 | 82.801s | 2191.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-48.smt2 | 82.875s | 1617.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-50.smt2 | 82.961s | 1610.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-46.smt2 | 83.468s | 1703.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-48.smt2 | 83.644s | 1436.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-50.smt2 | 86.162s | 1445.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-47.smt2 | 86.195s | 1450.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-48.smt2 | 86.442s | 1960.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-48.smt2 | 87.092s | 2104.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-49.smt2 | 88.733s | 2360.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-50.smt2 | 88.738s | 1564.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-47.smt2 | 89.034s | 1595.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-48.smt2 | 89.362s | 1245.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-49.smt2 | 89.475s | 2372.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-50.smt2 | 90.788s | 1865.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-50.smt2 | 90.937s | 1251.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-49.smt2 | 91.159s | 2067.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-49.smt2 | 92.094s | 1308.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-50.smt2 | 92.233s | 2447.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-50.smt2 | 92.895s | 1572.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1262176.smt2 | 92.971s | 5567.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-48.smt2 | 93.073s | 1795.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-50.smt2 | 93.236s | 2251.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-50.smt2 | 94.374s | 1349.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-48.smt2 | 94.545s | 1645.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-48.smt2 | 94.749s | 1718.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-63-50.smt2 | 95.911s | 1646.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-50.smt2 | 96.938s | 1163.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-47.smt2 | 97.305s | 1486.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-47.smt2 | 98.562s | 1553.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-23-41.smt2 | 99.097s | 1824.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-46.smt2 | 99.112s | 1431.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-50.smt2 | 99.476s | 2625.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-50.smt2 | 100.210s | 2369.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-49.smt2 | 100.405s | 1366.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-31-42.smt2 | 101.061s | 2392.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1265513.smt2 | 101.261s | 5472.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-46.smt2 | 101.828s | 1457.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-50.smt2 | 106.326s | 1586.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-47.smt2 | 106.669s | 2051.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-278378.smt2 | 107.167s | 929.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-46.smt2 | 107.569s | 1157.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-48.smt2 | 108.918s | 1619.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-50.smt2 | 109.493s | 1436.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-49.smt2 | 110.124s | 1184.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1072007.smt2 | 110.320s | 5119.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-46.smt2 | 111.106s | 1390.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-49.smt2 | 111.550s | 2132.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-50.smt2 | 111.686s | 2487.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-50.smt2 | 111.771s | 2101.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-46.smt2 | 118.150s | 1597.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-44.smt2 | 118.187s | 2292.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-48.smt2 | 120.253s | 1237.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-46.smt2 | 121.908s | 2335.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-47.smt2 | 122.746s | 1316.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-48.smt2 | 123.654s | 1811.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-49.smt2 | 123.881s | 2480.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-48.smt2 | 124.100s | 2968.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-47.smt2 | 125.829s | 2001.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-49.smt2 | 125.976s | 1595.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-46.smt2 | 128.184s | 1667.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-46.smt2 | 130.718s | 2713.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-47.smt2 | 131.193s | 2038.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-50.smt2 | 132.345s | 2119.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-46.smt2 | 133.580s | 1256.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-47.smt2 | 133.690s | 2788.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-49.smt2 | 134.898s | 2041.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-49.smt2 | 135.830s | 1646.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-26-43.smt2 | 138.164s | 2321.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-46.smt2 | 139.681s | 1330.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-47.smt2 | 139.883s | 1704.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-48.smt2 | 140.382s | 1490.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-50.smt2 | 141.389s | 2130.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-47.smt2 | 143.004s | 2133.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-46.smt2 | 145.197s | 1494.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-46.smt2 | 145.712s | 2086.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-47.smt2 | 145.729s | 2134.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-47.smt2 | 147.873s | 2108.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-47.smt2 | 148.799s | 1348.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-46.smt2 | 149.140s | 2970.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-357303.smt2 | 153.227s | 1535.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-47.smt2 | 154.517s | 2896.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-45.smt2 | 155.652s | 2604.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-50.smt2 | 156.707s | 1519.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-46.smt2 | 157.310s | 1255.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-47.smt2 | 158.054s | 1579.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-48.smt2 | 158.768s | 1334.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-48.smt2 | 159.759s | 3044.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-50.smt2 | 159.839s | 1539.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-46.smt2 | 161.517s | 2614.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-49.smt2 | 162.899s | 1814.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-47.smt2 | 163.601s | 2872.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-46.smt2 | 165.733s | 2444.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-46.smt2 | 168.603s | 1741.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-50.smt2 | 168.608s | 1226.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-47.smt2 | 168.913s | 2285.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-495717.smt2 | 169.268s | 2218.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-46.smt2 | 169.294s | 1716.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-48.smt2 | 169.827s | 1438.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-46.smt2 | 171.184s | 1523.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-50.smt2 | 173.645s | 2575.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-47.smt2 | 175.348s | 1843.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-46.smt2 | 175.717s | 1644.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-46.smt2 | 176.454s | 2455.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-46.smt2 | 176.959s | 2665.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-46.smt2 | 179.104s | 2566.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-50.smt2 | 179.168s | 2093.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-46.smt2 | 181.302s | 3176.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-46.smt2 | 181.375s | 2057.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-46.smt2 | 182.264s | 1357.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-48.smt2 | 184.880s | 1851.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-47.smt2 | 184.894s | 1665.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-47.smt2 | 185.107s | 2328.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-47.smt2 | 185.575s | 2059.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-47.smt2 | 186.280s | 1691.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-49.smt2 | 188.197s | 1820.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-46.smt2 | 188.300s | 2571.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-46.smt2 | 188.798s | 2361.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-48.smt2 | 190.485s | 1445.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-47.smt2 | 191.346s | 1709.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-49.smt2 | 193.991s | 2110.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-48.smt2 | 195.527s | 3368.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-46.smt2 | 199.278s | 2839.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-49.smt2 | 200.574s | 2373.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-49.smt2 | 201.010s | 1739.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-48.smt2 | 204.312s | 1496.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-49.smt2 | 204.656s | 1807.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-47.smt2 | 205.129s | 1511.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-46.smt2 | 205.536s | 1407.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-47.smt2 | 208.332s | 1784.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-50.smt2 | 208.944s | 2501.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-48.smt2 | 208.962s | 1841.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-46.smt2 | 209.329s | 1718.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1138192.smt2 | 209.772s | 6044.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-49.smt2 | 210.764s | 2530.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-49.smt2 | 211.526s | 2633.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-46.smt2 | 212.780s | 1364.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-48.smt2 | 213.815s | 1623.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-47.smt2 | 214.655s | 2240.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-48.smt2 | 216.901s | 1464.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-48.smt2 | 218.870s | 1874.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-269353.smt2 | 220.652s | 910.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-48.smt2 | 220.769s | 1441.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-47.smt2 | 222.315s | 1511.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-46.smt2 | 222.538s | 1781.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-46.smt2 | 225.256s | 2104.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-49.smt2 | 229.793s | 1674.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-50.smt2 | 237.538s | 2025.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-47.smt2 | 239.803s | 3233.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-46.smt2 | 240.412s | 2717.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-50.smt2 | 240.518s | 3035.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-46.smt2 | 242.860s | 1859.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-47.smt2 | 245.932s | 1788.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-49.smt2 | 246.402s | 1521.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-47.smt2 | 248.710s | 2322.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-46.smt2 | 248.803s | 1639.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-46.smt2 | 253.969s | 1668.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-47.smt2 | 256.996s | 2052.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-47.smt2 | 257.147s | 1466.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-49.smt2 | 258.577s | 2313.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-48.smt2 | 259.118s | 2890.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-47.smt2 | 260.231s | 2366.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-47.smt2 | 269.680s | 2133.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-46.smt2 | 271.342s | 2320.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-50.smt2 | 272.948s | 3907.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-47.smt2 | 278.434s | 2694.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-283008.smt2 | 278.816s | 963.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-49.smt2 | 279.155s | 2910.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-48.smt2 | 279.472s | 2017.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-48.smt2 | 280.467s | 3006.0MiB| sat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER11-15-fair.smt2 | 289.390s | 465.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-50.smt2 | 289.848s | 2108.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-50.smt2 | 293.923s | 3308.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-46.smt2 | 297.370s | 2177.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-49.smt2 | 297.682s | 2723.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-50.smt2 | 297.943s | 2298.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-658040.smt2 | 299.586s | 3386.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-47.smt2 | 307.733s | 2268.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-49.smt2 | 308.427s | 1997.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-368069.smt2 | 308.932s | 1592.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-49.smt2 | 310.555s | 2748.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-50.smt2 | 310.780s | 2282.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-478122.smt2 | 312.939s | 2331.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-50.smt2 | 314.832s | 2527.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-762853.smt2 | 315.869s | 4442.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-50.smt2 | 318.227s | 2640.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-48.smt2 | 327.143s | 2211.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-47.smt2 | 328.437s | 3378.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-49.smt2 | 330.056s | 3278.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-48.smt2 | 330.570s | 2342.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-49.smt2 | 331.424s | 2554.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-46.smt2 | 335.909s | 1562.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-49.smt2 | 336.000s | 2198.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-47.smt2 | 338.643s | 2121.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-49.smt2 | 341.394s | 3750.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-49.smt2 | 343.634s | 2545.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-50.smt2 | 348.135s | 2329.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-49.smt2 | 348.382s | 1804.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-47.smt2 | 350.496s | 3376.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-50.smt2 | 352.767s | 2682.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-48.smt2 | 353.906s | 1824.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-49.smt2 | 355.618s | 3168.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-49.smt2 | 355.940s | 2519.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-49.smt2 | 357.847s | 2247.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-47.smt2 | 359.919s | 1624.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-48.smt2 | 362.996s | 1962.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-47.smt2 | 365.159s | 1872.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-48.smt2 | 368.392s | 4438.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-47.smt2 | 368.513s | 3104.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-49.smt2 | 374.362s | 2578.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-48.smt2 | 375.669s | 2003.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-50.smt2 | 378.420s | 1808.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-48.smt2 | 382.143s | 2976.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-50.smt2 | 384.564s | 2590.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-46.smt2 | 395.636s | 3177.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-50.smt2 | 402.293s | 2864.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-47.smt2 | 404.923s | 1644.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-50.smt2 | 408.362s | 2734.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-49.smt2 | 409.593s | 3413.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-47.smt2 | 410.380s | 1911.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-46.smt2 | 412.242s | 2364.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-48.smt2 | 416.217s | 1364.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-49.smt2 | 417.952s | 3745.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-47.smt2 | 418.156s | 1319.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-48.smt2 | 421.227s | 3408.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-50.smt2 | 424.126s | 2071.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-46.smt2 | 425.730s | 3387.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-48.smt2 | 430.748s | 4726.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-50.smt2 | 433.290s | 3372.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-50.smt2 | 433.668s | 3631.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-48.smt2 | 434.715s | 3271.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-50.smt2 | 436.598s | 2387.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-47.smt2 | 455.951s | 4824.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-47.smt2 | 457.124s | 1836.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-49.smt2 | 459.196s | 1634.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-50.smt2 | 467.753s | 2693.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-49.smt2 | 468.904s | 2994.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-48.smt2 | 479.620s | 3786.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-49.smt2 | 481.889s | 3086.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-49.smt2 | 486.929s | 3735.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-49.smt2 | 501.676s | 3656.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-49.smt2 | 501.730s | 2382.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-46.smt2 | 509.151s | 3163.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-49.smt2 | 523.161s | 2396.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-50.smt2 | 535.424s | 3545.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-50.smt2 | 536.653s | 1774.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-50.smt2 | 540.315s | 4140.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-47.smt2 | 544.976s | 1800.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-49.smt2 | 549.045s | 2211.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-50.smt2 | 553.091s | 3520.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-50.smt2 | 558.464s | 2516.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-49.smt2 | 558.799s | 1403.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-49.smt2 | 569.672s | 3308.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-49.smt2 | 586.932s | 1794.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-49.smt2 | 593.875s | 2199.0MiB| sat | 0 | | | |non-incremental/QF_LIA/RWS/Example_7.txt.smt2 | 600.076s | 513.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/RWS/Example_15.txt.smt2 | 600.112s | 528.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-285271.smt2 | 600.151s | 964.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-50.smt2 | 600.204s | 1625.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-49.smt2 | 600.209s | 1583.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-49.smt2 | 600.228s | 1886.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-50.smt2 | 600.249s | 1974.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-50.smt2 | 600.250s | 2145.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-50.smt2 | 600.261s | 2104.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-321761.smt2 | 600.264s | 1290.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-48.smt2 | 600.270s | 2091.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-49.smt2 | 600.297s | 2513.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-50.smt2 | 600.314s | 2748.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-50.smt2 | 600.334s | 2841.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-50.smt2 | 600.353s | 3339.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-48.smt2 | 600.355s | 3274.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-50.smt2 | 600.359s | 3124.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-50.smt2 | 600.363s | 2960.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-47.smt2 | 600.364s | 3031.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-49.smt2 | 600.366s | 2764.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-50.smt2 | 600.379s | 3258.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-50.smt2 | 600.381s | 2980.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-50.smt2 | 600.387s | 3517.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/20231117-c_inference/80_80_71_17_unsat.smt2 | 600.404s | 3499.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-50.smt2 | 600.409s | 3262.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-50.smt2 | 600.410s | 3354.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-50.smt2 | 600.412s | 2389.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-50.smt2 | 600.414s | 3645.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-49.smt2 | 600.447s | 3165.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-50.smt2 | 600.447s | 3922.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-49.smt2 | 600.465s | 3852.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-49.smt2 | 600.489s | 4737.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-729964.smt2 | 600.526s | 4295.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-49.smt2 | 600.530s | 4862.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-50.smt2 | 600.532s | 4369.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-49.smt2 | 600.575s | 3589.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-49.smt2 | 600.586s | 4866.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-50.smt2 | 600.589s | 4966.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-928960.smt2 | 600.669s | 5221.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1060546.smt2 | 600.893s | 7604.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-985518.smt2 | 600.935s | 7049.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-50.smt2 | 600.958s | 4767.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1228327.smt2 | 601.080s | 9944.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1400961.smt2 | 601.185s | 11.585GiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1472027.smt2 | 601.355s | 12.461GiB| timeout | 0 | | |