# data * SAT 98 * UNSAT 43 * TIMEOUT 137 * UNKNOWN 0 * UNSET 30 * ERROR 30 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: dio
Z3 repo: https://github.com/Z3Prover/z3
Z3 commit: 871e90b7757c3d64a2a172086ee909fd6a72af8b
Z3 branch: dio
Z3 options: "-T:60 -v:2 -st"
Z3 inputs: inputs/certora
Z3 commit message: do not use conflicts with fresh vars to create branches

Signed-off-by: Lev Nachmanson
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |65782_cd31513fdcd15701933b_6_QF_UFLIA.smt2 | 0.593s | 182.0MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTNIA.smt2 | 0.601s | 184.0MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFDTNIA.smt2 | 0.603s | 181.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTLIA.smt2 | 0.634s | 183.0MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTLIA.smt2 | 0.641s | 184.0MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFLIA.smt2 | 0.645s | 184.0MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFNIA.smt2 | 0.659s | 181.0MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFNIA.smt2 | 0.700s | 184.0MiB| unsat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFLIA.smt2 | 0.706s | 185.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTNIA.smt2 | 0.724s | 187.0MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFLIA.smt2 | 0.725s | 186.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFLIA.smt2 | 0.725s | 184.0MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFLIA.smt2 | 0.734s | 186.0MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFDTLIA.smt2 | 0.765s | 182.0MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTNIA.smt2 | 0.766s | 190.0MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTLIA.smt2 | 0.772s | 184.0MiB| unsat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTNIA.smt2 | 0.775s | 186.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTLIA.smt2 | 0.794s | 193.0MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTLIA.smt2 | 0.799s | 185.0MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTLIA.smt2 | 0.808s | 199.0MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTNIA.smt2 | 0.823s | 188.0MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTNIA.smt2 | 0.850s | 187.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTNIA.smt2 | 0.853s | 189.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTNIA.smt2 | 0.883s | 184.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFNIA.smt2 | 0.884s | 185.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTLIA.smt2 | 0.893s | 196.0MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTLIA.smt2 | 0.906s | 185.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFNIA.smt2 | 0.939s | 196.0MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTNIA.smt2 | 0.948s | 186.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFLIA.smt2 | 0.964s | 190.0MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTLIA.smt2 | 0.970s | 187.0MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFNIA.smt2 | 0.986s | 182.0MiB| unsat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTNIA.smt2 | 0.986s | 186.0MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTNIA.smt2 | 0.993s | 188.0MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFNIA.smt2 | 1.003s | 190.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTLIA.smt2 | 1.025s | 195.0MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFNIA.smt2 | 1.025s | 187.0MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFNIA.smt2 | 1.062s | 188.0MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTLIA.smt2 | 1.098s | 214.0MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTNIA.smt2 | 1.117s | 185.0MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFLIA.smt2 | 1.140s | 198.0MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFLIA.smt2 | 1.167s | 196.0MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTNIA.smt2 | 1.205s | 187.0MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTLIA.smt2 | 1.290s | 189.0MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTLIA.smt2 | 1.329s | 199.0MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTLIA.smt2 | 1.367s | 193.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTLIA.smt2 | 1.406s | 208.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTNIA.smt2 | 1.506s | 201.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTLIA.smt2 | 1.548s | 208.0MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTLIA.smt2 | 1.581s | 217.0MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTLIA.smt2 | 1.608s | 217.0MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTLIA.smt2 | 1.612s | 196.0MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTNIA.smt2 | 1.618s | 186.0MiB| unsat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTLIA.smt2 | 1.627s | 202.0MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTNIA.smt2 | 1.644s | 215.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTNIA.smt2 | 1.703s | 217.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTLIA.smt2 | 1.705s | 210.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTLIA.smt2 | 1.889s | 195.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFNIA.smt2 | 1.944s | 188.0MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFNIA.smt2 | 1.980s | 218.0MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTLIA.smt2 | 2.156s | 206.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTLIA.smt2 | 2.169s | 226.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTLIA.smt2 | 2.325s | 221.0MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTNIA.smt2 | 2.340s | 218.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTNIA.smt2 | 2.558s | 205.0MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFNIA.smt2 | 2.559s | 234.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTNIA.smt2 | 2.611s | 202.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTLIA.smt2 | 2.716s | 237.0MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTLIA.smt2 | 2.722s | 190.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTNIA.smt2 | 2.803s | 236.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTLIA.smt2 | 2.880s | 204.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTLIA.smt2 | 2.882s | 265.0MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTNIA.smt2 | 3.074s | 189.0MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTNIA.smt2 | 3.204s | 265.0MiB| unsat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTNIA.smt2 | 3.300s | 241.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTNIA.smt2 | 3.368s | 222.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTNIA.smt2 | 3.397s | 196.0MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFNIA.smt2 | 3.427s | 186.0MiB| unsat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTNIA.smt2 | 3.565s | 202.0MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFLIA.smt2 | 3.817s | 249.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFLIA.smt2 | 3.843s | 203.0MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTLIA.smt2 | 3.846s | 227.0MiB| unsat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTLIA.smt2 | 3.877s | 192.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTLIA.smt2 | 3.938s | 236.0MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTNIA.smt2 | 3.989s | 212.0MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFLIA.smt2 | 4.059s | 233.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTNIA.smt2 | 4.130s | 208.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTNIA.smt2 | 4.171s | 200.0MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFNIA.smt2 | 4.392s | 192.0MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFLIA.smt2 | 4.542s | 269.0MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFLIA.smt2 | 4.759s | 246.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFLIA.smt2 | 4.781s | 197.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTLIA.smt2 | 4.858s | 283.0MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTLIA.smt2 | 5.162s | 234.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTLIA.smt2 | 5.809s | 375.0MiB| unsat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFNIA.smt2 | 6.527s | 221.0MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTLIA.smt2 | 7.007s | 248.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTNIA.smt2 | 7.340s | 304.0MiB| unsat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFLIA.smt2 | 7.449s | 277.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFLIA.smt2 | 7.487s | 259.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFLIA.smt2 | 7.983s | 209.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTLIA.smt2 | 8.114s | 393.0MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFLIA.smt2 | 8.668s | 692.0MiB| unsat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTNIA.smt2 | 9.723s | 224.0MiB| unsat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTNIA.smt2 | 9.745s | 226.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFNIA.smt2 | 9.799s | 225.0MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFNIA.smt2 | 9.846s | 209.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFLIA.smt2 | 9.957s | 315.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFLIA.smt2 | 10.082s | 318.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTLIA.smt2 | 11.296s | 224.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTLIA.smt2 | 11.379s | 268.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTLIA.smt2 | 11.737s | 310.0MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTLIA.smt2 | 11.752s | 291.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFLIA.smt2 | 12.206s | 321.0MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTLIA.smt2 | 13.159s | 195.0MiB| sat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTLIA.smt2 | 13.200s | 241.0MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFNIA.smt2 | 14.080s | 201.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTNIA.smt2 | 14.215s | 297.0MiB| unsat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFNIA.smt2 | 15.079s | 6168.0MiB| unset | 137 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTLIA.smt2 | 15.577s | 210.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2 | 16.310s | 344.0MiB| unsat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFLIA.smt2 | 17.332s | 394.0MiB| unsat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTLIA.smt2 | 17.336s | 361.0MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTLIA.smt2 | 17.659s | 588.0MiB| unsat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFLIA.smt2 | 18.009s | 6112.0MiB| unset | 137 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTNIA.smt2 | 18.324s | 196.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTNIA.smt2 | 20.142s | 307.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTLIA.smt2 | 20.506s | 317.0MiB| unsat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTNIA.smt2 | 20.882s | 247.0MiB| unsat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFNIA.smt2 | 21.078s | 7462.0MiB| unset | 137 | | | |41958_32933c5a1384696720a2_63_QF_UFNIA.smt2 | 22.505s | 189.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFNIA.smt2 | 22.730s | 588.0MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFLIA.smt2 | 24.081s | 10.345GiB| unset | 137 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFNIA.smt2 | 24.328s | 8881.0MiB| unset | 137 | | | |38347_092cc73601c78e45f4f9_56_QF_UFNIA.smt2 | 25.623s | 10.603GiB| unset | 137 | | | |41958_45c688a4814eb926c254_59_QF_UFLIA.smt2 | 25.738s | 7700.0MiB| unset | 137 | | | |66603_accdadf23a1cf70ae043_72_QF_UFNIA.smt2 | 26.524s | 755.0MiB| unsat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFNIA.smt2 | 27.644s | 8977.0MiB| unset | 137 | | | |39657_2866defdd1f2434b69ab_47_QF_UFNIA.smt2 | 27.803s | 585.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFNIA.smt2 | 27.966s | 247.0MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFNIA.smt2 | 28.528s | 8309.0MiB| unset | 137 | | | |66603_accdadf23a1cf70ae043_76_QF_UFLIA.smt2 | 28.707s | 1877.0MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFNIA.smt2 | 30.012s | 7031.0MiB| unset | 137 | | | |72771_f9d228efc97cf1458e38_64_QF_UFNIA.smt2 | 30.049s | 9259.0MiB| unset | 137 | | | |83314_a702bf8b823398c9e37a_2_UFNIA.smt2 | 30.770s | 7140.0MiB| unset | 137 | | | |3106_1c933134166dbad31f79_39_QF_UFLIA.smt2 | 31.006s | 5882.0MiB| unset | 137 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTLIA.smt2 | 33.323s | 356.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFNIA.smt2 | 33.409s | 585.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFLIA.smt2 | 34.628s | 649.0MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFNIA.smt2 | 35.419s | 11.466GiB| unset | 137 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFNIA.smt2 | 35.474s | 12.923GiB| unset | 137 | | | |44289_4066055e0f64d96da11a_14_QF_UFNIA.smt2 | 35.533s | 8865.0MiB| unset | 137 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFNIA.smt2 | 36.077s | 7199.0MiB| unset | 137 | | | |83314_a702bf8b823398c9e37a_4_UFNIA.smt2 | 37.123s | 6481.0MiB| unset | 137 | | | |83314_a702bf8b823398c9e37a_3_UFDTNIA.smt2 | 40.629s | 232.0MiB| unsat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFNIA.smt2 | 40.809s | 6061.0MiB| unset | 137 | | | |30078_f817a923328f75af7e60_28_QF_UFLIA.smt2 | 40.993s | 645.0MiB| unsat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFLIA.smt2 | 41.322s | 6385.0MiB| unset | 137 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFNIA.smt2 | 42.096s | 15.516GiB| unset | 137 | | | |39657_1c7158801cd59dc13f05_45_QF_UFLIA.smt2 | 42.572s | 519.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTLIA.smt2 | 42.737s | 10.507GiB| unset | 137 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTNIA.smt2 | 44.368s | 191.0MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFLIA.smt2 | 44.400s | 10.968GiB| unset | 137 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTNIA.smt2 | 45.075s | 6146.0MiB| unset | 137 | | | |940_590f27b1c3c800d3243e_32_QF_UFNIA.smt2 | 45.088s | 12.527GiB| unset | 137 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTNIA.smt2 | 47.514s | 664.0MiB| timeout | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFNIA.smt2 | 48.387s | 9610.0MiB| unset | 137 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFLIA.smt2 | 48.754s | 8252.0MiB| unset | 137 | | | |940_590f27b1c3c800d3243e_32_QF_UFLIA.smt2 | 48.781s | 493.0MiB| timeout | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFNIA.smt2 | 50.016s | 13.339GiB| unset | 137 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFNIA.smt2 | 54.154s | 6310.0MiB| unset | 137 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFNIA.smt2 | 54.962s | 1826.0MiB| timeout | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTNIA.smt2 | 55.789s | 1031.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFLIA.smt2 | 55.870s | 803.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTNIA.smt2 | 55.940s | 190.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFLIA.smt2 | 56.144s | 746.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFLIA.smt2 | 56.605s | 1059.0MiB| timeout | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTNIA.smt2 | 56.688s | 247.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTNIA.smt2 | 56.753s | 203.0MiB| timeout | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFNIA.smt2 | 56.860s | 623.0MiB| timeout | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTLIA.smt2 | 56.882s | 1002.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTNIA.smt2 | 57.010s | 223.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFLIA.smt2 | 57.029s | 1528.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTLIA.smt2 | 57.049s | 1041.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_0_UFLIA.smt2 | 57.165s | 779.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTLIA.smt2 | 57.219s | 443.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFLIA.smt2 | 57.275s | 718.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTLIA.smt2 | 57.393s | 890.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFNIA.smt2 | 57.399s | 1042.0MiB| timeout | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFLIA.smt2 | 57.457s | 10.528GiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFLIA.smt2 | 57.464s | 832.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFLIA.smt2 | 57.517s | 209.0MiB| timeout | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFLIA.smt2 | 57.550s | 593.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFNIA.smt2 | 57.552s | 4844.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFLIA.smt2 | 57.575s | 461.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFNIA.smt2 | 57.645s | 878.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFLIA.smt2 | 57.659s | 629.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFNIA.smt2 | 57.665s | 846.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTNIA.smt2 | 57.731s | 233.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTNIA.smt2 | 57.757s | 188.0MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFNIA.smt2 | 57.759s | 949.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTLIA.smt2 | 57.760s | 2105.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTLIA.smt2 | 57.806s | 759.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFNIA.smt2 | 57.817s | 350.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFNIA.smt2 | 57.840s | 881.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTLIA.smt2 | 57.852s | 459.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTLIA.smt2 | 57.881s | 1562.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTNIA.smt2 | 57.896s | 190.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTNIA.smt2 | 57.905s | 198.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTNIA.smt2 | 57.915s | 342.0MiB| timeout | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFLIA.smt2 | 57.934s | 1367.0MiB| timeout | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFNIA.smt2 | 57.943s | 92.516MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFNIA.smt2 | 57.949s | 848.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFLIA.smt2 | 57.963s | 8731.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTLIA.smt2 | 58.023s | 576.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTNIA.smt2 | 58.031s | 798.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFLIA.smt2 | 58.036s | 535.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTLIA.smt2 | 58.043s | 190.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTNIA.smt2 | 58.057s | 610.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFNIA.smt2 | 58.079s | 1253.0MiB| timeout | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFNIA.smt2 | 58.088s | 664.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFNIA.smt2 | 58.121s | 232.0MiB| timeout | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFNIA.smt2 | 58.174s | 8109.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFLIA.smt2 | 58.185s | 755.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFNIA.smt2 | 58.190s | 186.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTNIA.smt2 | 58.197s | 315.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFLIA.smt2 | 58.211s | 473.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFLIA.smt2 | 58.218s | 552.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTNIA.smt2 | 58.251s | 194.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTLIA.smt2 | 58.266s | 1894.0MiB| timeout | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFLIA.smt2 | 58.292s | 3314.0MiB| timeout | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTNIA.smt2 | 58.298s | 252.0MiB| timeout | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFLIA.smt2 | 58.305s | 1214.0MiB| timeout | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFLIA.smt2 | 58.349s | 284.0MiB| timeout | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTNIA.smt2 | 58.367s | 1079.0MiB| timeout | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFNIA.smt2 | 58.368s | 5954.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTNIA.smt2 | 58.377s | 931.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFNIA.smt2 | 58.389s | 269.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTNIA.smt2 | 58.444s | 301.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTNIA.smt2 | 58.477s | 438.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFLIA.smt2 | 58.484s | 390.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTLIA.smt2 | 58.486s | 929.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTNIA.smt2 | 58.492s | 2822.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFLIA.smt2 | 58.498s | 532.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFLIA.smt2 | 58.551s | 264.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTNIA.smt2 | 58.575s | 4261.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTNIA.smt2 | 58.578s | 393.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFLIA.smt2 | 58.588s | 695.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFNIA.smt2 | 58.589s | 4821.0MiB| timeout | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFLIA.smt2 | 58.593s | 657.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTNIA.smt2 | 58.607s | 429.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTNIA.smt2 | 58.622s | 196.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTLIA.smt2 | 58.683s | 978.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTNIA.smt2 | 58.685s | 1126.0MiB| timeout | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTLIA.smt2 | 58.696s | 2688.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTLIA.smt2 | 58.739s | 648.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFLIA.smt2 | 58.742s | 374.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFLIA.smt2 | 58.749s | 702.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTLIA.smt2 | 58.768s | 561.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTLIA.smt2 | 58.769s | 7487.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTLIA.smt2 | 58.782s | 592.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFNIA.smt2 | 58.807s | 197.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTNIA.smt2 | 58.807s | 859.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFLIA.smt2 | 58.814s | 221.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTNIA.smt2 | 58.844s | 991.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFLIA.smt2 | 58.865s | 2105.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTNIA.smt2 | 58.909s | 2419.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFNIA.smt2 | 58.919s | 225.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTLIA.smt2 | 58.922s | 838.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFLIA.smt2 | 58.924s | 3038.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFNIA.smt2 | 58.971s | 1711.0MiB| timeout | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTNIA.smt2 | 59.016s | 3530.0MiB| timeout | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFNIA.smt2 | 59.045s | 5537.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTLIA.smt2 | 59.047s | 190.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTNIA.smt2 | 59.063s | 185.0MiB| timeout | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFNIA.smt2 | 59.091s | 927.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFLIA.smt2 | 59.130s | 502.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTLIA.smt2 | 59.164s | 857.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTNIA.smt2 | 59.168s | 595.0MiB| timeout | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFLIA.smt2 | 59.198s | 10.171GiB| timeout | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFNIA.smt2 | 59.205s | 225.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFLIA.smt2 | 59.242s | 2236.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFNIA.smt2 | 59.247s | 439.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTNIA.smt2 | 59.279s | 441.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFNIA.smt2 | 59.287s | 9033.0MiB| unset | 137 | | | |940_590f27b1c3c800d3243e_31_QF_UFLIA.smt2 | 59.293s | 4957.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFNIA.smt2 | 59.293s | 4471.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTNIA.smt2 | 59.310s | 303.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFNIA.smt2 | 59.378s | 521.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFNIA.smt2 | 59.393s | 1277.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFLIA.smt2 | 59.394s | 1708.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFLIA.smt2 | 59.394s | 1024.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTNIA.smt2 | 59.422s | 239.0MiB| timeout | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFLIA.smt2 | 59.479s | 4191.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTLIA.smt2 | 59.637s | 9116.0MiB| timeout | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFNIA.smt2 | 59.653s | 5635.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFNIA.smt2 | 59.671s | 254.0MiB| timeout | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFNIA.smt2 | 59.808s | 7438.0MiB| timeout | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFLIA.smt2 | 59.831s | 1315.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTLIA.smt2 | 59.871s | 599.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTNIA.smt2 | 59.932s | 193.0MiB| timeout | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFLIA.smt2 | 60.002s | 458.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTLIA.smt2 | 60.027s | 2256.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTLIA.smt2 | 60.042s | 474.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFLIA.smt2 | 60.069s | 956.0MiB| timeout | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFNIA.smt2 | 60.342s | 19.225GiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTLIA.smt2 | 61.448s | 15.074GiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFLIA.smt2 | 61.859s | 8961.0MiB| timeout | 0 | | |