# . * SAT 161 * UNSAT 44 * TIMEOUT 103 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: dio_certora_no_gcd
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: 7ee34151501242638597e0af7e4c3e1cd5934046
Z3 branch: 
Z3 options: "-T:600 -st lp.dio=true lp.dio_run_gcd=false"
Z3 inputs: inputs/certora
Z3 commit message: make gcd call in dio optional

Signed-off-by: Lev Nachmanson
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |65782_cd31513fdcd15701933b_6_QF_UFDTLIA.smt2 | 0.111s | 21.492MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFNIA.smt2 | 0.111s | 21.028MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFLIA.smt2 | 0.143s | 23.608MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFDTNIA.smt2 | 0.162s | 21.016MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTLIA.smt2 | 0.166s | 23.432MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFNIA.smt2 | 0.167s | 23.076MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFLIA.smt2 | 0.178s | 21.676MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTNIA.smt2 | 0.199s | 22.788MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTLIA.smt2 | 0.224s | 23.24MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFLIA.smt2 | 0.236s | 23.736MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFLIA.smt2 | 0.238s | 25.4MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTNIA.smt2 | 0.257s | 26.052MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTNIA.smt2 | 0.264s | 27.292MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTNIA.smt2 | 0.271s | 23.956MiB| unsat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTLIA.smt2 | 0.272s | 24.54MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFNIA.smt2 | 0.276s | 23.512MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFLIA.smt2 | 0.369s | 25.548MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTNIA.smt2 | 0.395s | 28.336MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTLIA.smt2 | 0.505s | 25.744MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTLIA.smt2 | 0.523s | 33.304MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTLIA.smt2 | 0.543s | 25.204MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFNIA.smt2 | 0.568s | 25.32MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFLIA.smt2 | 0.591s | 26.432MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTLIA.smt2 | 0.658s | 27.704MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTNIA.smt2 | 0.669s | 26.472MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTLIA.smt2 | 0.718s | 30.328MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTNIA.smt2 | 0.722s | 28.988MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFNIA.smt2 | 0.744s | 24.908MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTNIA.smt2 | 0.805s | 30.216MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTNIA.smt2 | 0.820s | 25.808MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTLIA.smt2 | 0.830s | 26.38MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTLIA.smt2 | 0.875s | 34.024MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTNIA.smt2 | 0.948s | 28.532MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTLIA.smt2 | 1.029s | 32.936MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFNIA.smt2 | 1.031s | 27.376MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFLIA.smt2 | 1.112s | 33.908MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFNIA.smt2 | 1.224s | 23.052MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTNIA.smt2 | 1.353s | 27.224MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTLIA.smt2 | 1.460s | 36.096MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFNIA.smt2 | 1.469s | 37.44MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTNIA.smt2 | 1.589s | 22.888MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTNIA.smt2 | 1.598s | 27.32MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTLIA.smt2 | 1.608s | 35.92MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTNIA.smt2 | 1.669s | 24.956MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFLIA.smt2 | 1.694s | 35.744MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFNIA.smt2 | 1.708s | 30.752MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTLIA.smt2 | 2.034s | 55.048MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTNIA.smt2 | 2.136s | 41.5MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFLIA.smt2 | 2.402s | 39.736MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTNIA.smt2 | 2.476s | 55.516MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFLIA.smt2 | 2.560s | 30.884MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTLIA.smt2 | 2.641s | 50.676MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTLIA.smt2 | 2.846s | 57.54MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTLIA.smt2 | 3.121s | 47.376MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTNIA.smt2 | 3.326s | 57.348MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTLIA.smt2 | 3.363s | 42.74MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTLIA.smt2 | 3.425s | 57.644MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTNIA.smt2 | 3.559s | 42.884MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFNIA.smt2 | 3.571s | 45.436MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTNIA.smt2 | 3.848s | 26.732MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTNIA.smt2 | 3.869s | 46.428MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFNIA.smt2 | 3.933s | 29.976MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTNIA.smt2 | 3.982s | 61.992MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTLIA.smt2 | 4.046s | 37.58MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTNIA.smt2 | 4.080s | 58.644MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFNIA.smt2 | 4.109s | 23.924MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTLIA.smt2 | 4.136s | 50.668MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTLIA.smt2 | 4.142s | 28.456MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTLIA.smt2 | 4.195s | 44.616MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTNIA.smt2 | 4.565s | 35.988MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTLIA.smt2 | 4.635s | 52.0MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFLIA.smt2 | 4.948s | 49.392MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTLIA.smt2 | 5.005s | 65.3MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTNIA.smt2 | 5.283s | 102.0MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTLIA.smt2 | 5.486s | 65.98MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFNIA.smt2 | 5.616s | 26.108MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTNIA.smt2 | 5.729s | 30.532MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFNIA.smt2 | 5.931s | 62.8MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTLIA.smt2 | 6.052s | 29.572MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFNIA.smt2 | 6.206s | 33.92MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTNIA.smt2 | 6.465s | 78.584MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFLIA.smt2 | 6.792s | 32.9MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFNIA.smt2 | 6.828s | 44.04MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTLIA.smt2 | 7.018s | 104.0MiB| unsat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTLIA.smt2 | 7.211s | 29.936MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTLIA.smt2 | 7.525s | 32.128MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTNIA.smt2 | 8.042s | 95.672MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTNIA.smt2 | 8.183s | 51.08MiB| sat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFNIA.smt2 | 8.282s | 31.26MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTNIA.smt2 | 8.313s | 47.496MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFLIA.smt2 | 8.353s | 57.564MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFLIA.smt2 | 8.850s | 37.544MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTNIA.smt2 | 8.868s | 25.42MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFLIA.smt2 | 9.041s | 48.832MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTNIA.smt2 | 9.502s | 43.812MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFNIA.smt2 | 9.781s | 67.204MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTLIA.smt2 | 9.790s | 84.508MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTLIA.smt2 | 10.065s | 81.544MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFNIA.smt2 | 10.097s | 28.864MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTLIA.smt2 | 10.428s | 67.32MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFNIA.smt2 | 11.588s | 44.792MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFLIA.smt2 | 12.027s | 72.244MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTNIA.smt2 | 12.164s | 58.148MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTNIA.smt2 | 12.416s | 72.384MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTNIA.smt2 | 12.502s | 26.832MiB| unsat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFNIA.smt2 | 13.962s | 91.32MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFLIA.smt2 | 14.990s | 87.44MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTLIA.smt2 | 15.216s | 66.676MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTNIA.smt2 | 15.411s | 77.484MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTLIA.smt2 | 16.243s | 126.0MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFLIA.smt2 | 16.845s | 73.272MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFLIA.smt2 | 17.868s | 85.576MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFNIA.smt2 | 18.041s | 33.884MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTLIA.smt2 | 20.913s | 83.236MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFNIA.smt2 | 21.253s | 102.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTLIA.smt2 | 21.811s | 122.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFLIA.smt2 | 21.845s | 89.28MiB| sat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTLIA.smt2 | 22.846s | 51.148MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTNIA.smt2 | 24.500s | 54.344MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTNIA.smt2 | 24.508s | 142.0MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTLIA.smt2 | 25.280s | 229.0MiB| unsat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFLIA.smt2 | 26.448s | 90.108MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTLIA.smt2 | 27.352s | 80.156MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFLIA.smt2 | 27.791s | 62.004MiB| sat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFLIA.smt2 | 27.937s | 46.308MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTLIA.smt2 | 28.002s | 126.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFLIA.smt2 | 29.575s | 98.0MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFLIA.smt2 | 29.793s | 47.064MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTNIA.smt2 | 30.189s | 46.204MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTNIA.smt2 | 30.474s | 135.0MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFNIA.smt2 | 33.480s | 41.116MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTNIA.smt2 | 34.133s | 27.704MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFNIA.smt2 | 34.687s | 34.624MiB| unsat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTLIA.smt2 | 37.069s | 79.916MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFNIA.smt2 | 38.937s | 54.06MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTNIA.smt2 | 39.489s | 36.752MiB| unsat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFLIA.smt2 | 40.074s | 284.0MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTNIA.smt2 | 40.085s | 57.32MiB| sat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTLIA.smt2 | 40.529s | 78.372MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFNIA.smt2 | 45.513s | 188.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFNIA.smt2 | 47.039s | 90.024MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFLIA.smt2 | 47.093s | 117.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFLIA.smt2 | 49.925s | 532.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFLIA.smt2 | 50.031s | 149.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFNIA.smt2 | 51.901s | 156.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFLIA.smt2 | 52.155s | 162.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFNIA.smt2 | 55.233s | 147.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFNIA.smt2 | 55.714s | 236.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFLIA.smt2 | 56.017s | 148.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTNIA.smt2 | 57.607s | 129.0MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTNIA.smt2 | 60.892s | 37.544MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTLIA.smt2 | 61.690s | 147.0MiB| unsat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFNIA.smt2 | 65.023s | 245.0MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTNIA.smt2 | 67.385s | 89.744MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFNIA.smt2 | 68.659s | 120.0MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFLIA.smt2 | 75.278s | 45.272MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTNIA.smt2 | 78.359s | 195.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTLIA.smt2 | 81.530s | 50.38MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTNIA.smt2 | 81.842s | 170.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFLIA.smt2 | 82.119s | 192.0MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFNIA.smt2 | 84.686s | 157.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2 | 87.767s | 193.0MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTNIA.smt2 | 89.296s | 184.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTNIA.smt2 | 90.140s | 138.0MiB| unsat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFLIA.smt2 | 91.293s | 193.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFLIA.smt2 | 93.669s | 79.58MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFNIA.smt2 | 100.488s | 49.816MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFNIA.smt2 | 104.180s | 267.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFLIA.smt2 | 106.709s | 1714.0MiB| unsat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTNIA.smt2 | 109.209s | 88.424MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFNIA.smt2 | 109.989s | 186.0MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTNIA.smt2 | 111.893s | 71.96MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTLIA.smt2 | 114.082s | 158.0MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFLIA.smt2 | 116.866s | 121.0MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFNIA.smt2 | 117.184s | 69.168MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFNIA.smt2 | 121.503s | 242.0MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTLIA.smt2 | 131.241s | 142.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFNIA.smt2 | 138.500s | 416.0MiB| unsat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFNIA.smt2 | 146.736s | 121.0MiB| sat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFNIA.smt2 | 149.010s | 162.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFNIA.smt2 | 151.574s | 64.844MiB| sat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTNIA.smt2 | 158.497s | 136.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFNIA.smt2 | 168.948s | 166.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFLIA.smt2 | 171.786s | 459.0MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTLIA.smt2 | 175.801s | 117.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTLIA.smt2 | 187.485s | 25.176MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFNIA.smt2 | 226.418s | 184.0MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTNIA.smt2 | 233.994s | 43.672MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTNIA.smt2 | 241.489s | 171.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFNIA.smt2 | 243.478s | 431.0MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFNIA.smt2 | 250.729s | 139.0MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTNIA.smt2 | 253.635s | 122.0MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTLIA.smt2 | 259.491s | 418.0MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFNIA.smt2 | 272.326s | 120.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTNIA.smt2 | 277.004s | 271.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFLIA.smt2 | 309.522s | 476.0MiB| unsat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFNIA.smt2 | 351.355s | 596.0MiB| sat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTLIA.smt2 | 378.138s | 241.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFLIA.smt2 | 400.053s | 188.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFNIA.smt2 | 439.753s | 138.0MiB| sat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFNIA.smt2 | 445.475s | 386.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTNIA.smt2 | 476.967s | 110.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFNIA.smt2 | 486.088s | 127.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTLIA.smt2 | 511.982s | 851.0MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFNIA.smt2 | 573.796s | 588.0MiB| unsat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTNIA.smt2 | 596.903s | 108.0MiB| timeout | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFLIA.smt2 | 599.097s | 345.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTNIA.smt2 | 599.131s | 59.912MiB| timeout | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFLIA.smt2 | 599.163s | 200.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFLIA.smt2 | 599.217s | 792.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTLIA.smt2 | 599.245s | 795.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFNIA.smt2 | 599.256s | 81.436MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTLIA.smt2 | 599.262s | 451.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTLIA.smt2 | 599.289s | 332.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTLIA.smt2 | 599.336s | 714.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFLIA.smt2 | 599.345s | 240.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTLIA.smt2 | 599.359s | 259.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFLIA.smt2 | 599.372s | 397.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTLIA.smt2 | 599.389s | 244.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTLIA.smt2 | 599.391s | 744.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTNIA.smt2 | 599.425s | 106.0MiB| timeout | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFLIA.smt2 | 599.426s | 605.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTNIA.smt2 | 599.438s | 138.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTLIA.smt2 | 599.441s | 1216.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTLIA.smt2 | 599.443s | 336.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFNIA.smt2 | 599.445s | 333.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFLIA.smt2 | 599.454s | 296.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFNIA.smt2 | 599.464s | 132.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTNIA.smt2 | 599.464s | 62.432MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTLIA.smt2 | 599.468s | 412.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFLIA.smt2 | 599.469s | 928.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTLIA.smt2 | 599.493s | 235.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFLIA.smt2 | 599.493s | 183.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTLIA.smt2 | 599.495s | 288.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTNIA.smt2 | 599.497s | 49.112MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFLIA.smt2 | 599.499s | 64.972MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTNIA.smt2 | 599.499s | 318.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFNIA.smt2 | 599.512s | 131.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTLIA.smt2 | 599.515s | 327.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTLIA.smt2 | 599.519s | 211.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTLIA.smt2 | 599.525s | 2112.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFNIA.smt2 | 599.542s | 704.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFNIA.smt2 | 599.543s | 51.024MiB| timeout | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTNIA.smt2 | 599.553s | 288.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFNIA.smt2 | 599.556s | 632.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTNIA.smt2 | 599.567s | 236.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFLIA.smt2 | 599.568s | 374.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTNIA.smt2 | 599.578s | 119.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFLIA.smt2 | 599.580s | 607.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFNIA.smt2 | 599.587s | 32.548MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFLIA.smt2 | 599.587s | 200.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTNIA.smt2 | 599.598s | 259.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFLIA.smt2 | 599.601s | 601.0MiB| timeout | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFLIA.smt2 | 599.602s | 169.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFLIA.smt2 | 599.604s | 234.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFNIA.smt2 | 599.604s | 683.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFLIA.smt2 | 599.608s | 44.756MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTNIA.smt2 | 599.610s | 212.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFNIA.smt2 | 599.611s | 262.0MiB| timeout | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFNIA.smt2 | 599.611s | 309.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFNIA.smt2 | 599.614s | 344.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFLIA.smt2 | 599.616s | 732.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTLIA.smt2 | 599.617s | 461.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTNIA.smt2 | 599.627s | 95.648MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFNIA.smt2 | 599.632s | 100.0MiB| timeout | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFLIA.smt2 | 599.634s | 262.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFLIA.smt2 | 599.635s | 384.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFLIA.smt2 | 599.639s | 673.0MiB| timeout | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFNIA.smt2 | 599.640s | 224.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFNIA.smt2 | 599.675s | 93.204MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFLIA.smt2 | 599.676s | 397.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFLIA.smt2 | 599.685s | 272.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFLIA.smt2 | 599.686s | 581.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFNIA.smt2 | 599.691s | 61.568MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFLIA.smt2 | 599.696s | 438.0MiB| timeout | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFLIA.smt2 | 599.705s | 154.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTNIA.smt2 | 599.708s | 467.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFLIA.smt2 | 599.708s | 147.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTNIA.smt2 | 599.714s | 34.132MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFNIA.smt2 | 599.714s | 234.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTLIA.smt2 | 599.716s | 1418.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFNIA.smt2 | 599.719s | 320.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFNIA.smt2 | 599.721s | 371.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTNIA.smt2 | 599.724s | 84.536MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTLIA.smt2 | 599.732s | 919.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFLIA.smt2 | 599.738s | 1155.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTNIA.smt2 | 599.741s | 192.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTLIA.smt2 | 599.747s | 622.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTNIA.smt2 | 599.747s | 26.288MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFLIA.smt2 | 599.753s | 291.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFNIA.smt2 | 599.757s | 58.004MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTNIA.smt2 | 599.760s | 77.46MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTLIA.smt2 | 599.762s | 354.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFLIA.smt2 | 599.763s | 1229.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFLIA.smt2 | 599.767s | 543.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFNIA.smt2 | 599.773s | 82.392MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFLIA.smt2 | 599.775s | 439.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFLIA.smt2 | 599.785s | 329.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTLIA.smt2 | 599.787s | 678.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFLIA.smt2 | 599.802s | 802.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFNIA.smt2 | 599.823s | 640.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFNIA.smt2 | 599.830s | 1545.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTLIA.smt2 | 599.839s | 32.324MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTLIA.smt2 | 599.848s | 2056.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFNIA.smt2 | 599.886s | 967.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFLIA.smt2 | 599.890s | 1343.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFLIA.smt2 | 599.897s | 2217.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFLIA.smt2 | 600.010s | 2249.0MiB| timeout | 0 | | |