# . * SAT 159 * UNSAT 42 * TIMEOUT 106 * UNKNOWN 0 * UNSET 1 * ERROR 1 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: dio_certora_no_gcd_if_no_ignored_terms
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: 7e88064da96d8fb914a7be50776e5e9ed363bad2
Z3 branch: 
Z3 options: "-T:600 -st lp.dio=true lp.dio_run_gcd=false"
Z3 inputs: inputs/certora
Z3 commit message: allow gcd when dio ignores some terms

Signed-off-by: Lev Nachmanson
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |65782_cd31513fdcd15701933b_6_QF_UFDTLIA.smt2 | 0.102s | 21.488MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFNIA.smt2 | 0.120s | 20.88MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFLIA.smt2 | 0.140s | 21.536MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFLIA.smt2 | 0.140s | 23.772MiB| unsat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTLIA.smt2 | 0.152s | 23.252MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTLIA.smt2 | 0.178s | 24.548MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTNIA.smt2 | 0.208s | 22.788MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFNIA.smt2 | 0.225s | 23.12MiB| unsat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTNIA.smt2 | 0.225s | 24.048MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTLIA.smt2 | 0.228s | 23.236MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFLIA.smt2 | 0.248s | 23.824MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFDTNIA.smt2 | 0.255s | 20.82MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTNIA.smt2 | 0.258s | 27.256MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFLIA.smt2 | 0.259s | 25.4MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTNIA.smt2 | 0.289s | 26.052MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFNIA.smt2 | 0.355s | 23.54MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFLIA.smt2 | 0.363s | 25.42MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTLIA.smt2 | 0.440s | 25.3MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTNIA.smt2 | 0.495s | 26.468MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTNIA.smt2 | 0.521s | 30.112MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTLIA.smt2 | 0.567s | 25.74MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFLIA.smt2 | 0.567s | 26.332MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTLIA.smt2 | 0.567s | 33.332MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTNIA.smt2 | 0.569s | 28.328MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFNIA.smt2 | 0.588s | 25.484MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTLIA.smt2 | 0.688s | 30.344MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTNIA.smt2 | 0.841s | 28.996MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTLIA.smt2 | 0.850s | 26.496MiB| unsat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFNIA.smt2 | 0.936s | 23.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTLIA.smt2 | 0.947s | 27.572MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTLIA.smt2 | 0.958s | 32.96MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTNIA.smt2 | 0.995s | 28.56MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFNIA.smt2 | 1.120s | 24.832MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTNIA.smt2 | 1.189s | 27.396MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFNIA.smt2 | 1.196s | 27.34MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTLIA.smt2 | 1.261s | 34.204MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFLIA.smt2 | 1.390s | 33.992MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFNIA.smt2 | 1.394s | 37.436MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTNIA.smt2 | 1.399s | 26.74MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTLIA.smt2 | 1.507s | 36.068MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTNIA.smt2 | 1.508s | 22.856MiB| unsat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTNIA.smt2 | 1.524s | 26.54MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFNIA.smt2 | 1.548s | 30.712MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTNIA.smt2 | 1.568s | 27.332MiB| unsat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTLIA.smt2 | 1.791s | 54.88MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTLIA.smt2 | 1.841s | 36.028MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTNIA.smt2 | 2.052s | 41.616MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFLIA.smt2 | 2.423s | 39.688MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTNIA.smt2 | 2.538s | 55.568MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTLIA.smt2 | 2.657s | 57.74MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTLIA.smt2 | 2.715s | 28.584MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTLIA.smt2 | 2.920s | 50.664MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTLIA.smt2 | 2.991s | 42.7MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFLIA.smt2 | 3.239s | 31.104MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTLIA.smt2 | 3.243s | 47.46MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFLIA.smt2 | 3.411s | 35.776MiB| unsat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFNIA.smt2 | 3.565s | 45.488MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTNIA.smt2 | 3.574s | 25.032MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTLIA.smt2 | 3.634s | 51.908MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTLIA.smt2 | 3.638s | 32.408MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTLIA.smt2 | 3.734s | 37.56MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTNIA.smt2 | 3.852s | 42.94MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFNIA.smt2 | 4.074s | 29.988MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTLIA.smt2 | 4.077s | 50.476MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTNIA.smt2 | 4.211s | 26.988MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTNIA.smt2 | 4.252s | 46.492MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTNIA.smt2 | 4.279s | 58.54MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFNIA.smt2 | 4.618s | 23.88MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTLIA.smt2 | 4.773s | 65.1MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTLIA.smt2 | 4.774s | 44.652MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTNIA.smt2 | 4.976s | 57.448MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTNIA.smt2 | 5.126s | 36.028MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTNIA.smt2 | 5.313s | 62.184MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFNIA.smt2 | 5.390s | 26.152MiB| unsat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFLIA.smt2 | 5.546s | 49.572MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTLIA.smt2 | 5.817s | 29.564MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTLIA.smt2 | 5.855s | 66.056MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTNIA.smt2 | 5.958s | 103.0MiB| unsat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFNIA.smt2 | 6.084s | 62.828MiB| sat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTNIA.smt2 | 6.160s | 30.476MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTLIA.smt2 | 6.164s | 29.9MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFLIA.smt2 | 6.660s | 32.716MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTLIA.smt2 | 6.800s | 104.0MiB| unsat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTNIA.smt2 | 6.815s | 78.704MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTNIA.smt2 | 7.113s | 43.972MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTNIA.smt2 | 7.922s | 95.76MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTNIA.smt2 | 9.436s | 25.632MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFLIA.smt2 | 9.499s | 72.212MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFNIA.smt2 | 9.662s | 67.028MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTLIA.smt2 | 9.718s | 81.464MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFLIA.smt2 | 9.987s | 37.628MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFNIA.smt2 | 10.266s | 44.82MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTNIA.smt2 | 10.441s | 47.564MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTLIA.smt2 | 10.736s | 67.336MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTLIA.smt2 | 10.955s | 57.528MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFNIA.smt2 | 11.454s | 28.86MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTNIA.smt2 | 11.943s | 27.048MiB| unsat | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTLIA.smt2 | 11.985s | 23.216MiB| unsat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTNIA.smt2 | 12.180s | 51.264MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFLIA.smt2 | 12.211s | 58.92MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTLIA.smt2 | 12.995s | 126.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFLIA.smt2 | 13.129s | 48.92MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFNIA.smt2 | 14.606s | 90.112MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTNIA.smt2 | 14.816s | 72.168MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTLIA.smt2 | 15.052s | 84.368MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTNIA.smt2 | 15.296s | 58.172MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFLIA.smt2 | 16.478s | 85.608MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFLIA.smt2 | 16.583s | 73.024MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFNIA.smt2 | 16.744s | 38.768MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFLIA.smt2 | 17.008s | 87.596MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTLIA.smt2 | 17.575s | 66.824MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTNIA.smt2 | 17.768s | 77.432MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFLIA.smt2 | 18.676s | 60.992MiB| sat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTLIA.smt2 | 18.887s | 51.304MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFLIA.smt2 | 19.170s | 89.532MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFNIA.smt2 | 19.655s | 102.0MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFNIA.smt2 | 20.180s | 33.924MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTLIA.smt2 | 21.216s | 83.228MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFNIA.smt2 | 21.795s | 47.924MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTLIA.smt2 | 22.385s | 80.18MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFLIA.smt2 | 22.909s | 98.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTNIA.smt2 | 23.270s | 142.0MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFLIA.smt2 | 24.254s | 46.52MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFLIA.smt2 | 25.657s | 46.972MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFLIA.smt2 | 26.499s | 89.936MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFLIA.smt2 | 26.839s | 532.0MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTLIA.smt2 | 29.023s | 123.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFNIA.smt2 | 30.830s | 33.016MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTNIA.smt2 | 31.246s | 54.356MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTNIA.smt2 | 33.813s | 53.748MiB| unset | 139 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTLIA.smt2 | 34.358s | 229.0MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTNIA.smt2 | 34.745s | 27.704MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFNIA.smt2 | 34.909s | 34.66MiB| unsat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTLIA.smt2 | 35.887s | 79.932MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFNIA.smt2 | 37.210s | 60.792MiB| sat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTLIA.smt2 | 38.928s | 78.44MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTLIA.smt2 | 39.071s | 50.424MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFNIA.smt2 | 42.555s | 188.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTLIA.smt2 | 44.292s | 126.0MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFLIA.smt2 | 45.605s | 284.0MiB| unsat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFLIA.smt2 | 46.961s | 117.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFLIA.smt2 | 47.423s | 149.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTNIA.smt2 | 48.338s | 57.104MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTNIA.smt2 | 49.167s | 137.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTNIA.smt2 | 51.007s | 129.0MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFNIA.smt2 | 51.725s | 236.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTLIA.smt2 | 52.617s | 147.0MiB| unsat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFNIA.smt2 | 52.681s | 261.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFLIA.smt2 | 52.827s | 162.0MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTNIA.smt2 | 53.056s | 36.9MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTNIA.smt2 | 53.640s | 170.0MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTNIA.smt2 | 55.746s | 36.804MiB| unsat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFNIA.smt2 | 56.777s | 108.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFNIA.smt2 | 58.402s | 89.82MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFNIA.smt2 | 60.675s | 157.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTNIA.smt2 | 61.057s | 45.924MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFNIA.smt2 | 64.625s | 41.292MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTNIA.smt2 | 66.576s | 135.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTNIA.smt2 | 66.867s | 184.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFLIA.smt2 | 67.570s | 148.0MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFLIA.smt2 | 68.233s | 45.528MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTNIA.smt2 | 68.539s | 138.0MiB| unsat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTNIA.smt2 | 71.193s | 88.3MiB| unsat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFNIA.smt2 | 75.981s | 156.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFLIA.smt2 | 79.618s | 79.636MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFNIA.smt2 | 81.653s | 147.0MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTNIA.smt2 | 82.427s | 89.796MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFNIA.smt2 | 95.338s | 120.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTNIA.smt2 | 102.353s | 195.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFNIA.smt2 | 116.064s | 186.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2 | 119.924s | 193.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFNIA.smt2 | 120.456s | 416.0MiB| unsat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFNIA.smt2 | 122.040s | 162.0MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTNIA.smt2 | 127.552s | 72.08MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFLIA.smt2 | 129.831s | 122.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTLIA.smt2 | 132.578s | 158.0MiB| unsat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFLIA.smt2 | 136.907s | 193.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFLIA.smt2 | 149.348s | 1714.0MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFNIA.smt2 | 156.761s | 166.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFLIA.smt2 | 158.937s | 192.0MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTLIA.smt2 | 172.784s | 418.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFLIA.smt2 | 174.082s | 459.0MiB| unsat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFNIA.smt2 | 189.058s | 242.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFNIA.smt2 | 189.677s | 189.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFNIA.smt2 | 192.783s | 139.0MiB| sat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTNIA.smt2 | 195.760s | 136.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFNIA.smt2 | 221.081s | 431.0MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTLIA.smt2 | 247.168s | 117.0MiB| sat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTNIA.smt2 | 249.298s | 226.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTNIA.smt2 | 267.233s | 272.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFLIA.smt2 | 287.218s | 476.0MiB| unsat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTLIA.smt2 | 321.360s | 142.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFNIA.smt2 | 326.225s | 596.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFNIA.smt2 | 330.743s | 389.0MiB| sat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTLIA.smt2 | 350.813s | 241.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFNIA.smt2 | 370.295s | 120.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFNIA.smt2 | 433.773s | 127.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFNIA.smt2 | 434.540s | 138.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFLIA.smt2 | 481.326s | 189.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTLIA.smt2 | 524.106s | 851.0MiB| unsat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTNIA.smt2 | 546.728s | 138.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTNIA.smt2 | 567.963s | 110.0MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTNIA.smt2 | 596.540s | 99.14MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFNIA.smt2 | 597.044s | 52.484MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTNIA.smt2 | 598.869s | 292.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFLIA.smt2 | 598.872s | 205.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFLIA.smt2 | 598.929s | 769.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFLIA.smt2 | 599.086s | 344.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFNIA.smt2 | 599.108s | 640.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTNIA.smt2 | 599.137s | 171.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFLIA.smt2 | 599.238s | 2225.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFLIA.smt2 | 599.269s | 1241.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTLIA.smt2 | 599.316s | 232.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFLIA.smt2 | 599.332s | 1343.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFNIA.smt2 | 599.339s | 265.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTNIA.smt2 | 599.352s | 136.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFNIA.smt2 | 599.352s | 135.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTLIA.smt2 | 599.358s | 1418.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTLIA.smt2 | 599.365s | 208.0MiB| timeout | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFNIA.smt2 | 599.365s | 227.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFLIA.smt2 | 599.373s | 295.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTNIA.smt2 | 599.392s | 56.26MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFNIA.smt2 | 599.410s | 1545.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFNIA.smt2 | 599.417s | 120.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFLIA.smt2 | 599.420s | 621.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTLIA.smt2 | 599.423s | 407.0MiB| timeout | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFNIA.smt2 | 599.425s | 310.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTNIA.smt2 | 599.429s | 243.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFLIA.smt2 | 599.442s | 437.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTLIA.smt2 | 599.468s | 1170.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFNIA.smt2 | 599.476s | 368.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTLIA.smt2 | 599.480s | 761.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFLIA.smt2 | 599.489s | 225.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFNIA.smt2 | 599.492s | 36.664MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTLIA.smt2 | 599.494s | 339.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFLIA.smt2 | 599.499s | 388.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFNIA.smt2 | 599.500s | 332.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTNIA.smt2 | 599.514s | 184.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFLIA.smt2 | 599.518s | 675.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTLIA.smt2 | 599.520s | 590.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTLIA.smt2 | 599.530s | 665.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFNIA.smt2 | 599.533s | 110.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTLIA.smt2 | 599.540s | 336.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFLIA.smt2 | 599.551s | 44.044MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTLIA.smt2 | 599.568s | 394.0MiB| timeout | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFLIA.smt2 | 599.569s | 150.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFNIA.smt2 | 599.575s | 632.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFLIA.smt2 | 599.578s | 379.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTLIA.smt2 | 599.581s | 468.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTNIA.smt2 | 599.582s | 182.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFLIA.smt2 | 599.585s | 152.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFNIA.smt2 | 599.591s | 944.0MiB| timeout | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFNIA.smt2 | 599.593s | 406.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTNIA.smt2 | 599.596s | 187.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFNIA.smt2 | 599.599s | 121.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTLIA.smt2 | 599.610s | 2107.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTLIA.smt2 | 599.613s | 267.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFLIA.smt2 | 599.613s | 281.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFLIA.smt2 | 599.616s | 291.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFLIA.smt2 | 599.621s | 433.0MiB| timeout | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFLIA.smt2 | 599.628s | 169.0MiB| timeout | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFLIA.smt2 | 599.628s | 264.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFLIA.smt2 | 599.629s | 799.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTNIA.smt2 | 599.629s | 94.22MiB| timeout | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFLIA.smt2 | 599.629s | 356.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFLIA.smt2 | 599.630s | 581.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFNIA.smt2 | 599.636s | 100.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTLIA.smt2 | 599.638s | 370.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTLIA.smt2 | 599.642s | 931.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTNIA.smt2 | 599.643s | 102.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFLIA.smt2 | 599.648s | 708.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTNIA.smt2 | 599.649s | 31.928MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFNIA.smt2 | 599.650s | 313.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFNIA.smt2 | 599.651s | 86.4MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFNIA.smt2 | 599.651s | 77.788MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFNIA.smt2 | 599.657s | 704.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFLIA.smt2 | 599.665s | 2092.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFLIA.smt2 | 599.668s | 405.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTLIA.smt2 | 599.668s | 675.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFNIA.smt2 | 599.674s | 29.136MiB| timeout | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFLIA.smt2 | 599.674s | 209.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTNIA.smt2 | 599.675s | 50.304MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFLIA.smt2 | 599.676s | 60.168MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFLIA.smt2 | 599.682s | 548.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFNIA.smt2 | 599.684s | 798.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFLIA.smt2 | 599.691s | 764.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTNIA.smt2 | 599.699s | 114.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFLIA.smt2 | 599.704s | 274.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFNIA.smt2 | 599.707s | 367.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTLIA.smt2 | 599.708s | 263.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTLIA.smt2 | 599.714s | 788.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFNIA.smt2 | 599.722s | 52.06MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFNIA.smt2 | 599.726s | 98.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTLIA.smt2 | 599.728s | 33.636MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTLIA.smt2 | 599.744s | 1216.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTNIA.smt2 | 599.746s | 68.256MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFNIA.smt2 | 599.761s | 571.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFNIA.smt2 | 599.775s | 231.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFLIA.smt2 | 599.782s | 182.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFNIA.smt2 | 599.794s | 61.24MiB| timeout | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFLIA.smt2 | 599.802s | 639.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTLIA.smt2 | 599.804s | 261.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTLIA.smt2 | 599.805s | 485.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFLIA.smt2 | 599.806s | 264.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTNIA.smt2 | 599.829s | 467.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFLIA.smt2 | 599.832s | 950.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFLIA.smt2 | 599.838s | 1184.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTNIA.smt2 | 599.853s | 25.548MiB| timeout | 0 | | |