# . * SAT 160 * UNSAT 52 * TIMEOUT 96 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: dio calls period = 4 plus random seed
Job tag: dio_certora_random_seed_7
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 smt.random_seed=8"
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_UFDTNIA.smt2 | 0.106s | 21.024MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTLIA.smt2 | 0.132s | 23.244MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFNIA.smt2 | 0.135s | 21.024MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFDTLIA.smt2 | 0.138s | 21.492MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFNIA.smt2 | 0.144s | 23.112MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTLIA.smt2 | 0.151s | 23.316MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFLIA.smt2 | 0.158s | 23.6MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFLIA.smt2 | 0.164s | 21.712MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTNIA.smt2 | 0.184s | 23.896MiB| unsat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFLIA.smt2 | 0.230s | 25.34MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTLIA.smt2 | 0.243s | 24.444MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFLIA.smt2 | 0.320s | 23.888MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTNIA.smt2 | 0.439s | 25.7MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTNIA.smt2 | 0.447s | 26.572MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFNIA.smt2 | 0.464s | 23.452MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTNIA.smt2 | 0.488s | 28.22MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTNIA.smt2 | 0.492s | 27.784MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTLIA.smt2 | 0.493s | 25.752MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTNIA.smt2 | 0.494s | 30.128MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFLIA.smt2 | 0.522s | 25.928MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTNIA.smt2 | 0.567s | 22.96MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTLIA.smt2 | 0.653s | 30.428MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTNIA.smt2 | 0.695s | 26.148MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFNIA.smt2 | 0.745s | 24.244MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTLIA.smt2 | 0.754s | 33.384MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTLIA.smt2 | 0.835s | 25.652MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFNIA.smt2 | 0.844s | 26.916MiB| unsat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTLIA.smt2 | 0.861s | 32.944MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTLIA.smt2 | 0.869s | 26.652MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFLIA.smt2 | 0.883s | 26.176MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTNIA.smt2 | 0.885s | 29.312MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFNIA.smt2 | 0.945s | 29.42MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTLIA.smt2 | 0.956s | 34.112MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTNIA.smt2 | 1.077s | 27.188MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTNIA.smt2 | 1.408s | 23.184MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTNIA.smt2 | 1.440s | 29.296MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTNIA.smt2 | 1.463s | 24.58MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTLIA.smt2 | 1.616s | 27.676MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTLIA.smt2 | 1.627s | 36.292MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTNIA.smt2 | 1.733s | 26.644MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFLIA.smt2 | 1.809s | 35.752MiB| unsat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFNIA.smt2 | 1.914s | 26.72MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFNIA.smt2 | 2.009s | 23.14MiB| unsat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTNIA.smt2 | 2.039s | 41.496MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFNIA.smt2 | 2.082s | 38.092MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTLIA.smt2 | 2.215s | 36.412MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFNIA.smt2 | 2.269s | 29.604MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTLIA.smt2 | 2.294s | 55.404MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFLIA.smt2 | 2.301s | 35.444MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTNIA.smt2 | 2.350s | 42.808MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTNIA.smt2 | 2.441s | 57.812MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTLIA.smt2 | 2.519s | 57.628MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTLIA.smt2 | 2.595s | 52.86MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTLIA.smt2 | 2.616s | 42.716MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTNIA.smt2 | 2.644s | 27.704MiB| unsat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTLIA.smt2 | 2.666s | 57.792MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTNIA.smt2 | 3.150s | 57.456MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFNIA.smt2 | 3.403s | 46.564MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTLIA.smt2 | 3.534s | 51.188MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTLIA.smt2 | 3.690s | 38.764MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFNIA.smt2 | 3.827s | 26.016MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFLIA.smt2 | 3.873s | 43.124MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTLIA.smt2 | 3.951s | 47.576MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTLIA.smt2 | 4.137s | 62.364MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFNIA.smt2 | 4.245s | 40.576MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTLIA.smt2 | 4.368s | 44.528MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTNIA.smt2 | 4.541s | 35.936MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFLIA.smt2 | 4.641s | 32.448MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTLIA.smt2 | 4.642s | 31.564MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFLIA.smt2 | 5.168s | 48.08MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTLIA.smt2 | 5.196s | 78.704MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTLIA.smt2 | 5.398s | 65.176MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTNIA.smt2 | 5.786s | 27.004MiB| unsat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTLIA.smt2 | 5.805s | 28.984MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTNIA.smt2 | 6.130s | 77.536MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTNIA.smt2 | 6.304s | 102.0MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTLIA.smt2 | 6.345s | 52.976MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFLIA.smt2 | 6.390s | 30.32MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTLIA.smt2 | 6.797s | 104.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTNIA.smt2 | 6.840s | 47.272MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTNIA.smt2 | 7.120s | 57.272MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTLIA.smt2 | 7.169s | 85.564MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTNIA.smt2 | 7.403s | 96.132MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFNIA.smt2 | 7.746s | 32.052MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFNIA.smt2 | 7.877s | 44.608MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFLIA.smt2 | 8.665s | 73.92MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFNIA.smt2 | 9.122s | 32.712MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTLIA.smt2 | 9.575s | 67.156MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTLIA.smt2 | 10.543s | 42.524MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFNIA.smt2 | 10.547s | 64.472MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTNIA.smt2 | 10.840s | 58.08MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTNIA.smt2 | 10.902s | 44.196MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFLIA.smt2 | 11.996s | 61.232MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTLIA.smt2 | 12.386s | 120.0MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTLIA.smt2 | 14.149s | 30.508MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTNIA.smt2 | 14.932s | 63.428MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTNIA.smt2 | 15.126s | 64.88MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTNIA.smt2 | 15.267s | 49.348MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTLIA.smt2 | 15.294s | 98.808MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFNIA.smt2 | 15.586s | 73.064MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFNIA.smt2 | 16.026s | 90.224MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTLIA.smt2 | 17.237s | 67.952MiB| unsat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFNIA.smt2 | 17.425s | 70.552MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFNIA.smt2 | 17.772s | 98.12MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTNIA.smt2 | 18.138s | 27.14MiB| unsat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTLIA.smt2 | 18.508s | 72.352MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTNIA.smt2 | 18.805s | 58.3MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFLIA.smt2 | 19.174s | 87.82MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFLIA.smt2 | 19.452s | 54.524MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFLIA.smt2 | 19.548s | 90.516MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFLIA.smt2 | 20.303s | 85.152MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFLIA.smt2 | 21.125s | 40.352MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTLIA.smt2 | 21.751s | 74.532MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFNIA.smt2 | 21.774s | 34.62MiB| unsat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFNIA.smt2 | 22.038s | 90.256MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTNIA.smt2 | 23.775s | 35.156MiB| unsat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTNIA.smt2 | 24.667s | 83.52MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFNIA.smt2 | 25.609s | 39.136MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTNIA.smt2 | 25.881s | 78.292MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTNIA.smt2 | 26.313s | 142.0MiB| unsat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTLIA.smt2 | 28.079s | 43.244MiB| sat | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTNIA.smt2 | 28.809s | 28.268MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFLIA.smt2 | 28.947s | 103.0MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTLIA.smt2 | 29.443s | 34.512MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFLIA.smt2 | 29.525s | 42.968MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTLIA.smt2 | 29.596s | 125.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTNIA.smt2 | 29.735s | 57.892MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTNIA.smt2 | 30.761s | 98.976MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTNIA.smt2 | 32.214s | 70.48MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFNIA.smt2 | 32.343s | 57.884MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTLIA.smt2 | 33.408s | 240.0MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTNIA.smt2 | 33.561s | 196.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTNIA.smt2 | 33.837s | 92.4MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFLIA.smt2 | 34.786s | 99.488MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFLIA.smt2 | 36.149s | 533.0MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTNIA.smt2 | 36.633s | 127.0MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTNIA.smt2 | 38.556s | 61.32MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTNIA.smt2 | 40.919s | 129.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFLIA.smt2 | 42.962s | 142.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFLIA.smt2 | 43.599s | 87.484MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTNIA.smt2 | 44.293s | 47.728MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFLIA.smt2 | 48.795s | 139.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTLIA.smt2 | 49.874s | 144.0MiB| unsat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFLIA.smt2 | 52.340s | 127.0MiB| sat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTLIA.smt2 | 54.534s | 83.768MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFLIA.smt2 | 54.652s | 218.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFNIA.smt2 | 55.103s | 48.372MiB| unsat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFNIA.smt2 | 55.210s | 30.796MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFLIA.smt2 | 55.728s | 89.368MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTNIA.smt2 | 57.545s | 163.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFLIA.smt2 | 57.730s | 159.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFNIA.smt2 | 59.544s | 226.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTNIA.smt2 | 60.034s | 138.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFLIA.smt2 | 61.201s | 190.0MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFLIA.smt2 | 63.090s | 154.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2 | 63.140s | 163.0MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTLIA.smt2 | 66.110s | 131.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTNIA.smt2 | 69.344s | 205.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFNIA.smt2 | 70.724s | 198.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFNIA.smt2 | 76.488s | 30.976MiB| unsat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFNIA.smt2 | 78.473s | 70.948MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFNIA.smt2 | 79.852s | 417.0MiB| unsat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFLIA.smt2 | 80.816s | 74.752MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTNIA.smt2 | 81.555s | 91.336MiB| unsat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTLIA.smt2 | 89.311s | 99.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFNIA.smt2 | 89.599s | 303.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTLIA.smt2 | 91.980s | 69.172MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFNIA.smt2 | 98.955s | 171.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFLIA.smt2 | 101.050s | 1718.0MiB| unsat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFNIA.smt2 | 103.051s | 170.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFNIA.smt2 | 107.269s | 441.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTLIA.smt2 | 108.275s | 24.912MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTLIA.smt2 | 110.510s | 149.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFLIA.smt2 | 125.415s | 435.0MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFNIA.smt2 | 129.652s | 227.0MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFLIA.smt2 | 129.763s | 381.0MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTNIA.smt2 | 134.051s | 37.636MiB| unsat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTLIA.smt2 | 136.647s | 486.0MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFNIA.smt2 | 138.886s | 190.0MiB| sat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFNIA.smt2 | 145.886s | 158.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFNIA.smt2 | 151.682s | 423.0MiB| unsat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFNIA.smt2 | 154.324s | 241.0MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFNIA.smt2 | 156.725s | 133.0MiB| sat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTLIA.smt2 | 157.351s | 206.0MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFLIA.smt2 | 158.204s | 321.0MiB| unsat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTNIA.smt2 | 160.361s | 56.636MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFNIA.smt2 | 181.460s | 111.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFLIA.smt2 | 188.410s | 157.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFNIA.smt2 | 191.839s | 256.0MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFLIA.smt2 | 192.049s | 169.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTNIA.smt2 | 192.307s | 308.0MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFLIA.smt2 | 193.181s | 56.156MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFNIA.smt2 | 203.938s | 35.72MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFLIA.smt2 | 210.985s | 490.0MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFNIA.smt2 | 239.227s | 114.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTNIA.smt2 | 270.961s | 24.448MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFNIA.smt2 | 302.601s | 180.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFNIA.smt2 | 330.417s | 135.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFLIA.smt2 | 334.699s | 39.952MiB| unsat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTNIA.smt2 | 402.515s | 104.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTLIA.smt2 | 434.197s | 856.0MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFLIA.smt2 | 460.411s | 145.0MiB| unsat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFNIA.smt2 | 487.986s | 124.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTNIA.smt2 | 489.239s | 44.844MiB| unsat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTNIA.smt2 | 498.129s | 128.0MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFNIA.smt2 | 504.494s | 208.0MiB| sat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFNIA.smt2 | 505.880s | 383.0MiB| sat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTNIA.smt2 | 526.464s | 322.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFNIA.smt2 | 567.231s | 588.0MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFNIA.smt2 | 575.269s | 55.476MiB| sat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFLIA.smt2 | 575.432s | 122.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTNIA.smt2 | 586.225s | 51.284MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFNIA.smt2 | 597.889s | 577.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTNIA.smt2 | 598.164s | 267.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTLIA.smt2 | 598.370s | 273.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFNIA.smt2 | 599.100s | 308.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFLIA.smt2 | 599.167s | 43.94MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFNIA.smt2 | 599.215s | 113.0MiB| timeout | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFNIA.smt2 | 599.262s | 312.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTNIA.smt2 | 599.284s | 30.688MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFLIA.smt2 | 599.293s | 809.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFNIA.smt2 | 599.324s | 194.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFLIA.smt2 | 599.332s | 698.0MiB| timeout | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFLIA.smt2 | 599.338s | 590.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFLIA.smt2 | 599.341s | 244.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTLIA.smt2 | 599.362s | 237.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFNIA.smt2 | 599.386s | 376.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTLIA.smt2 | 599.411s | 776.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFLIA.smt2 | 599.435s | 231.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFLIA.smt2 | 599.436s | 1343.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTLIA.smt2 | 599.443s | 2113.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFLIA.smt2 | 599.449s | 202.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFLIA.smt2 | 599.450s | 751.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFNIA.smt2 | 599.453s | 322.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFLIA.smt2 | 599.454s | 224.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFLIA.smt2 | 599.455s | 308.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTLIA.smt2 | 599.477s | 1006.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTLIA.smt2 | 599.491s | 421.0MiB| timeout | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFLIA.smt2 | 599.501s | 331.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTNIA.smt2 | 599.513s | 195.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFNIA.smt2 | 599.517s | 302.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTLIA.smt2 | 599.523s | 248.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFNIA.smt2 | 599.533s | 156.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFLIA.smt2 | 599.535s | 286.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFLIA.smt2 | 599.537s | 195.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTLIA.smt2 | 599.547s | 341.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFLIA.smt2 | 599.551s | 871.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTLIA.smt2 | 599.553s | 1418.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFNIA.smt2 | 599.559s | 92.444MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTNIA.smt2 | 599.563s | 143.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFLIA.smt2 | 599.568s | 847.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTNIA.smt2 | 599.573s | 264.0MiB| timeout | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFLIA.smt2 | 599.575s | 167.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTNIA.smt2 | 599.578s | 102.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFNIA.smt2 | 599.582s | 85.656MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFLIA.smt2 | 599.583s | 454.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTNIA.smt2 | 599.587s | 89.496MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTLIA.smt2 | 599.587s | 277.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFNIA.smt2 | 599.587s | 640.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTNIA.smt2 | 599.592s | 73.8MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFLIA.smt2 | 599.598s | 395.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTLIA.smt2 | 599.607s | 1170.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTLIA.smt2 | 599.623s | 477.0MiB| timeout | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFLIA.smt2 | 599.624s | 227.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTLIA.smt2 | 599.631s | 773.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTNIA.smt2 | 599.652s | 488.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFNIA.smt2 | 599.663s | 904.0MiB| timeout | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFLIA.smt2 | 599.664s | 150.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTNIA.smt2 | 599.665s | 97.48MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTLIA.smt2 | 599.668s | 252.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTLIA.smt2 | 599.680s | 411.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTLIA.smt2 | 599.688s | 727.0MiB| timeout | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFNIA.smt2 | 599.691s | 143.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFLIA.smt2 | 599.691s | 315.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTNIA.smt2 | 599.693s | 192.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFNIA.smt2 | 599.702s | 78.932MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTLIA.smt2 | 599.704s | 524.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTNIA.smt2 | 599.708s | 89.652MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFLIA.smt2 | 599.711s | 413.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFNIA.smt2 | 599.714s | 59.036MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFNIA.smt2 | 599.717s | 632.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFLIA.smt2 | 599.720s | 582.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFLIA.smt2 | 599.723s | 410.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFLIA.smt2 | 599.725s | 1288.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTLIA.smt2 | 599.736s | 745.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTLIA.smt2 | 599.744s | 576.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTNIA.smt2 | 599.745s | 57.556MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFNIA.smt2 | 599.746s | 49.056MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFNIA.smt2 | 599.747s | 590.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFLIA.smt2 | 599.751s | 1002.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFNIA.smt2 | 599.756s | 377.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFNIA.smt2 | 599.759s | 43.484MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFLIA.smt2 | 599.760s | 718.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFLIA.smt2 | 599.791s | 162.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFNIA.smt2 | 599.794s | 91.116MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTLIA.smt2 | 599.800s | 1056.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFLIA.smt2 | 599.803s | 443.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTLIA.smt2 | 599.808s | 273.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFNIA.smt2 | 599.810s | 753.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTNIA.smt2 | 599.814s | 104.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFLIA.smt2 | 599.820s | 2078.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTLIA.smt2 | 599.828s | 31.74MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTNIA.smt2 | 599.839s | 96.444MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTNIA.smt2 | 599.845s | 245.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFNIA.smt2 | 599.858s | 1545.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTLIA.smt2 | 599.860s | 482.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFLIA.smt2 | 599.917s | 2307.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFLIA.smt2 | 599.920s | 1285.0MiB| timeout | 0 | | |