# data * SAT 267 * UNSAT 0 * TIMEOUT 0 * UNKNOWN 0 * UNSET 0 * ERROR 2 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: smt-clausal-lookahead-60-qfufnia-sat
Z3 repo: https://github.com/Z3Prover/z3
Z3 commit: d3bf25ce856f3ea316b69e82dd762f907dbd8e4b
Z3 branch: master
Z3 options: "-T:60 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify smt)" smt.sls.enable=true smt.sls.parallel=false model_validate=true sls.arith_use_clausal_lookahead=true"
Z3 inputs: inputs/QF_UFNIA_SAT
Z3 commit message: throttle value smt -> sls
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |00003.smt2 | 0.015s | 52.352MiB| sat | 0 | | | |qf_AndOrXor_2417_values_0.smt2 | 0.015s | 52.464MiB| sat | 0 | | | |qf_AndOrXor_716_values_0.smt2 | 0.015s | 52.404MiB| sat | 0 | | | |qf_AndOrXor_2285_values_0.smt2 | 0.016s | 52.448MiB| sat | 0 | | | |qf_AndOrXor_2263_values_0.smt2 | 0.017s | 52.564MiB| sat | 0 | | | |00005.smt2 | 0.017s | 52.412MiB| sat | 0 | | | |int_check_ne_bvlshr1_ltr_inv_g.smt2 | 0.017s | 52.924MiB| sat | 0 | | | |qf_AndOrXor_2063_values_0.smt2 | 0.018s | 52.56MiB| sat | 0 | | | |00002.smt2 | 0.018s | 52.552MiB| sat | 0 | | | |qf_AndOrXor_1733_values_0.smt2 | 0.018s | 52.352MiB| sat | 0 | | | |qf_AddSub_1564_values_0.smt2 | 0.018s | 53.432MiB| sat | 0 | | | |00251.smt2 | 0.018s | 52.364MiB| sat | 0 | | | |qf_AndOrXor_144_values_0.smt2 | 0.019s | 52.488MiB| sat | 0 | | | |qf_AndOrXor_757_values_0.smt2 | 0.019s | 52.524MiB| sat | 0 | | | |qf_AndOrXor_709_values_0.smt2 | 0.019s | 52.424MiB| sat | 0 | | | |int_check_ne_bvneg_ltr_inv_g.smt2 | 0.019s | 52.772MiB| sat | 0 | | | |qf_AndOrXor_135_values_0.smt2 | 0.019s | 52.436MiB| sat | 0 | | | |int_check_bvsgt_bvneg_rtl.smt2 | 0.019s | 53.296MiB| sat | 0 | | | |qf_Select_423_values_57.smt2 | 0.020s | 53.076MiB| sat | 0 | | | |qf_AndOrXor_1253_values_0.smt2 | 0.020s | 52.428MiB| sat | 0 | | | |int_check_bvsle_bvand_ltr_inv_g.smt2 | 0.021s | 52.82MiB| sat | 0 | | | |int_check_bvsge_bvmul_rtl.smt2 | 0.021s | 53.252MiB| sat | 0 | | | |int_check_bvsgt_bvand_rtl.smt2 | 0.022s | 53.056MiB| sat | 0 | | | |int_check_bvsgt_bvneg_ltr_inv_g.smt2 | 0.022s | 53.26MiB| sat | 0 | | | |qf_Select_430_values_60.smt2 | 0.022s | 53.084MiB| sat | 0 | | | |int_check_ne_bvand_ltr_inv_g.smt2 | 0.022s | 52.496MiB| sat | 0 | | | |00194.smt2 | 0.022s | 52.56MiB| sat | 0 | | | |qf_AndOrXor_2430_values_0.smt2 | 0.022s | 52.42MiB| sat | 0 | | | |int_check_bvule_bvlshr0_ltr_inv_g.smt2 | 0.023s | 53.044MiB| sat | 0 | | | |qf_AndOrXor_1230_values_0.smt2 | 0.023s | 52.58MiB| sat | 0 | | | |int_check_bvslt_bvudiv0_rtl.smt2 | 0.023s | 53.244MiB| sat | 0 | | | |00020.smt2 | 0.023s | 52.436MiB| sat | 0 | | | |int_check_bvule_bvudiv1_rtl.smt2 | 0.023s | 52.732MiB| sat | 0 | | | |qf_AndOrXor_2113_values_0.smt2 | 0.024s | 52.58MiB| sat | 0 | | | |qf_AndOrXor_2486_values_0.smt2 | 0.024s | 53.184MiB| sat | 0 | | | |int_check_eq_bvand_rtl.smt2 | 0.024s | 52.456MiB| sat | 0 | | | |int_check_ne_bvand_rtl.smt2 | 0.024s | 52.516MiB| sat | 0 | | | |int_check_ne_bvor_ltr_inv_g.smt2 | 0.024s | 52.448MiB| sat | 0 | | | |int_check_bvuge_bvmul_rtl.smt2 | 0.024s | 52.972MiB| sat | 0 | | | |qf_AndOrXor_2658_values_0.smt2 | 0.024s | 52.376MiB| sat | 0 | | | |int_check_bvsle_bvurem0_rtl.smt2 | 0.024s | 53.32MiB| sat | 0 | | | |int_check_bvslt_bvnot_rtl.smt2 | 0.024s | 53.068MiB| sat | 0 | | | |qf_Select_747_values_0.smt2 | 0.024s | 53.284MiB| sat | 0 | | | |int_check_bvslt_bvadd_rtl.smt2 | 0.024s | 53.072MiB| sat | 0 | | | |qf_AndOrXor_2118_values_0.smt2 | 0.024s | 52.576MiB| sat | 0 | | | |qf_AndOrXor_1241_values_0.smt2 | 0.024s | 52.56MiB| sat | 0 | | | |int_check_bvsgt_bvadd_ltr_inv_r.smt2 | 0.024s | 53.012MiB| sat | 0 | | | |qf_AndOrXor_2247_values_0.smt2 | 0.025s | 52.588MiB| sat | 0 | | | |int_check_ne_bvshl1_ltr_inv_g.smt2 | 0.025s | 52.82MiB| sat | 0 | | | |int_check_bvugt_bvor_rtl.smt2 | 0.025s | 52.524MiB| sat | 0 | | | |qf_AndOrXor_745_values_0.smt2 | 0.025s | 52.448MiB| sat | 0 | | | |qf_AndOrXor_2607_values_0.smt2 | 0.025s | 52.368MiB| sat | 0 | | | |qf_AndOrXor_827_values_0.smt2 | 0.025s | 52.58MiB| sat | 0 | | | |qf_AndOrXor_1795_values_0.smt2 | 0.025s | 52.816MiB| sat | 0 | | | |qf_AndOrXor_151_values_0.smt2 | 0.025s | 52.5MiB| sat | 0 | | | |qf_AndOrXor_2188_values_0.smt2 | 0.025s | 52.564MiB| sat | 0 | | | |00149.smt2 | 0.025s | 52.44MiB| sat | 0 | | | |00967.smt2 | 0.025s | 52.528MiB| sat | 0 | | | |qf_AndOrXor_516_values_0.smt2 | 0.025s | 53.168MiB| sat | 0 | | | |int_check_bvslt_bvor_rtl.smt2 | 0.025s | 53.072MiB| sat | 0 | | | |int_check_bvuge_bvand_ltr_inv_g.smt2 | 0.025s | 52.56MiB| sat | 0 | | | |int_check_bvult_bvor_rtl.smt2 | 0.025s | 52.448MiB| sat | 0 | | | |int_check_bvugt_bvand_ltr_inv_g.smt2 | 0.025s | 52.44MiB| sat | 0 | | | |int_check_bvule_bvudiv0_ltr_inv_g.smt2 | 0.026s | 52.892MiB| sat | 0 | | | |qf_AndOrXor_732-2_values_0.smt2 | 0.026s | 52.588MiB| sat | 0 | | | |qf_AndOrXor_2627_values_0.smt2 | 0.026s | 52.416MiB| sat | 0 | | | |int_check_bvuge_bvor_ltr_inv_g.smt2 | 0.026s | 52.532MiB| sat | 0 | | | |qf_AndOrXor_2231_values_0.smt2 | 0.026s | 52.6MiB| sat | 0 | | | |qf_Select_576b_values_0.smt2 | 0.026s | 53.532MiB| sat | 0 | | | |int_check_bvugt_bvlshr0_rtl.smt2 | 0.026s | 53.116MiB| sat | 0 | | | |qf_AndOrXor_1864_values_0.smt2 | 0.026s | 53.288MiB| sat | 0 | | | |qf_InstCombineShift279_values_0.smt2 | 0.026s | 53.224MiB| sat | 0 | | | |int_check_bvult_bvand_ltr_inv_g.smt2 | 0.026s | 52.456MiB| sat | 0 | | | |int_check_eq_bvmul_rtl.smt2 | 0.026s | 52.996MiB| sat | 0 | | | |00104.smt2 | 0.026s | 52.792MiB| sat | 0 | | | |qf_AndOrXor_1979_values_0.smt2 | 0.026s | 52.632MiB| sat | 0 | | | |int_check_bvsge_bvor_ltr_inv_g.smt2 | 0.026s | 53.136MiB| sat | 0 | | | |qf_AndOrXor_1280_values_0.smt2 | 0.026s | 52.348MiB| sat | 0 | | | |qf_AndOrXor_819_values_0.smt2 | 0.026s | 53.072MiB| sat | 0 | | | |int_check_bvule_bvlshr1_ltr_inv_g.smt2 | 0.026s | 52.988MiB| sat | 0 | | | |int_check_bvslt_bvor_ltr_inv_g.smt2 | 0.026s | 53.228MiB| sat | 0 | | | |int_check_bvsgt_bvadd_ltr_inv_g.smt2 | 0.026s | 53.348MiB| sat | 0 | | | |int_check_bvule_bvand_ltr_inv_g.smt2 | 0.026s | 52.564MiB| sat | 0 | | | |int_check_bvult_bvand_rtl.smt2 | 0.026s | 52.396MiB| sat | 0 | | | |qf_AndOrXor_2297_values_0.smt2 | 0.027s | 52.46MiB| sat | 0 | | | |int_check_bvugt_bvor_ltr_inv_g.smt2 | 0.027s | 52.468MiB| sat | 0 | | | |int_check_bvuge_bvand_rtl.smt2 | 0.027s | 52.396MiB| sat | 0 | | | |int_check_bvult_bvudiv1_rtl.smt2 | 0.027s | 52.952MiB| sat | 0 | | | |int_check_eq_bvurem1_ltr_inv_g.smt2 | 0.027s | 53.46MiB| sat | 0 | | | |qf_AndOrXor_2123_values_0.smt2 | 0.027s | 52.46MiB| sat | 0 | | | |int_check_bvslt_bvudiv1_rtl.smt2 | 0.027s | 53.38MiB| sat | 0 | | | |int_check_bvsge_bvnot_ltr_inv_g.smt2 | 0.027s | 52.868MiB| sat | 0 | | | |qf_AndOrXor_537_values_0.smt2 | 0.027s | 53.032MiB| sat | 0 | | | |qf_Select_420_values_0.smt2 | 0.027s | 52.812MiB| sat | 0 | | | |00105.smt2 | 0.027s | 52.684MiB| sat | 0 | | | |qf_AndOrXor_1294_values_0.smt2 | 0.027s | 52.54MiB| sat | 0 | | | |int_check_bvsle_bvnot_ltr_inv_g.smt2 | 0.028s | 52.888MiB| sat | 0 | | | |n0-00001.smt2 | 0.028s | 52.348MiB| sat | 0 | | | |00247.smt2 | 0.028s | 52.304MiB| sat | 0 | | | |int_check_ne_bvor_rtl.smt2 | 0.028s | 52.62MiB| sat | 0 | | | |int_check_bvsgt_bvnot_rtl.smt2 | 0.028s | 52.856MiB| sat | 0 | | | |int_check_bvule_bvudiv0_rtl.smt2 | 0.028s | 53.012MiB| sat | 0 | | | |qf_AndOrXor_2595_values_0.smt2 | 0.028s | 52.528MiB| sat | 0 | | | |00102.smt2 | 0.028s | 52.488MiB| sat | 0 | | | |qf_AndOrXor_2367_values_0.smt2 | 0.028s | 52.504MiB| sat | 0 | | | |qf_AndOrXor_2475_values_0.smt2 | 0.028s | 53.352MiB| sat | 0 | | | |00294.smt2 | 0.028s | 52.46MiB| sat | 0 | | | |int_check_bvsle_bvor_rtl.smt2 | 0.028s | 53.068MiB| sat | 0 | | | |int_check_ne_bvadd_ltr_inv_r.smt2 | 0.028s | 52.976MiB| sat | 0 | | | |00428.smt2 | 0.028s | 52.948MiB| sat | 0 | | | |int_check_bvsle_bvadd_ltr_inv_r.smt2 | 0.028s | 53.008MiB| sat | 0 | | | |qf_AndOrXor_698_values_0.smt2 | 0.028s | 52.44MiB| sat | 0 | | | |qf_AndOrXor_2647_values_0.smt2 | 0.028s | 52.496MiB| sat | 0 | | | |int_check_bvsle_bvurem0_ltr_inv_g.smt2 | 0.028s | 53.34MiB| sat | 0 | | | |int_check_ne_bvnot_ltr_inv_g.smt2 | 0.029s | 52.516MiB| sat | 0 | | | |01052.smt2 | 0.029s | 52.352MiB| sat | 0 | | | |qf_AndOrXor_1247_values_0.smt2 | 0.029s | 52.416MiB| sat | 0 | | | |int_check_bvslt_bvnot_ltr_inv_g.smt2 | 0.029s | 52.768MiB| sat | 0 | | | |00402.smt2 | 0.029s | 52.816MiB| sat | 0 | | | |qf_AddSub_1624_values_0.smt2 | 0.029s | 52.804MiB| sat | 0 | | | |int_check_bvsle_bvand_rtl.smt2 | 0.029s | 53.056MiB| sat | 0 | | | |qf_AndOrXor_1012_values_0.smt2 | 0.029s | 53.148MiB| sat | 0 | | | |00413.smt2 | 0.029s | 53.196MiB| sat | 0 | | | |int_check_bvuge_bvurem1_ltr_inv_g.smt2 | 0.029s | 53.048MiB| sat | 0 | | | |qf_InstCombineShift239_values_0.smt2 | 0.029s | 53.196MiB| sat | 0 | | | |int_check_ne_bvashr1_ltr_inv_r.smt2 | 0.029s | 53.476MiB| sat | 0 | | | |int_check_bvsgt_bvor_ltr_inv_g.smt2 | 0.029s | 52.988MiB| sat | 0 | | | |00324.smt2 | 0.029s | 52.692MiB| sat | 0 | | | |int_check_bvult_bvudiv1_ltr_inv_g.smt2 | 0.029s | 53.304MiB| sat | 0 | | | |int_check_bvsle_bvor_ltr_inv_g.smt2 | 0.029s | 53.004MiB| sat | 0 | | | |qf_AndOrXor_2243_values_0.smt2 | 0.030s | 52.524MiB| sat | 0 | | | |qf_AndOrXor_1288_values_0.smt2 | 0.030s | 52.56MiB| sat | 0 | | | |qf_AddSub_1560_values_0.smt2 | 0.030s | 52.876MiB| sat | 0 | | | |qf_AndOrXor_523_values_0.smt2 | 0.030s | 53.192MiB| sat | 0 | | | |qf_Select_433_values_0.smt2 | 0.030s | 53.136MiB| sat | 0 | | | |qf_AddSub_1599_values_0.smt2 | 0.030s | 53.708MiB| sat | 0 | | | |qf_AndOrXor_2052_values_0.smt2 | 0.030s | 52.62MiB| sat | 0 | | | |00415.smt2 | 0.030s | 52.988MiB| sat | 0 | | | |int_check_bvsle_bvshl1_rtl.smt2 | 0.030s | 53.304MiB| sat | 0 | | | |qf_AddSub_1040_values_0.smt2 | 0.030s | 53.028MiB| sat | 0 | | | |00314.smt2 | 0.030s | 53.612MiB| sat | 0 | | | |int_check_bvsgt_bvor_rtl.smt2 | 0.031s | 52.912MiB| sat | 0 | | | |int_check_bvuge_bvurem1_rtl.smt2 | 0.031s | 53.312MiB| sat | 0 | | | |int_check_bvsgt_bvmul_rtl.smt2 | 0.031s | 53.232MiB| sat | 0 | | | |qf_AndOrXor_2581_values_0.smt2 | 0.031s | 52.368MiB| sat | 0 | | | |int_check_ne_bvadd_ltr_inv_g.smt2 | 0.031s | 52.916MiB| sat | 0 | | | |00243.smt2 | 0.031s | 52.42MiB| sat | 0 | | | |qf_AndOrXor_2008_values_0.smt2 | 0.031s | 52.592MiB| sat | 0 | | | |int_check_bvsge_bvand_ltr_inv_g.smt2 | 0.031s | 53.076MiB| sat | 0 | | | |qf_InstCombineShift440_values_0.smt2 | 0.031s | 53.2MiB| sat | 0 | | | |int_check_bvslt_bvand_rtl.smt2 | 0.031s | 53.168MiB| sat | 0 | | | |00304.smt2 | 0.031s | 54.796MiB| sat | 0 | | | |qf_AndOrXor_2515_values_0.smt2 | 0.031s | 53.336MiB| sat | 0 | | | |int_check_bvsgt_bvashr1_rtl.smt2 | 0.031s | 53.616MiB| sat | 0 | | | |qf_AddSub_1295_values_0.smt2 | 0.031s | 52.896MiB| sat | 0 | | | |int_check_bvugt_bvand_rtl.smt2 | 0.032s | 52.488MiB| sat | 0 | | | |int_check_bvslt_bvadd_ltr_inv_r.smt2 | 0.032s | 53.076MiB| sat | 0 | | | |int_check_bvsge_bvor_rtl.smt2 | 0.032s | 53.072MiB| sat | 0 | | | |qf_AddSub_1043_values_0.smt2 | 0.032s | 53.196MiB| sat | 0 | | | |int_check_bvugt_bvmul_rtl.smt2 | 0.032s | 53.028MiB| sat | 0 | | | |int_check_bvsge_bvshl0_rtl.smt2 | 0.032s | 53.28MiB| sat | 0 | | | |int_check_eq_bvor_rtl.smt2 | 0.032s | 52.628MiB| sat | 0 | | | |int_check_bvsgt_bvnot_ltr_inv_g.smt2 | 0.032s | 52.836MiB| sat | 0 | | | |00249.smt2 | 0.033s | 52.56MiB| sat | 0 | | | |int_check_bvsle_bvshl0_rtl.smt2 | 0.033s | 53.436MiB| sat | 0 | | | |qf_AndOrXor_2265_values_0.smt2 | 0.033s | 52.536MiB| sat | 0 | | | |int_check_bvsgt_bvurem0_ltr_inv_g.smt2 | 0.033s | 53.62MiB| sat | 0 | | | |int_check_ne_bvashr1_rtl.smt2 | 0.033s | 53.304MiB| sat | 0 | | | |qf_AndOrXor_2284_values_0.smt2 | 0.033s | 52.432MiB| sat | 0 | | | |00085.smt2 | 0.033s | 52.42MiB| sat | 0 | | | |int_check_bvuge_bvlshr0_ltr_inv_g.smt2 | 0.033s | 53.308MiB| sat | 0 | | | |qf_AndOrXor_732-1_values_0.smt2 | 0.034s | 52.484MiB| sat | 0 | | | |int_check_bvule_bvashr1_ltr_inv_g.smt2 | 0.034s | 53.316MiB| sat | 0 | | | |qf_AddSub_1604_values_0.smt2 | 0.035s | 53.668MiB| sat | 0 | | | |00035.smt2 | 0.035s | 52.516MiB| sat | 0 | | | |00235.smt2 | 0.035s | 52.436MiB| sat | 0 | | | |int_check_bvsge_bvashr0_rtl.smt2 | 0.035s | 53.7MiB| sat | 0 | | | |qf_AndOrXor_2617_values_0.smt2 | 0.035s | 52.472MiB| sat | 0 | | | |int_check_bvsge_bvand_rtl.smt2 | 0.035s | 53.416MiB| sat | 0 | | | |int_check_bvslt_bvneg_ltr_inv_g.smt2 | 0.036s | 53.168MiB| sat | 0 | | | |int_check_bvule_bvor_ltr_inv_g.smt2 | 0.036s | 52.56MiB| sat | 0 | | | |int_check_ne_bvshl0_rtl.smt2 | 0.036s | 52.992MiB| sat | 0 | | | |int_check_eq_bvurem1_rtl.smt2 | 0.036s | 53.42MiB| sat | 0 | | | |qf_AndOrXor_280_values_3.smt2 | 0.036s | 53.352MiB| sat | 0 | | | |int_check_bvslt_bvshl1_rtl.smt2 | 0.037s | 53.38MiB| sat | 0 | | | |int_check_bvsgt_bvlshr0_ltr_inv_r.smt2 | 0.037s | 53.576MiB| sat | 0 | | | |int_check_bvslt_bvurem0_rtl.smt2 | 0.037s | 53.216MiB| sat | 0 | | | |int_check_bvsle_bvneg_ltr_inv_g.smt2 | 0.037s | 53.176MiB| sat | 0 | | | |int_check_bvsgt_bvand_ltr_inv_g.smt2 | 0.037s | 52.9MiB| sat | 0 | | | |qf_AndOrXor_2160_values_0.smt2 | 0.038s | 52.704MiB| sat | 0 | | | |qf_Select_576a_values_0.smt2 | 0.039s | 53.688MiB| sat | 0 | | | |qf_Select_704_values_0.smt2 | 0.039s | 52.916MiB| sat | 0 | | | |int_check_bvsgt_bvudiv0_rtl.smt2 | 0.039s | 53.576MiB| sat | 0 | | | |int_check_bvslt_bvneg_rtl.smt2 | 0.039s | 53.084MiB| sat | 0 | | | |int_check_ne_bvlshr0_rtl.smt2 | 0.042s | 53.024MiB| sat | 0 | | | |int_check_bvugt_bvlshr1_rtl.smt2 | 0.044s | 53.248MiB| sat | 0 | | | |int_check_bvslt_bvurem1_ltr_inv_g.smt2 | 0.046s | 53.476MiB| sat | 0 | | | |int_check_bvsle_bvudiv1_rtl.smt2 | 0.046s | 53.632MiB| sat | 0 | | | |00018.smt2 | 0.048s | 54.24MiB| sat | 0 | | | |int_check_ne_bvlshr1_rtl.smt2 | 0.048s | 53.056MiB| sat | 0 | | | |int_check_bvsle_bvurem1_rtl.smt2 | 0.050s | 53.46MiB| sat | 0 | | | |int_check_bvult_bvor_ltr_inv_g.smt2 | 0.050s | 52.496MiB| sat | 0 | | | |int_check_bvslt_bvurem1_rtl.smt2 | 0.050s | 53.424MiB| sat | 0 | | | |int_check_bvuge_bvudiv0_rtl.smt2 | 0.051s | 53.124MiB| sat | 0 | | | |int_check_bvult_bvlshr1_ltr_inv_g.smt2 | 0.051s | 53.06MiB| sat | 0 | | | |qf_AndOrXor_2416_values_0.smt2 | 0.052s | 52.468MiB| sat | 0 | | | |qf_Select_427_values_0.smt2 | 0.053s | 52.932MiB| sat | 0 | | | |int_check_bvule_bvor_rtl.smt2 | 0.053s | 52.62MiB| sat | 0 | | | |qf_AndOrXor_2587_values_0.smt2 | 0.053s | 52.436MiB| sat | 0 | | | |qf_AndOrXor_2429_values_0.smt2 | 0.054s | 52.364MiB| sat | 0 | | | |int_check_bvsge_bvlshr0_ltr_inv_r.smt2 | 0.055s | 53.332MiB| sat | 0 | | | |int_check_bvule_bvshl1_ltr_inv_g.smt2 | 0.056s | 52.824MiB| sat | 0 | | | |qf_AndOrXor_2264_values_0.smt2 | 0.056s | 52.56MiB| sat | 0 | | | |qf_AddSub_1202_values_0.smt2 | 0.056s | 53.268MiB| sat | 0 | | | |int_check_bvuge_bvashr0_ltr_inv_g.smt2 | 0.057s | 53.384MiB| sat | 0 | | | |int_check_bvslt_bvurem0_ltr_inv_r.smt2 | 0.057s | 53.28MiB| sat | 0 | | | |qf_AndOrXor_363_values_0.smt2 | 0.057s | 53.232MiB| sat | 0 | | | |qf_AndOrXor_530_values_0.smt2 | 0.057s | 52.876MiB| sat | 0 | | | |int_check_bvsle_bvlshr1_ltr_inv_g.smt2 | 0.057s | 53.376MiB| sat | 0 | | | |qf_InstCombineShift476_values_0.smt2 | 0.058s | 53.268MiB| sat | 0 | | | |int_check_bvult_bvshl1_ltr_inv_g.smt2 | 0.058s | 52.82MiB| sat | 0 | | | |int_check_bvslt_bvadd_ltr_inv_g.smt2 | 0.060s | 53.04MiB| sat | 0 | | | |qf_AndOrXor_273_values_7.smt2 | 0.060s | 53.188MiB| sat | 0 | | | |qf_AndOrXor_364_values_0.smt2 | 0.060s | 53.248MiB| sat | 0 | | | |int_check_bvsgt_bvurem1_ltr_inv_g.smt2 | 0.061s | 53.908MiB| sat | 0 | | | |qf_AndOrXor_298_values_0.smt2 | 0.061s | 53.488MiB| sat | 0 | | | |int_check_bvsge_bvudiv0_rtl.smt2 | 0.061s | 53.72MiB| sat | 0 | | | |int_check_ne_bvurem0_ltr_inv_g.smt2 | 0.062s | 53.136MiB| sat | 0 | | | |int_check_bvult_bvlshr0_ltr_inv_g.smt2 | 0.062s | 53.084MiB| sat | 0 | | | |int_check_bvsle_bvurem1_ltr_inv_r.smt2 | 0.062s | 53.56MiB| sat | 0 | | | |int_check_bvslt_bvand_ltr_inv_g.smt2 | 0.063s | 53.464MiB| sat | 0 | | | |qf_AndOrXor_937_values_0.smt2 | 0.065s | 53.372MiB| sat | 0 | | | |int_check_bvsge_bvadd_ltr_inv_r.smt2 | 0.065s | 53.484MiB| sat | 0 | | | |int_check_bvsle_bvlshr1_rtl.smt2 | 0.070s | 53.488MiB| sat | 0 | | | |int_check_bvslt_bvlshr1_rtl.smt2 | 0.074s | 53.356MiB| sat | 0 | | | |int_check_bvsge_bvurem0_rtl.smt2 | 0.074s | 53.52MiB| sat | 0 | | | |int_check_ne_bvlshr0_ltr_inv_g.smt2 | 0.079s | 53.148MiB| sat | 0 | | | |00379.smt2 | 0.084s | 55.04MiB| sat | 1 | | | |int_check_bvuge_bvlshr1_rtl.smt2 | 0.085s | 53.404MiB| sat | 0 | | | |int_check_bvsge_bvurem0_ltr_inv_g.smt2 | 0.086s | 53.516MiB| sat | 0 | | | |int_check_bvslt_bvmul_rtl.smt2 | 0.086s | 54.024MiB| sat | 0 | | | |int_check_bvsge_bvshl0_ltr_inv_g.smt2 | 0.087s | 53.424MiB| sat | 1 | | | |int_check_eq_bvshl0_rtl.smt2 | 0.089s | 53.26MiB| sat | 0 | | | |00793.smt2 | 0.091s | 58.344MiB| sat | 0 | | | |int_check_bvsge_bvashr0_ltr_inv_g.smt2 | 0.095s | 53.828MiB| sat | 0 | | | |int_check_bvule_bvashr1_rtl.smt2 | 0.097s | 53.628MiB| sat | 0 | | | |int_check_bvuge_bvlshr0_rtl.smt2 | 0.100s | 53.288MiB| sat | 0 | | | |int_check_bvsle_bvlshr0_rtl.smt2 | 0.102s | 53.572MiB| sat | 0 | | | |int_check_bvslt_bvshl0_rtl.smt2 | 0.105s | 53.8MiB| sat | 0 | | | |int_check_bvsgt_bvashr0_ltr_inv_g.smt2 | 0.117s | 54.068MiB| sat | 0 | | | |int_check_bvsge_bvashr1_ltr_inv_g.smt2 | 0.118s | 53.712MiB| sat | 0 | | | |int_check_bvsgt_bvudiv1_rtl.smt2 | 0.125s | 53.784MiB| sat | 0 | | | |int_check_bvslt_bvlshr1_ltr_inv_g.smt2 | 0.127s | 53.948MiB| sat | 0 | | | |int_check_bvult_bvashr0_ltr_inv_g.smt2 | 0.129s | 53.56MiB| sat | 0 | | | |qf_muldivrem_876_values_0.smt2 | 0.136s | 53.624MiB| sat | 0 | | | |int_check_bvsle_bvudiv0_ltr_inv_g.smt2 | 0.153s | 53.784MiB| sat | 0 | | | |int_check_bvult_bvashr1_ltr_inv_g.smt2 | 0.155s | 53.78MiB| sat | 0 | | | |int_check_bvugt_bvshl0_rtl.smt2 | 0.177s | 54.044MiB| sat | 0 | | | |int_check_bvule_bvashr0_ltr_inv_g.smt2 | 0.194s | 54.0MiB| sat | 0 | | | |int_check_ne_bvudiv0_ltr_inv_g.smt2 | 0.204s | 53.688MiB| sat | 0 | | | |qf_Select_746_values_0.smt2 | 0.204s | 54.008MiB| sat | 0 | | | |int_check_bvsge_bvlshr1_rtl.smt2 | 0.217s | 53.812MiB| sat | 0 | | | |int_check_bvsle_bvashr1_ltr_inv_g.smt2 | 0.255s | 53.668MiB| sat | 0 | | | |int_check_bvslt_bvashr1_ltr_inv_g.smt2 | 0.258s | 53.844MiB| sat | 0 | | | |qf_Select_741_values_0.smt2 | 0.299s | 54.084MiB| sat | 0 | | | |int_check_bvsge_bvurem1_rtl.smt2 | 0.312s | 53.836MiB| sat | 0 | | | |qf_Select_740_values_0.smt2 | 0.394s | 54.044MiB| sat | 0 | | |