# . * SAT 390 * UNSAT 377 * TIMEOUT 33 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-QF_LIA_hard-timeout10min-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.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.884s | 305.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1567.smt2 | 0.917s | 309.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1533.smt2 | 0.926s | 304.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1607.smt2 | 0.934s | 314.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1575.smt2 | 0.938s | 309.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1565.smt2 | 1.062s | 308.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1591.smt2 | 1.093s | 313.0MiB| sat | 0 | | | |non-incremental/QF_LIA/convert/convert-jpg2gif-query-1617.smt2 | 1.104s | 316.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-14.smt2 | 3.191s | 957.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-526410.smt2 | 3.357s | 784.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-03.smt2 | 3.474s | 1442.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-10.smt2 | 3.768s | 1896.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-09.smt2 | 3.907s | 2259.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-01.smt2 | 3.938s | 2284.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-15.smt2 | 4.043s | 2258.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-343499.smt2 | 4.218s | 779.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-02.smt2 | 4.291s | 2262.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-04.smt2 | 4.377s | 2197.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-15.smt2 | 4.382s | 2193.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-14.smt2 | 4.383s | 2205.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-05.smt2 | 4.406s | 2223.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-13.smt2 | 4.432s | 2198.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-04.smt2 | 4.435s | 2209.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-06.smt2 | 4.502s | 2187.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-12.smt2 | 4.655s | 2200.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-08.smt2 | 4.687s | 2202.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-14.smt2 | 4.713s | 913.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-08.smt2 | 4.840s | 910.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-527358.smt2 | 4.863s | 926.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-06.smt2 | 4.987s | 2187.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-00.smt2 | 5.018s | 2212.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-11.smt2 | 5.032s | 2263.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-08.smt2 | 5.066s | 900.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-07.smt2 | 5.272s | 2196.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-413904.smt2 | 5.273s | 973.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-11.smt2 | 5.316s | 1321.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-15.smt2 | 5.594s | 1215.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-10.smt2 | 5.715s | 3291.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-03.smt2 | 5.807s | 4262.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-10.smt2 | 5.970s | 4481.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-12.smt2 | 6.193s | 4482.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-03.smt2 | 6.216s | 4656.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-07.smt2 | 6.252s | 4729.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-09.smt2 | 6.387s | 4707.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-06.smt2 | 6.551s | 1316.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-00.smt2 | 6.605s | 4863.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-00.smt2 | 6.612s | 4655.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-12.smt2 | 6.631s | 1320.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-05.smt2 | 6.649s | 1316.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-13.smt2 | 6.702s | 4965.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-06.smt2 | 6.715s | 4787.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-13.smt2 | 6.742s | 4639.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-09.smt2 | 6.745s | 4636.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-00.smt2 | 6.745s | 1314.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-01.smt2 | 6.796s | 1320.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-11.smt2 | 6.801s | 1314.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1007795.smt2 | 6.830s | 1407.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-10.smt2 | 6.846s | 1314.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-14.smt2 | 6.867s | 1317.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-05.smt2 | 6.944s | 4724.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-08.smt2 | 6.973s | 1322.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-07.smt2 | 7.106s | 1311.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-02.smt2 | 7.236s | 4697.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-14.smt2 | 7.284s | 4904.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r1000w0010/RC-08.smt2 | 7.756s | 1601.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-03.smt2 | 7.882s | 2560.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-916576.smt2 | 7.966s | 1395.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-392137.smt2 | 8.142s | 986.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1270163.smt2 | 8.314s | 1546.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-04.smt2 | 8.399s | 5695.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-03.smt2 | 8.733s | 6575.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-13.smt2 | 8.743s | 7105.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-01.smt2 | 8.770s | 7102.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-15.smt2 | 8.881s | 7104.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-11.smt2 | 9.000s | 7104.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-06.smt2 | 9.065s | 7106.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-05.smt2 | 9.127s | 7106.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-09.smt2 | 9.127s | 7113.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-00.smt2 | 9.151s | 7108.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-928134.smt2 | 9.275s | 1685.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-42.smt2 | 9.462s | 496.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-02.smt2 | 9.464s | 7213.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-08.smt2 | 9.518s | 7101.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-379665.smt2 | 9.577s | 1047.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-10.smt2 | 9.718s | 7101.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-02.smt2 | 9.741s | 7048.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-14.smt2 | 9.764s | 7105.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-415996.smt2 | 9.773s | 1106.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-09.smt2 | 9.836s | 7048.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-13.smt2 | 9.869s | 7047.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-01.smt2 | 10.266s | 6946.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-267105.smt2 | 10.307s | 831.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-38.smt2 | 10.527s | 575.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-38.smt2 | 10.646s | 596.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1148089.smt2 | 10.862s | 1811.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1015084.smt2 | 10.943s | 1674.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-916807.smt2 | 11.194s | 1929.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-689472.smt2 | 11.234s | 1655.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-12.smt2 | 11.461s | 14.182GiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-794687.smt2 | 11.834s | 1802.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-37.smt2 | 11.957s | 494.0MiB| sat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-04.smt2 | 11.964s | 11.219GiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-705295.smt2 | 12.075s | 1785.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-38.smt2 | 12.247s | 620.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-07.smt2 | 12.522s | 14.961GiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1205831.smt2 | 12.702s | 2244.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-39.smt2 | 13.500s | 624.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-47.smt2 | 13.899s | 265.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-38.smt2 | 14.138s | 540.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-758897.smt2 | 14.550s | 1948.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-48.smt2 | 14.689s | 674.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-47.smt2 | 14.739s | 265.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-38.smt2 | 14.813s | 724.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-901628.smt2 | 15.244s | 1954.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-196.smt2 | 15.372s | 1346.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-917322.smt2 | 15.562s | 2039.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-40.smt2 | 15.677s | 714.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-39.smt2 | 16.230s | 834.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-39.smt2 | 16.234s | 678.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-39.smt2 | 16.654s | 733.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-864173.smt2 | 16.702s | 2384.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-199.smt2 | 16.716s | 1468.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-41.smt2 | 16.970s | 690.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-197.smt2 | 17.251s | 1256.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-200.smt2 | 17.297s | 1263.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-198.smt2 | 17.466s | 1246.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-48.smt2 | 17.707s | 266.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-39.smt2 | 17.843s | 566.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-8-49.smt2 | 17.870s | 818.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-50.smt2 | 18.109s | 827.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-618384.smt2 | 18.346s | 1789.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-24-49.smt2 | 18.655s | 898.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-42.smt2 | 19.349s | 680.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-50.smt2 | 19.642s | 733.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-40.smt2 | 19.861s | 584.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-481231.smt2 | 19.974s | 1543.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-41.smt2 | 20.062s | 838.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-16-49.smt2 | 20.153s | 998.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-48.smt2 | 20.318s | 839.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-196.smt2 | 20.652s | 1305.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-40.smt2 | 20.659s | 841.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-43.smt2 | 20.665s | 844.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-199.smt2 | 20.874s | 1395.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-47.smt2 | 21.068s | 693.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-50.smt2 | 21.114s | 1017.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-49.smt2 | 21.258s | 928.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1185949.smt2 | 21.388s | 2700.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1360077.smt2 | 21.939s | 3200.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-48.smt2 | 22.020s | 787.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-23-50.smt2 | 22.030s | 971.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-37-50.smt2 | 22.232s | 962.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-41.smt2 | 22.319s | 725.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-46.smt2 | 22.421s | 956.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-41.smt2 | 22.661s | 997.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1192684.smt2 | 22.848s | 2781.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-49.smt2 | 22.907s | 883.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-44.smt2 | 22.916s | 800.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-13-50.smt2 | 22.950s | 952.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-50.smt2 | 23.027s | 889.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-32-50.smt2 | 23.063s | 862.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-40.smt2 | 23.252s | 880.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-200.smt2 | 23.303s | 1289.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-198.smt2 | 23.396s | 1283.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1317230.smt2 | 23.904s | 3351.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-50.smt2 | 24.188s | 968.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-49.smt2 | 24.377s | 942.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-50.smt2 | 24.467s | 998.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-196.smt2 | 24.484s | 893.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-43.smt2 | 24.579s | 566.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-49.smt2 | 24.583s | 856.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER10-13-fair.smt2 | 24.750s | 347.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-48-50.smt2 | 24.875s | 965.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-42.smt2 | 24.940s | 905.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-41.smt2 | 24.950s | 739.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-50.smt2 | 24.997s | 1038.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-19-50.smt2 | 25.034s | 1001.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-41.smt2 | 25.107s | 901.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-41.smt2 | 25.179s | 969.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-49.smt2 | 25.323s | 872.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-47.smt2 | 25.362s | 885.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-42-50.smt2 | 25.375s | 969.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-49.smt2 | 25.377s | 956.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-197.smt2 | 25.449s | 873.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-49.smt2 | 25.488s | 881.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-48.smt2 | 25.534s | 1150.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-41.smt2 | 25.572s | 543.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-49.smt2 | 25.669s | 993.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1361831.smt2 | 25.737s | 3374.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-49.smt2 | 25.881s | 846.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-46.smt2 | 26.214s | 901.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-67-50.smt2 | 26.223s | 941.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-57-49.smt2 | 26.271s | 866.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1121941.smt2 | 26.334s | 2990.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-37-47.smt2 | 26.417s | 658.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-42.smt2 | 26.533s | 829.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-45.smt2 | 26.606s | 963.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-283008.smt2 | 26.795s | 887.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1317511.smt2 | 26.816s | 3455.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-19-49.smt2 | 26.905s | 848.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-59-50.smt2 | 27.099s | 1037.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1275621.smt2 | 27.192s | 3519.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-49.smt2 | 27.334s | 1001.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-47.smt2 | 27.405s | 948.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-60-50.smt2 | 27.456s | 1012.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-198.smt2 | 27.528s | 1037.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-76-50.smt2 | 27.723s | 925.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-69-50.smt2 | 27.745s | 975.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-50.smt2 | 27.880s | 942.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-408585.smt2 | 28.104s | 1491.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-45.smt2 | 28.183s | 890.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-42.smt2 | 28.210s | 919.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-65-50.smt2 | 28.543s | 944.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-42.smt2 | 28.557s | 665.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-70-50.smt2 | 28.711s | 976.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-42.smt2 | 29.126s | 986.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-49.smt2 | 29.176s | 985.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-42.smt2 | 29.252s | 1167.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-40-50.smt2 | 29.421s | 915.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-199.smt2 | 29.500s | 1072.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-46.smt2 | 29.585s | 984.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-57-50.smt2 | 29.596s | 1065.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-64-50.smt2 | 29.675s | 919.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-77-50.smt2 | 29.683s | 922.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-49.smt2 | 29.756s | 1004.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-44.smt2 | 29.785s | 968.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-42.smt2 | 29.884s | 868.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-50.smt2 | 30.378s | 937.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-50.smt2 | 30.453s | 611.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-45.smt2 | 30.588s | 993.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-48.smt2 | 30.614s | 788.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-48.smt2 | 30.928s | 988.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-49.smt2 | 31.165s | 1104.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-42.smt2 | 31.218s | 737.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-42.smt2 | 31.324s | 974.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-329386.smt2 | 31.423s | 1113.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-43.smt2 | 31.759s | 1006.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-50.smt2 | 31.823s | 839.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-46.smt2 | 31.868s | 974.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-46.smt2 | 32.315s | 970.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-46.smt2 | 32.390s | 983.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-43.smt2 | 32.479s | 1193.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-48.smt2 | 32.504s | 1032.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-44.smt2 | 32.711s | 1039.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-47.smt2 | 32.719s | 984.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-45.smt2 | 32.789s | 1093.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-50.smt2 | 32.871s | 1125.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-17-47.smt2 | 32.901s | 846.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-68-50.smt2 | 33.017s | 926.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-50.smt2 | 33.515s | 973.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-49.smt2 | 33.577s | 889.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-48.smt2 | 33.627s | 907.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-42.smt2 | 33.760s | 1264.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-49.smt2 | 33.804s | 955.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-50.smt2 | 33.958s | 1012.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-42.smt2 | 33.973s | 1190.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-48.smt2 | 34.114s | 1127.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-58-50.smt2 | 34.228s | 930.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-43.smt2 | 34.543s | 1087.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-50.smt2 | 35.040s | 1044.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-46.smt2 | 35.175s | 1445.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-63-50.smt2 | 35.206s | 917.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-45.smt2 | 35.339s | 1095.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-47.smt2 | 35.373s | 1046.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-43.smt2 | 35.416s | 768.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-43.smt2 | 35.433s | 1169.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-43.smt2 | 35.508s | 999.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-44.smt2 | 35.521s | 1117.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-47.smt2 | 35.529s | 992.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-39-50.smt2 | 35.741s | 1224.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-47.smt2 | 35.804s | 1231.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-46.smt2 | 35.863s | 1475.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-50.smt2 | 36.075s | 928.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-45.smt2 | 36.122s | 1126.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-45.smt2 | 36.425s | 1402.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-48.smt2 | 36.543s | 967.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-47.smt2 | 36.715s | 993.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-47.smt2 | 36.733s | 1005.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-48.smt2 | 36.870s | 942.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-906586.smt2 | 36.964s | 3276.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-48.smt2 | 37.193s | 1191.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-48.smt2 | 37.368s | 798.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-48.smt2 | 37.411s | 1007.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-43.smt2 | 37.441s | 1162.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-44.smt2 | 37.519s | 1504.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-45.smt2 | 37.601s | 878.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-43.smt2 | 37.644s | 1116.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-46.smt2 | 37.756s | 1497.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-46.smt2 | 37.827s | 1370.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-45.smt2 | 37.850s | 1060.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-50.smt2 | 37.931s | 1258.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-45.smt2 | 38.055s | 1268.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-44.smt2 | 38.181s | 1222.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-50.smt2 | 38.193s | 1090.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-47.smt2 | 38.266s | 1098.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-44.smt2 | 38.344s | 1180.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-44.smt2 | 38.350s | 1428.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-49.smt2 | 38.408s | 1363.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-46.smt2 | 38.541s | 1006.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-48.smt2 | 38.697s | 1149.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-48.smt2 | 38.759s | 845.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-48.smt2 | 38.990s | 1037.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-46.smt2 | 39.147s | 1003.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1365816.smt2 | 39.154s | 4205.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-46.smt2 | 39.469s | 1024.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-47.smt2 | 39.535s | 1285.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-49.smt2 | 39.815s | 1137.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-46.smt2 | 39.948s | 1074.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-47.smt2 | 39.990s | 1158.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-44.smt2 | 40.065s | 1099.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-46.smt2 | 40.344s | 1341.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-48.smt2 | 40.445s | 610.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-46.smt2 | 40.470s | 1203.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-200.smt2 | 40.748s | 896.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-48.smt2 | 40.897s | 1205.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-45.smt2 | 40.940s | 1576.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-47.smt2 | 41.016s | 1110.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-43.smt2 | 41.184s | 1145.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-49.smt2 | 41.287s | 1212.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-44.smt2 | 41.341s | 1326.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-44.smt2 | 41.567s | 1414.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-48.smt2 | 41.881s | 1217.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-47.smt2 | 42.001s | 1510.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-44.smt2 | 42.014s | 1410.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-45.smt2 | 42.442s | 1074.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-45.smt2 | 42.738s | 1407.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-247831.smt2 | 42.849s | 786.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-46.smt2 | 42.916s | 1158.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-43.smt2 | 43.075s | 1439.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-48.smt2 | 43.350s | 1028.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-49.smt2 | 43.395s | 709.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-49.smt2 | 43.580s | 1078.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-47.smt2 | 43.710s | 1508.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-48.smt2 | 43.814s | 1331.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-269353.smt2 | 43.897s | 869.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-48.smt2 | 44.244s | 1302.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-50.smt2 | 44.269s | 1134.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-46.smt2 | 44.288s | 1316.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-47.smt2 | 44.336s | 881.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-49.smt2 | 44.620s | 1125.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-49.smt2 | 44.801s | 1221.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-45.smt2 | 44.879s | 1392.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-47.smt2 | 45.185s | 1091.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-48.smt2 | 45.239s | 739.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-49.smt2 | 45.746s | 1103.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-48.smt2 | 45.879s | 1369.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-50.smt2 | 45.963s | 1040.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-47.smt2 | 46.208s | 1294.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-48.smt2 | 46.243s | 1407.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-49.smt2 | 46.336s | 1121.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-47.smt2 | 46.792s | 1261.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-50.smt2 | 47.077s | 1053.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-49.smt2 | 47.209s | 1105.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-46.smt2 | 47.469s | 1667.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-48.smt2 | 47.475s | 1174.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-49.smt2 | 47.708s | 1546.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-50.smt2 | 47.720s | 1184.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-47.smt2 | 48.002s | 1735.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-45.smt2 | 48.151s | 1251.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-50.smt2 | 48.183s | 1417.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-49.smt2 | 48.499s | 690.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-48.smt2 | 48.544s | 1524.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-47.smt2 | 48.562s | 1401.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-49.smt2 | 48.637s | 1158.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-48.smt2 | 48.668s | 1502.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-46.smt2 | 48.668s | 853.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-47.smt2 | 49.267s | 1504.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-47.smt2 | 49.372s | 1366.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-49.smt2 | 49.407s | 1125.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-46.smt2 | 49.433s | 1494.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-46.smt2 | 49.777s | 1508.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-48.smt2 | 50.075s | 1315.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-48.smt2 | 50.101s | 1075.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-49.smt2 | 50.530s | 1234.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-21-40.smt2 | 50.579s | 1490.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-17-47.smt2 | 50.645s | 1096.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-46.smt2 | 50.795s | 1052.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-48.smt2 | 50.894s | 1445.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-50.smt2 | 51.107s | 1164.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-50.smt2 | 51.174s | 795.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-50.smt2 | 51.200s | 1187.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-49.smt2 | 51.239s | 1381.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-45.smt2 | 51.381s | 1440.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-47.smt2 | 51.411s | 1497.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-48.smt2 | 51.459s | 1766.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-46.smt2 | 51.514s | 1170.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-14-49.smt2 | 51.645s | 1164.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-47.smt2 | 51.869s | 1332.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-13-50.smt2 | 52.049s | 1297.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-45.smt2 | 52.189s | 1363.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-44.smt2 | 52.878s | 1814.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-48.smt2 | 52.910s | 1393.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-50.smt2 | 52.924s | 1178.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-49.smt2 | 53.503s | 1635.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-48.smt2 | 54.047s | 1312.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-47.smt2 | 54.194s | 1662.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-50.smt2 | 54.326s | 1274.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-46.smt2 | 54.368s | 1705.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-50.smt2 | 54.649s | 1242.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-50.smt2 | 54.813s | 1405.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-48.smt2 | 54.947s | 1962.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-41-50.smt2 | 55.085s | 1047.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-48.smt2 | 55.298s | 1469.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-50.smt2 | 55.368s | 1325.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-50.smt2 | 55.467s | 1310.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-50.smt2 | 55.522s | 990.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-47.smt2 | 55.551s | 1516.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-49.smt2 | 55.923s | 1902.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-46.smt2 | 56.113s | 1441.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-49.smt2 | 56.669s | 1411.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-44.smt2 | 56.852s | 1750.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-50.smt2 | 57.105s | 1406.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-47.smt2 | 57.318s | 1583.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-48.smt2 | 57.319s | 1553.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-50.smt2 | 57.629s | 1185.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-47.smt2 | 57.798s | 1400.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-49.smt2 | 58.107s | 1764.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-50.smt2 | 58.274s | 1534.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-46.smt2 | 58.388s | 1493.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-48.smt2 | 58.987s | 1586.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-46.smt2 | 59.103s | 1434.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-47.smt2 | 59.331s | 1936.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-49.smt2 | 59.766s | 1107.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-48.smt2 | 60.046s | 1483.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1268455.smt2 | 60.050s | 4142.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-46.smt2 | 60.158s | 1032.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-48.smt2 | 60.202s | 1435.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-48.smt2 | 60.211s | 1422.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-48.smt2 | 60.705s | 1707.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-50.smt2 | 61.105s | 1572.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-46.smt2 | 61.531s | 1159.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-47.smt2 | 61.772s | 1733.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-46.smt2 | 61.852s | 1270.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-48.smt2 | 61.919s | 1507.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-49.smt2 | 62.145s | 1696.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-49.smt2 | 62.420s | 1564.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-48.smt2 | 62.520s | 1698.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-49.smt2 | 62.735s | 1528.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-49.smt2 | 63.406s | 1614.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-47.smt2 | 63.546s | 1596.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-48.smt2 | 63.850s | 1406.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-47.smt2 | 64.013s | 1389.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-50.smt2 | 64.035s | 1803.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-48.smt2 | 64.276s | 1780.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-46.smt2 | 64.500s | 1440.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-48.smt2 | 64.726s | 1634.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-47.smt2 | 65.055s | 1562.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-50.smt2 | 65.353s | 1742.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-49.smt2 | 65.361s | 1423.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-48.smt2 | 65.427s | 1535.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-50.smt2 | 65.486s | 1233.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-48.smt2 | 65.690s | 1736.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-50.smt2 | 65.706s | 1846.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-48.smt2 | 65.725s | 1364.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-46.smt2 | 66.058s | 1315.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-48.smt2 | 66.168s | 2032.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-48.smt2 | 66.332s | 1939.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-49.smt2 | 66.529s | 1517.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-47.smt2 | 66.641s | 1705.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-49.smt2 | 66.838s | 968.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-48.smt2 | 67.067s | 2082.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-49.smt2 | 67.166s | 1401.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-321761.smt2 | 67.457s | 1110.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-46.smt2 | 67.463s | 2285.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-48.smt2 | 67.596s | 1503.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-46.smt2 | 67.846s | 1096.0MiB| sat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER10-14-fair.smt2 | 68.470s | 385.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-47.smt2 | 68.517s | 1497.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-48.smt2 | 68.847s | 1773.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-47.smt2 | 69.184s | 1672.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-49.smt2 | 69.680s | 1279.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-46.smt2 | 69.699s | 2038.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-49.smt2 | 69.709s | 1854.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-46.smt2 | 70.081s | 1843.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-48.smt2 | 70.125s | 1842.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-49.smt2 | 70.187s | 1869.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-50.smt2 | 70.497s | 1107.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-49.smt2 | 70.621s | 1020.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-48.smt2 | 70.661s | 1079.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-46.smt2 | 71.497s | 1755.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-50.smt2 | 71.819s | 1746.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-49.smt2 | 71.916s | 1698.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-46.smt2 | 72.249s | 1879.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-48.smt2 | 72.512s | 1445.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1452366.smt2 | 72.828s | 5566.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-48.smt2 | 74.385s | 1131.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-50.smt2 | 75.468s | 2495.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-48.smt2 | 75.688s | 1557.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-46.smt2 | 75.698s | 1515.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-48.smt2 | 75.867s | 1440.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-49.smt2 | 76.069s | 1766.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-47.smt2 | 76.099s | 2212.0MiB| sat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-518109.smt2 | 76.557s | 1838.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-50.smt2 | 76.887s | 1557.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-48.smt2 | 77.008s | 1732.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-45.smt2 | 77.097s | 1959.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-50.smt2 | 77.836s | 1745.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-49.smt2 | 78.248s | 2173.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-48.smt2 | 78.326s | 1886.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-50.smt2 | 78.535s | 2088.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-44.smt2 | 79.542s | 2289.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-48.smt2 | 79.582s | 1720.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-47.smt2 | 80.552s | 1732.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-49.smt2 | 81.177s | 1392.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-49.smt2 | 82.075s | 1828.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-49.smt2 | 82.267s | 1830.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-50.smt2 | 82.552s | 1400.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-50.smt2 | 82.582s | 2498.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-63-50.smt2 | 83.361s | 1708.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-50.smt2 | 84.411s | 1882.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-48.smt2 | 84.861s | 1799.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-46.smt2 | 85.196s | 1855.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-46.smt2 | 85.268s | 1888.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-50.smt2 | 85.409s | 1762.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-50.smt2 | 85.801s | 1562.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-50.smt2 | 85.816s | 2182.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-50.smt2 | 86.282s | 1123.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-49.smt2 | 86.372s | 1733.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-48.smt2 | 87.001s | 1715.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-48.smt2 | 87.339s | 1748.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-46.smt2 | 87.876s | 1456.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1262176.smt2 | 88.167s | 5717.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-47.smt2 | 88.186s | 1589.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-50.smt2 | 88.936s | 2546.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-50.smt2 | 91.659s | 2355.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-50.smt2 | 91.746s | 1302.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-50.smt2 | 91.788s | 1332.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-48.smt2 | 92.014s | 1964.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER11-14-fair.smt2 | 92.415s | 448.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-50.smt2 | 92.601s | 1365.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-48.smt2 | 93.258s | 1632.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-26-43.smt2 | 93.447s | 1760.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1265513.smt2 | 93.537s | 5583.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-49.smt2 | 93.621s | 1722.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-50.smt2 | 94.241s | 1279.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-46.smt2 | 94.352s | 1243.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-46.smt2 | 95.194s | 2348.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-49.smt2 | 96.042s | 1030.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-49.smt2 | 96.693s | 2321.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-50.smt2 | 97.638s | 1799.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-48.smt2 | 99.655s | 1680.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-50.smt2 | 100.133s | 2498.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-46.smt2 | 100.305s | 2008.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-50.smt2 | 100.928s | 2304.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-48.smt2 | 101.353s | 1549.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-49.smt2 | 101.487s | 2194.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-48.smt2 | 102.098s | 2523.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-48.smt2 | 102.328s | 1429.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-50.smt2 | 104.104s | 1700.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-46.smt2 | 104.182s | 2264.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-50.smt2 | 104.505s | 2278.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-50.smt2 | 104.524s | 2222.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-50.smt2 | 105.074s | 2107.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-49.smt2 | 105.235s | 2397.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-48.smt2 | 105.582s | 1482.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-49.smt2 | 105.797s | 1325.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-47.smt2 | 107.415s | 2007.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-47.smt2 | 108.140s | 1996.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-46.smt2 | 108.378s | 1943.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-49.smt2 | 108.532s | 1475.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-46.smt2 | 109.440s | 1993.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-47.smt2 | 109.491s | 1233.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-50.smt2 | 109.543s | 2032.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-50.smt2 | 109.719s | 1697.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-46.smt2 | 110.240s | 1675.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-23-41.smt2 | 111.819s | 2397.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-48.smt2 | 114.241s | 1711.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-47.smt2 | 121.073s | 2413.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-31-42.smt2 | 121.155s | 1632.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-48.smt2 | 123.191s | 1921.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-47.smt2 | 125.704s | 2410.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-50.smt2 | 126.303s | 3044.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-46.smt2 | 126.706s | 1186.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-46.smt2 | 127.502s | 1526.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-50.smt2 | 127.681s | 2026.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-50.smt2 | 127.904s | 1593.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-47.smt2 | 131.138s | 2689.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-48.smt2 | 133.846s | 1894.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-49.smt2 | 137.634s | 1817.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-46.smt2 | 137.973s | 2509.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-48.smt2 | 139.249s | 1654.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-47.smt2 | 139.639s | 2295.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-46.smt2 | 139.897s | 1628.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-47.smt2 | 141.271s | 1604.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-48.smt2 | 143.215s | 1880.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-46.smt2 | 143.426s | 2972.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-46.smt2 | 144.188s | 2957.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-48.smt2 | 144.714s | 1688.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-49.smt2 | 145.106s | 1711.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1072007.smt2 | 145.277s | 5843.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-47.smt2 | 145.368s | 2818.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-46.smt2 | 146.369s | 1327.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-48.smt2 | 147.075s | 2098.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-47.smt2 | 147.690s | 2329.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-46.smt2 | 148.555s | 2239.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-47.smt2 | 149.145s | 1999.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-47.smt2 | 150.700s | 3180.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-49.smt2 | 154.778s | 2576.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-48.smt2 | 155.572s | 1447.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-50.smt2 | 157.163s | 1627.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-278378.smt2 | 159.236s | 965.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-46.smt2 | 159.925s | 2348.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-47.smt2 | 162.056s | 1466.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-49.smt2 | 163.079s | 1825.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-47.smt2 | 163.603s | 2026.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-50.smt2 | 166.069s | 1620.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-49.smt2 | 169.625s | 2152.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-47.smt2 | 172.028s | 2161.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-46.smt2 | 172.111s | 3021.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-47.smt2 | 172.262s | 2700.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-49.smt2 | 172.541s | 2464.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-46.smt2 | 174.690s | 2785.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-495717.smt2 | 174.936s | 2267.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-46.smt2 | 177.153s | 2778.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-47.smt2 | 177.538s | 2066.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-50.smt2 | 177.681s | 2069.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-47.smt2 | 179.233s | 1952.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-47.smt2 | 182.040s | 2410.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-46.smt2 | 182.743s | 2161.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-48.smt2 | 183.654s | 2296.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-48.smt2 | 184.618s | 1844.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-49.smt2 | 184.699s | 1590.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-46.smt2 | 191.079s | 1643.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-46.smt2 | 192.916s | 3005.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-46.smt2 | 194.392s | 1794.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-46.smt2 | 195.268s | 2344.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-48.smt2 | 197.686s | 2364.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-50.smt2 | 198.517s | 2715.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-47.smt2 | 198.622s | 1860.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-1138192.smt2 | 200.607s | 6155.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-48.smt2 | 202.187s | 1393.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-46.smt2 | 202.533s | 2072.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-48.smt2 | 204.167s | 1668.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-47.smt2 | 205.736s | 1901.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-48.smt2 | 206.207s | 1483.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-46.smt2 | 208.059s | 1502.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-49.smt2 | 208.693s | 2157.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-47.smt2 | 209.264s | 2292.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-47.smt2 | 210.643s | 1835.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-46.smt2 | 212.478s | 1911.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-47.smt2 | 213.190s | 3041.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-49.smt2 | 214.034s | 1490.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-46.smt2 | 215.039s | 2830.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-48.smt2 | 219.626s | 2518.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-48.smt2 | 220.619s | 2964.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-49.smt2 | 222.814s | 2433.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-46.smt2 | 224.490s | 2258.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-47.smt2 | 225.564s | 1535.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-47.smt2 | 228.079s | 1885.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-48.smt2 | 228.328s | 3917.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-47.smt2 | 229.899s | 1582.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-47.smt2 | 229.972s | 1614.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-46.smt2 | 233.787s | 1883.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-46.smt2 | 234.040s | 4384.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-49.smt2 | 237.716s | 3058.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-50.smt2 | 238.192s | 2426.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-50.smt2 | 239.469s | 1968.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-47.smt2 | 240.296s | 1787.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-47.smt2 | 240.599s | 2257.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-50.smt2 | 242.244s | 3067.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-50.smt2 | 243.559s | 2113.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-50.smt2 | 245.442s | 2468.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-47.smt2 | 247.841s | 2530.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-47.smt2 | 248.325s | 2020.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-49.smt2 | 249.758s | 4585.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-48.smt2 | 250.801s | 1946.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-48.smt2 | 254.933s | 2406.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-729964.smt2 | 261.121s | 4042.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-46.smt2 | 261.746s | 2396.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-47.smt2 | 268.736s | 2678.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-46.smt2 | 270.505s | 1868.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-47.smt2 | 270.907s | 2061.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-50.smt2 | 271.876s | 2704.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-47.smt2 | 273.221s | 2370.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-658040.smt2 | 276.108s | 3446.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-47.smt2 | 277.945s | 1549.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-47.smt2 | 279.073s | 1568.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-46.smt2 | 279.776s | 1840.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-46.smt2 | 280.443s | 1668.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-46.smt2 | 280.488s | 2423.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-49.smt2 | 280.533s | 3897.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-49.smt2 | 280.749s | 2104.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/mathsat/FISCHER11-15-fair.smt2 | 281.432s | 485.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-762853.smt2 | 284.304s | 4455.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-50.smt2 | 285.525s | 1942.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-48.smt2 | 286.345s | 1977.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-46.smt2 | 286.878s | 2572.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-47.smt2 | 287.057s | 3088.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-50.smt2 | 287.303s | 2205.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-46.smt2 | 288.378s | 2904.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-47.smt2 | 290.087s | 2003.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-49.smt2 | 293.232s | 1802.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-48.smt2 | 293.493s | 2771.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-50.smt2 | 293.785s | 1792.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-50.smt2 | 294.692s | 3389.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-49.smt2 | 296.377s | 3826.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-48.smt2 | 297.946s | 3908.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-48.smt2 | 299.525s | 4712.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-47.smt2 | 300.137s | 3263.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-49.smt2 | 301.114s | 2947.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-49.smt2 | 305.579s | 2786.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-47.smt2 | 308.440s | 1885.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-49.smt2 | 314.611s | 3107.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-47.smt2 | 316.366s | 2633.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-49.smt2 | 318.318s | 3154.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-49.smt2 | 318.763s | 1499.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-47.smt2 | 320.141s | 1950.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-48.smt2 | 324.018s | 2114.0MiB| sat | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-368069.smt2 | 324.586s | 1628.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-49.smt2 | 328.479s | 2062.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-49.smt2 | 336.050s | 1837.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-49.smt2 | 340.318s | 3721.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-47.smt2 | 342.173s | 1618.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-46.smt2 | 347.897s | 1943.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-49.smt2 | 349.252s | 1860.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-50.smt2 | 352.136s | 4063.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-49.smt2 | 362.931s | 3429.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-50.smt2 | 369.270s | 2113.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-49.smt2 | 371.875s | 2372.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-478122.smt2 | 372.154s | 2367.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-46.smt2 | 383.993s | 3953.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-48.smt2 | 391.788s | 4036.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-48.smt2 | 398.539s | 1819.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-50.smt2 | 404.786s | 1700.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-49.smt2 | 406.298s | 2405.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-48.smt2 | 408.370s | 2176.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-50.smt2 | 409.140s | 2247.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-49.smt2 | 409.879s | 3727.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-49.smt2 | 410.204s | 2409.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-48.smt2 | 414.015s | 3308.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-50.smt2 | 414.034s | 4038.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-49.smt2 | 425.943s | 3114.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-48.smt2 | 429.544s | 3094.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-50.smt2 | 431.731s | 3099.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-49.smt2 | 446.856s | 2542.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-49.smt2 | 449.931s | 3780.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-49.smt2 | 451.155s | 3712.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-50.smt2 | 452.309s | 2465.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-46.smt2 | 454.103s | 4755.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-928960.smt2 | 459.213s | 4984.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-49.smt2 | 464.053s | 1731.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-49.smt2 | 464.070s | 2319.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-50.smt2 | 467.941s | 3032.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-49.smt2 | 482.021s | 4170.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-49.smt2 | 484.045s | 3881.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-49.smt2 | 494.511s | 5035.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-50.smt2 | 494.798s | 3216.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-50.smt2 | 499.675s | 2037.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-50.smt2 | 511.923s | 2624.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-50.smt2 | 516.679s | 2238.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-47.smt2 | 527.623s | 3608.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-50.smt2 | 529.802s | 3299.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-47.smt2 | 530.486s | 2456.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-49.smt2 | 532.660s | 2083.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-48.smt2 | 543.274s | 4061.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-50.smt2 | 544.918s | 2256.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-50.smt2 | 549.564s | 2039.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-49.smt2 | 553.090s | 2574.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-50.smt2 | 562.611s | 2303.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-49.smt2 | 564.489s | 2147.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-50.smt2 | 568.643s | 3025.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-50.smt2 | 573.163s | 1957.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-49.smt2 | 579.625s | 5537.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-357303.smt2 | 580.155s | 1623.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-50.smt2 | 584.745s | 3190.0MiB| sat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-50.smt2 | 586.088s | 3509.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-50.smt2 | 587.570s | 2328.0MiB| unsat | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1400961.smt2 | 594.611s | 11.728GiB| sat | 0 | | | |non-incremental/QF_LIA/RWS/Example_7.txt.smt2 | 600.103s | 501.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/RWS/Example_15.txt.smt2 | 600.134s | 561.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/tropical-matrix/constraint-285271.smt2 | 600.166s | 998.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-50.smt2 | 600.188s | 1395.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-49.smt2 | 600.243s | 2101.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-49.smt2 | 600.252s | 1772.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-50.smt2 | 600.260s | 2052.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-49.smt2 | 600.297s | 3120.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-50.smt2 | 600.334s | 2570.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-50.smt2 | 600.341s | 2617.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-50.smt2 | 600.350s | 2411.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-50.smt2 | 600.362s | 3319.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-48.smt2 | 600.384s | 3458.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-50.smt2 | 600.396s | 3105.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-49.smt2 | 600.415s | 3220.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/20231117-c_inference/80_80_71_17_unsat.smt2 | 600.417s | 3789.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-48.smt2 | 600.420s | 2644.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-50.smt2 | 600.439s | 4232.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-50.smt2 | 600.442s | 3937.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-49.smt2 | 600.464s | 4328.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-50.smt2 | 600.499s | 4022.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-49.smt2 | 600.505s | 3144.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-50.smt2 | 600.507s | 4587.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-49.smt2 | 600.507s | 4180.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-50.smt2 | 600.532s | 3268.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-47.smt2 | 600.577s | 3452.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-50.smt2 | 600.583s | 5195.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-49.smt2 | 600.602s | 5734.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-985518.smt2 | 600.828s | 7120.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-49.smt2 | 600.839s | 5487.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1228327.smt2 | 601.024s | 10.08GiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1060546.smt2 | 601.185s | 7595.0MiB| timeout | 0 | | | |non-incremental/QF_LIA/arctic-matrix/constraint-1472027.smt2 | 601.361s | 12.69GiB| timeout | 0 | | |