# data * SAT 124 * UNSAT 39 * TIMEOUT 134 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: smt-clausal-lookahead-60-qfufnia-unknown
Z3 repo: https://github.com/Z3Prover/z3
Z3 commit: f5749502379a3fdecdbae07053f6f188c56c3c3f
Z3 branch: master
Z3 options: "-T:60 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify smt)" smt.sls.enable=true smt.sls.parallel=false model_validate=true sls.arith_use_clausal_lookahead=true"
Z3 inputs: inputs/QF_UFNIA_UNKNOWN
Z3 commit message: fix #7521 (#7531)
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |int_check_bvule_bvurem1_ltr_inv_g.smt2 | 0.014s | 52.716MiB| unsat | 0 | | | |int_check_bvult_bvurem1_ltr_inv_g.smt2 | 0.014s | 52.772MiB| unsat | 0 | | | |qf_Select_700_values_123.smt2 | 0.014s | 53.068MiB| unsat | 0 | | | |qf_Select_705_values_0.smt2 | 0.015s | 52.812MiB| unsat | 0 | | | |int_check_bvult_bvneg_ltr_inv_g.smt2 | 0.015s | 52.576MiB| unsat | 0 | | | |int_check_bvule_bvneg_ltr_inv_g.smt2 | 0.016s | 52.792MiB| unsat | 0 | | | |qf_AndOrXor_1869_values_0.smt2 | 0.016s | 52.92MiB| unsat | 0 | | | |int_check_bvsge_bvlshr0_rtl.smt2 | 0.016s | 53.328MiB| sat | 0 | | | |qf_AndOrXor_794_values_121.smt2 | 0.016s | 52.812MiB| unsat | 0 | | | |int_check_bvult_bvurem0_ltr_inv_g.smt2 | 0.016s | 52.556MiB| unsat | 0 | | | |qf_Select_727_values_0.smt2 | 0.017s | 53.068MiB| unsat | 0 | | | |qf_AndOrXor_230_values_0.smt2 | 0.017s | 53.068MiB| sat | 0 | | | |qf_InstCombineShift497a_values_0.smt2 | 0.017s | 53.324MiB| sat | 0 | | | |int_check_bvule_bvudiv1_ltr_inv_g.smt2 | 0.017s | 53.068MiB| sat | 0 | | | |int_check_bvsgt_bvadd_rtl.smt2 | 0.017s | 53.068MiB| sat | 0 | | | |int_check_bvsgt_bvshl0_rtl.smt2 | 0.018s | 53.176MiB| sat | 0 | | | |qf_AndOrXor_1894_values_0.smt2 | 0.018s | 52.872MiB| unsat | 0 | | | |qf_AndOrXor_210_values_0.smt2 | 0.018s | 53.016MiB| sat | 0 | | | |int_check_bvugt_bvudiv1_rtl.smt2 | 0.018s | 53.076MiB| unsat | 0 | | | |int_check_bvsgt_bvshl0_ltr_inv_g.smt2 | 0.019s | 53.592MiB| sat | 0 | | | |int_check_bvsgt_bvashr0_rtl.smt2 | 0.019s | 53.812MiB| sat | 0 | | | |int_check_bvsle_bvurem1_ltr_inv_g.smt2 | 0.019s | 53.324MiB| sat | 0 | | | |int_check_bvslt_bvlshr0_rtl.smt2 | 0.019s | 53.324MiB| sat | 0 | | | |int_check_bvsle_bvashr0_rtl.smt2 | 0.019s | 53.584MiB| sat | 0 | | | |int_check_bvuge_bvashr1_rtl.smt2 | 0.020s | 53.324MiB| sat | 0 | | | |int_check_bvsgt_bvashr1_ltr_inv_g.smt2 | 0.020s | 53.584MiB| sat | 0 | | | |qf_Select_575a_values_0.smt2 | 0.020s | 54.092MiB| sat | 0 | | | |int_check_bvsgt_bvlshr0_rtl.smt2 | 0.020s | 53.812MiB| sat | 0 | | | |qf_AndOrXor_2443_values_0.smt2 | 0.020s | 53.58MiB| sat | 0 | | | |int_check_bvsgt_bvurem0_rtl.smt2 | 0.022s | 53.556MiB| sat | 0 | | | |qf_AndOrXor_290_values_7.smt2 | 0.022s | 53.324MiB| sat | 0 | | | |qf_InstCombineShift497b_values_0.smt2 | 0.022s | 54.352MiB| sat | 0 | | | |int_check_bvule_bvurem0_ltr_inv_g.smt2 | 0.023s | 52.516MiB| unsat | 0 | | | |int_check_bvugt_bvudiv0_rtl.smt2 | 0.025s | 53.324MiB| unsat | 0 | | | |qf_Select_575b_values_0.smt2 | 0.025s | 53.48MiB| sat | 0 | | | |int_check_ne_bvashr0_ltr_inv_g.smt2 | 0.030s | 53.444MiB| sat | 0 | | | |int_check_eq_bvashr0_rtl.smt2 | 0.031s | 54.068MiB| sat | 0 | | | |int_check_eq_bvurem0_rtl.smt2 | 0.036s | 53.328MiB| unsat | 0 | | | |int_check_bvugt_bvurem0_rtl.smt2 | 0.043s | 53.488MiB| unsat | 0 | | | |int_check_bvuge_bvurem0_rtl.smt2 | 0.044s | 53.264MiB| unsat | 0 | | | |int_check_eq_bvurem0_ltr_inv_g.smt2 | 0.047s | 53.252MiB| unsat | 0 | | | |int_check_bvsge_bvudiv1_rtl.smt2 | 0.053s | 53.652MiB| sat | 0 | | | |int_check_bvsle_bvudiv0_rtl.smt2 | 0.057s | 53.868MiB| sat | 0 | | | |int_check_bvuge_bvshl0_rtl.smt2 | 0.059s | 53.396MiB| sat | 0 | | | |int_check_ne_bvashr1_ltr_inv_g.smt2 | 0.062s | 53.58MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFNIA.smt2 | 0.068s | 54.86MiB| sat | 0 | | | |int_check_eq_bvudiv0_rtl.smt2 | 0.080s | 53.444MiB| unsat | 0 | | | |qf_InstCombineShift497c_values_0.smt2 | 0.081s | 54.348MiB| sat | 0 | | | |int_check_bvsge_bvashr1_rtl.smt2 | 0.092s | 53.6MiB| sat | 0 | | | |int_check_bvsge_bvneg_ltr_inv_g.smt2 | 0.097s | 53.624MiB| unsat | 0 | | | |int_check_bvsle_bvashr1_rtl.smt2 | 0.097s | 53.616MiB| sat | 0 | | | |int_check_bvugt_bvashr0_ltr_inv_g.smt2 | 0.107s | 53.748MiB| sat | 0 | | | |int_check_bvsle_bvashr0_ltr_inv_g.smt2 | 0.116s | 53.832MiB| sat | 0 | | | |int_check_bvslt_bvashr1_rtl.smt2 | 0.121s | 54.292MiB| sat | 0 | | | |int_check_eq_bvudiv1_rtl.smt2 | 0.126s | 53.856MiB| unsat | 0 | | | |int_check_bvsge_bvurem1_ltr_inv_g.smt2 | 0.131s | 54.204MiB| sat | 0 | | | |int_check_bvsle_bvshl0_ltr_inv_g.smt2 | 0.140s | 53.876MiB| sat | 0 | | | |int_check_bvugt_bvashr1_rtl.smt2 | 0.143s | 54.352MiB| sat | 0 | | | |int_check_bvugt_bvashr1_ltr_inv_g.smt2 | 0.159s | 54.336MiB| sat | 0 | | | |int_check_bvslt_bvudiv0_ltr_inv_g.smt2 | 0.162s | 53.836MiB| sat | 0 | | | |int_check_bvslt_bvlshr0_ltr_inv_g.smt2 | 0.162s | 53.86MiB| sat | 0 | | | |n99-0002.smt2 | 0.170s | 58.916MiB| sat | 0 | | | |qf_Select_510_values_0.smt2 | 0.171s | 54.348MiB| sat | 0 | | | |int_check_bvuge_bvashr1_ltr_inv_g.smt2 | 0.175s | 53.532MiB| sat | 0 | | | |qf_AddSub_1619_values_0.smt2 | 0.180s | 53.6MiB| unsat | 0 | | | |int_check_bvslt_bvashr0_rtl.smt2 | 0.185s | 54.84MiB| sat | 0 | | | |n134-0038.smt2 | 0.225s | 59.112MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFNIA.smt2 | 0.253s | 58.508MiB| sat | 0 | | | |int_check_bvult_bvashr1_rtl.smt2 | 0.257s | 53.72MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFNIA.smt2 | 0.283s | 60.68MiB| unsat | 0 | | | |int_check_bvsgt_bvurem1_rtl.smt2 | 0.303s | 54.468MiB| sat | 0 | | | |int_check_bvsgt_bvlshr1_rtl.smt2 | 0.337s | 54.092MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFNIA.smt2 | 0.350s | 66.404MiB| sat | 0 | | | |qf_AddSub_1165_values_0.smt2 | 0.464s | 54.192MiB| unsat | 0 | | | |int_check_bvsle_bvadd_ltr_inv_g.smt2 | 0.476s | 54.752MiB| unsat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFNIA.smt2 | 0.503s | 75.896MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFNIA.smt2 | 0.533s | 77.0MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFNIA.smt2 | 0.536s | 86.436MiB| sat | 0 | | | |qf_AddSub_1574_values_0.smt2 | 0.597s | 54.472MiB| unsat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFNIA.smt2 | 0.788s | 68.532MiB| sat | 0 | | | |n86-0040.smt2 | 0.817s | 76.444MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFNIA.smt2 | 0.911s | 64.624MiB| sat | 0 | | | |n125-0029.smt2 | 1.109s | 65.484MiB| sat | 0 | | | |n92-0047.smt2 | 1.340s | 128.0MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFNIA.smt2 | 1.364s | 60.816MiB| sat | 0 | | | |n124-0028.smt2 | 1.374s | 72.404MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFNIA.smt2 | 1.590s | 86.884MiB| sat | 0 | | | |n101-0004.smt2 | 1.891s | 64.436MiB| sat | 0 | | | |n128-0032.smt2 | 1.999s | 120.0MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFNIA.smt2 | 2.050s | 110.0MiB| sat | 0 | | | |n65-0019.smt2 | 2.053s | 74.052MiB| sat | 0 | | | |n17-0021.smt2 | 2.321s | 151.0MiB| unsat | 0 | | | |n104-0007.smt2 | 2.355s | 144.0MiB| unsat | 0 | | | |n108-0012.smt2 | 2.394s | 126.0MiB| unsat | 0 | | | |n110-0014.smt2 | 2.434s | 73.908MiB| sat | 0 | | | |n100-0003.smt2 | 2.849s | 79.564MiB| sat | 0 | | | |n135-0039.smt2 | 2.934s | 85.38MiB| sat | 0 | | | |int_check_bvsge_bvlshr0_ltr_inv_g.smt2 | 3.052s | 55.608MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFNIA.smt2 | 4.273s | 152.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFNIA.smt2 | 4.274s | 168.0MiB| sat | 0 | | | |n27-0034.smt2 | 4.295s | 325.0MiB| unsat | 0 | | | |n12-0013.smt2 | 4.316s | 126.0MiB| sat | 0 | | | |n18-0022.smt2 | 4.322s | 97.0MiB| sat | 0 | | | |n30-0037.smt2 | 4.432s | 108.0MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFNIA.smt2 | 4.485s | 67.592MiB| unsat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFNIA.smt2 | 4.588s | 109.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFNIA.smt2 | 4.935s | 168.0MiB| sat | 0 | | | |n26-0033.smt2 | 6.128s | 365.0MiB| unsat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFNIA.smt2 | 6.192s | 203.0MiB| sat | 0 | | | |n41-0048.smt2 | 6.620s | 110.0MiB| unsat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFNIA.smt2 | 6.713s | 161.0MiB| sat | 0 | | | |n57-0010.smt2 | 6.958s | 117.0MiB| sat | 0 | | | |n90-0045.smt2 | 7.142s | 91.248MiB| sat | 0 | | | |n55-0008.smt2 | 7.415s | 71.76MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFNIA.smt2 | 7.757s | 88.808MiB| sat | 0 | | | |n119-0023.smt2 | 7.841s | 108.0MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFNIA.smt2 | 8.007s | 79.068MiB| sat | 0 | | | |n58-0011.smt2 | 8.361s | 66.764MiB| sat | 0 | | | |n107-0011.smt2 | 8.428s | 119.0MiB| sat | 0 | | | |n53-0006.smt2 | 8.614s | 61.764MiB| sat | 0 | | | |n73-0027.smt2 | 8.809s | 89.672MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFNIA.smt2 | 8.903s | 209.0MiB| sat | 0 | | | |n105-0008.smt2 | 8.994s | 93.72MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFNIA.smt2 | 9.108s | 283.0MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFNIA.smt2 | 9.351s | 56.432MiB| sat | 0 | | | |n127-0031.smt2 | 9.405s | 93.092MiB| sat | 0 | | | |n9-0009.smt2 | 9.563s | 113.0MiB| sat | 0 | | | |n5-0005.smt2 | 10.223s | 91.508MiB| sat | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFNIA.smt2 | 10.468s | 246.0MiB| sat | 0 | | | |n37-0044.smt2 | 10.594s | 133.0MiB| sat | 0 | | | |n61-0015.smt2 | 11.056s | 193.0MiB| sat | 0 | | | |n102-0005.smt2 | 11.106s | 62.68MiB| sat | 0 | | | |n34-0041.smt2 | 11.301s | 137.0MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFNIA.smt2 | 11.372s | 264.0MiB| sat | 0 | | | |qf_muldivrem_152_values_0.smt2 | 11.410s | 73.012MiB| unsat | 0 | | | |n1-0001.smt2 | 11.691s | 1131.0MiB| unsat | 0 | | | |n96-0051.smt2 | 11.913s | 195.0MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFNIA.smt2 | 11.929s | 73.068MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFNIA.smt2 | 12.324s | 122.0MiB| sat | 0 | | | |n88-0042.smt2 | 12.611s | 106.0MiB| sat | 0 | | | |n59-0012.smt2 | 14.844s | 100.0MiB| sat | 0 | | | |n38-0045.smt2 | 15.052s | 167.0MiB| sat | 0 | | | |n114-0018.smt2 | 19.480s | 155.0MiB| sat | 0 | | | |n137-0041.smt2 | 20.640s | 128.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFNIA.smt2 | 22.846s | 827.0MiB| unsat | 0 | | | |n25-0032.smt2 | 22.877s | 315.0MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFNIA.smt2 | 22.905s | 187.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFNIA.smt2 | 23.372s | 279.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFNIA.smt2 | 24.478s | 414.0MiB| sat | 0 | | | |n35-0042.smt2 | 24.755s | 263.0MiB| sat | 0 | | | |n31-0038.smt2 | 24.809s | 83.688MiB| sat | 0 | | | |n46-0053.smt2 | 29.271s | 202.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_2_UFNIA.smt2 | 31.153s | 208.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFNIA.smt2 | 32.509s | 312.0MiB| sat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFNIA.smt2 | 34.212s | 226.0MiB| sat | 0 | | | |n3-0003.smt2 | 37.592s | 111.0MiB| sat | 0 | | | |n0-0000.smt2 | 43.828s | 213.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFNIA.smt2 | 47.628s | 374.0MiB| sat | 0 | | | |n106-0009.smt2 | 49.034s | 69.008MiB| sat | 0 | | | |n23-0030.smt2 | 55.186s | 364.0MiB| sat | 0 | | | |n19-0024.smt2 | 56.100s | 182.0MiB| sat | 0 | | | |n91-0046.smt2 | 56.217s | 164.0MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFNIA.smt2 | 58.379s | 79.584MiB| timeout | 0 | | | |n89-0044.smt2 | 59.147s | 147.0MiB| unsat | 0 | | | |0065.smt2 | 59.180s | 231.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFNIA.smt2 | 59.594s | 761.0MiB| timeout | 0 | | | |n113-0017.smt2 | 59.604s | 233.0MiB| timeout | 0 | | | |n50-0003.smt2 | 59.653s | 87.728MiB| timeout | 0 | | | |n94-0049.smt2 | 59.688s | 143.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFNIA.smt2 | 59.731s | 70.372MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFNIA.smt2 | 59.754s | 68.004MiB| timeout | 0 | | | |n42-0049.smt2 | 59.797s | 256.0MiB| timeout | 0 | | | |n56-0009.smt2 | 59.821s | 108.0MiB| timeout | 0 | | | |0066.smt2 | 59.831s | 2562.0MiB| timeout | 0 | | | |n21-0027.smt2 | 59.850s | 224.0MiB| timeout | 0 | | | |n22-0029.smt2 | 59.850s | 302.0MiB| timeout | 0 | | | |n76-0030.smt2 | 59.856s | 1045.0MiB| timeout | 0 | | | |n80-0034.smt2 | 59.866s | 79.1MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFNIA.smt2 | 59.868s | 57.992MiB| timeout | 0 | | | |n66-0020.smt2 | 59.870s | 300.0MiB| timeout | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFNIA.smt2 | 59.883s | 195.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFNIA.smt2 | 59.888s | 387.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFNIA.smt2 | 59.890s | 332.0MiB| timeout | 0 | | | |n82-0036.smt2 | 59.892s | 205.0MiB| timeout | 0 | | | |n133-0037.smt2 | 59.899s | 60.56MiB| timeout | 0 | | | |n36-0043.smt2 | 59.902s | 520.0MiB| timeout | 0 | | | |n122-0026.smt2 | 59.904s | 150.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFNIA.smt2 | 59.909s | 438.0MiB| timeout | 0 | | | |n117-0021.smt2 | 59.909s | 376.0MiB| timeout | 0 | | | |n51-0004.smt2 | 59.909s | 77.62MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFNIA.smt2 | 59.911s | 70.04MiB| timeout | 0 | | | |n116-0020.smt2 | 59.915s | 812.0MiB| timeout | 0 | | | |int_check_eq_bvlshr0_rtl.smt2 | 59.924s | 119.0MiB| timeout | 0 | | | |n78-0032.smt2 | 59.933s | 525.0MiB| timeout | 0 | | | |n47-0000.smt2 | 59.934s | 99.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFNIA.smt2 | 59.935s | 170.0MiB| timeout | 0 | | | |n115-0019.smt2 | 59.935s | 130.0MiB| timeout | 0 | | | |n6-0006.smt2 | 59.938s | 72.472MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFNIA.smt2 | 59.941s | 72.556MiB| timeout | 0 | | | |n16-0019.smt2 | 59.941s | 227.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFNIA.smt2 | 59.942s | 68.32MiB| timeout | 0 | | | |n70-0024.smt2 | 59.942s | 1047.0MiB| timeout | 0 | | | |n77-0031.smt2 | 59.943s | 644.0MiB| timeout | 0 | | | |n84-0038.smt2 | 59.947s | 524.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFNIA.smt2 | 59.947s | 113.0MiB| timeout | 0 | | | |n118-0022.smt2 | 59.952s | 513.0MiB| timeout | 0 | | | |n54-0007.smt2 | 59.953s | 256.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFNIA.smt2 | 59.954s | 109.0MiB| timeout | 0 | | | |n126-0030.smt2 | 59.955s | 144.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFNIA.smt2 | 59.956s | 57.0MiB| timeout | 0 | | | |n109-0013.smt2 | 59.956s | 270.0MiB| timeout | 0 | | | |0054.smt2 | 59.957s | 1405.0MiB| timeout | 0 | | | |0061.smt2 | 59.962s | 184.0MiB| timeout | 0 | | | |n74-0028.smt2 | 59.962s | 168.0MiB| timeout | 0 | | | |qf_muldivrem_290_292_values_0.smt2 | 59.963s | 125.0MiB| timeout | 0 | | | |n131-0035.smt2 | 59.963s | 66.492MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFNIA.smt2 | 59.963s | 134.0MiB| timeout | 0 | | | |qf_muldivrem_229_values_0.smt2 | 59.964s | 120.0MiB| timeout | 0 | | | |n48-0001.smt2 | 59.964s | 108.0MiB| timeout | 0 | | | |n69-0023.smt2 | 59.965s | 144.0MiB| timeout | 0 | | | |qf_InstCombineShift497d_values_0.smt2 | 59.966s | 110.0MiB| timeout | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFNIA.smt2 | 59.967s | 119.0MiB| timeout | 0 | | | |n103-0006.smt2 | 59.968s | 69.912MiB| timeout | 0 | | | |n120-0024.smt2 | 59.968s | 130.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFNIA.smt2 | 59.968s | 102.0MiB| timeout | 0 | | | |n93-0048.smt2 | 59.969s | 136.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFNIA.smt2 | 59.972s | 481.0MiB| timeout | 0 | | | |n43-0050.smt2 | 59.973s | 1095.0MiB| timeout | 0 | | | |0056.smt2 | 59.973s | 268.0MiB| timeout | 0 | | | |n75-0029.smt2 | 59.975s | 89.24MiB| timeout | 0 | | | |n52-0005.smt2 | 59.976s | 74.172MiB| timeout | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFNIA.smt2 | 59.977s | 128.0MiB| timeout | 0 | | | |qf_muldivrem_239_values_0.smt2 | 59.977s | 147.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFNIA.smt2 | 59.977s | 68.684MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFNIA.smt2 | 59.978s | 126.0MiB| timeout | 0 | | | |n44-0051.smt2 | 59.978s | 517.0MiB| timeout | 0 | | | |0060.smt2 | 59.981s | 180.0MiB| timeout | 0 | | | |n97-0000.smt2 | 59.981s | 97.028MiB| timeout | 0 | | | |0064.smt2 | 59.983s | 628.0MiB| timeout | 0 | | | |n32-0039.smt2 | 59.983s | 392.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFNIA.smt2 | 59.984s | 110.0MiB| timeout | 0 | | | |n132-0036.smt2 | 59.984s | 64.064MiB| timeout | 0 | | | |n72-0026.smt2 | 59.984s | 536.0MiB| timeout | 0 | | | |n2-0002.smt2 | 59.984s | 486.0MiB| timeout | 0 | | | |0057.smt2 | 59.985s | 222.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFNIA.smt2 | 59.986s | 93.276MiB| timeout | 0 | | | |n40-0047.smt2 | 59.986s | 374.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFNIA.smt2 | 59.986s | 87.844MiB| timeout | 0 | | | |n129-0033.smt2 | 59.987s | 115.0MiB| timeout | 0 | | | |n130-0034.smt2 | 59.988s | 272.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFNIA.smt2 | 59.988s | 336.0MiB| timeout | 0 | | | |n83-0037.smt2 | 59.988s | 561.0MiB| timeout | 0 | | | |n123-0027.smt2 | 59.989s | 74.432MiB| timeout | 0 | | | |n13-0015.smt2 | 59.989s | 345.0MiB| timeout | 0 | | | |n87-0041.smt2 | 59.990s | 105.0MiB| timeout | 0 | | | |n121-0025.smt2 | 59.991s | 436.0MiB| timeout | 0 | | | |n98-0001.smt2 | 59.991s | 123.0MiB| timeout | 0 | | | |n7-0007.smt2 | 59.991s | 280.0MiB| timeout | 0 | | | |n10-0010.smt2 | 59.992s | 210.0MiB| timeout | 0 | | | |n49-0002.smt2 | 59.993s | 98.0MiB| timeout | 0 | | | |n112-0016.smt2 | 59.994s | 859.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFNIA.smt2 | 59.994s | 338.0MiB| timeout | 0 | | | |n63-0017.smt2 | 59.995s | 216.0MiB| timeout | 0 | | | |n60-0014.smt2 | 59.996s | 369.0MiB| timeout | 0 | | | |n11-0012.smt2 | 60.000s | 100.0MiB| timeout | 0 | | | |n64-0018.smt2 | 60.000s | 218.0MiB| timeout | 0 | | | |n79-0033.smt2 | 60.000s | 350.0MiB| timeout | 0 | | | |0067.smt2 | 60.002s | 449.0MiB| timeout | 0 | | | |n8-0008.smt2 | 60.005s | 238.0MiB| timeout | 0 | | | |n28-0035.smt2 | 60.006s | 322.0MiB| timeout | 0 | | | |n33-0040.smt2 | 60.006s | 567.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFNIA.smt2 | 60.006s | 243.0MiB| timeout | 0 | | | |n4-0004.smt2 | 60.007s | 116.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFNIA.smt2 | 60.008s | 96.172MiB| timeout | 0 | | | |n111-0015.smt2 | 60.010s | 951.0MiB| timeout | 0 | | | |n136-0040.smt2 | 60.011s | 486.0MiB| timeout | 0 | | | |0058.smt2 | 60.012s | 790.0MiB| timeout | 0 | | | |n68-0022.smt2 | 60.012s | 328.0MiB| timeout | 0 | | | |n24-0031.smt2 | 60.014s | 356.0MiB| timeout | 0 | | | |n71-0025.smt2 | 60.015s | 1025.0MiB| timeout | 0 | | | |n95-0050.smt2 | 60.021s | 917.0MiB| timeout | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFNIA.smt2 | 60.021s | 653.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFNIA.smt2 | 60.023s | 1023.0MiB| timeout | 0 | | | |n67-0021.smt2 | 60.023s | 590.0MiB| timeout | 0 | | | |0063.smt2 | 60.026s | 2067.0MiB| timeout | 0 | | | |n81-0035.smt2 | 60.026s | 391.0MiB| timeout | 0 | | | |n85-0039.smt2 | 60.026s | 740.0MiB| timeout | 0 | | | |n20-0026.smt2 | 60.034s | 861.0MiB| timeout | 0 | | | |n39-0046.smt2 | 60.035s | 1697.0MiB| timeout | 0 | | | |n45-0052.smt2 | 60.042s | 1293.0MiB| timeout | 0 | | | |0059.smt2 | 60.051s | 841.0MiB| timeout | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFNIA.smt2 | 60.054s | 229.0MiB| timeout | 0 | | | |0055.smt2 | 60.055s | 1408.0MiB| timeout | 0 | | | |0062.smt2 | 60.055s | 2695.0MiB| timeout | 0 | | | |n29-0036.smt2 | 60.056s | 1714.0MiB| timeout | 0 | | | |n62-0016.smt2 | 60.062s | 325.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFNIA.smt2 | 61.226s | 107.0MiB| timeout | 0 | | |