# .

* SAT 0
* UNSAT 0
* TIMEOUT 0
* UNKNOWN 0

* UNSET 308

* ERROR 308

# Meta data

<pre>
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: f607331856df120dbe3bbb0652b7041e3a617e50
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: type annotations across Python versions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFLIA.smt2      |    0.002s | 1560.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_4_UFLIA.smt2                      |    0.002s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_75_QF_UFNIA.smt2                  |    0.002s | 1560.0KiB| unset | 110 |  |  |
|38347_525a1ca0331f2bcbf520_54_QF_UFLIA.smt2                  |    0.002s | 1560.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTLIA.smt2    |    0.002s | 1788.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTLIA.smt2    |    0.002s | 1560.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTLIA.smt2    |    0.002s | 1560.0KiB| unset | 110 |  |  |
|63058_64ab9a7ef7b6c3492507_22_QF_UFLIA.smt2                  |    0.002s | 1496.0KiB| unset | 110 |  |  |
|93493_4ea6163ed03941199c785278ccc42812_49_QF_UFNIA.smt2      |    0.002s | 1560.0KiB| unset | 110 |  |  |
|63058_64ab9a7ef7b6c3492507_23_QF_UFNIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_29_QF_UFLIA.smt2                    |    0.003s | 1736.0KiB| unset | 110 |  |  |
|30078_f817a923328f75af7e60_28_QF_UFLIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFLIA.smt2      |    0.003s | 1560.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_38_QF_UFNIA.smt2                   |    0.003s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_72_QF_UFNIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_38_QF_UFLIA.smt2                   |    0.003s | 1560.0KiB| unset | 110 |  |  |
|52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFLIA.smt2      |    0.003s | 1560.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_33_QF_UFLIA.smt2                    |    0.003s | 1564.0KiB| unset | 110 |  |  |
|93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFNIA.smt2      |    0.003s | 1560.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFLIA.smt2      |    0.003s | 1560.0KiB| unset | 110 |  |  |
|52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFLIA.smt2      |    0.003s | 1792.0KiB| unset | 110 |  |  |
|63058_64ab9a7ef7b6c3492507_24_QF_UFLIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|38347_525a1ca0331f2bcbf520_54_QF_UFDTLIA.smt2                |    0.003s | 1560.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTLIA.smt2    |    0.003s | 1560.0KiB| unset | 110 |  |  |
|93493_5990a6bf5f2740164f77_50_QF_UFLIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|30078_f817a923328f75af7e60_27_QF_UFNIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_76_QF_UFNIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_33_QF_UFDTLIA.smt2                  |    0.003s | 1564.0KiB| unset | 110 |  |  |
|63058_64ab9a7ef7b6c3492507_23_QF_UFLIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_75_QF_UFLIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|30078_f817a923328f75af7e60_28_QF_UFNIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_76_QF_UFLIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_72_QF_UFLIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_74_QF_UFLIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFLIA.smt2      |    0.003s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_76_QF_UFDTLIA.smt2                |    0.003s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_74_QF_UFNIA.smt2                  |    0.003s | 1564.0KiB| unset | 110 |  |  |
|63058_55d6bef5390186355f11_26_QF_UFLIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFNIA.smt2      |    0.003s | 1560.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_1_UFDTLIA.smt2                    |    0.003s | 1560.0KiB| unset | 110 |  |  |
|93493_4ea6163ed03941199c785278ccc42812_49_QF_UFLIA.smt2      |    0.003s | 1560.0KiB| unset | 110 |  |  |
|93493_5990a6bf5f2740164f77_50_QF_UFNIA.smt2                  |    0.003s | 1560.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_39_QF_UFLIA.smt2                   |    0.004s | 1508.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFNIA.smt2      |    0.004s | 1560.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTLIA.smt2    |    0.004s | 1560.0KiB| unset | 110 |  |  |
|41958_32933c5a1384696720a2_61_QF_UFNIA.smt2                  |    0.004s | 1564.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_31_QF_UFDTNIA.smt2                  |    0.004s | 1564.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_58_QF_UFDTNIA.smt2                |    0.004s | 1560.0KiB| unset | 110 |  |  |
|72658_63104dadde9c6026353f_70_QF_UFDTNIA.smt2                |    0.004s | 1536.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_8_QF_UFDTLIA.smt2                 |    0.004s | 1560.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_40_QF_UFDTNIA.smt2                 |    0.004s | 1560.0KiB| unset | 110 |  |  |
|11775_ad46e5b8db4748c51973_42_QF_UFLIA.smt2                  |    0.004s | 1560.0KiB| unset | 110 |  |  |
|63058_55d6bef5390186355f11_26_QF_UFNIA.smt2                  |    0.004s | 1560.0KiB| unset | 110 |  |  |
|17512_5c1021b0faa6b6e1791b_21_QF_UFLIA.smt2                  |    0.004s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_73_QF_UFLIA.smt2                  |    0.004s | 1560.0KiB| unset | 110 |  |  |
|41958_32933c5a1384696720a2_63_QF_UFDTNIA.smt2                |    0.004s | 1560.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFLIA.smt2      |    0.004s | 1560.0KiB| unset | 110 |  |  |
|93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTNIA.smt2    |    0.004s | 1564.0KiB| unset | 110 |  |  |
|52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTLIA.smt2    |    0.004s | 1556.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_73_QF_UFNIA.smt2                  |    0.004s | 1560.0KiB| unset | 110 |  |  |
|3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFNIA.smt2       |    0.004s | 1564.0KiB| unset | 110 |  |  |
|17512_5c1021b0faa6b6e1791b_20_QF_UFDTLIA.smt2                |    0.004s | 1560.0KiB| unset | 110 |  |  |
|93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTNIA.smt2    |    0.004s | 1560.0KiB| unset | 110 |  |  |
|44289_e5a2e5c780236919ee6a_18_QF_UFLIA.smt2                  |    0.004s | 1556.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_4_UFDTLIA.smt2                    |    0.004s | 1560.0KiB| unset | 110 |  |  |
|44289_e5a2e5c780236919ee6a_18_QF_UFNIA.smt2                  |    0.004s | 1556.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFLIA.smt2      |    0.004s | 1560.0KiB| unset | 110 |  |  |
|72658_63104dadde9c6026353f_71_QF_UFNIA.smt2                  |    0.004s | 1556.0KiB| unset | 110 |  |  |
|11775_ad46e5b8db4748c51973_43_QF_UFDTNIA.smt2                |    0.004s | 1544.0KiB| unset | 110 |  |  |
|93493_5990a6bf5f2740164f77_50_QF_UFDTLIA.smt2                |    0.004s | 1560.0KiB| unset | 110 |  |  |
|63058_64ab9a7ef7b6c3492507_23_QF_UFDTLIA.smt2                |    0.004s | 1560.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_38_QF_UFDTNIA.smt2                 |    0.004s | 1564.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_74_QF_UFDTLIA.smt2                |    0.004s | 1560.0KiB| unset | 110 |  |  |
|63058_64ab9a7ef7b6c3492507_22_QF_UFNIA.smt2                  |    0.004s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_75_QF_UFDTNIA.smt2                |    0.004s | 1560.0KiB| unset | 110 |  |  |
|30078_f817a923328f75af7e60_27_QF_UFLIA.smt2                  |    0.004s | 1788.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_38_QF_UFDTLIA.smt2                 |    0.004s | 1560.0KiB| unset | 110 |  |  |
|41958_45c688a4814eb926c254_59_QF_UFDTLIA.smt2                |    0.004s | 1556.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_40_QF_UFLIA.smt2                   |    0.004s | 1560.0KiB| unset | 110 |  |  |
|41958_45c688a4814eb926c254_60_QF_UFNIA.smt2                  |    0.004s | 1564.0KiB| unset | 110 |  |  |
|44289_4066055e0f64d96da11a_15_QF_UFDTNIA.smt2                |    0.004s | 1560.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_32_QF_UFNIA.smt2                    |    0.005s | 1560.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_0_UFDTLIA.smt2                    |    0.005s | 1564.0KiB| unset | 110 |  |  |
|39657_1c7158801cd59dc13f05_46_QF_UFLIA.smt2                  |    0.005s | 1564.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_32_QF_UFDTNIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_32_QF_UFLIA.smt2                    |    0.005s | 1352.0KiB| unset | 110 |  |  |
|39657_1c7158801cd59dc13f05_46_QF_UFDTLIA.smt2                |    0.005s | 1564.0KiB| unset | 110 |  |  |
|30078_f817a923328f75af7e60_27_QF_UFDTNIA.smt2                |    0.005s | 1556.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTNIA.smt2    |    0.005s | 1560.0KiB| unset | 110 |  |  |
|52759_b3ecd2335fd16ec2eee2_9_UFNIA.smt2                      |    0.005s | 1560.0KiB| unset | 110 |  |  |
|41958_45c688a4814eb926c254_59_QF_UFDTNIA.smt2                |    0.005s | 1388.0KiB| unset | 110 |  |  |
|41958_32933c5a1384696720a2_62_QF_UFNIA.smt2                  |    0.005s | 1564.0KiB| unset | 110 |  |  |
|52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTNIA.smt2    |    0.005s | 1560.0KiB| unset | 110 |  |  |
|63058_55d6bef5390186355f11_26_QF_UFDTLIA.smt2                |    0.005s | 1424.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_30_QF_UFNIA.smt2                    |    0.005s | 1560.0KiB| unset | 110 |  |  |
|44289_e5a2e5c780236919ee6a_17_QF_UFDTNIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|17512_5c1021b0faa6b6e1791b_19_QF_UFDTNIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|41958_45c688a4814eb926c254_59_QF_UFLIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFLIA.smt2      |    0.005s | 1556.0KiB| unset | 110 |  |  |
|93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTLIA.smt2    |    0.005s | 1560.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_31_QF_UFDTLIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|41958_32933c5a1384696720a2_63_QF_UFDTLIA.smt2                |    0.005s | 1564.0KiB| unset | 110 |  |  |
|30078_f817a923328f75af7e60_28_QF_UFDTLIA.smt2                |    0.005s | 1564.0KiB| unset | 110 |  |  |
|39657_1c7158801cd59dc13f05_45_QF_UFDTNIA.smt2                |    0.005s | 1536.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_55_QF_UFNIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_31_QF_UFLIA.smt2                    |    0.005s | 1556.0KiB| unset | 110 |  |  |
|39657_2866defdd1f2434b69ab_47_QF_UFDTNIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_3_UFDTLIA.smt2                    |    0.005s | 1568.0KiB| unset | 110 |  |  |
|17512_5c1021b0faa6b6e1791b_19_QF_UFDTLIA.smt2                |    0.005s | 1564.0KiB| unset | 110 |  |  |
|17512_5c1021b0faa6b6e1791b_19_QF_UFNIA.smt2                  |    0.005s | 1360.0KiB| unset | 110 |  |  |
|52759_b3ecd2335fd16ec2eee2_9_UFDTNIA.smt2                    |    0.005s | 1548.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_0_UFNIA.smt2                      |    0.005s | 1500.0KiB| unset | 110 |  |  |
|44788_1965f0d6d94d5d8054ba_36_QF_UFNIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|44788_1965f0d6d94d5d8054ba_34_QF_UFDTNIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|52759_b3ecd2335fd16ec2eee2_9_UFLIA.smt2                      |    0.005s | 1564.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_6_QF_UFLIA.smt2                   |    0.005s | 1560.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_58_QF_UFLIA.smt2                  |    0.005s | 1580.0KiB| unset | 110 |  |  |
|44788_1965f0d6d94d5d8054ba_35_QF_UFLIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|39657_1c7158801cd59dc13f05_45_QF_UFLIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFNIA.smt2      |    0.005s | 1560.0KiB| unset | 110 |  |  |
|44788_1965f0d6d94d5d8054ba_34_QF_UFDTLIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFLIA.smt2      |    0.005s | 1560.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_5_QF_UFDTNIA.smt2                 |    0.005s | 1560.0KiB| unset | 110 |  |  |
|41958_45c688a4814eb926c254_60_QF_UFDTLIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_5_QF_UFNIA.smt2                   |    0.005s | 1448.0KiB| unset | 110 |  |  |
|63058_aa742630eef64f949de269382c1f9035_25_UFLIA.smt2         |    0.005s | 1560.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_1_UFNIA.smt2                      |    0.005s | 1552.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_74_QF_UFDTNIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_39_QF_UFNIA.smt2                   |    0.005s | 1560.0KiB| unset | 110 |  |  |
|41958_45c688a4814eb926c254_59_QF_UFNIA.smt2                  |    0.005s | 1788.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_2_UFLIA.smt2                      |    0.005s | 1560.0KiB| unset | 110 |  |  |
|11775_ad46e5b8db4748c51973_43_QF_UFDTLIA.smt2                |    0.005s | 1764.0KiB| unset | 110 |  |  |
|44289_4066055e0f64d96da11a_15_QF_UFDTLIA.smt2                |    0.005s | 1540.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_8_QF_UFNIA.smt2                   |    0.005s | 1556.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_1_UFDTNIA.smt2                    |    0.005s | 1560.0KiB| unset | 110 |  |  |
|63058_64ab9a7ef7b6c3492507_22_QF_UFDTLIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_56_QF_UFDTLIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_8_QF_UFDTNIA.smt2                 |    0.005s | 1512.0KiB| unset | 110 |  |  |
|44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFNIA.smt2      |    0.005s | 1476.0KiB| unset | 110 |  |  |
|52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFLIA.smt2      |    0.005s | 1372.0KiB| unset | 110 |  |  |
|93493_798593962ee29ad45ac8_52_QF_UFDTNIA.smt2                |    0.005s | 1524.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_57_QF_UFLIA.smt2                  |    0.005s | 1564.0KiB| unset | 110 |  |  |
|17512_5c1021b0faa6b6e1791b_19_QF_UFLIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|63058_aa742630eef64f949de269382c1f9035_25_UFNIA.smt2         |    0.005s | 1560.0KiB| unset | 110 |  |  |
|39657_1c7158801cd59dc13f05_44_QF_UFLIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|72771_f9d228efc97cf1458e38_64_QF_UFLIA.smt2                  |    0.005s | 1524.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_8_QF_UFLIA.smt2                   |    0.005s | 1560.0KiB| unset | 110 |  |  |
|72658_63104dadde9c6026353f_71_QF_UFDTNIA.smt2                |    0.005s | 1616.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFNIA.smt2      |    0.005s | 1564.0KiB| unset | 110 |  |  |
|44289_4066055e0f64d96da11a_14_QF_UFNIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_5_QF_UFLIA.smt2                   |    0.005s | 1564.0KiB| unset | 110 |  |  |
|41958_32933c5a1384696720a2_62_QF_UFLIA.smt2                  |    0.005s | 1556.0KiB| unset | 110 |  |  |
|63058_64ab9a7ef7b6c3492507_24_QF_UFDTNIA.smt2                |    0.005s | 1552.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_29_QF_UFDTLIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_7_QF_UFDTNIA.smt2                 |    0.005s | 1448.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_55_QF_UFDTNIA.smt2                |    0.005s | 1332.0KiB| unset | 110 |  |  |
|11775_ad46e5b8db4748c51973_42_QF_UFNIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_72_QF_UFDTLIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|44788_1965f0d6d94d5d8054ba_35_QF_UFDTLIA.smt2                |    0.005s | 1564.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_56_QF_UFNIA.smt2                  |    0.005s | 1552.0KiB| unset | 110 |  |  |
|63058_64ab9a7ef7b6c3492507_24_QF_UFNIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_41_QF_UFNIA.smt2                   |    0.005s | 1524.0KiB| unset | 110 |  |  |
|44788_1965f0d6d94d5d8054ba_34_QF_UFLIA.smt2                  |    0.005s | 1556.0KiB| unset | 110 |  |  |
|93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTLIA.smt2    |    0.005s | 1560.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_40_QF_UFDTLIA.smt2                 |    0.005s | 1564.0KiB| unset | 110 |  |  |
|63058_aa742630eef64f949de269382c1f9035_25_UFDTNIA.smt2       |    0.005s | 1560.0KiB| unset | 110 |  |  |
|38347_525a1ca0331f2bcbf520_54_QF_UFDTNIA.smt2                |    0.005s | 1556.0KiB| unset | 110 |  |  |
|11775_ad46e5b8db4748c51973_42_QF_UFDTLIA.smt2                |    0.005s | 1564.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFNIA.smt2      |    0.005s | 1560.0KiB| unset | 110 |  |  |
|93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTNIA.smt2    |    0.005s | 1564.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFNIA.smt2      |    0.005s | 1560.0KiB| unset | 110 |  |  |
|41958_32933c5a1384696720a2_62_QF_UFDTLIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTNIA.smt2    |    0.005s | 1560.0KiB| unset | 110 |  |  |
|44289_4066055e0f64d96da11a_14_QF_UFDTLIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_1_UFLIA.smt2                      |    0.005s | 1560.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_57_QF_UFDTLIA.smt2                |    0.005s | 1564.0KiB| unset | 110 |  |  |
|44289_4066055e0f64d96da11a_15_QF_UFNIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|44289_4066055e0f64d96da11a_14_QF_UFDTNIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_57_QF_UFDTNIA.smt2                |    0.005s | 1788.0KiB| unset | 110 |  |  |
|52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFNIA.smt2      |    0.005s | 1564.0KiB| unset | 110 |  |  |
|38347_525a1ca0331f2bcbf520_54_QF_UFNIA.smt2                  |    0.005s | 1564.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_6_QF_UFNIA.smt2                   |    0.005s | 1560.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_4_UFNIA.smt2                      |    0.005s | 1560.0KiB| unset | 110 |  |  |
|39657_1c7158801cd59dc13f05_44_QF_UFDTLIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTLIA.smt2    |    0.005s | 1560.0KiB| unset | 110 |  |  |
|93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTLIA.smt2    |    0.005s | 1556.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_58_QF_UFNIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|72771_f9d228efc97cf1458e38_64_QF_UFDTNIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_56_QF_UFDTNIA.smt2                |    0.005s | 1564.0KiB| unset | 110 |  |  |
|72658_63104dadde9c6026353f_71_QF_UFLIA.smt2                  |    0.005s | 1560.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_41_QF_UFDTNIA.smt2                 |    0.005s | 1560.0KiB| unset | 110 |  |  |
|44788_1965f0d6d94d5d8054ba_35_QF_UFDTNIA.smt2                |    0.005s | 1560.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_7_QF_UFNIA.smt2                   |    0.006s | 1560.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_39_QF_UFDTNIA.smt2                 |    0.006s | 1560.0KiB| unset | 110 |  |  |
|44788_1965f0d6d94d5d8054ba_34_QF_UFNIA.smt2                  |    0.006s | 1556.0KiB| unset | 110 |  |  |
|93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFLIA.smt2      |    0.006s | 1560.0KiB| unset | 110 |  |  |
|17512_5c1021b0faa6b6e1791b_21_QF_UFNIA.smt2                  |    0.006s | 1564.0KiB| unset | 110 |  |  |
|39657_2866defdd1f2434b69ab_48_QF_UFLIA.smt2                  |    0.006s | 1560.0KiB| unset | 110 |  |  |
|63058_64ab9a7ef7b6c3492507_22_QF_UFDTNIA.smt2                |    0.006s | 1568.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_5_QF_UFDTLIA.smt2                 |    0.006s | 1560.0KiB| unset | 110 |  |  |
|52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTNIA.smt2    |    0.006s | 1560.0KiB| unset | 110 |  |  |
|63058_64ab9a7ef7b6c3492507_23_QF_UFDTNIA.smt2                |    0.006s | 1552.0KiB| unset | 110 |  |  |
|39657_1c7158801cd59dc13f05_46_QF_UFNIA.smt2                  |    0.006s | 1560.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_4_UFDTNIA.smt2                    |    0.006s | 1576.0KiB| unset | 110 |  |  |
|39657_2866defdd1f2434b69ab_48_QF_UFNIA.smt2                  |    0.006s | 1556.0KiB| unset | 110 |  |  |
|39657_2866defdd1f2434b69ab_47_QF_UFDTLIA.smt2                |    0.006s | 1580.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTNIA.smt2    |    0.006s | 1560.0KiB| unset | 110 |  |  |
|41958_45c688a4814eb926c254_60_QF_UFLIA.smt2                  |    0.006s | 1560.0KiB| unset | 110 |  |  |
|39657_1c7158801cd59dc13f05_44_QF_UFDTNIA.smt2                |    0.006s | 1560.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_2_UFDTNIA.smt2                    |    0.006s | 1564.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_30_QF_UFDTNIA.smt2                  |    0.006s | 1552.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_56_QF_UFLIA.smt2                  |    0.006s | 1788.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_29_QF_UFNIA.smt2                    |    0.006s | 1556.0KiB| unset | 110 |  |  |
|52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTLIA.smt2    |    0.006s | 1516.0KiB| unset | 110 |  |  |
|30078_f817a923328f75af7e60_27_QF_UFDTLIA.smt2                |    0.006s | 1560.0KiB| unset | 110 |  |  |
|44788_1965f0d6d94d5d8054ba_36_QF_UFLIA.smt2                  |    0.006s | 1484.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_7_QF_UFLIA.smt2                   |    0.006s | 1560.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_55_QF_UFDTLIA.smt2                |    0.006s | 1560.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_32_QF_UFDTLIA.smt2                  |    0.006s | 1560.0KiB| unset | 110 |  |  |
|93493_798593962ee29ad45ac8_52_QF_UFNIA.smt2                  |    0.006s | 1376.0KiB| unset | 110 |  |  |
|44289_e5a2e5c780236919ee6a_17_QF_UFDTLIA.smt2                |    0.006s | 1560.0KiB| unset | 110 |  |  |
|44289_4066055e0f64d96da11a_14_QF_UFLIA.smt2                  |    0.006s | 1524.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_2_UFDTLIA.smt2                    |    0.006s | 1560.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_33_QF_UFNIA.smt2                    |    0.006s | 1560.0KiB| unset | 110 |  |  |
|93493_798593962ee29ad45ac8_52_QF_UFDTLIA.smt2                |    0.006s | 1552.0KiB| unset | 110 |  |  |
|44788_1965f0d6d94d5d8054ba_36_QF_UFDTNIA.smt2                |    0.006s | 1560.0KiB| unset | 110 |  |  |
|52759_b3ecd2335fd16ec2eee2_9_UFDTLIA.smt2                    |    0.006s | 1556.0KiB| unset | 110 |  |  |
|41958_45c688a4814eb926c254_60_QF_UFDTNIA.smt2                |    0.006s | 1560.0KiB| unset | 110 |  |  |
|44289_4066055e0f64d96da11a_15_QF_UFLIA.smt2                  |    0.006s | 1792.0KiB| unset | 110 |  |  |
|93493_5990a6bf5f2740164f77_50_QF_UFDTNIA.smt2                |    0.006s | 1560.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_2_UFNIA.smt2                      |    0.006s | 1564.0KiB| unset | 110 |  |  |
|63058_aa742630eef64f949de269382c1f9035_25_UFDTLIA.smt2       |    0.006s | 1560.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_41_QF_UFLIA.smt2                   |    0.006s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_72_QF_UFDTNIA.smt2                |    0.006s | 1560.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_55_QF_UFLIA.smt2                  |    0.006s | 1560.0KiB| unset | 110 |  |  |
|44289_e5a2e5c780236919ee6a_17_QF_UFNIA.smt2                  |    0.006s | 1560.0KiB| unset | 110 |  |  |
|52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2    |    0.006s | 1560.0KiB| unset | 110 |  |  |
|17512_5c1021b0faa6b6e1791b_21_QF_UFDTLIA.smt2                |    0.006s | 1560.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_0_UFDTNIA.smt2                    |    0.006s | 1560.0KiB| unset | 110 |  |  |
|17512_5c1021b0faa6b6e1791b_20_QF_UFNIA.smt2                  |    0.006s | 1560.0KiB| unset | 110 |  |  |
|52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTNIA.smt2    |    0.006s | 1560.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_58_QF_UFDTLIA.smt2                |    0.006s | 1560.0KiB| unset | 110 |  |  |
|17512_5c1021b0faa6b6e1791b_20_QF_UFLIA.smt2                  |    0.006s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_73_QF_UFDTLIA.smt2                |    0.006s | 1528.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_31_QF_UFNIA.smt2                    |    0.006s | 1560.0KiB| unset | 110 |  |  |
|52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFNIA.smt2      |    0.006s | 1560.0KiB| unset | 110 |  |  |
|93493_798593962ee29ad45ac8_52_QF_UFLIA.smt2                  |    0.006s | 1528.0KiB| unset | 110 |  |  |
|11775_ad46e5b8db4748c51973_42_QF_UFDTNIA.smt2                |    0.006s | 1564.0KiB| unset | 110 |  |  |
|72658_63104dadde9c6026353f_70_QF_UFLIA.smt2                  |    0.006s | 1540.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_3_UFDTNIA.smt2                    |    0.006s | 1560.0KiB| unset | 110 |  |  |
|11775_ad46e5b8db4748c51973_43_QF_UFLIA.smt2                  |    0.006s | 1560.0KiB| unset | 110 |  |  |
|39657_2866defdd1f2434b69ab_47_QF_UFLIA.smt2                  |    0.006s | 1480.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_3_UFNIA.smt2                      |    0.006s | 1560.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_41_QF_UFDTLIA.smt2                 |    0.006s | 1356.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_30_QF_UFLIA.smt2                    |    0.006s | 1560.0KiB| unset | 110 |  |  |
|17512_5c1021b0faa6b6e1791b_20_QF_UFDTNIA.smt2                |    0.006s | 1576.0KiB| unset | 110 |  |  |
|72658_63104dadde9c6026353f_70_QF_UFDTLIA.smt2                |    0.006s | 1552.0KiB| unset | 110 |  |  |
|72658_63104dadde9c6026353f_71_QF_UFDTLIA.smt2                |    0.006s | 1576.0KiB| unset | 110 |  |  |
|39657_1c7158801cd59dc13f05_45_QF_UFNIA.smt2                  |    0.006s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_73_QF_UFDTNIA.smt2                |    0.006s | 1564.0KiB| unset | 110 |  |  |
|41958_32933c5a1384696720a2_63_QF_UFNIA.smt2                  |    0.006s | 1548.0KiB| unset | 110 |  |  |
|41958_32933c5a1384696720a2_61_QF_UFDTLIA.smt2                |    0.006s | 1544.0KiB| unset | 110 |  |  |
|39657_1c7158801cd59dc13f05_45_QF_UFDTLIA.smt2                |    0.006s | 1560.0KiB| unset | 110 |  |  |
|41958_32933c5a1384696720a2_62_QF_UFDTNIA.smt2                |    0.006s | 1788.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_0_UFLIA.smt2                      |    0.006s | 1556.0KiB| unset | 110 |  |  |
|39657_2866defdd1f2434b69ab_48_QF_UFDTNIA.smt2                |    0.006s | 1564.0KiB| unset | 110 |  |  |
|44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTNIA.smt2    |    0.006s | 1560.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_7_QF_UFDTLIA.smt2                 |    0.006s | 1560.0KiB| unset | 110 |  |  |
|41958_32933c5a1384696720a2_61_QF_UFDTNIA.smt2                |    0.006s | 1560.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_33_QF_UFDTNIA.smt2                  |    0.006s | 1552.0KiB| unset | 110 |  |  |
|52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTLIA.smt2    |    0.006s | 1560.0KiB| unset | 110 |  |  |
|44289_e5a2e5c780236919ee6a_17_QF_UFLIA.smt2                  |    0.006s | 1340.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_39_QF_UFDTLIA.smt2                 |    0.007s | 1560.0KiB| unset | 110 |  |  |
|39657_1c7158801cd59dc13f05_46_QF_UFDTNIA.smt2                |    0.007s | 1436.0KiB| unset | 110 |  |  |
|44289_e5a2e5c780236919ee6a_18_QF_UFDTLIA.smt2                |    0.007s | 1564.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_30_QF_UFDTLIA.smt2                  |    0.007s | 1560.0KiB| unset | 110 |  |  |
|72771_f9d228efc97cf1458e38_64_QF_UFDTLIA.smt2                |    0.007s | 1560.0KiB| unset | 110 |  |  |
|39657_1c7158801cd59dc13f05_44_QF_UFNIA.smt2                  |    0.007s | 1556.0KiB| unset | 110 |  |  |
|39657_2866defdd1f2434b69ab_48_QF_UFDTLIA.smt2                |    0.007s | 1812.0KiB| unset | 110 |  |  |
|3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFLIA.smt2       |    0.007s | 1560.0KiB| unset | 110 |  |  |
|940_590f27b1c3c800d3243e_29_QF_UFDTNIA.smt2                  |    0.007s | 1556.0KiB| unset | 110 |  |  |
|63058_55d6bef5390186355f11_26_QF_UFDTNIA.smt2                |    0.007s | 1568.0KiB| unset | 110 |  |  |
|11775_ad46e5b8db4748c51973_43_QF_UFNIA.smt2                  |    0.007s | 1556.0KiB| unset | 110 |  |  |
|44788_1965f0d6d94d5d8054ba_36_QF_UFDTLIA.smt2                |    0.007s | 1420.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_6_QF_UFDTNIA.smt2                 |    0.007s | 1560.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_76_QF_UFDTNIA.smt2                |    0.007s | 1388.0KiB| unset | 110 |  |  |
|30078_f817a923328f75af7e60_28_QF_UFDTNIA.smt2                |    0.007s | 1552.0KiB| unset | 110 |  |  |
|66603_accdadf23a1cf70ae043_75_QF_UFDTLIA.smt2                |    0.007s | 1412.0KiB| unset | 110 |  |  |
|38347_092cc73601c78e45f4f9_57_QF_UFNIA.smt2                  |    0.007s | 1564.0KiB| unset | 110 |  |  |
|41958_32933c5a1384696720a2_61_QF_UFLIA.smt2                  |    0.007s | 1384.0KiB| unset | 110 |  |  |
|3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTLIA.smt2     |    0.007s | 1564.0KiB| unset | 110 |  |  |
|63058_64ab9a7ef7b6c3492507_24_QF_UFDTLIA.smt2                |    0.007s | 1560.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFNIA.smt2      |    0.007s | 1556.0KiB| unset | 110 |  |  |
|83314_a702bf8b823398c9e37a_3_UFLIA.smt2                      |    0.008s | 1472.0KiB| unset | 110 |  |  |
|52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTNIA.smt2    |    0.008s | 1560.0KiB| unset | 110 |  |  |
|72771_f9d228efc97cf1458e38_64_QF_UFNIA.smt2                  |    0.008s | 1560.0KiB| unset | 110 |  |  |
|17512_5c1021b0faa6b6e1791b_21_QF_UFDTNIA.smt2                |    0.008s | 1560.0KiB| unset | 110 |  |  |
|44289_e5a2e5c780236919ee6a_18_QF_UFDTNIA.smt2                |    0.008s | 1560.0KiB| unset | 110 |  |  |
|41958_32933c5a1384696720a2_63_QF_UFLIA.smt2                  |    0.008s | 1432.0KiB| unset | 110 |  |  |
|44788_1965f0d6d94d5d8054ba_35_QF_UFNIA.smt2                  |    0.008s | 1480.0KiB| unset | 110 |  |  |
|3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTNIA.smt2     |    0.008s | 1412.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTNIA.smt2    |    0.008s | 1472.0KiB| unset | 110 |  |  |
|39657_2866defdd1f2434b69ab_47_QF_UFNIA.smt2                  |    0.008s | 1560.0KiB| unset | 110 |  |  |
|25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTNIA.smt2    |    0.009s | 1564.0KiB| unset | 110 |  |  |
|93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFNIA.smt2      |    0.009s | 1564.0KiB| unset | 110 |  |  |
|65782_cd31513fdcd15701933b_6_QF_UFDTLIA.smt2                 |    0.009s | 1448.0KiB| unset | 110 |  |  |
|72658_63104dadde9c6026353f_70_QF_UFNIA.smt2                  |    0.010s | 1556.0KiB| unset | 110 |  |  |
|3106_1c933134166dbad31f79_40_QF_UFNIA.smt2                   |    0.011s | 1560.0KiB| unset | 110 |  |  |