# . * SAT 163 * UNSAT 45 * TIMEOUT 99 * UNKNOWN 0 * UNSET 1 * ERROR 1 # Meta data 
Ramon benchmark for Z3
-
Job description: dio calls period = 4
Job tag: dio_calls_period_4_certora
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: d4ba75eb7965f81013c49e1716a17eacb01bbf3d
Z3 branch: 
Z3 options: "-T:600  -st lp.dio_eqs=true lp.dio_calls_period=4"
Z3 inputs: inputs/certora
Z3 commit message: add parameter m_dio_calls_period

Signed-off-by: Lev Nachmanson
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |65782_cd31513fdcd15701933b_6_QF_UFNIA.smt2 | 0.091s | 20.888MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFDTNIA.smt2 | 0.108s | 20.816MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFDTLIA.smt2 | 0.135s | 21.596MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFLIA.smt2 | 0.140s | 21.528MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFLIA.smt2 | 0.141s | 23.78MiB| unsat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTLIA.smt2 | 0.156s | 23.34MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTLIA.smt2 | 0.187s | 23.26MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTLIA.smt2 | 0.188s | 24.404MiB| unsat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTNIA.smt2 | 0.207s | 23.864MiB| unsat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFNIA.smt2 | 0.212s | 23.148MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTNIA.smt2 | 0.220s | 23.02MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFLIA.smt2 | 0.220s | 23.74MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFLIA.smt2 | 0.257s | 25.208MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFNIA.smt2 | 0.305s | 23.576MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTNIA.smt2 | 0.315s | 27.288MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTNIA.smt2 | 0.343s | 26.116MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFLIA.smt2 | 0.454s | 25.364MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTLIA.smt2 | 0.513s | 25.308MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTLIA.smt2 | 0.530s | 25.664MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTNIA.smt2 | 0.575s | 30.108MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTLIA.smt2 | 0.595s | 33.16MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFLIA.smt2 | 0.610s | 26.296MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTNIA.smt2 | 0.614s | 26.572MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFNIA.smt2 | 0.637s | 25.412MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTLIA.smt2 | 0.659s | 30.368MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTLIA.smt2 | 0.693s | 27.564MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFNIA.smt2 | 0.863s | 23.336MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTLIA.smt2 | 0.877s | 26.452MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFNIA.smt2 | 0.931s | 24.812MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTNIA.smt2 | 0.983s | 28.492MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTLIA.smt2 | 1.008s | 34.224MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTNIA.smt2 | 1.016s | 28.936MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTLIA.smt2 | 1.036s | 32.964MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFLIA.smt2 | 1.205s | 34.08MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTNIA.smt2 | 1.223s | 28.232MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTNIA.smt2 | 1.325s | 27.348MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFNIA.smt2 | 1.330s | 37.568MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTLIA.smt2 | 1.359s | 35.78MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTLIA.smt2 | 1.519s | 36.032MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTNIA.smt2 | 1.530s | 23.02MiB| unsat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFLIA.smt2 | 1.547s | 35.74MiB| unsat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTNIA.smt2 | 1.574s | 26.74MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTLIA.smt2 | 1.669s | 54.848MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTNIA.smt2 | 1.678s | 27.248MiB| unsat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTNIA.smt2 | 2.019s | 41.62MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTNIA.smt2 | 2.164s | 25.028MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFLIA.smt2 | 2.213s | 39.7MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFNIA.smt2 | 2.355s | 30.588MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTNIA.smt2 | 2.498s | 55.524MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTLIA.smt2 | 2.542s | 57.728MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTLIA.smt2 | 2.779s | 57.5MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTLIA.smt2 | 2.807s | 50.796MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTLIA.smt2 | 3.205s | 47.376MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFNIA.smt2 | 3.224s | 45.508MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFNIA.smt2 | 3.254s | 30.156MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTLIA.smt2 | 3.489s | 32.432MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFNIA.smt2 | 3.506s | 27.36MiB| unsat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTNIA.smt2 | 3.597s | 42.14MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTLIA.smt2 | 3.658s | 42.7MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTNIA.smt2 | 3.899s | 57.5MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTNIA.smt2 | 3.902s | 26.52MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTNIA.smt2 | 3.923s | 58.436MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTLIA.smt2 | 3.930s | 37.548MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTLIA.smt2 | 3.932s | 28.712MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTNIA.smt2 | 4.122s | 46.396MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFLIA.smt2 | 4.156s | 30.948MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTNIA.smt2 | 4.199s | 62.244MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTLIA.smt2 | 4.419s | 44.764MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTNIA.smt2 | 4.431s | 27.0MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFLIA.smt2 | 4.469s | 49.716MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTNIA.smt2 | 4.526s | 35.952MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTLIA.smt2 | 4.594s | 50.512MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFNIA.smt2 | 4.827s | 23.856MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTLIA.smt2 | 5.252s | 65.308MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTLIA.smt2 | 5.383s | 29.756MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTLIA.smt2 | 5.443s | 29.74MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTLIA.smt2 | 5.542s | 66.088MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFLIA.smt2 | 5.600s | 32.872MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFNIA.smt2 | 5.750s | 62.632MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFNIA.smt2 | 5.949s | 26.088MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTNIA.smt2 | 6.080s | 103.0MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTLIA.smt2 | 6.281s | 52.024MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTNIA.smt2 | 6.883s | 47.488MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTLIA.smt2 | 7.553s | 104.0MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTNIA.smt2 | 8.400s | 95.752MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTNIA.smt2 | 8.513s | 78.424MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTNIA.smt2 | 8.762s | 25.68MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTNIA.smt2 | 9.073s | 30.812MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTNIA.smt2 | 9.292s | 43.764MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFLIA.smt2 | 9.383s | 37.64MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFNIA.smt2 | 9.917s | 43.956MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTNIA.smt2 | 10.292s | 72.324MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTNIA.smt2 | 10.417s | 51.116MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTLIA.smt2 | 11.010s | 84.612MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFLIA.smt2 | 11.090s | 49.656MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTNIA.smt2 | 11.203s | 27.096MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFLIA.smt2 | 11.760s | 72.412MiB| unsat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFNIA.smt2 | 11.929s | 28.848MiB| unsat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTLIA.smt2 | 12.317s | 81.28MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTLIA.smt2 | 12.368s | 67.34MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFLIA.smt2 | 12.437s | 58.968MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTLIA.smt2 | 13.192s | 23.24MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFNIA.smt2 | 13.757s | 67.1MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFNIA.smt2 | 13.764s | 33.44MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTLIA.smt2 | 14.234s | 67.332MiB| unsat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFLIA.smt2 | 15.058s | 73.184MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFLIA.smt2 | 15.085s | 89.108MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFNIA.smt2 | 15.279s | 90.22MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTNIA.smt2 | 15.741s | 58.216MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTNIA.smt2 | 16.102s | 67.4MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFLIA.smt2 | 16.396s | 61.388MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFNIA.smt2 | 16.622s | 46.604MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFLIA.smt2 | 17.486s | 85.396MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTNIA.smt2 | 18.011s | 53.052MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTLIA.smt2 | 18.194s | 126.0MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTNIA.smt2 | 18.337s | 34.728MiB| unsat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFLIA.smt2 | 18.742s | 90.152MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFNIA.smt2 | 18.850s | 38.692MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTNIA.smt2 | 18.877s | 54.588MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFNIA.smt2 | 19.020s | 63.408MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTNIA.smt2 | 19.788s | 77.852MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTLIA.smt2 | 19.799s | 83.308MiB| sat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTLIA.smt2 | 20.791s | 51.132MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFLIA.smt2 | 21.243s | 87.592MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFNIA.smt2 | 21.483s | 33.804MiB| unsat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFLIA.smt2 | 21.716s | 98.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTLIA.smt2 | 23.065s | 80.364MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTLIA.smt2 | 23.875s | 229.0MiB| unsat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFLIA.smt2 | 24.413s | 47.048MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTNIA.smt2 | 24.450s | 45.016MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFNIA.smt2 | 27.708s | 102.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFLIA.smt2 | 28.585s | 46.392MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTNIA.smt2 | 32.195s | 197.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTLIA.smt2 | 33.680s | 123.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTNIA.smt2 | 33.802s | 57.164MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTNIA.smt2 | 34.194s | 81.82MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTNIA.smt2 | 34.776s | 142.0MiB| unsat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTLIA.smt2 | 34.937s | 50.556MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFNIA.smt2 | 34.973s | 37.988MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFLIA.smt2 | 35.565s | 533.0MiB| unsat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTNIA.smt2 | 36.456s | 56.464MiB| unset | 139 | | | |30078_f817a923328f75af7e60_27_QF_UFDTLIA.smt2 | 36.977s | 147.0MiB| unsat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTLIA.smt2 | 37.731s | 78.328MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTNIA.smt2 | 37.801s | 129.0MiB| unsat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFNIA.smt2 | 41.327s | 107.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFNIA.smt2 | 42.479s | 57.796MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFLIA.smt2 | 43.335s | 117.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFLIA.smt2 | 44.688s | 148.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTNIA.smt2 | 45.619s | 179.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFNIA.smt2 | 46.059s | 187.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTNIA.smt2 | 46.361s | 137.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFNIA.smt2 | 49.087s | 236.0MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTLIA.smt2 | 51.996s | 79.988MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFNIA.smt2 | 53.036s | 157.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFNIA.smt2 | 54.609s | 260.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTLIA.smt2 | 54.857s | 126.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFNIA.smt2 | 59.414s | 86.536MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFLIA.smt2 | 62.165s | 284.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFLIA.smt2 | 63.178s | 149.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFNIA.smt2 | 65.999s | 156.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTNIA.smt2 | 66.903s | 138.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFLIA.smt2 | 68.968s | 162.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFLIA.smt2 | 70.709s | 192.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTNIA.smt2 | 79.358s | 182.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFLIA.smt2 | 85.097s | 79.636MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFLIA.smt2 | 88.899s | 45.284MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFLIA.smt2 | 93.727s | 121.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTNIA.smt2 | 101.551s | 135.0MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTNIA.smt2 | 103.540s | 36.784MiB| unsat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFNIA.smt2 | 103.641s | 147.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFNIA.smt2 | 105.388s | 416.0MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFLIA.smt2 | 108.806s | 1714.0MiB| unsat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFNIA.smt2 | 111.094s | 137.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTNIA.smt2 | 111.156s | 88.404MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFNIA.smt2 | 111.253s | 186.0MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFNIA.smt2 | 111.258s | 127.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTNIA.smt2 | 113.010s | 32.12MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTNIA.smt2 | 114.920s | 197.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFNIA.smt2 | 118.988s | 46.984MiB| unsat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2 | 124.604s | 193.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFNIA.smt2 | 130.386s | 189.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTLIA.smt2 | 131.924s | 158.0MiB| unsat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTLIA.smt2 | 143.786s | 142.0MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFLIA.smt2 | 145.349s | 193.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFNIA.smt2 | 149.477s | 431.0MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTLIA.smt2 | 155.775s | 117.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFNIA.smt2 | 166.167s | 166.0MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTLIA.smt2 | 175.243s | 418.0MiB| unsat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFNIA.smt2 | 184.935s | 242.0MiB| sat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTNIA.smt2 | 186.613s | 132.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFLIA.smt2 | 193.512s | 477.0MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFNIA.smt2 | 204.574s | 99.46MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFNIA.smt2 | 214.126s | 137.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFLIA.smt2 | 226.004s | 455.0MiB| unsat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTNIA.smt2 | 229.030s | 226.0MiB| sat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTLIA.smt2 | 244.488s | 241.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFNIA.smt2 | 263.265s | 120.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFLIA.smt2 | 305.860s | 189.0MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFNIA.smt2 | 357.992s | 188.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTNIA.smt2 | 358.977s | 111.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFNIA.smt2 | 469.944s | 596.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTLIA.smt2 | 477.674s | 31.208MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTNIA.smt2 | 480.090s | 180.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFNIA.smt2 | 497.239s | 138.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTLIA.smt2 | 506.393s | 851.0MiB| unsat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTNIA.smt2 | 519.873s | 138.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFNIA.smt2 | 551.526s | 588.0MiB| unsat | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTNIA.smt2 | 565.683s | 227.0MiB| sat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFNIA.smt2 | 566.349s | 377.0MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFLIA.smt2 | 597.477s | 627.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFNIA.smt2 | 597.897s | 96.052MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFLIA.smt2 | 598.306s | 200.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTLIA.smt2 | 599.086s | 1418.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFLIA.smt2 | 599.194s | 521.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTNIA.smt2 | 599.209s | 60.796MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFLIA.smt2 | 599.291s | 184.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFLIA.smt2 | 599.344s | 622.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFLIA.smt2 | 599.379s | 60.604MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTLIA.smt2 | 599.389s | 730.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFNIA.smt2 | 599.393s | 633.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFLIA.smt2 | 599.418s | 424.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFLIA.smt2 | 599.424s | 287.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTLIA.smt2 | 599.465s | 273.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFLIA.smt2 | 599.475s | 282.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFNIA.smt2 | 599.479s | 454.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFLIA.smt2 | 599.489s | 399.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFNIA.smt2 | 599.500s | 687.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTNIA.smt2 | 599.520s | 140.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFLIA.smt2 | 599.523s | 238.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFNIA.smt2 | 599.528s | 45.9MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFLIA.smt2 | 599.530s | 279.0MiB| timeout | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFLIA.smt2 | 599.532s | 151.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFNIA.smt2 | 599.536s | 60.132MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTLIA.smt2 | 599.540s | 222.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTNIA.smt2 | 599.540s | 225.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFNIA.smt2 | 599.542s | 92.608MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTLIA.smt2 | 599.552s | 688.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTLIA.smt2 | 599.554s | 913.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFNIA.smt2 | 599.554s | 320.0MiB| timeout | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFLIA.smt2 | 599.555s | 210.0MiB| timeout | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFLIA.smt2 | 599.555s | 351.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTNIA.smt2 | 599.557s | 109.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTLIA.smt2 | 599.559s | 258.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFLIA.smt2 | 599.564s | 806.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTLIA.smt2 | 599.566s | 229.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTNIA.smt2 | 599.570s | 119.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFNIA.smt2 | 599.574s | 365.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTLIA.smt2 | 599.578s | 345.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTLIA.smt2 | 599.580s | 336.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFNIA.smt2 | 599.582s | 60.72MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFLIA.smt2 | 599.592s | 793.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFLIA.smt2 | 599.600s | 726.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFNIA.smt2 | 599.600s | 950.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTNIA.smt2 | 599.604s | 314.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTLIA.smt2 | 599.613s | 484.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFLIA.smt2 | 599.623s | 154.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFLIA.smt2 | 599.631s | 386.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFLIA.smt2 | 599.640s | 396.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTLIA.smt2 | 599.642s | 1170.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFLIA.smt2 | 599.642s | 371.0MiB| timeout | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFNIA.smt2 | 599.646s | 323.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTLIA.smt2 | 599.653s | 330.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTNIA.smt2 | 599.660s | 82.012MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFNIA.smt2 | 599.661s | 272.0MiB| timeout | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFLIA.smt2 | 599.663s | 173.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFNIA.smt2 | 599.663s | 95.964MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTNIA.smt2 | 599.664s | 30.624MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTLIA.smt2 | 599.673s | 783.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFLIA.smt2 | 599.673s | 1245.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTNIA.smt2 | 599.673s | 450.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFNIA.smt2 | 599.688s | 99.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFNIA.smt2 | 599.694s | 31.488MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFLIA.smt2 | 599.694s | 579.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFNIA.smt2 | 599.695s | 110.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTNIA.smt2 | 599.698s | 167.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFNIA.smt2 | 599.700s | 218.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTLIA.smt2 | 599.711s | 2145.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFLIA.smt2 | 599.712s | 249.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFNIA.smt2 | 599.712s | 689.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTLIA.smt2 | 599.720s | 428.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTLIA.smt2 | 599.725s | 613.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTNIA.smt2 | 599.727s | 55.564MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFLIA.smt2 | 599.731s | 285.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFNIA.smt2 | 599.746s | 50.624MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTLIA.smt2 | 599.759s | 341.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTNIA.smt2 | 599.764s | 51.304MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFLIA.smt2 | 599.770s | 1343.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTLIA.smt2 | 599.774s | 473.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFLIA.smt2 | 599.776s | 59.984MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTNIA.smt2 | 599.779s | 207.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFNIA.smt2 | 599.779s | 1545.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFLIA.smt2 | 599.781s | 2204.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFLIA.smt2 | 599.782s | 1152.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTLIA.smt2 | 599.788s | 691.0MiB| timeout | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFLIA.smt2 | 599.789s | 634.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFNIA.smt2 | 599.789s | 359.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFLIA.smt2 | 599.792s | 856.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFNIA.smt2 | 599.798s | 640.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTLIA.smt2 | 599.799s | 286.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFNIA.smt2 | 599.822s | 35.244MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTNIA.smt2 | 599.824s | 26.444MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFNIA.smt2 | 599.830s | 76.776MiB| timeout | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFLIA.smt2 | 599.852s | 282.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFLIA.smt2 | 599.855s | 680.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFLIA.smt2 | 599.859s | 2153.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFLIA.smt2 | 599.873s | 428.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFNIA.smt2 | 599.886s | 346.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTLIA.smt2 | 599.903s | 1217.0MiB| timeout | 0 | | |