# . * SAT 148 * UNSAT 40 * TIMEOUT 120 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: quotient_pairs=false inputs/certora
Job tag: fix_in_qp_false_certora
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: 186ef6a0cd3f0fc8821795515994089cfc4e65db
Z3 branch: modgb
Z3 options: "-T:200 smt.arith.nl.grobner_quotient_pairs=false"
Z3 inputs: inputs/certora
Z3 commit message: fix unsound grobner-quotient-pair lemma: skip lc with non-integral coefficients

pdd::reduce() can introduce non-integral coefficients via leading-term
division. The quotient lemma reasoning assumed lc_comb = lc_i - lc_j
was always integer-valued, which failed when lc had non-integral coefficients.
Filter out such entries when building var_to_facts.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |63058_aa742630eef64f949de269382c1f9035_25_UFNIA.smt2 | 0.090s | 22.94MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFDTLIA.smt2 | 0.113s | 21.496MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFLIA.smt2 | 0.120s | 21.528MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFDTNIA.smt2 | 0.129s | 21.02MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFNIA.smt2 | 0.138s | 21.072MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFLIA.smt2 | 0.159s | 23.812MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTNIA.smt2 | 0.172s | 23.008MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTLIA.smt2 | 0.172s | 23.488MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTLIA.smt2 | 0.182s | 23.396MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFLIA.smt2 | 0.226s | 24.084MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFLIA.smt2 | 0.228s | 25.564MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTLIA.smt2 | 0.260s | 24.7MiB| unsat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTNIA.smt2 | 0.270s | 23.992MiB| unsat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTNIA.smt2 | 0.341s | 26.696MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFNIA.smt2 | 0.395s | 24.048MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFLIA.smt2 | 0.442s | 25.696MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTLIA.smt2 | 0.493s | 33.612MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTNIA.smt2 | 0.544s | 28.264MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFLIA.smt2 | 0.557s | 26.56MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTLIA.smt2 | 0.575s | 26.464MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTNIA.smt2 | 0.622s | 27.676MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTLIA.smt2 | 0.638s | 25.284MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTNIA.smt2 | 0.650s | 29.176MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTLIA.smt2 | 0.714s | 30.612MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFNIA.smt2 | 0.741s | 24.532MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFNIA.smt2 | 0.773s | 27.376MiB| unsat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTNIA.smt2 | 0.829s | 27.076MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTLIA.smt2 | 0.845s | 28.064MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTNIA.smt2 | 0.880s | 29.688MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTNIA.smt2 | 0.918s | 30.568MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTLIA.smt2 | 0.945s | 26.768MiB| unsat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTNIA.smt2 | 0.975s | 27.508MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTLIA.smt2 | 1.156s | 34.704MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTNIA.smt2 | 1.297s | 27.664MiB| unsat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFNIA.smt2 | 1.384s | 26.248MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFLIA.smt2 | 1.401s | 36.28MiB| unsat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTLIA.smt2 | 1.465s | 38.044MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTLIA.smt2 | 1.467s | 35.636MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFLIA.smt2 | 1.487s | 34.332MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTNIA.smt2 | 1.519s | 23.296MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFNIA.smt2 | 1.547s | 26.3MiB| unsat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTNIA.smt2 | 1.627s | 30.22MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTLIA.smt2 | 1.636s | 36.504MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFNIA.smt2 | 1.641s | 31.904MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTNIA.smt2 | 1.926s | 24.972MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTNIA.smt2 | 1.958s | 43.612MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFNIA.smt2 | 2.113s | 31.996MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFNIA.smt2 | 2.336s | 23.428MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFLIA.smt2 | 2.356s | 40.104MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTNIA.smt2 | 2.499s | 39.38MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTLIA.smt2 | 2.593s | 55.464MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTLIA.smt2 | 2.783s | 60.232MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFLIA.smt2 | 2.850s | 31.212MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTNIA.smt2 | 2.857s | 25.772MiB| unsat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTNIA.smt2 | 2.887s | 27.516MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTLIA.smt2 | 2.977s | 55.408MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTLIA.smt2 | 2.995s | 43.54MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTLIA.smt2 | 3.015s | 60.476MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTNIA.smt2 | 3.024s | 58.664MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTNIA.smt2 | 3.151s | 61.116MiB| sat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFNIA.smt2 | 3.221s | 28.188MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTLIA.smt2 | 3.450s | 49.42MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFNIA.smt2 | 3.595s | 34.884MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTNIA.smt2 | 3.676s | 48.364MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTNIA.smt2 | 3.803s | 59.908MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFNIA.smt2 | 4.008s | 43.788MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTLIA.smt2 | 4.019s | 53.092MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTLIA.smt2 | 4.148s | 33.124MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTLIA.smt2 | 4.156s | 55.336MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTLIA.smt2 | 4.381s | 39.528MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTLIA.smt2 | 4.692s | 66.316MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFNIA.smt2 | 4.827s | 31.536MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTNIA.smt2 | 4.853s | 63.464MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTLIA.smt2 | 4.967s | 45.548MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTNIA.smt2 | 5.163s | 103.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTLIA.smt2 | 5.210s | 63.92MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFNIA.smt2 | 5.358s | 49.324MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFLIA.smt2 | 5.569s | 57.384MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTNIA.smt2 | 5.615s | 37.352MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTLIA.smt2 | 5.655s | 66.896MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTLIA.smt2 | 5.866s | 105.0MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFLIA.smt2 | 6.150s | 51.94MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTNIA.smt2 | 6.210s | 47.276MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFLIA.smt2 | 6.425s | 34.708MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTNIA.smt2 | 7.194s | 46.028MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFNIA.smt2 | 7.421s | 73.104MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTLIA.smt2 | 7.774s | 30.536MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFNIA.smt2 | 7.941s | 65.94MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFLIA.smt2 | 7.947s | 101.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTNIA.smt2 | 7.965s | 82.54MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFNIA.smt2 | 7.989s | 44.908MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFLIA.smt2 | 8.228s | 88.636MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTLIA.smt2 | 8.233s | 66.752MiB| unsat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTLIA.smt2 | 9.295s | 31.504MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTLIA.smt2 | 9.989s | 31.768MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFNIA.smt2 | 11.775s | 45.448MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFLIA.smt2 | 12.012s | 72.988MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFLIA.smt2 | 12.046s | 68.696MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTLIA.smt2 | 12.833s | 83.12MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFNIA.smt2 | 12.865s | 41.248MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTNIA.smt2 | 12.999s | 52.032MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTNIA.smt2 | 14.068s | 144.0MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFLIA.smt2 | 14.102s | 43.952MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTNIA.smt2 | 15.472s | 82.744MiB| sat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTLIA.smt2 | 15.701s | 52.836MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTLIA.smt2 | 15.840s | 129.0MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTNIA.smt2 | 16.375s | 33.492MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFLIA.smt2 | 16.898s | 66.128MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFNIA.smt2 | 17.413s | 99.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTNIA.smt2 | 17.547s | 64.896MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTLIA.smt2 | 17.584s | 129.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFNIA.smt2 | 17.851s | 66.184MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTLIA.smt2 | 19.461s | 81.1MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTNIA.smt2 | 19.478s | 64.844MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTNIA.smt2 | 19.979s | 60.772MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTLIA.smt2 | 20.383s | 80.024MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTNIA.smt2 | 21.311s | 34.764MiB| unsat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFLIA.smt2 | 21.764s | 73.724MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFLIA.smt2 | 21.943s | 540.0MiB| unsat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFLIA.smt2 | 22.426s | 91.112MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTNIA.smt2 | 23.066s | 102.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFNIA.smt2 | 24.377s | 105.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTNIA.smt2 | 25.725s | 64.532MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFNIA.smt2 | 28.971s | 52.408MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTLIA.smt2 | 29.297s | 130.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTLIA.smt2 | 29.946s | 24.016MiB| unsat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTLIA.smt2 | 30.291s | 81.948MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFLIA.smt2 | 32.194s | 68.872MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTLIA.smt2 | 33.720s | 93.42MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTLIA.smt2 | 36.959s | 234.0MiB| unsat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFLIA.smt2 | 37.049s | 125.0MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTNIA.smt2 | 37.183s | 63.784MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFLIA.smt2 | 38.139s | 114.0MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFLIA.smt2 | 39.315s | 44.252MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTNIA.smt2 | 40.138s | 63.828MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFNIA.smt2 | 42.028s | 206.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFLIA.smt2 | 42.589s | 118.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTNIA.smt2 | 43.642s | 222.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTNIA.smt2 | 43.869s | 131.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFLIA.smt2 | 44.107s | 166.0MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFNIA.smt2 | 45.847s | 45.432MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTNIA.smt2 | 48.926s | 76.14MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTLIA.smt2 | 50.710s | 150.0MiB| unsat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFLIA.smt2 | 53.469s | 150.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTNIA.smt2 | 53.833s | 94.812MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTLIA.smt2 | 55.423s | 152.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTNIA.smt2 | 56.409s | 50.068MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFNIA.smt2 | 57.171s | 143.0MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFLIA.smt2 | 57.869s | 54.816MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFNIA.smt2 | 58.627s | 37.572MiB| unsat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTNIA.smt2 | 59.215s | 90.748MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFLIA.smt2 | 63.324s | 287.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFLIA.smt2 | 63.763s | 190.0MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFNIA.smt2 | 68.065s | 129.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFNIA.smt2 | 68.140s | 94.224MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFNIA.smt2 | 70.119s | 219.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFLIA.smt2 | 71.483s | 274.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2 | 81.268s | 196.0MiB| unsat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFLIA.smt2 | 81.869s | 49.792MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTNIA.smt2 | 83.227s | 178.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTLIA.smt2 | 83.704s | 145.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTNIA.smt2 | 84.087s | 33.988MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTNIA.smt2 | 84.539s | 37.408MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTNIA.smt2 | 87.807s | 139.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTLIA.smt2 | 92.034s | 161.0MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFNIA.smt2 | 98.051s | 325.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFNIA.smt2 | 102.293s | 231.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFNIA.smt2 | 108.191s | 250.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFNIA.smt2 | 108.694s | 422.0MiB| unsat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFNIA.smt2 | 111.426s | 208.0MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTLIA.smt2 | 112.792s | 135.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFLIA.smt2 | 120.511s | 135.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFNIA.smt2 | 122.012s | 488.0MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFNIA.smt2 | 123.408s | 177.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTNIA.smt2 | 139.638s | 265.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFLIA.smt2 | 142.793s | 1737.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFLIA.smt2 | 152.906s | 232.0MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTLIA.smt2 | 153.960s | 423.0MiB| unsat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFLIA.smt2 | 155.261s | 216.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFLIA.smt2 | 157.983s | 465.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFNIA.smt2 | 158.915s | 426.0MiB| unsat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTNIA.smt2 | 161.687s | 99.288MiB| unsat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTLIA.smt2 | 181.016s | 857.0MiB| unsat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFNIA.smt2 | 181.752s | 287.0MiB| sat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTLIA.smt2 | 183.147s | 236.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFNIA.smt2 | 192.666s | 37.784MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTLIA.smt2 | 196.626s | 118.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFLIA.smt2 | 197.426s | 71.26MiB| sat | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFNIA.smt2 | 200.018s | 42.412MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFNIA.smt2 | 200.019s | 25.916MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTNIA.smt2 | 200.022s | 64.316MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTLIA.smt2 | 200.023s | 30.008MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFNIA.smt2 | 200.024s | 38.668MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFNIA.smt2 | 200.025s | 95.008MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTNIA.smt2 | 200.028s | 24.608MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTNIA.smt2 | 200.030s | 47.456MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTNIA.smt2 | 200.030s | 60.02MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTNIA.smt2 | 200.031s | 35.14MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTNIA.smt2 | 200.033s | 66.148MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFNIA.smt2 | 200.033s | 47.46MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTNIA.smt2 | 200.033s | 87.64MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTNIA.smt2 | 200.033s | 46.852MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFNIA.smt2 | 200.034s | 67.664MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFNIA.smt2 | 200.034s | 65.476MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFNIA.smt2 | 200.035s | 46.18MiB| timeout | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFLIA.smt2 | 200.035s | 134.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFLIA.smt2 | 200.036s | 37.324MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTNIA.smt2 | 200.036s | 59.66MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTNIA.smt2 | 200.036s | 28.868MiB| timeout | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFLIA.smt2 | 200.038s | 126.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFLIA.smt2 | 200.038s | 34.608MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFNIA.smt2 | 200.039s | 50.664MiB| timeout | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFNIA.smt2 | 200.040s | 230.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFNIA.smt2 | 200.040s | 112.0MiB| timeout | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFNIA.smt2 | 200.041s | 107.0MiB| timeout | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTLIA.smt2 | 200.041s | 65.58MiB| timeout | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTNIA.smt2 | 200.042s | 46.424MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTLIA.smt2 | 200.042s | 222.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFNIA.smt2 | 200.042s | 66.676MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTNIA.smt2 | 200.043s | 229.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFNIA.smt2 | 200.043s | 41.332MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFNIA.smt2 | 200.043s | 89.776MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTLIA.smt2 | 200.044s | 190.0MiB| timeout | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFLIA.smt2 | 200.045s | 167.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFLIA.smt2 | 200.045s | 190.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFLIA.smt2 | 200.045s | 105.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTLIA.smt2 | 200.046s | 193.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFLIA.smt2 | 200.046s | 154.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTNIA.smt2 | 200.046s | 48.588MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTNIA.smt2 | 200.047s | 209.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFLIA.smt2 | 200.047s | 203.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFLIA.smt2 | 200.048s | 199.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTLIA.smt2 | 200.048s | 189.0MiB| timeout | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFNIA.smt2 | 200.049s | 186.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTNIA.smt2 | 200.049s | 180.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFLIA.smt2 | 200.049s | 253.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTLIA.smt2 | 200.049s | 298.0MiB| timeout | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFNIA.smt2 | 200.050s | 118.0MiB| timeout | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFNIA.smt2 | 200.050s | 180.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTNIA.smt2 | 200.050s | 184.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTNIA.smt2 | 200.051s | 188.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTNIA.smt2 | 200.051s | 44.508MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTNIA.smt2 | 200.052s | 227.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFNIA.smt2 | 200.053s | 160.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTLIA.smt2 | 200.053s | 239.0MiB| timeout | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFNIA.smt2 | 200.054s | 61.78MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFLIA.smt2 | 200.055s | 164.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFNIA.smt2 | 200.055s | 190.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTLIA.smt2 | 200.055s | 286.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTNIA.smt2 | 200.056s | 182.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFNIA.smt2 | 200.056s | 260.0MiB| timeout | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFNIA.smt2 | 200.057s | 206.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_0_UFLIA.smt2 | 200.057s | 158.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFNIA.smt2 | 200.057s | 268.0MiB| timeout | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTNIA.smt2 | 200.059s | 225.0MiB| timeout | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFNIA.smt2 | 200.059s | 121.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFNIA.smt2 | 200.059s | 368.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFLIA.smt2 | 200.060s | 331.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFNIA.smt2 | 200.060s | 194.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFLIA.smt2 | 200.062s | 247.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTLIA.smt2 | 200.063s | 213.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFLIA.smt2 | 200.066s | 395.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFLIA.smt2 | 200.066s | 202.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTNIA.smt2 | 200.067s | 151.0MiB| timeout | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFNIA.smt2 | 200.067s | 338.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTNIA.smt2 | 200.067s | 274.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFNIA.smt2 | 200.069s | 209.0MiB| timeout | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFLIA.smt2 | 200.070s | 285.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTNIA.smt2 | 200.073s | 395.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFLIA.smt2 | 200.075s | 628.0MiB| timeout | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFLIA.smt2 | 200.076s | 479.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFLIA.smt2 | 200.076s | 403.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTLIA.smt2 | 200.076s | 443.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFLIA.smt2 | 200.077s | 348.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFLIA.smt2 | 200.084s | 440.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFLIA.smt2 | 200.086s | 435.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFLIA.smt2 | 200.086s | 252.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFLIA.smt2 | 200.087s | 589.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTLIA.smt2 | 200.088s | 412.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFLIA.smt2 | 200.089s | 547.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFNIA.smt2 | 200.092s | 578.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFLIA.smt2 | 200.093s | 499.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTLIA.smt2 | 200.095s | 656.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTLIA.smt2 | 200.095s | 540.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTLIA.smt2 | 200.096s | 700.0MiB| timeout | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFNIA.smt2 | 200.096s | 435.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTLIA.smt2 | 200.097s | 561.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTLIA.smt2 | 200.098s | 606.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFLIA.smt2 | 200.099s | 575.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTLIA.smt2 | 200.099s | 730.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFLIA.smt2 | 200.100s | 821.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFNIA.smt2 | 200.101s | 646.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFNIA.smt2 | 200.102s | 475.0MiB| timeout | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFLIA.smt2 | 200.103s | 466.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFNIA.smt2 | 200.110s | 638.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTLIA.smt2 | 200.116s | 733.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFLIA.smt2 | 200.122s | 606.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTLIA.smt2 | 200.125s | 363.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFLIA.smt2 | 200.139s | 1120.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFLIA.smt2 | 200.142s | 696.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTLIA.smt2 | 200.145s | 1180.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFNIA.smt2 | 200.153s | 1160.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFLIA.smt2 | 200.155s | 1355.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTLIA.smt2 | 200.177s | 1430.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFNIA.smt2 | 200.185s | 1565.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTLIA.smt2 | 200.203s | 1974.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFLIA.smt2 | 200.205s | 1940.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFLIA.smt2 | 200.222s | 2190.0MiB| timeout | 0 | | |