# . * SAT 204 * UNSAT 422 * TIMEOUT 750 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: smt-sls
Runner: GCR-SANDBOX-011
Z3 repo: Z3Prover/z3
Z3 commit: 58e64ea8264b42feb5a9c824bd4f3944aed65616
Z3 branch: master
Z3 options: "-T:300 smt.arith.nl.grobner_exp_delay=false"
Z3 inputs: inputs/QF_BV_small
Z3 commit message: try exponential delay in grobner

Signed-off-by: Lev Nachmanson
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |brummayerbiere3_isqrtinvalidvc.smt2 | 0.147s | 30.768MiB| sat | 0 | | | |float_mult2.c.3.smt2 | 0.960s | 43.132MiB| sat | 0 | | | |sage_app1_bench_1146.smt2 | 1.112s | 92.788MiB| sat | 0 | | | |gulwani-pldi08_mccarthy91.phx.smt2 | 1.226s | 47.504MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_bst_yices_predicate_2208.smt2 | 1.302s | 72.46MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_bst_yices_predicate_2106.smt2 | 1.387s | 72.424MiB| unsat | 0 | | | |sage_app1_bench_1015.smt2 | 1.561s | 168.0MiB| sat | 0 | | | |float_f23.smt2 | 1.816s | 100.0MiB| sat | 0 | | | |sage_app1_bench_994.smt2 | 1.851s | 168.0MiB| sat | 0 | | | |sage_app1_bench_2465.smt2 | 1.946s | 168.0MiB| sat | 0 | | | |sage_app1_bench_1017.smt2 | 2.055s | 168.0MiB| sat | 0 | | | |sage_app1_bench_517.smt2 | 2.084s | 169.0MiB| sat | 0 | | | |float_test_v3_r3_vr5_c1_s16641.smt2 | 2.215s | 87.72MiB| sat | 0 | | | |sage_app1_bench_2375.smt2 | 2.225s | 168.0MiB| sat | 0 | | | |sage_app1_bench_329.smt2 | 2.454s | 169.0MiB| sat | 0 | | | |sage_app1_bench_2598.smt2 | 2.645s | 168.0MiB| sat | 0 | | | |sage_app1_bench_174.smt2 | 2.761s | 168.0MiB| sat | 0 | | | |sage_app1_bench_2252.smt2 | 2.769s | 163.0MiB| sat | 0 | | | |sage_app1_bench_2322.smt2 | 2.773s | 163.0MiB| sat | 0 | | | |sage_app1_bench_1128.smt2 | 2.801s | 173.0MiB| sat | 0 | | | |sage_app1_bench_352.smt2 | 2.853s | 168.0MiB| sat | 0 | | | |sage_app1_bench_2466.smt2 | 2.947s | 168.0MiB| sat | 0 | | | |sage_app1_bench_1126.smt2 | 3.061s | 163.0MiB| sat | 0 | | | |sage_app1_bench_691.smt2 | 3.087s | 168.0MiB| sat | 0 | | | |sage_app1_bench_836.smt2 | 3.170s | 168.0MiB| sat | 0 | | | |sage_app1_bench_2004.smt2 | 3.204s | 168.0MiB| sat | 0 | | | |rubik_7moves_mti_8-Atd_00004_bmc.smt2 | 3.312s | 32.072MiB| sat | 0 | | | |sage_app1_bench_1140.smt2 | 3.371s | 162.0MiB| sat | 0 | | | |sage_app1_bench_99.smt2 | 3.387s | 168.0MiB| sat | 0 | | | |sage_app1_bench_2266.smt2 | 3.523s | 167.0MiB| sat | 0 | | | |sage_app1_bench_2089.smt2 | 3.830s | 163.0MiB| sat | 0 | | | |float_mult1.c.10.smt2 | 3.872s | 106.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_bst_hdp_predicate_3215.smt2 | 3.961s | 857.0MiB| unsat | 0 | | | |float_div3.c.10.smt2 | 3.987s | 223.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_bst_yices_predicate_2921_0.smt2 | 4.002s | 441.0MiB| unsat | 0 | | | |sage_app1_bench_2088.smt2 | 4.039s | 163.0MiB| sat | 0 | | | |20210219-Sydr_master_pk2bm_predicate_384.smt2 | 4.109s | 58.3MiB| unsat | 0 | | | |sage_app1_bench_333.smt2 | 4.314s | 169.0MiB| sat | 0 | | | |sage_app1_bench_338.smt2 | 4.445s | 169.0MiB| sat | 0 | | | |float_mult2.c.10.smt2 | 4.512s | 111.0MiB| sat | 0 | | | |sage_app1_bench_681.smt2 | 4.717s | 168.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_bst_hdp_predicate_3422.smt2 | 4.927s | 898.0MiB| unsat | 0 | | | |sage_app1_bench_1448.smt2 | 4.933s | 163.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_bst_yices_predicate_2772_96.smt2 | 5.012s | 848.0MiB| unsat | 0 | | | |float_test_v3_r3_vr10_c1_s29304.smt2 | 5.149s | 91.176MiB| sat | 0 | | | |sage_app1_bench_2124.smt2 | 5.286s | 163.0MiB| sat | 0 | | | |sage_app1_bench_692.smt2 | 5.365s | 169.0MiB| sat | 0 | | | |float_mult1.c.20.smt2 | 5.427s | 212.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g17.smt2 | 5.437s | 606.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g16.smt2 | 5.444s | 621.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_bst_yices_predicate_2474_41.smt2 | 5.508s | 500.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g18.smt2 | 5.520s | 618.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g56.smt2 | 5.664s | 586.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g21.smt2 | 5.718s | 647.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_bst_hdp_predicate_3086.smt2 | 5.862s | 877.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_079_048.smt2 | 5.888s | 535.0MiB| unsat | 0 | | | |sage_app1_bench_1006.smt2 | 6.150s | 168.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_1924.smt2 | 6.165s | 767.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g02.smt2 | 6.218s | 600.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_1934.smt2 | 6.257s | 768.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2012.smt2 | 6.268s | 769.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2021.smt2 | 6.299s | 769.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_bst_cjpeg_predicate_488.smt2 | 6.307s | 1582.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_1981.smt2 | 6.311s | 769.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g47.smt2 | 6.328s | 597.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2118.smt2 | 6.345s | 771.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2110.smt2 | 6.485s | 770.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_hdp_predicate_2871.smt2 | 6.512s | 543.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g03.smt2 | 6.519s | 602.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g46.smt2 | 6.661s | 599.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_004_095_096.smt2 | 6.721s | 1000.0MiB| unsat | 0 | | | |mcm_15.smt2 | 6.730s | 108.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2210.smt2 | 6.795s | 772.0MiB| unsat | 0 | | | |brummayerbiere3_maxor032.smt2 | 6.821s | 41.528MiB| unsat | 0 | | | |brummayerbiere2_smulov1bw16.smt2 | 6.825s | 32.032MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_031_064.smt2 | 6.882s | 292.0MiB| unsat | 0 | | | |sage_app1_bench_1459.smt2 | 6.889s | 163.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_577.smt2 | 6.935s | 399.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_573.smt2 | 6.938s | 400.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_574.smt2 | 7.030s | 399.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2300.smt2 | 7.044s | 969.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_514.smt2 | 7.050s | 397.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2441.smt2 | 7.114s | 777.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_127_080.smt2 | 7.164s | 1000.0MiB| unsat | 0 | | | |brummayerbiere3_mulhs08.smt2 | 7.179s | 28.896MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_159_064.smt2 | 7.184s | 540.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_006_0004.smt2 | 7.243s | 39.144MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2391.smt2 | 7.281s | 971.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2473.smt2 | 7.284s | 972.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_a02.smt2 | 7.306s | 47.232MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_hdp_predicate_3051.smt2 | 7.329s | 1049.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_bst_cjpeg_predicate_642.smt2 | 7.334s | 1591.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2589.smt2 | 7.449s | 976.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2396.smt2 | 7.461s | 971.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2480.smt2 | 7.477s | 973.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g74.smt2 | 7.506s | 969.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_582.smt2 | 7.534s | 402.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_003_0008.smt2 | 7.544s | 38.436MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_bst_hdp_predicate_3128.smt2 | 7.560s | 847.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_159_032.smt2 | 7.582s | 541.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g29.smt2 | 7.602s | 649.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_yices_predicate_1661.smt2 | 7.626s | 599.0MiB| unsat | 0 | | | |sage_app1_bench_2428.smt2 | 7.635s | 168.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g88.smt2 | 7.700s | 646.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_002_143_128.smt2 | 7.716s | 999.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g22.smt2 | 7.739s | 969.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2603.smt2 | 7.811s | 986.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2494.smt2 | 7.862s | 974.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_002_159_128.smt2 | 7.974s | 1000.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_143_064.smt2 | 8.003s | 539.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_015_080.smt2 | 8.062s | 78.468MiB| unsat | 0 | | | |brummayerbiere2_smulov4bw0256.smt2 | 8.124s | 286.0MiB| sat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_002_0016.smt2 | 8.204s | 43.708MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g80.smt2 | 8.261s | 968.0MiB| sat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_005_0004.smt2 | 8.301s | 38.76MiB| unsat | 0 | | | |sage_app1_bench_2468.smt2 | 8.307s | 168.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g95.smt2 | 8.355s | 968.0MiB| sat | 0 | | | |sage_app1_bench_2031.smt2 | 8.430s | 163.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g91.smt2 | 8.459s | 968.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_494.smt2 | 8.462s | 391.0MiB| unsat | 0 | | | |sage_app1_bench_2644.smt2 | 8.483s | 163.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_492.smt2 | 8.488s | 383.0MiB| unsat | 0 | | | |float_test_v3_r3_vr10_c1_s14052.smt2 | 8.525s | 99.288MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_111_048.smt2 | 8.626s | 549.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g82.smt2 | 8.744s | 984.0MiB| sat | 0 | | | |sage_app1_bench_2028.smt2 | 8.774s | 163.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_bst_readelf_predicate_3225.smt2 | 8.779s | 1642.0MiB| unsat | 0 | | | |sage_app1_bench_1021.smt2 | 8.939s | 168.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_143_032.smt2 | 8.949s | 538.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_yices_predicate_2130.smt2 | 8.966s | 465.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_079_112.smt2 | 8.993s | 1025.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_503.smt2 | 9.002s | 392.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g40.smt2 | 9.039s | 988.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g70.smt2 | 9.051s | 358.0MiB| sat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_004_0004.smt2 | 9.114s | 37.06MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_593.smt2 | 9.177s | 403.0MiB| unsat | 0 | | | |2019-Wolf-fmbench_2018E_zipcpu-busdelay-unrolled-nomem.smt2 | 9.178s | 316.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_553.smt2 | 9.346s | 397.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_bst_hdp_predicate_3295.smt2 | 9.376s | 885.0MiB| sat | 0 | | | |sage_app1_bench_1027.smt2 | 9.401s | 168.0MiB| sat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_002_0016.smt2 | 9.427s | 41.572MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_637.smt2 | 9.447s | 405.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_004_004_0016.smt2 | 9.459s | 41.484MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_031_112.smt2 | 9.471s | 288.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_561.smt2 | 9.499s | 399.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_565.smt2 | 9.506s | 398.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_578.smt2 | 9.508s | 399.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_620.smt2 | 9.596s | 404.0MiB| unsat | 0 | | | |sage_app1_bench_847.smt2 | 9.725s | 168.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_562.smt2 | 9.782s | 397.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g07.smt2 | 9.792s | 691.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_063_064.smt2 | 9.849s | 543.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_yodl_predicate_4996.smt2 | 9.874s | 982.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g08.smt2 | 9.935s | 662.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_002_015_128.smt2 | 9.948s | 43.68MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_625.smt2 | 9.957s | 403.0MiB| unsat | 0 | | | |float_square.8.0.i.smt2 | 9.961s | 90.46MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_646.smt2 | 9.975s | 406.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g73.smt2 | 10.001s | 493.0MiB| sat | 0 | | | |float_newton.5.1.i.smt2 | 10.040s | 124.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_687.smt2 | 10.118s | 413.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g84.smt2 | 10.123s | 673.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_601.smt2 | 10.152s | 403.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_608.smt2 | 10.157s | 404.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_665.smt2 | 10.184s | 410.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_630.smt2 | 10.200s | 407.0MiB| unsat | 0 | | | |sage_app1_bench_914.smt2 | 10.201s | 163.0MiB| sat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_006_0004.smt2 | 10.268s | 46.336MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_651.smt2 | 10.283s | 408.0MiB| unsat | 0 | | | |log-slicing_bvmul_10.smt2 | 10.306s | 58.344MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_642.smt2 | 10.317s | 408.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_683.smt2 | 10.387s | 413.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g30.smt2 | 10.394s | 727.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g45.smt2 | 10.421s | 971.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_691.smt2 | 10.430s | 414.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_678.smt2 | 10.434s | 412.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_660.smt2 | 10.563s | 409.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_695.smt2 | 10.603s | 414.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_111_096.smt2 | 10.652s | 1004.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2289.smt2 | 10.654s | 772.0MiB| unsat | 0 | | | |brummayerbiere3_icbrteqcheck.smt2 | 10.662s | 42.296MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_680.smt2 | 10.672s | 411.0MiB| unsat | 0 | | | |mcm_08.smt2 | 10.686s | 70.12MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_655.smt2 | 10.694s | 408.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_002_0032.smt2 | 10.710s | 43.684MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_674.smt2 | 10.710s | 411.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g36.smt2 | 10.742s | 721.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_702.smt2 | 10.818s | 415.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_670.smt2 | 10.832s | 410.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_699.smt2 | 10.938s | 414.0MiB| unsat | 0 | | | |sage_app1_bench_1914.smt2 | 10.944s | 163.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_015_048.smt2 | 10.959s | 81.94MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g99.smt2 | 11.006s | 997.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g27.smt2 | 11.019s | 661.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_004_159_080.smt2 | 11.054s | 1021.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_minigzip_predicate_704.smt2 | 11.145s | 415.0MiB| unsat | 0 | | | |brummayerbiere2_umulov1bw048.smt2 | 11.176s | 55.388MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_127_048.smt2 | 11.187s | 1020.0MiB| unsat | 0 | | | |brummayerbiere2_umulov2bw0256.smt2 | 11.212s | 286.0MiB| unsat | 0 | | | |sage_app1_bench_1135.smt2 | 11.224s | 169.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g31.smt2 | 11.352s | 1160.0MiB| sat | 0 | | | |sage_app1_bench_1916.smt2 | 11.502s | 163.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_047_080.smt2 | 11.668s | 543.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2348.smt2 | 11.670s | 970.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_005_0004.smt2 | 11.812s | 39.86MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_yices_predicate_1420.smt2 | 11.831s | 447.0MiB| sat | 0 | | | |brummayerbiere3_minxor032.smt2 | 11.861s | 38.132MiB| unsat | 0 | | | |sage_app1_bench_1132.smt2 | 12.067s | 173.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_031_080.smt2 | 12.122s | 527.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_readelf_predicate_2508.smt2 | 12.265s | 975.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g79.smt2 | 12.356s | 1170.0MiB| sat | 0 | | | |sage_app1_bench_2263.smt2 | 12.392s | 162.0MiB| sat | 0 | | | |sage_app1_bench_2270.smt2 | 12.397s | 168.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_095_064.smt2 | 12.412s | 1023.0MiB| unsat | 0 | | | |brummayerbiere3_isqrtaddinvalidvc.smt2 | 12.516s | 36.956MiB| sat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_007_0004.smt2 | 12.593s | 43.548MiB| unsat | 0 | | | |20210219-Sydr_master_pk2bm_predicate_232.smt2 | 12.666s | 51.64MiB| unsat | 0 | | | |sage_app1_bench_2129.smt2 | 12.667s | 163.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g64.smt2 | 12.690s | 969.0MiB| sat | 0 | | | |mcm_48.smt2 | 12.708s | 213.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_004_127_096.smt2 | 12.715s | 1041.0MiB| unsat | 0 | | | |sage_app1_bench_869.smt2 | 12.762s | 168.0MiB| sat | 0 | | | |sage_app1_bench_1481.smt2 | 13.031s | 163.0MiB| sat | 0 | | | |bruttomesso_simple_processor_simple_processors_004_003_0032.smt2 | 13.080s | 45.032MiB| unsat | 0 | | | |calypto_problem_3.smt2 | 13.108s | 45.876MiB| unsat | 0 | | | |sage_app1_bench_2138.smt2 | 13.139s | 162.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_004_047_128.smt2 | 13.293s | 534.0MiB| unsat | 0 | | | |float_div2.c.10.smt2 | 13.296s | 236.0MiB| sat | 0 | | | |sage_app1_bench_2005.smt2 | 13.404s | 169.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_hdp_predicate_3210.smt2 | 13.461s | 2039.0MiB| unsat | 0 | | | |sage_app1_bench_37.smt2 | 13.567s | 163.0MiB| sat | 0 | | | |sage_app1_bench_1950.smt2 | 13.808s | 163.0MiB| sat | 0 | | | |float_div2.c.30.smt2 | 13.904s | 752.0MiB| sat | 0 | | | |mcm_03.smt2 | 13.920s | 118.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_004_031_128.smt2 | 14.056s | 291.0MiB| unsat | 0 | | | |20210219-Sydr_master_yices_predicate_567.smt2 | 14.270s | 57.58MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_004_095_112.smt2 | 14.329s | 1431.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_143_080.smt2 | 14.492s | 1011.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_159_096.smt2 | 14.574s | 1440.0MiB| unsat | 0 | | | |float_div2.c.20.smt2 | 14.660s | 463.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_faad_predicate_1215.smt2 | 14.982s | 1345.0MiB| unsat | 0 | | | |mcm_177.smt2 | 15.020s | 724.0MiB| sat | 0 | | | |brummayerbiere3_minandmaxor032.smt2 | 15.031s | 48.228MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g93.smt2 | 15.099s | 1933.0MiB| sat | 0 | | | |sage_app1_bench_2020.smt2 | 15.130s | 168.0MiB| sat | 0 | | | |mcm_44.smt2 | 15.171s | 82.704MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_004_0008.smt2 | 15.390s | 41.716MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_159_048.smt2 | 15.471s | 1026.0MiB| unsat | 0 | | | |sage_app1_bench_181.smt2 | 15.765s | 163.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_004_079_128.smt2 | 15.983s | 1432.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_111_112.smt2 | 16.062s | 1439.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_pk2bm_predicate_232.smt2 | 16.114s | 53.796MiB| unsat | 0 | | | |fft_Sz256_6615.smt2 | 16.546s | 34.148MiB| unsat | 0 | | | |sage_app1_bench_880.smt2 | 16.567s | 168.0MiB| sat | 0 | | | |RWS_Example_11.txt.smt2 | 16.657s | 55.452MiB| sat | 0 | | | |sage_app1_bench_1470.smt2 | 16.799s | 163.0MiB| sat | 0 | | | |float_test_v5_r5_vr10_c1_s5996.smt2 | 17.074s | 226.0MiB| sat | 0 | | | |brummayerbiere_countbitsrotate016.smt2 | 17.150s | 32.592MiB| unsat | 0 | | | |sage_app1_bench_1913.smt2 | 17.194s | 163.0MiB| sat | 0 | | | |float_add_01_100_3.smt2 | 17.418s | 63.964MiB| unsat | 0 | | | |float_add_01_1_1.smt2 | 17.573s | 65.488MiB| unsat | 0 | | | |brummayerbiere_nlzbe256.smt2 | 17.649s | 861.0MiB| unsat | 0 | | | |sage_app1_bench_1915.smt2 | 17.682s | 163.0MiB| sat | 0 | | | |rubik_8moves_mti_9-Atd_00004_bmc.smt2 | 17.803s | 37.568MiB| sat | 0 | | | |mcm_26.smt2 | 18.210s | 155.0MiB| sat | 0 | | | |sage_app1_bench_1525.smt2 | 18.307s | 163.0MiB| sat | 0 | | | |sage_app1_bench_1917.smt2 | 18.330s | 163.0MiB| sat | 0 | | | |float_square.5.0.i.smt2 | 18.511s | 90.98MiB| unsat | 0 | | | |float_test_v3_r8_vr1_c1_s733.smt2 | 18.567s | 223.0MiB| unsat | 0 | | | |bmc-bv_ex30.smt2 | 18.695s | 1472.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_hdp_predicate_3128.smt2 | 18.702s | 1124.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_nested_hdp_predicate_3128.smt2 | 18.712s | 855.0MiB| sat | 0 | | | |RWS_Example_18.txt.smt2 | 18.926s | 81.416MiB| sat | 0 | | | |2019-Mann_digital-estimation-convergence-fwd_prove_ind.smt2 | 19.811s | 54.764MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_015_064.smt2 | 19.846s | 84.78MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_095_128.smt2 | 19.886s | 1442.0MiB| unsat | 0 | | | |sage_app1_bench_1873.smt2 | 19.899s | 163.0MiB| sat | 0 | | | |brummayerbiere3_maxxor016.smt2 | 20.105s | 36.16MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_hdp_predicate_2973.smt2 | 20.515s | 1094.0MiB| sat | 0 | | | |bmc-bv_intSqRoot.smt2 | 20.613s | 1811.0MiB| unsat | 0 | | | |log-slicing_bvsrem_12.smt2 | 20.647s | 58.632MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_079_064.smt2 | 21.156s | 1004.0MiB| unsat | 0 | | | |20210219-Sydr_master_pk2bm_predicate_449.smt2 | 21.191s | 82.084MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_047_096.smt2 | 21.349s | 1039.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_063_128.smt2 | 21.360s | 1002.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_a01.smt2 | 21.409s | 46.072MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_003_0008.smt2 | 21.445s | 43.112MiB| unsat | 0 | | | |float_test_v5_r5_vr10_c1_s5379.smt2 | 21.687s | 229.0MiB| sat | 0 | | | |mcm_41.smt2 | 21.775s | 115.0MiB| sat | 0 | | | |float_div.c.10.smt2 | 22.254s | 243.0MiB| sat | 0 | | | |sage_app1_bench_2128.smt2 | 22.570s | 163.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_111_064.smt2 | 23.008s | 1047.0MiB| unsat | 0 | | | |brummayerbiere3_minand064.smt2 | 23.010s | 113.0MiB| unsat | 0 | | | |sage_app1_bench_1559.smt2 | 23.142s | 163.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_004_159_112.smt2 | 23.156s | 1466.0MiB| unsat | 0 | | | |mcm_87.smt2 | 23.178s | 101.0MiB| unsat | 0 | | | |float_newton.6.1.i.smt2 | 23.395s | 128.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_004_127_112.smt2 | 23.527s | 1445.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_047_112.smt2 | 23.554s | 1440.0MiB| unsat | 0 | | | |float_mul_03_30_3.smt2 | 24.061s | 77.124MiB| unsat | 0 | | | |log-slicing_bvashr_0250.smt2 | 24.086s | 83.648MiB| unsat | 0 | | | |pspace_shift1add.10000.smt2 | 24.193s | 44.024MiB| unsat | 0 | | | |float_square.6.0.i.smt2 | 24.319s | 94.36MiB| unsat | 0 | | | |brummayerbiere2_smulov2bw080.smt2 | 24.457s | 107.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_031_096.smt2 | 24.477s | 537.0MiB| unsat | 0 | | | |float_mul_03_30_7.smt2 | 24.669s | 77.512MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_143_048.smt2 | 24.727s | 1025.0MiB| unsat | 0 | | | |float_mul_03_30_2.smt2 | 24.729s | 76.472MiB| unsat | 0 | | | |float_sqrt.c.5.smt2 | 24.864s | 960.0MiB| sat | 0 | | | |float_sine.4.0.i.smt2 | 25.343s | 95.436MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_111_080.smt2 | 25.482s | 1485.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_008_0004.smt2 | 25.960s | 46.192MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_127_128.smt2 | 25.986s | 1471.0MiB| unsat | 0 | | | |float_test_v5_r5_vr1_c1_s15604.smt2 | 26.087s | 228.0MiB| sat | 0 | | | |float_square.3.0.i.smt2 | 26.170s | 98.148MiB| unsat | 0 | | | |float_test_v3_r8_vr10_c1_s5590.smt2 | 26.239s | 221.0MiB| sat | 0 | | | |float_mul_03_30_1.smt2 | 26.242s | 78.284MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_143_064.smt2 | 26.580s | 1469.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_063_080.smt2 | 26.686s | 1043.0MiB| unsat | 0 | | | |float_add_01_1000_4.smt2 | 26.824s | 65.76MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_002_0032.smt2 | 26.839s | 55.16MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_111_128.smt2 | 26.923s | 1450.0MiB| unsat | 0 | | | |float_test_v3_r8_vr1_c1_s20372.smt2 | 27.025s | 222.0MiB| unsat | 0 | | | |float_add_01_10_2.smt2 | 27.117s | 67.604MiB| unsat | 0 | | | |float_test_v3_r8_vr5_c1_s1507.smt2 | 27.341s | 224.0MiB| unsat | 0 | | | |float_mul_03_30_5.smt2 | 27.588s | 76.148MiB| unsat | 0 | | | |float_square.7.0.i.smt2 | 28.438s | 97.344MiB| unsat | 0 | | | |float_test_v3_r8_vr5_c1_s10746.smt2 | 28.448s | 224.0MiB| unsat | 0 | | | |pspace_shift1add.10997.smt2 | 28.707s | 44.956MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_015_096.smt2 | 28.776s | 81.792MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_127_064.smt2 | 28.830s | 1054.0MiB| unsat | 0 | | | |fft_Sz512_15368.smt2 | 29.088s | 49.792MiB| sat | 0 | | | |float_mul_03_30_6.smt2 | 29.187s | 77.18MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_047_128.smt2 | 29.219s | 1452.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_faad_predicate_1385.smt2 | 29.258s | 2534.0MiB| unsat | 0 | | | |float_test_v3_r8_vr10_c1_s18214.smt2 | 29.305s | 223.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_hdp_predicate_3250.smt2 | 29.553s | 1618.0MiB| unsat | 0 | | | |log-slicing_bvslt_5000.smt2 | 29.971s | 431.0MiB| unsat | 0 | | | |sage_app1_bench_947.smt2 | 30.039s | 163.0MiB| sat | 0 | | | |mcm_11.smt2 | 30.210s | 84.792MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_079_080.smt2 | 30.764s | 1442.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_nested_pk2bm_predicate_449.smt2 | 30.981s | 87.124MiB| unsat | 0 | | | |mcm_123.smt2 | 32.043s | 679.0MiB| sat | 0 | | | |float_square.1.0.i.smt2 | 32.666s | 96.148MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_063_112.smt2 | 32.860s | 1490.0MiB| unsat | 0 | | | |float_div.c.20.smt2 | 32.937s | 479.0MiB| sat | 0 | | | |brummayerbiere3_maxxormaxorand016.smt2 | 32.992s | 45.276MiB| unsat | 0 | | | |log-slicing_bvashr_0273.smt2 | 33.588s | 120.0MiB| unsat | 0 | | | |float_newton.4.1.i.smt2 | 33.636s | 125.0MiB| sat | 0 | | | |pspace_shift1add.11994.smt2 | 34.672s | 46.804MiB| unsat | 0 | | | |log-slicing_bvmul_11.smt2 | 34.682s | 57.688MiB| unsat | 0 | | | |brummayerbiere_bitrev8192.smt2 | 34.830s | 47.88MiB| unsat | 0 | | | |log-slicing_bvlshr_0400.smt2 | 35.590s | 83.94MiB| unsat | 0 | | | |log-slicing_bvshl_0400.smt2 | 36.433s | 84.124MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_143_096.smt2 | 36.655s | 1051.0MiB| unsat | 0 | | | |brummayerbiere2_smulov3bw0384.smt2 | 36.919s | 875.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_159_064.smt2 | 37.526s | 1482.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_004_0008.smt2 | 37.931s | 50.736MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_004_004_0032.smt2 | 38.335s | 59.384MiB| unsat | 0 | | | |float_test_v5_r5_vr5_c1_s9855.smt2 | 38.446s | 231.0MiB| sat | 0 | | | |calypto_problem_24.smt2 | 38.527s | 72.04MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_063_096.smt2 | 38.707s | 1449.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_159_128.smt2 | 39.146s | 1496.0MiB| unsat | 0 | | | |float_sine.2.0.i.smt2 | 39.938s | 102.0MiB| unsat | 0 | | | |float_mul_03_3_1.smt2 | 39.965s | 87.488MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_031_112.smt2 | 40.091s | 542.0MiB| unsat | 0 | | | |mcm_94.smt2 | 40.104s | 369.0MiB| sat | 0 | | | |log-slicing_bvslt_5743.smt2 | 40.255s | 434.0MiB| unsat | 0 | | | |log-slicing_bvashr_0296.smt2 | 41.649s | 153.0MiB| unsat | 0 | | | |float_test_v5_r5_vr1_c1_s16138.smt2 | 41.672s | 229.0MiB| sat | 0 | | | |pspace_shift1add.12991.smt2 | 41.776s | 48.496MiB| unsat | 0 | | | |float_test_v5_r5_vr1_c1_s14623.smt2 | 41.844s | 227.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_004_143_112.smt2 | 41.919s | 1455.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g48.smt2 | 41.959s | 663.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_a00.smt2 | 43.234s | 44.836MiB| unsat | 0 | | | |float_add_01_100_4.smt2 | 44.500s | 70.252MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_003_0016.smt2 | 44.538s | 55.344MiB| unsat | 0 | | | |float_div2.c.40.smt2 | 44.642s | 909.0MiB| sat | 0 | | | |float_test_v3_r8_vr10_c1_s4660.smt2 | 45.215s | 222.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_127_080.smt2 | 47.100s | 1494.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_015_112.smt2 | 47.193s | 83.396MiB| unsat | 0 | | | |pspace_shift1add.13988.smt2 | 47.708s | 50.376MiB| unsat | 0 | | | |brummayerbiere2_smulov2bw096.smt2 | 47.766s | 137.0MiB| unsat | 0 | | | |mcm_33.smt2 | 48.506s | 125.0MiB| sat | 0 | | | |mcm_152.smt2 | 48.821s | 408.0MiB| sat | 0 | | | |log-slicing_bvslt_6486.smt2 | 49.793s | 439.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_159_080.smt2 | 50.558s | 1507.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_faad_predicate_1530.smt2 | 51.145s | 3134.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_004_143_128.smt2 | 52.014s | 1494.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_095_080.smt2 | 52.130s | 1451.0MiB| unsat | 0 | | | |log-slicing_bvsrem_13.smt2 | 52.407s | 58.9MiB| unsat | 0 | | | |brummayerbiere2_umulov1bw064.smt2 | 52.576s | 88.112MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_031_128.smt2 | 52.989s | 837.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_063_128.smt2 | 54.061s | 1503.0MiB| unsat | 0 | | | |float_test_v3_r8_vr5_c1_s8257.smt2 | 54.645s | 223.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_079_096.smt2 | 55.053s | 1484.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_005_0008.smt2 | 56.116s | 49.528MiB| unsat | 0 | | | |log-slicing_bvsdiv_15.smt2 | 56.550s | 59.4MiB| unsat | 0 | | | |pspace_shift1add.14985.smt2 | 57.125s | 52.084MiB| unsat | 0 | | | |log-slicing_bvashr_0319.smt2 | 57.389s | 154.0MiB| unsat | 0 | | | |log-slicing_bvshl_0453.smt2 | 57.506s | 84.98MiB| unsat | 0 | | | |float_add_01_10_3.smt2 | 57.529s | 74.116MiB| unsat | 0 | | | |log-slicing_bvult_6000.smt2 | 57.672s | 433.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_003_0016.smt2 | 57.944s | 62.152MiB| unsat | 0 | | | |float_add_01_1_2.smt2 | 58.180s | 74.58MiB| unsat | 0 | | | |mcm_09.smt2 | 58.666s | 92.124MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_006_0008.smt2 | 58.931s | 56.616MiB| unsat | 0 | | | |float_test_v5_r5_vr5_c1_s2800.smt2 | 59.692s | 231.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_015_080.smt2 | 60.132s | 151.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_111_096.smt2 | 60.353s | 2025.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_143_080.smt2 | 61.083s | 1506.0MiB| unsat | 0 | | | |pspace_shift1add.15982.smt2 | 61.641s | 54.22MiB| unsat | 0 | | | |2019-Mann_digital-estimation-convergence-bmc-fwd.smt2 | 65.065s | 6494.0MiB| unsat | 0 | | | |float_test_v5_r5_vr5_c1_s24018.smt2 | 65.150s | 227.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_004_015_128.smt2 | 65.338s | 115.0MiB| unsat | 0 | | | |log-slicing_bvslt_7972.smt2 | 65.487s | 446.0MiB| unsat | 0 | | | |log-slicing_bvurem_13.smt2 | 65.693s | 58.636MiB| unsat | 0 | | | |float_sqrt.c.15.smt2 | 66.221s | 2138.0MiB| sat | 0 | | | |float_sine.6.0.i.smt2 | 66.735s | 105.0MiB| unsat | 0 | | | |brummayerbiere3_minor064.smt2 | 67.682s | 113.0MiB| unsat | 0 | | | |float_sqrt.c.2.smt2 | 67.942s | 382.0MiB| sat | 0 | | | |rubik_8moves_mti_8-Atd_00004_bmc.smt2 | 68.427s | 40.016MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_faad_predicate_1624.smt2 | 69.369s | 4283.0MiB| unsat | 0 | | | |float_square.2.0.i.smt2 | 69.573s | 108.0MiB| unsat | 0 | | | |log-slicing_bvlshr_0494.smt2 | 70.293s | 116.0MiB| unsat | 0 | | | |log-slicing_bvlshr_0447.smt2 | 70.733s | 84.768MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_004_0016.smt2 | 71.350s | 64.288MiB| unsat | 0 | | | |mcm_18.smt2 | 72.409s | 219.0MiB| sat | 0 | | | |brummayerbiere3_isqrt.smt2 | 72.525s | 38.192MiB| unsat | 0 | | | |RWS_Example_20.txt.smt2 | 72.667s | 927.0MiB| sat | 0 | | | |brummayerbiere3_minxorminand032.smt2 | 72.697s | 64.496MiB| unsat | 0 | | | |float_sine.7.0.i.smt2 | 73.082s | 107.0MiB| unsat | 0 | | | |float_add_01_1_3.smt2 | 74.163s | 76.54MiB| unsat | 0 | | | |pspace_shift1add.16979.smt2 | 74.831s | 82.028MiB| unsat | 0 | | | |mcm_86.smt2 | 75.453s | 181.0MiB| unsat | 0 | | | |mcm_156.smt2 | 75.877s | 576.0MiB| sat | 0 | | | |calypto_problem_7.smt2 | 75.937s | 105.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_faad_predicate_1677.smt2 | 76.088s | 5229.0MiB| unsat | 0 | | | |float_sine.5.0.i.smt2 | 76.754s | 108.0MiB| unsat | 0 | | | |log-slicing_bvslt_7229.smt2 | 77.989s | 444.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_095_096.smt2 | 78.046s | 1498.0MiB| unsat | 0 | | | |mcm_84.smt2 | 78.775s | 115.0MiB| unsat | 0 | | | |log-slicing_bvadd_12887.smt2 | 78.856s | 504.0MiB| unsat | 0 | | | |float_square.4.0.i.smt2 | 79.626s | 101.0MiB| unsat | 0 | | | |log-slicing_bvshl_0506.smt2 | 79.678s | 116.0MiB| unsat | 0 | | | |log-slicing_bvult_6997.smt2 | 79.902s | 443.0MiB| unsat | 0 | | | |brummayerbiere2_smulov1bw24.smt2 | 80.694s | 48.428MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_079_128.smt2 | 80.860s | 2821.0MiB| unsat | 0 | | | |mcm_42.smt2 | 80.995s | 108.0MiB| unsat | 0 | | | |log-slicing_bvashr_0342.smt2 | 81.435s | 156.0MiB| unsat | 0 | | | |pspace_shift1add.17976.smt2 | 81.526s | 84.192MiB| unsat | 0 | | | |float_sine.8.0.i.smt2 | 81.619s | 110.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_127_096.smt2 | 82.294s | 2039.0MiB| unsat | 0 | | | |float_sine.3.0.i.smt2 | 82.588s | 107.0MiB| unsat | 0 | | | |float_test_v7_r7_vr10_c1_s24535.smt2 | 82.869s | 445.0MiB| sat | 0 | | | |log-slicing_bvadd_13774.smt2 | 83.228s | 510.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_079_112.smt2 | 83.266s | 2025.0MiB| unsat | 0 | | | |float_div3.c.50.smt2 | 83.283s | 1303.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_a90.smt2 | 83.602s | 625.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_pk2bm_predicate_410.smt2 | 85.357s | 80.18MiB| unsat | 0 | | | |brummayerbiere_countbits064.smt2 | 85.511s | 53.428MiB| unsat | 0 | | | |brummayerbiere3_isqrtnoif.smt2 | 85.585s | 41.216MiB| unsat | 0 | | | |calypto_problem_8.smt2 | 85.849s | 106.0MiB| sat | 0 | | | |log-slicing_bvadd_12000.smt2 | 85.900s | 494.0MiB| unsat | 0 | | | |float_mult2.c.20.smt2 | 86.716s | 225.0MiB| sat | 0 | | | |brummayerbiere2_umulov2bw0384.smt2 | 86.811s | 874.0MiB| unsat | 0 | | | |brummayerbiere3_isqrteqcheck.smt2 | 89.454s | 43.632MiB| unsat | 0 | | | |20210219-Sydr_master_pk2bm_predicate_438.smt2 | 90.411s | 84.008MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_159_096.smt2 | 90.780s | 2852.0MiB| unsat | 0 | | | |log-slicing_bvudiv_15.smt2 | 92.010s | 59.26MiB| unsat | 0 | | | |2018-Mann_fifo_data_integrity_w8d8b30.smt2 | 92.199s | 58.272MiB| unsat | 0 | | | |float_test_v7_r7_vr5_c1_s3582.smt2 | 92.869s | 463.0MiB| sat | 0 | | | |brummayerbiere3_isqrtaddnoif.smt2 | 92.960s | 47.06MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_004_0016.smt2 | 93.835s | 67.332MiB| unsat | 0 | | | |brummayerbiere2_smulov2bw112.smt2 | 93.950s | 188.0MiB| unsat | 0 | | | |20210219-Sydr_symbolic_memory_linear_pk2bm_predicate_438.smt2 | 94.120s | 83.068MiB| unsat | 0 | | | |pspace_shift1add.18973.smt2 | 94.250s | 86.928MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_095_112.smt2 | 94.790s | 2818.0MiB| unsat | 0 | | | |brummayerbiere3_maxand064.smt2 | 96.464s | 112.0MiB| unsat | 0 | | | |mcm_04.smt2 | 98.377s | 114.0MiB| unsat | 0 | | | |float_add_01_10_4.smt2 | 98.814s | 81.12MiB| unsat | 0 | | | |calypto_problem_20.smt2 | 99.359s | 53.268MiB| unsat | 0 | | | |20210219-Sydr_master_pk2bm_predicate_410.smt2 | 99.540s | 78.548MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_127_112.smt2 | 100.468s | 2868.0MiB| unsat | 0 | | | |log-slicing_bvlshr_0541.smt2 | 100.588s | 155.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_003_0032.smt2 | 101.991s | 77.028MiB| unsat | 0 | | | |float_add_01_1_4.smt2 | 102.899s | 81.36MiB| unsat | 0 | | | |log-slicing_bvshl_0559.smt2 | 104.040s | 157.0MiB| unsat | 0 | | | |log-slicing_bvashr_0365.smt2 | 104.373s | 158.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_143_096.smt2 | 104.387s | 2070.0MiB| unsat | 0 | | | |float_div.c.40.smt2 | 105.129s | 933.0MiB| sat | 0 | | | |float_sine.1.0.i.smt2 | 105.355s | 107.0MiB| sat | 0 | | | |pspace_shift1add.19970.smt2 | 106.264s | 89.268MiB| unsat | 0 | | | |float_test_v5_r5_vr10_c1_s7194.smt2 | 108.548s | 231.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_pk2bm_predicate_446.smt2 | 109.236s | 86.744MiB| unsat | 0 | | | |mcm_24.smt2 | 109.976s | 220.0MiB| sat | 0 | | | |log-slicing_bvadd_14661.smt2 | 110.058s | 518.0MiB| unsat | 0 | | | |log-slicing_bvsrem_14.smt2 | 111.759s | 60.648MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_015_096.smt2 | 113.938s | 157.0MiB| unsat | 0 | | | |pspace_shift1add.20967.smt2 | 115.801s | 91.812MiB| unsat | 0 | | | |log-slicing_bvsdiv_16.smt2 | 116.047s | 59.408MiB| unsat | 0 | | | |mcm_34.smt2 | 116.149s | 107.0MiB| unsat | 0 | | | |log-slicing_bvlshr_0588.smt2 | 116.502s | 158.0MiB| unsat | 0 | | | |log-slicing_bvashr_0388.smt2 | 116.504s | 159.0MiB| unsat | 0 | | | |float_mult1.c.30.smt2 | 118.520s | 301.0MiB| sat | 0 | | | |float_newton.8.2.i.smt2 | 119.295s | 255.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_a14.smt2 | 121.987s | 85.712MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_005_0008.smt2 | 122.943s | 77.004MiB| unsat | 0 | | | |float_mult2.c.30.smt2 | 125.613s | 336.0MiB| sat | 0 | | | |20200415-Yurichev_t2.smt2 | 126.922s | 113.0MiB| unsat | 0 | | | |mcm_99.smt2 | 128.392s | 189.0MiB| unsat | 0 | | | |float_test_v7_r7_vr5_c1_s14675.smt2 | 128.478s | 455.0MiB| sat | 0 | | | |pspace_shift1add.21964.smt2 | 128.541s | 94.608MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_a08.smt2 | 129.126s | 154.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_111_128.smt2 | 129.479s | 2871.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_127_128.smt2 | 131.192s | 2923.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_a11.smt2 | 131.704s | 94.092MiB| unsat | 0 | | | |log-slicing_bvsmod_12.smt2 | 133.834s | 61.848MiB| unsat | 0 | | | |pspace_shift1add.22961.smt2 | 133.933s | 97.452MiB| unsat | 0 | | | |log-slicing_bvashr_0411.smt2 | 134.186s | 160.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_095_128.smt2 | 135.509s | 2851.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_a04.smt2 | 137.231s | 85.428MiB| unsat | 0 | | | |float_div3.c.20.smt2 | 138.435s | 480.0MiB| sat | 0 | | | |brummayerbiere2_smulov4bw0384.smt2 | 139.231s | 875.0MiB| sat | 0 | | | |pspace_ndist.a.20499.smt2 | 143.200s | 404.0MiB| unsat | 0 | | | |calypto_problem_22.smt2 | 143.281s | 60.864MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_159_128.smt2 | 143.722s | 2959.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_006_0016.smt2 | 145.958s | 75.804MiB| unsat | 0 | | | |mcm_93.smt2 | 147.706s | 146.0MiB| unsat | 0 | | | |log-slicing_bvadd_17322.smt2 | 147.719s | 635.0MiB| unsat | 0 | | | |mcm_01.smt2 | 148.022s | 157.0MiB| sat | 0 | | | |log-slicing_bvmul_12.smt2 | 150.361s | 62.172MiB| unsat | 0 | | | |pspace_shift1add.23958.smt2 | 151.186s | 97.0MiB| unsat | 0 | | | |brummayerbiere2_umulov1bw080.smt2 | 152.957s | 152.0MiB| unsat | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_1492.smt2 | 153.128s | 78.748MiB| sat | 0 | | | |brummayerbiere3_isqrtadd.smt2 | 155.908s | 45.848MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_111_112.smt2 | 157.469s | 2847.0MiB| unsat | 0 | | | |mcm_05.smt2 | 157.936s | 166.0MiB| sat | 0 | | | |log-slicing_bvadd_19096.smt2 | 158.007s | 920.0MiB| unsat | 0 | | | |log-slicing_bvshl_0612.smt2 | 158.085s | 158.0MiB| unsat | 0 | | | |mcm_35.smt2 | 159.350s | 161.0MiB| sat | 0 | | | |log-slicing_bvashr_0434.smt2 | 160.779s | 160.0MiB| unsat | 0 | | | |pspace_shift1add.24955.smt2 | 162.222s | 101.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_g11.smt2 | 162.999s | 496.0MiB| sat | 0 | | | |log-slicing_bvadd_18209.smt2 | 164.583s | 642.0MiB| unsat | 0 | | | |brummayerbiere_nextpoweroftwo256.smt2 | 167.555s | 1859.0MiB| unsat | 0 | | | |log-slicing_bvlshr_0635.smt2 | 168.122s | 159.0MiB| unsat | 0 | | | |brummayerbiere2_smulov3bw0512.smt2 | 169.561s | 1184.0MiB| unsat | 0 | | | |brummayerbiere2_umulov2bw0512.smt2 | 171.063s | 1180.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_a03.smt2 | 173.406s | 68.256MiB| unsat | 0 | | | |float_test_v7_r7_vr1_c1_s22845.smt2 | 173.732s | 453.0MiB| sat | 0 | | | |bruttomesso_lfsr_lfsr_008_143_112.smt2 | 174.087s | 2882.0MiB| unsat | 0 | | | |RWS_Example_19.txt.smt2 | 174.555s | 473.0MiB| sat | 0 | | | |mcm_131.smt2 | 175.700s | 371.0MiB| unsat | 0 | | | |log-slicing_bvadd_15548.smt2 | 175.905s | 525.0MiB| unsat | 0 | | | |mcm_36.smt2 | 177.309s | 136.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_a06.smt2 | 178.126s | 65.412MiB| unsat | 0 | | | |pspace_shift1add.25952.smt2 | 180.275s | 104.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_005_0032.smt2 | 183.046s | 102.0MiB| unsat | 0 | | | |pspace_ndist.a.20000.smt2 | 183.328s | 401.0MiB| unsat | 0 | | | |float_test_v5_r10_vr1_c1_s32538.smt2 | 184.836s | 458.0MiB| unsat | 0 | | | |mcm_85.smt2 | 187.192s | 192.0MiB| sat | 0 | | | |float_div3.c.30.smt2 | 187.819s | 750.0MiB| sat | 0 | | | |log-slicing_bvurem_14.smt2 | 187.993s | 60.36MiB| unsat | 0 | | | |pspace_shift1add.26949.smt2 | 190.147s | 107.0MiB| unsat | 0 | | | |log-slicing_bvult_7994.smt2 | 194.280s | 444.0MiB| unsat | 0 | | | |mcm_20.smt2 | 196.871s | 223.0MiB| sat | 0 | | | |brummayerbiere2_smulov2bw160.smt2 | 198.215s | 351.0MiB| unsat | 0 | | | |mcm_101.smt2 | 202.128s | 193.0MiB| unsat | 0 | | | |float_test_v5_r10_vr1_c1_s13516.smt2 | 202.327s | 455.0MiB| sat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_004_0032.smt2 | 203.318s | 108.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_005_0016.smt2 | 206.163s | 88.52MiB| unsat | 0 | | | |pspace_shift1add.27946.smt2 | 207.275s | 111.0MiB| unsat | 0 | | | |pspace_shift1add.29940.smt2 | 207.998s | 118.0MiB| unsat | 0 | | | |log-slicing_bvlshr_0682.smt2 | 208.157s | 160.0MiB| unsat | 0 | | | |float_test_v5_r10_vr1_c1_s19145.smt2 | 210.723s | 457.0MiB| sat | 0 | | | |log-slicing_bvashr_0480.smt2 | 210.970s | 162.0MiB| unsat | 0 | | | |log-slicing_bvshl_0665.smt2 | 215.147s | 160.0MiB| unsat | 0 | | | |log-slicing_bvadd_16435.smt2 | 215.678s | 628.0MiB| unsat | 0 | | | |pspace_shift1add.28943.smt2 | 217.290s | 114.0MiB| unsat | 0 | | | |2017-BuchwaldFried_synthesis.dump.ia32_RorMem_base_index_scale_disp2--Add32.Add32.Add32.Add32.load32.Or32.Or32.store32.am_shl32.0001.smt2 | 219.577s | 79.46MiB| unsat | 0 | | | |20210219-Sydr_master_pk2bm_predicate_446.smt2 | 226.811s | 91.244MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_a10.smt2 | 227.835s | 72.284MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_015_112.smt2 | 229.164s | 160.0MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_006_0008.smt2 | 232.386s | 83.58MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_159_112.smt2 | 234.148s | 2911.0MiB| unsat | 0 | | | |pspace_ndist.a.21996.smt2 | 234.914s | 512.0MiB| unsat | 0 | | | |float_div3.c.40.smt2 | 237.669s | 939.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_a09.smt2 | 242.277s | 82.968MiB| unsat | 0 | | | |float_gaussian.c.25.smt2 | 246.496s | 1278.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g00.smt2 | 247.555s | 301.0MiB| sat | 0 | | | |log-slicing_bvashr_0457.smt2 | 248.083s | 161.0MiB| unsat | 0 | | | |float_test_v5_r10_vr5_c1_s13195.smt2 | 249.724s | 459.0MiB| sat | 0 | | | |mcm_54.smt2 | 250.995s | 237.0MiB| sat | 0 | | | |mcm_167.smt2 | 252.213s | 1278.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g59.smt2 | 253.245s | 599.0MiB| sat | 0 | | | |20210312-Bouvier_vlsat3_g89.smt2 | 256.612s | 688.0MiB| sat | 0 | | | |float_test_v7_r12_vr5_c1_s8938.smt2 | 258.681s | 777.0MiB| sat | 0 | | | |20210219-Sydr_symbolic_memory_linear_pk2bm_predicate_430.smt2 | 260.802s | 86.928MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_006_004_0032.smt2 | 265.286s | 103.0MiB| unsat | 0 | | | |bruttomesso_lfsr_lfsr_008_143_128.smt2 | 266.476s | 2943.0MiB| unsat | 0 | | | |float_test_v5_r15_vr10_c1_s11127.smt2 | 268.884s | 657.0MiB| sat | 0 | | | |log-slicing_bvshl_0718.smt2 | 269.101s | 161.0MiB| unsat | 0 | | | |log-slicing_bvadd_20870.smt2 | 270.634s | 932.0MiB| unsat | 0 | | | |log-slicing_bvslt_10944.smt2 | 271.831s | 882.0MiB| unsat | 0 | | | |log-slicing_bvslt_8715.smt2 | 272.103s | 880.0MiB| unsat | 0 | | | |log-slicing_bvlshr_0729.smt2 | 272.901s | 161.0MiB| unsat | 0 | | | |log-slicing_bvashr_0503.smt2 | 276.087s | 163.0MiB| unsat | 0 | | | |mcm_155.smt2 | 276.419s | 697.0MiB| sat | 0 | | | |log-slicing_bvlshr_0823.smt2 | 276.585s | 229.0MiB| unsat | 0 | | | |float_newton.1.1.i.smt2 | 276.716s | 154.0MiB| unsat | 0 | | | |mcm_29.smt2 | 278.032s | 172.0MiB| sat | 0 | | | |pspace_ndist.a.20998.smt2 | 278.292s | 413.0MiB| unsat | 0 | | | |float_newton.8.3.i.smt2 | 280.750s | 428.0MiB| sat | 0 | | | |float_test_v5_r15_vr1_c1_s32559.smt2 | 282.200s | 653.0MiB| unsat | 0 | | | |20210312-Bouvier_vlsat3_a57.smt2 | 284.527s | 73.808MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_007_0008.smt2 | 284.659s | 88.148MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_005_0016.smt2 | 285.910s | 94.268MiB| unsat | 0 | | | |bruttomesso_simple_processor_simple_processors_008_003_0032.smt2 | 286.584s | 117.0MiB| unsat | 0 | | | |log-slicing_bvadd_19983.smt2 | 291.992s | 926.0MiB| unsat | 0 | | | |log-slicing_bvudiv_16.smt2 | 292.724s | 61.928MiB| unsat | 0 | | | |float_div2.c.50.smt2 | 292.794s | 1320.0MiB| sat | 0 | | | |log-slicing_bvslt_9458.smt2 | 293.278s | 882.0MiB| unsat | 0 | | | |float_test_v7_r12_vr5_c1_s14336.smt2 | 295.756s | 777.0MiB| sat | 0 | | | |mcm_112.smt2 | 298.203s | 649.0MiB| sat | 0 | | | |20210219-Sydr_master_pk2bm_predicate_430.smt2 | 298.664s | 86.396MiB| unsat | 0 | | | |20210219-Sydr_master_yices_predicate_3426.smt2 | 300.012s | 116.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_388.smt2 | 300.012s | 92.088MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a73.smt2 | 300.013s | 84.332MiB| timeout | 0 | | | |brummayerbiere_countbitsrotate032.smt2 | 300.013s | 63.344MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a72.smt2 | 300.013s | 83.832MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a34.smt2 | 300.014s | 83.5MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a29.smt2 | 300.014s | 88.056MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_5044.smt2 | 300.015s | 142.0MiB| timeout | 0 | | | |log-slicing_bvsmod_13.smt2 | 300.015s | 68.336MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_1254.smt2 | 300.015s | 74.628MiB| timeout | 0 | | | |calypto_problem_17.smt2 | 300.016s | 89.084MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a81.smt2 | 300.016s | 320.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_10340.smt2 | 300.016s | 204.0MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_928.smt2 | 300.017s | 93.668MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_4911.smt2 | 300.017s | 130.0MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_690.smt2 | 300.017s | 71.368MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a78.smt2 | 300.018s | 77.812MiB| timeout | 0 | | | |log-slicing_bvshl_0771.smt2 | 300.018s | 227.0MiB| timeout | 0 | | | |fft_Sz512_15128_2.smt2 | 300.018s | 67.704MiB| timeout | 0 | | | |log-slicing_bvshl_1195.smt2 | 300.018s | 317.0MiB| timeout | 0 | | | |log-slicing_bvsmod_15.smt2 | 300.019s | 73.672MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a58.smt2 | 300.019s | 159.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a66.smt2 | 300.019s | 595.0MiB| timeout | 0 | | | |fft_Sz512_15127_4.smt2 | 300.019s | 78.076MiB| timeout | 0 | | | |pspace_power2sum.5699.smt2 | 300.020s | 278.0MiB| timeout | 0 | | | |float_mul_03_30_4.smt2 | 300.022s | 119.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a37.smt2 | 300.022s | 82.584MiB| timeout | 0 | | | |log-slicing_bvshl_0877.smt2 | 300.023s | 229.0MiB| timeout | 0 | | | |brummayerbiere_countbitssrl064.smt2 | 300.025s | 120.0MiB| timeout | 0 | | | |brummayerbiere2_smulov1bw48.smt2 | 300.025s | 114.0MiB| timeout | 0 | | | |log-slicing_bvsmod_16.smt2 | 300.025s | 76.956MiB| timeout | 0 | | | |log-slicing_bvurem_20.smt2 | 300.025s | 225.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_9785.smt2 | 300.026s | 204.0MiB| timeout | 0 | | | |log-slicing_bvsmod_14.smt2 | 300.026s | 73.008MiB| timeout | 0 | | | |log-slicing_bvlshr_1340.smt2 | 300.026s | 419.0MiB| timeout | 0 | | | |RWS_Example_7.txt.smt2 | 300.026s | 117.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a70.smt2 | 300.026s | 303.0MiB| timeout | 0 | | | |fft_Sz512_15127_0.smt2 | 300.026s | 85.916MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_1395.smt2 | 300.027s | 74.888MiB| timeout | 0 | | | |fft_Sz512_15128_4.smt2 | 300.027s | 79.944MiB| timeout | 0 | | | |log-slicing_bvshl_1036.smt2 | 300.027s | 311.0MiB| timeout | 0 | | | |float_newton.7.2.i.smt2 | 300.027s | 266.0MiB| timeout | 0 | | | |calypto_problem_18.smt2 | 300.027s | 93.776MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_1248.smt2 | 300.027s | 72.684MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_12524.smt2 | 300.027s | 294.0MiB| timeout | 0 | | | |log-slicing_bvsdiv_17.smt2 | 300.027s | 228.0MiB| timeout | 0 | | | |pspace_power2sum.6097.smt2 | 300.027s | 280.0MiB| timeout | 0 | | | |calypto_problem_13.smt2 | 300.028s | 111.0MiB| timeout | 0 | | | |2019-Wolf-fmbench_2018E_VexRiscv-regch0-15-unrolled-nomem.smt2 | 300.029s | 201.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a51.smt2 | 300.029s | 76.276MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a38.smt2 | 300.029s | 97.0MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_1299.smt2 | 300.030s | 84.112MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_7677.smt2 | 300.030s | 165.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a79.smt2 | 300.030s | 83.684MiB| timeout | 0 | | | |fft_Sz512_15127_7.smt2 | 300.031s | 64.024MiB| timeout | 0 | | | |log-slicing_bvmul_13.smt2 | 300.031s | 66.572MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a48.smt2 | 300.031s | 87.392MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_199.smt2 | 300.031s | 69.912MiB| timeout | 0 | | | |fft_Sz512_15127_6.smt2 | 300.031s | 71.296MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_1474.smt2 | 300.032s | 74.92MiB| timeout | 0 | | | |calypto_problem_21.smt2 | 300.032s | 70.936MiB| timeout | 0 | | | |log-slicing_bvlshr_1105.smt2 | 300.032s | 315.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g20.smt2 | 300.032s | 510.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_4597.smt2 | 300.032s | 132.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_5377.smt2 | 300.032s | 135.0MiB| timeout | 0 | | | |log-slicing_bvsrem_18.smt2 | 300.032s | 229.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a77.smt2 | 300.032s | 346.0MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_1323.smt2 | 300.032s | 89.688MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_7492.smt2 | 300.033s | 186.0MiB| timeout | 0 | | | |log-slicing_bvsdiv_21.smt2 | 300.033s | 227.0MiB| timeout | 0 | | | |brummayerbiere_countbitssrl032.smt2 | 300.033s | 70.412MiB| timeout | 0 | | | |log-slicing_bvsrem_16.smt2 | 300.033s | 71.584MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_9701.smt2 | 300.033s | 202.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_5971.smt2 | 300.033s | 130.0MiB| timeout | 0 | | | |calypto_problem_10.smt2 | 300.033s | 88.232MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_9399.smt2 | 300.033s | 202.0MiB| timeout | 0 | | | |mcm_17.smt2 | 300.033s | 231.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_5316.smt2 | 300.034s | 135.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_2968.smt2 | 300.034s | 97.112MiB| timeout | 0 | | | |20210219-Sydr_master_jasper_predicate_93.smt2 | 300.034s | 74.576MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_3155.smt2 | 300.034s | 104.0MiB| timeout | 0 | | | |bruttomesso_simple_processor_simple_processors_008_008_0008.smt2 | 300.034s | 86.128MiB| timeout | 0 | | | |fft_Sz512_15128_6.smt2 | 300.034s | 75.348MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a46.smt2 | 300.034s | 181.0MiB| timeout | 0 | | | |log-slicing_bvudiv_17.smt2 | 300.034s | 222.0MiB| timeout | 0 | | | |20210219-Sydr_symbolic_memory_nested_yices_predicate_589.smt2 | 300.034s | 54.976MiB| timeout | 0 | | | |float_mul_000003_30000_1.smt2 | 300.034s | 98.0MiB| timeout | 0 | | | |log-slicing_bvsdiv_19.smt2 | 300.034s | 226.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_3655.smt2 | 300.034s | 115.0MiB| timeout | 0 | | | |float_mul_03_3000_1.smt2 | 300.034s | 116.0MiB| timeout | 0 | | | |mcm_70.smt2 | 300.035s | 358.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a21.smt2 | 300.035s | 89.296MiB| timeout | 0 | | | |mcm_60.smt2 | 300.035s | 369.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_7969.smt2 | 300.035s | 179.0MiB| timeout | 0 | | | |log-slicing_bvlshr_1011.smt2 | 300.035s | 233.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a62.smt2 | 300.035s | 303.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_10780.smt2 | 300.035s | 239.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_2341.smt2 | 300.035s | 94.488MiB| timeout | 0 | | | |fft_Sz512_15128_5.smt2 | 300.035s | 76.384MiB| timeout | 0 | | | |brummayerbiere3_maxxor032.smt2 | 300.036s | 78.924MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a85.smt2 | 300.036s | 82.72MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a18.smt2 | 300.036s | 82.476MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a74.smt2 | 300.036s | 160.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_5437.smt2 | 300.036s | 138.0MiB| timeout | 0 | | | |log-slicing_bvlshr_0917.smt2 | 300.036s | 231.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_5163.smt2 | 300.036s | 150.0MiB| timeout | 0 | | | |float_pow5.smt2 | 300.036s | 182.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a50.smt2 | 300.036s | 104.0MiB| timeout | 0 | | | |log-slicing_bvudiv_18.smt2 | 300.036s | 226.0MiB| timeout | 0 | | | |mcm_52.smt2 | 300.036s | 369.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_6974.smt2 | 300.036s | 188.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_8805.smt2 | 300.036s | 185.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_10305.smt2 | 300.036s | 202.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_1095.smt2 | 300.036s | 84.388MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_203.smt2 | 300.036s | 88.624MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_7206.smt2 | 300.037s | 174.0MiB| timeout | 0 | | | |log-slicing_bvudiv_24.smt2 | 300.037s | 289.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a95.smt2 | 300.037s | 174.0MiB| timeout | 0 | | | |mcm_02.smt2 | 300.037s | 137.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a59.smt2 | 300.037s | 87.424MiB| timeout | 0 | | | |log-slicing_bvlshr_1152.smt2 | 300.037s | 316.0MiB| timeout | 0 | | | |log-slicing_bvsmod_18.smt2 | 300.037s | 229.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a35.smt2 | 300.037s | 98.784MiB| timeout | 0 | | | |bruttomesso_simple_processor_simple_processors_008_006_0032.smt2 | 300.037s | 164.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a33.smt2 | 300.037s | 87.092MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a07.smt2 | 300.038s | 83.64MiB| timeout | 0 | | | |log-slicing_bvsmod_19.smt2 | 300.038s | 226.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_1110.smt2 | 300.038s | 84.604MiB| timeout | 0 | | | |log-slicing_bvudiv_21.smt2 | 300.038s | 227.0MiB| timeout | 0 | | | |galois_iffyInterleavedModMult-8.smt2 | 300.038s | 52.616MiB| timeout | 0 | | | |log-slicing_bvudiv_20.smt2 | 300.038s | 226.0MiB| timeout | 0 | | | |log-slicing_bvlshr_0964.smt2 | 300.038s | 233.0MiB| timeout | 0 | | | |log-slicing_bvshl_1407.smt2 | 300.038s | 421.0MiB| timeout | 0 | | | |float_newton.3.1.i.smt2 | 300.038s | 149.0MiB| timeout | 0 | | | |bruttomesso_simple_processor_simple_processors_006_006_0032.smt2 | 300.038s | 117.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a52.smt2 | 300.038s | 88.424MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_1670.smt2 | 300.039s | 92.672MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a20.smt2 | 300.039s | 86.288MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a47.smt2 | 300.039s | 90.828MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a31.smt2 | 300.039s | 84.796MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a98.smt2 | 300.039s | 305.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a99.smt2 | 300.039s | 158.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a75.smt2 | 300.039s | 173.0MiB| timeout | 0 | | | |bruttomesso_lfsr_lfsr_008_015_128.smt2 | 300.039s | 294.0MiB| timeout | 0 | | | |log-slicing_bvurem_19.smt2 | 300.039s | 225.0MiB| timeout | 0 | | | |brummayerbiere3_mulhs16.smt2 | 300.039s | 61.048MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a76.smt2 | 300.039s | 83.136MiB| timeout | 0 | | | |log-slicing_bvshl_1354.smt2 | 300.039s | 419.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a32.smt2 | 300.039s | 88.592MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_6403.smt2 | 300.039s | 151.0MiB| timeout | 0 | | | |calypto_problem_12.smt2 | 300.039s | 135.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a92.smt2 | 300.039s | 350.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_7034.smt2 | 300.040s | 183.0MiB| timeout | 0 | | | |bruttomesso_simple_processor_simple_processors_008_006_0016.smt2 | 300.040s | 108.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_11872.smt2 | 300.040s | 285.0MiB| timeout | 0 | | | |brummayerbiere3_maxxormaxorand032.smt2 | 300.040s | 106.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_8956.smt2 | 300.040s | 179.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a71.smt2 | 300.040s | 157.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_4478.smt2 | 300.040s | 130.0MiB| timeout | 0 | | | |calypto_problem_23.smt2 | 300.040s | 85.804MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_10446.smt2 | 300.040s | 231.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a80.smt2 | 300.041s | 304.0MiB| timeout | 0 | | | |challenge_multiplyOverflow.smt2 | 300.041s | 62.984MiB| timeout | 0 | | | |mcm_95.smt2 | 300.041s | 235.0MiB| timeout | 0 | | | |log-slicing_bvshl_1301.smt2 | 300.041s | 417.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_2746.smt2 | 300.041s | 110.0MiB| timeout | 0 | | | |pspace_power2sum.6694.smt2 | 300.041s | 217.0MiB| timeout | 0 | | | |bruttomesso_simple_processor_simple_processors_008_007_0032.smt2 | 300.041s | 178.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_5495.smt2 | 300.041s | 136.0MiB| timeout | 0 | | | |2017-BuchwaldFried_synthesis.dump.ia32_RorMem_base_index_scale_disp2--Add32.Add32.Add32.load32.Minus32.Or32.Shr32.store32.am_shl32.0001.smt2 | 300.041s | 89.416MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a27.smt2 | 300.041s | 96.752MiB| timeout | 0 | | | |mcm_19.smt2 | 300.041s | 174.0MiB| timeout | 0 | | | |challenge_integerOverflow.smt2 | 300.041s | 90.2MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_6055.smt2 | 300.041s | 147.0MiB| timeout | 0 | | | |float_test_v5_r10_vr10_c1_s21502.smt2 | 300.041s | 456.0MiB| timeout | 0 | | | |20210219-Sydr_symbolic_memory_nested_yices_predicate_865.smt2 | 300.041s | 81.588MiB| timeout | 0 | | | |fft_Sz512_15127_5.smt2 | 300.041s | 80.168MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a05.smt2 | 300.041s | 93.488MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_10530.smt2 | 300.041s | 239.0MiB| timeout | 0 | | | |20170501-Heizmann-UltimateAutomizer_modulus_true-unreach-call_true-no-overflow.i_242.smt2 | 300.041s | 111.0MiB| timeout | 0 | | | |fft_Sz512_15127_2.smt2 | 300.041s | 73.96MiB| timeout | 0 | | | |brummayerbiere_countbits128.smt2 | 300.041s | 127.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_10592.smt2 | 300.041s | 230.0MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_453.smt2 | 300.042s | 92.28MiB| timeout | 0 | | | |bruttomesso_simple_processor_simple_processors_008_008_0016.smt2 | 300.042s | 119.0MiB| timeout | 0 | | | |log-slicing_bvurem_17.smt2 | 300.042s | 223.0MiB| timeout | 0 | | | |fft_Sz512_15127_1.smt2 | 300.042s | 76.864MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a24.smt2 | 300.042s | 92.176MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_3021.smt2 | 300.042s | 108.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a43.smt2 | 300.042s | 86.648MiB| timeout | 0 | | | |log-slicing_bvsdiv_24.smt2 | 300.042s | 232.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a55.smt2 | 300.042s | 83.972MiB| timeout | 0 | | | |log-slicing_bvsdiv_25.smt2 | 300.042s | 224.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a56.smt2 | 300.042s | 80.324MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a36.smt2 | 300.042s | 87.308MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a69.smt2 | 300.042s | 80.476MiB| timeout | 0 | | | |log-slicing_bvurem_15.smt2 | 300.042s | 68.564MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a91.smt2 | 300.042s | 682.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a42.smt2 | 300.042s | 172.0MiB| timeout | 0 | | | |log-slicing_bvshl_0824.smt2 | 300.042s | 229.0MiB| timeout | 0 | | | |fft_Sz1024_unknown.smt2 | 300.042s | 123.0MiB| timeout | 0 | | | |mcm_38.smt2 | 300.042s | 162.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_2288.smt2 | 300.042s | 103.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_12163.smt2 | 300.042s | 286.0MiB| timeout | 0 | | | |mcm_28.smt2 | 300.042s | 167.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a13.smt2 | 300.043s | 77.46MiB| timeout | 0 | | | |log-slicing_bvmul_15.smt2 | 300.043s | 75.348MiB| timeout | 0 | | | |mcm_83.smt2 | 300.043s | 214.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_12466.smt2 | 300.043s | 295.0MiB| timeout | 0 | | | |2017-BuchwaldFried_synthesis.dump.ia32_RorMem_base_index_scale_disp2--Add32.Add32.Add32.Add32.load32.Shl32.Shr32.store32.am_shl32.0001.smt2 | 300.043s | 87.448MiB| timeout | 0 | | | |log-slicing_bvmul_16.smt2 | 300.043s | 76.224MiB| timeout | 0 | | | |20210219-Sydr_symbolic_memory_bst_yices_predicate_575.smt2 | 300.043s | 54.008MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_208.smt2 | 300.043s | 88.52MiB| timeout | 0 | | | |fft_Sz1024_34824.smt2 | 300.043s | 125.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_3908.smt2 | 300.043s | 142.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_3838.smt2 | 300.043s | 118.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_11693.smt2 | 300.043s | 230.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a68.smt2 | 300.043s | 79.516MiB| timeout | 0 | | | |log-slicing_bvsub_07988.smt2 | 300.043s | 367.0MiB| timeout | 0 | | | |log-slicing_bvudiv_22.smt2 | 300.043s | 226.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_1754.smt2 | 300.043s | 103.0MiB| timeout | 0 | | | |bruttomesso_simple_processor_simple_processors_008_007_0016.smt2 | 300.044s | 119.0MiB| timeout | 0 | | | |log-slicing_bvsub_05994.smt2 | 300.044s | 344.0MiB| timeout | 0 | | | |brummayerbiere3_maxor128.smt2 | 300.044s | 475.0MiB| timeout | 0 | | | |brummayerbiere3_maxxor064.smt2 | 300.044s | 127.0MiB| timeout | 0 | | | |brummayerbiere3_isqrtaddeqcheck.smt2 | 300.044s | 51.304MiB| timeout | 0 | | | |mcm_71.smt2 | 300.044s | 228.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a17.smt2 | 300.044s | 72.004MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a22.smt2 | 300.044s | 100.0MiB| timeout | 0 | | | |log-slicing_bvlshr_1293.smt2 | 300.044s | 418.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_9623.smt2 | 300.044s | 214.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a83.smt2 | 300.044s | 81.316MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_6625.smt2 | 300.044s | 172.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a23.smt2 | 300.044s | 88.124MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a12.smt2 | 300.045s | 84.004MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_8063.smt2 | 300.045s | 179.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a30.smt2 | 300.045s | 78.004MiB| timeout | 0 | | | |log-slicing_bvmul_17.smt2 | 300.045s | 225.0MiB| timeout | 0 | | | |mcm_102.smt2 | 300.045s | 369.0MiB| timeout | 0 | | | |log-slicing_bvsdiv_20.smt2 | 300.045s | 227.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a60.smt2 | 300.045s | 92.868MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_4720.smt2 | 300.045s | 131.0MiB| timeout | 0 | | | |mcm_53.smt2 | 300.045s | 234.0MiB| timeout | 0 | | | |brummayerbiere_countbitssrl128.smt2 | 300.045s | 853.0MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_206.smt2 | 300.045s | 70.348MiB| timeout | 0 | | | |log-slicing_bvshl_0930.smt2 | 300.045s | 231.0MiB| timeout | 0 | | | |brummayerbiere3_mulhs32.smt2 | 300.045s | 93.608MiB| timeout | 0 | | | |mcm_21.smt2 | 300.045s | 174.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a63.smt2 | 300.045s | 322.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a15.smt2 | 300.045s | 121.0MiB| timeout | 0 | | | |mcm_30.smt2 | 300.045s | 154.0MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_209.smt2 | 300.045s | 88.516MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_3225.smt2 | 300.045s | 111.0MiB| timeout | 0 | | | |bruttomesso_simple_processor_simple_processors_008_005_0032.smt2 | 300.045s | 125.0MiB| timeout | 0 | | | |20190311-bv-term-small-rw-Noetzli_bv-term-small-rw_524.smt2 | 300.045s | 93.636MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_10375.smt2 | 300.045s | 208.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_1592.smt2 | 300.045s | 94.732MiB| timeout | 0 | | | |mcm_103.smt2 | 300.046s | 239.0MiB| timeout | 0 | | | |float_newton.1.2.i.smt2 | 300.046s | 259.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_9019.smt2 | 300.046s | 181.0MiB| timeout | 0 | | | |mcm_91.smt2 | 300.046s | 240.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g96.smt2 | 300.046s | 350.0MiB| timeout | 0 | | | |log-slicing_bvlshr_1199.smt2 | 300.046s | 318.0MiB| timeout | 0 | | | |brummayerbiere3_maxor064.smt2 | 300.046s | 114.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a19.smt2 | 300.046s | 91.316MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a44.smt2 | 300.046s | 83.556MiB| timeout | 0 | | | |calypto_problem_16.smt2 | 300.046s | 78.7MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_11095.smt2 | 300.046s | 241.0MiB| timeout | 0 | | | |pspace_power2sum.8087.smt2 | 300.046s | 304.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a49.smt2 | 300.046s | 112.0MiB| timeout | 0 | | | |pspace_power2sum.5500.smt2 | 300.046s | 211.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_9154.smt2 | 300.046s | 204.0MiB| timeout | 0 | | | |log-slicing_bvlshr_0776.smt2 | 300.047s | 227.0MiB| timeout | 0 | | | |log-slicing_bvashr_0664.smt2 | 300.047s | 311.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g61.smt2 | 300.047s | 663.0MiB| timeout | 0 | | | |log-slicing_bvshl_1089.smt2 | 300.047s | 314.0MiB| timeout | 0 | | | |20210219-Sydr_symbolic_memory_linear_yices_predicate_865.smt2 | 300.047s | 94.56MiB| timeout | 0 | | | |log-slicing_bvashr_0710.smt2 | 300.047s | 315.0MiB| timeout | 0 | | | |fft_Sz512_15128_1.smt2 | 300.047s | 77.04MiB| timeout | 0 | | | |log-slicing_bvudiv_19.smt2 | 300.047s | 229.0MiB| timeout | 0 | | | |fft_Sz512_15127_3.smt2 | 300.047s | 62.968MiB| timeout | 0 | | | |brummayerbiere3_minxor064.smt2 | 300.047s | 117.0MiB| timeout | 0 | | | |fft_Sz512_15128_0.smt2 | 300.047s | 76.244MiB| timeout | 0 | | | |brummayerbiere_countbitsrotate064.smt2 | 300.047s | 126.0MiB| timeout | 0 | | | |brummayerbiere2_smulov1bw32.smt2 | 300.047s | 72.784MiB| timeout | 0 | | | |mcm_23.smt2 | 300.047s | 173.0MiB| timeout | 0 | | | |log-slicing_bvmul_14.smt2 | 300.047s | 78.14MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a16.smt2 | 300.047s | 78.092MiB| timeout | 0 | | | |log-slicing_bvashr_0641.smt2 | 300.047s | 310.0MiB| timeout | 0 | | | |mcm_47.smt2 | 300.047s | 227.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a28.smt2 | 300.047s | 81.564MiB| timeout | 0 | | | |log-slicing_bvashr_0572.smt2 | 300.048s | 307.0MiB| timeout | 0 | | | |log-slicing_bvshl_0983.smt2 | 300.048s | 233.0MiB| timeout | 0 | | | |brummayerbiere3_minandmaxor064.smt2 | 300.048s | 163.0MiB| timeout | 0 | | | |RWS_Example_15.txt.smt2 | 300.048s | 168.0MiB| timeout | 0 | | | |log-slicing_bvsub_04997.smt2 | 300.048s | 262.0MiB| timeout | 0 | | | |float_newton.6.2.i.smt2 | 300.048s | 260.0MiB| timeout | 0 | | | |20210219-Sydr_symbolic_memory_bst_yices_predicate_851.smt2 | 300.048s | 82.104MiB| timeout | 0 | | | |log-slicing_bvsrem_19.smt2 | 300.048s | 227.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_8123.smt2 | 300.048s | 192.0MiB| timeout | 0 | | | |pspace_ndist.a.23992.smt2 | 300.048s | 520.0MiB| timeout | 0 | | | |float_newton.2.1.i.smt2 | 300.048s | 148.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a45.smt2 | 300.048s | 81.944MiB| timeout | 0 | | | |log-slicing_bvsmod_20.smt2 | 300.048s | 227.0MiB| timeout | 0 | | | |log-slicing_bvsrem_17.smt2 | 300.048s | 228.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a41.smt2 | 300.048s | 157.0MiB| timeout | 0 | | | |log-slicing_bvlshr_0870.smt2 | 300.048s | 229.0MiB| timeout | 0 | | | |log-slicing_bvlshr_1387.smt2 | 300.048s | 420.0MiB| timeout | 0 | | | |log-slicing_bvadd_24418.smt2 | 300.048s | 977.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_1361.smt2 | 300.048s | 84.36MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a88.smt2 | 300.048s | 592.0MiB| timeout | 0 | | | |log-slicing_bvsub_13970.smt2 | 300.048s | 677.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_1177.smt2 | 300.048s | 87.392MiB| timeout | 0 | | | |mcm_69.smt2 | 300.048s | 222.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_6368.smt2 | 300.048s | 147.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a25.smt2 | 300.048s | 93.828MiB| timeout | 0 | | | |log-slicing_bvurem_22.smt2 | 300.049s | 226.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g32.smt2 | 300.049s | 684.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_6969.smt2 | 300.049s | 182.0MiB| timeout | 0 | | | |pspace_power2sum.9480.smt2 | 300.049s | 383.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_6769.smt2 | 300.049s | 180.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_2066.smt2 | 300.049s | 99.0MiB| timeout | 0 | | | |log-slicing_bvsdiv_18.smt2 | 300.049s | 226.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_9161.smt2 | 300.049s | 196.0MiB| timeout | 0 | | | |log-slicing_bvmul_18.smt2 | 300.049s | 224.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a87.smt2 | 300.049s | 507.0MiB| timeout | 0 | | | |mcm_32.smt2 | 300.049s | 164.0MiB| timeout | 0 | | | |pspace_power2sum.6893.smt2 | 300.049s | 286.0MiB| timeout | 0 | | | |mcm_81.smt2 | 300.049s | 238.0MiB| timeout | 0 | | | |pspace_power2sum.8286.smt2 | 300.049s | 307.0MiB| timeout | 0 | | | |log-slicing_bvshl_1142.smt2 | 300.049s | 316.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_8352.smt2 | 300.049s | 195.0MiB| timeout | 0 | | | |log-slicing_bvudiv_23.smt2 | 300.049s | 232.0MiB| timeout | 0 | | | |log-slicing_bvashr_0687.smt2 | 300.050s | 314.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_8566.smt2 | 300.050s | 198.0MiB| timeout | 0 | | | |mcm_98.smt2 | 300.050s | 224.0MiB| timeout | 0 | | | |log-slicing_bvurem_16.smt2 | 300.050s | 71.696MiB| timeout | 0 | | | |log-slicing_bvurem_18.smt2 | 300.050s | 225.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_10217.smt2 | 300.050s | 201.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_12114.smt2 | 300.050s | 289.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_8503.smt2 | 300.050s | 182.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_4109.smt2 | 300.050s | 117.0MiB| timeout | 0 | | | |mcm_51.smt2 | 300.050s | 196.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_8201.smt2 | 300.050s | 175.0MiB| timeout | 0 | | | |mcm_46.smt2 | 300.051s | 356.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a54.smt2 | 300.051s | 97.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_4285.smt2 | 300.051s | 136.0MiB| timeout | 0 | | | |log-slicing_bvsdiv_22.smt2 | 300.051s | 224.0MiB| timeout | 0 | | | |log-slicing_bvsub_04000.smt2 | 300.051s | 182.0MiB| timeout | 0 | | | |log-slicing_bvsub_10979.smt2 | 300.051s | 546.0MiB| timeout | 0 | | | |brummayerbiere3_minor128.smt2 | 300.051s | 434.0MiB| timeout | 0 | | | |mcm_89.smt2 | 300.051s | 237.0MiB| timeout | 0 | | | |mcm_92.smt2 | 300.051s | 189.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_8688.smt2 | 300.051s | 183.0MiB| timeout | 0 | | | |pspace_power2sum.7689.smt2 | 300.051s | 255.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_7828.smt2 | 300.051s | 173.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a53.smt2 | 300.051s | 94.688MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_10410.smt2 | 300.051s | 210.0MiB| timeout | 0 | | | |pspace_power2sum.8684.smt2 | 300.051s | 375.0MiB| timeout | 0 | | | |brummayerbiere2_umulov1bw192.smt2 | 300.051s | 468.0MiB| timeout | 0 | | | |log-slicing_bvudiv_25.smt2 | 300.051s | 289.0MiB| timeout | 0 | | | |mcm_97.smt2 | 300.052s | 237.0MiB| timeout | 0 | | | |float_newton.5.2.i.smt2 | 300.052s | 259.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a64.smt2 | 300.052s | 592.0MiB| timeout | 0 | | | |mcm_65.smt2 | 300.052s | 241.0MiB| timeout | 0 | | | |mcm_73.smt2 | 300.052s | 193.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_9097.smt2 | 300.052s | 194.0MiB| timeout | 0 | | | |float_newton.2.2.i.smt2 | 300.052s | 258.0MiB| timeout | 0 | | | |mcm_31.smt2 | 300.052s | 202.0MiB| timeout | 0 | | | |log-slicing_bvashr_0733.smt2 | 300.052s | 316.0MiB| timeout | 0 | | | |log-slicing_bvsub_06991.smt2 | 300.052s | 356.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_4843.smt2 | 300.052s | 147.0MiB| timeout | 0 | | | |brummayerbiere2_umulov1bw112.smt2 | 300.052s | 198.0MiB| timeout | 0 | | | |mcm_79.smt2 | 300.052s | 364.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a65.smt2 | 300.052s | 614.0MiB| timeout | 0 | | | |mcm_59.smt2 | 300.052s | 238.0MiB| timeout | 0 | | | |log-slicing_bvashr_0618.smt2 | 300.052s | 309.0MiB| timeout | 0 | | | |log-slicing_bvadd_28853.smt2 | 300.052s | 1028.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_5893.smt2 | 300.052s | 145.0MiB| timeout | 0 | | | |log-slicing_bvsdiv_23.smt2 | 300.052s | 226.0MiB| timeout | 0 | | | |float_newton.7.3.i.smt2 | 300.053s | 428.0MiB| timeout | 0 | | | |brummayerbiere3_minxor128.smt2 | 300.053s | 434.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_9221.smt2 | 300.053s | 186.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_6832.smt2 | 300.053s | 166.0MiB| timeout | 0 | | | |brummayerbiere3_maxand128.smt2 | 300.053s | 532.0MiB| timeout | 0 | | | |log-slicing_bvashr_0595.smt2 | 300.053s | 307.0MiB| timeout | 0 | | | |mcm_72.smt2 | 300.053s | 239.0MiB| timeout | 0 | | | |mcm_82.smt2 | 300.053s | 288.0MiB| timeout | 0 | | | |log-slicing_bvlshr_1058.smt2 | 300.053s | 313.0MiB| timeout | 0 | | | |log-slicing_bvsrem_15.smt2 | 300.053s | 68.264MiB| timeout | 0 | | | |mcm_39.smt2 | 300.053s | 257.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_7891.smt2 | 300.053s | 164.0MiB| timeout | 0 | | | |brummayerbiere2_umulov1bw128.smt2 | 300.053s | 309.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g94.smt2 | 300.053s | 495.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g41.smt2 | 300.053s | 612.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g97.smt2 | 300.054s | 971.0MiB| timeout | 0 | | | |float_test_v5_r10_vr5_c1_s8690.smt2 | 300.054s | 453.0MiB| timeout | 0 | | | |galois_iffyInterleavedModMult-32.smt2 | 300.054s | 160.0MiB| timeout | 0 | | | |float_mult2.c.50.smt2 | 300.054s | 501.0MiB| timeout | 0 | | | |float_test_v7_r7_vr1_c1_s4574.smt2 | 300.054s | 453.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_11183.smt2 | 300.054s | 225.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_5662.smt2 | 300.054s | 138.0MiB| timeout | 0 | | | |20200328-Favaro_mul_mba_synthesis.smt2 | 300.054s | 157.0MiB| timeout | 0 | | | |mcm_96.smt2 | 300.054s | 369.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_6910.smt2 | 300.054s | 173.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g83.smt2 | 300.054s | 971.0MiB| timeout | 0 | | | |mcm_62.smt2 | 300.054s | 369.0MiB| timeout | 0 | | | |mcm_100.smt2 | 300.054s | 240.0MiB| timeout | 0 | | | |float_test_v7_r7_vr1_c1_s24449.smt2 | 300.055s | 453.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a94.smt2 | 300.055s | 675.0MiB| timeout | 0 | | | |mcm_50.smt2 | 300.055s | 231.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a96.smt2 | 300.055s | 352.0MiB| timeout | 0 | | | |log-slicing_bvashr_0549.smt2 | 300.055s | 306.0MiB| timeout | 0 | | | |log-slicing_bvurem_21.smt2 | 300.055s | 229.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_2545.smt2 | 300.055s | 99.0MiB| timeout | 0 | | | |mcm_66.smt2 | 300.055s | 369.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a39.smt2 | 300.055s | 97.712MiB| timeout | 0 | | | |log-slicing_bvsrem_20.smt2 | 300.055s | 227.0MiB| timeout | 0 | | | |log-slicing_bvashr_0526.smt2 | 300.055s | 305.0MiB| timeout | 0 | | | |log-slicing_bvshl_1460.smt2 | 300.055s | 423.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g71.smt2 | 300.055s | 494.0MiB| timeout | 0 | | | |brummayerbiere3_minxorminand064.smt2 | 300.055s | 226.0MiB| timeout | 0 | | | |brummayerbiere2_umulov1bw096.smt2 | 300.056s | 162.0MiB| timeout | 0 | | | |brummayerbiere3_maxxor128.smt2 | 300.056s | 475.0MiB| timeout | 0 | | | |mcm_22.smt2 | 300.056s | 221.0MiB| timeout | 0 | | | |pipe_pipe-noabs.atlas.qf_bv.smt2 | 300.056s | 114.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a40.smt2 | 300.056s | 90.644MiB| timeout | 0 | | | |mcm_40.smt2 | 300.056s | 229.0MiB| timeout | 0 | | | |pspace_power2sum.9679.smt2 | 300.056s | 317.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a86.smt2 | 300.056s | 607.0MiB| timeout | 0 | | | |log-slicing_bvadd_27079.smt2 | 300.056s | 997.0MiB| timeout | 0 | | | |pspace_power2sum.7291.smt2 | 300.056s | 234.0MiB| timeout | 0 | | | |float_newton.3.3.i.smt2 | 300.057s | 428.0MiB| timeout | 0 | | | |bruttomesso_simple_processor_simple_processors_008_008_0032.smt2 | 300.057s | 278.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g38.smt2 | 300.057s | 598.0MiB| timeout | 0 | | | |pspace_power2sum.5898.smt2 | 300.057s | 278.0MiB| timeout | 0 | | | |brummayerbiere3_maxxormaxorand064.smt2 | 300.057s | 311.0MiB| timeout | 0 | | | |brummayerbiere3_mulhs64.smt2 | 300.057s | 186.0MiB| timeout | 0 | | | |pspace_power2sum.7888.smt2 | 300.057s | 245.0MiB| timeout | 0 | | | |mcm_37.smt2 | 300.057s | 202.0MiB| timeout | 0 | | | |mcm_77.smt2 | 300.057s | 239.0MiB| timeout | 0 | | | |mcm_27.smt2 | 300.057s | 224.0MiB| timeout | 0 | | | |mcm_64.smt2 | 300.058s | 369.0MiB| timeout | 0 | | | |log-slicing_bvsub_09982.smt2 | 300.058s | 527.0MiB| timeout | 0 | | | |mcm_49.smt2 | 300.058s | 186.0MiB| timeout | 0 | | | |log-slicing_bvsub_14967.smt2 | 300.058s | 703.0MiB| timeout | 0 | | | |mcm_74.smt2 | 300.058s | 369.0MiB| timeout | 0 | | | |log-slicing_bvsub_08985.smt2 | 300.058s | 377.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_10098.smt2 | 300.058s | 203.0MiB| timeout | 0 | | | |pspace_power2sum.8883.smt2 | 300.059s | 308.0MiB| timeout | 0 | | | |pspace_power2sum.7092.smt2 | 300.059s | 250.0MiB| timeout | 0 | | | |brummayerbiere3_minandmaxor128.smt2 | 300.059s | 866.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g25.smt2 | 300.059s | 582.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a89.smt2 | 300.059s | 613.0MiB| timeout | 0 | | | |mcm_57.smt2 | 300.059s | 369.0MiB| timeout | 0 | | | |mcm_67.smt2 | 300.059s | 237.0MiB| timeout | 0 | | | |float_newton.4.2.i.smt2 | 300.060s | 257.0MiB| timeout | 0 | | | |float_mult1.c.40.smt2 | 300.060s | 446.0MiB| timeout | 0 | | | |float_test_v5_r10_vr10_c1_s7608.smt2 | 300.060s | 450.0MiB| timeout | 0 | | | |log-slicing_bvadd_22644.smt2 | 300.060s | 966.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_11015.smt2 | 300.060s | 227.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a61.smt2 | 300.060s | 618.0MiB| timeout | 0 | | | |float_newton.3.2.i.smt2 | 300.060s | 262.0MiB| timeout | 0 | | | |mcm_124.smt2 | 300.060s | 426.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a84.smt2 | 300.061s | 553.0MiB| timeout | 0 | | | |mcm_61.smt2 | 300.061s | 241.0MiB| timeout | 0 | | | |float_test_v7_r7_vr10_c1_s32506.smt2 | 300.061s | 449.0MiB| timeout | 0 | | | |mcm_78.smt2 | 300.061s | 381.0MiB| timeout | 0 | | | |pspace_power2sum.8485.smt2 | 300.061s | 308.0MiB| timeout | 0 | | | |mcm_75.smt2 | 300.061s | 235.0MiB| timeout | 0 | | | |float_newton.6.3.i.smt2 | 300.061s | 428.0MiB| timeout | 0 | | | |pspace_ndist.a.29980.smt2 | 300.062s | 686.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g35.smt2 | 300.062s | 494.0MiB| timeout | 0 | | | |brummayerbiere3_minand128.smt2 | 300.062s | 436.0MiB| timeout | 0 | | | |log-slicing_bvshl_1248.smt2 | 300.062s | 416.0MiB| timeout | 0 | | | |mcm_76.smt2 | 300.062s | 369.0MiB| timeout | 0 | | | |mcm_58.smt2 | 300.062s | 369.0MiB| timeout | 0 | | | |log-slicing_bvlshr_1246.smt2 | 300.062s | 416.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a26.smt2 | 300.062s | 96.412MiB| timeout | 0 | | | |pspace_power2sum.9082.smt2 | 300.062s | 379.0MiB| timeout | 0 | | | |mcm_63.smt2 | 300.063s | 244.0MiB| timeout | 0 | | | |mcm_88.smt2 | 300.063s | 369.0MiB| timeout | 0 | | | |brummayerbiere2_smulov2bw128.smt2 | 300.063s | 270.0MiB| timeout | 0 | | | |mcm_90.smt2 | 300.063s | 369.0MiB| timeout | 0 | | | |pspace_power2sum.6495.smt2 | 300.063s | 234.0MiB| timeout | 0 | | | |float_test_v7_r12_vr1_c1_s22787.smt2 | 300.063s | 776.0MiB| timeout | 0 | | | |mcm_25.smt2 | 300.064s | 173.0MiB| timeout | 0 | | | |pspace_power2sum.9281.smt2 | 300.064s | 312.0MiB| timeout | 0 | | | |mcm_56.smt2 | 300.064s | 383.0MiB| timeout | 0 | | | |log-slicing_bvslt_16145.smt2 | 300.064s | 887.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g28.smt2 | 300.064s | 675.0MiB| timeout | 0 | | | |brummayerbiere_countbits256.smt2 | 300.064s | 588.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g63.smt2 | 300.065s | 602.0MiB| timeout | 0 | | | |brummayerbiere_countbitsrotate128.smt2 | 300.065s | 352.0MiB| timeout | 0 | | | |pspace_ndist.a.27984.smt2 | 300.065s | 572.0MiB| timeout | 0 | | | |mcm_16.smt2 | 300.065s | 258.0MiB| timeout | 0 | | | |mcm_55.smt2 | 300.065s | 198.0MiB| timeout | 0 | | | |pspace_power2sum.9878.smt2 | 300.065s | 388.0MiB| timeout | 0 | | | |mcm_80.smt2 | 300.065s | 369.0MiB| timeout | 0 | | | |brummayerbiere2_smulov2bw192.smt2 | 300.066s | 466.0MiB| timeout | 0 | | | |float_test_v7_r7_vr5_c1_s19694.smt2 | 300.066s | 451.0MiB| timeout | 0 | | | |log-slicing_bvadd_23531.smt2 | 300.066s | 973.0MiB| timeout | 0 | | | |log-slicing_bvult_15970.smt2 | 300.066s | 885.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g23.smt2 | 300.066s | 968.0MiB| timeout | 0 | | | |pspace_power2sum.6296.smt2 | 300.066s | 281.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g42.smt2 | 300.066s | 617.0MiB| timeout | 0 | | | |float_test_v5_r15_vr1_c1_s26845.smt2 | 300.066s | 656.0MiB| timeout | 0 | | | |float_test_v7_r12_vr5_c1_s29826.smt2 | 300.067s | 774.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g53.smt2 | 300.067s | 610.0MiB| timeout | 0 | | | |float_newton.2.3.i.smt2 | 300.067s | 428.0MiB| timeout | 0 | | | |brummayerbiere2_umulov1bw160.smt2 | 300.067s | 362.0MiB| timeout | 0 | | | |mcm_108.smt2 | 300.067s | 683.0MiB| timeout | 0 | | | |mcm_111.smt2 | 300.067s | 671.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g81.smt2 | 300.067s | 702.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g75.smt2 | 300.067s | 602.0MiB| timeout | 0 | | | |float_newton.1.3.i.smt2 | 300.067s | 428.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g12.smt2 | 300.067s | 496.0MiB| timeout | 0 | | | |float_newton.5.3.i.smt2 | 300.068s | 428.0MiB| timeout | 0 | | | |float_test_v7_r12_vr10_c1_s15994.smt2 | 300.068s | 775.0MiB| timeout | 0 | | | |pspace_ndist.a.24491.smt2 | 300.068s | 521.0MiB| timeout | 0 | | | |pspace_power2sum.7490.smt2 | 300.069s | 230.0MiB| timeout | 0 | | | |mcm_68.smt2 | 300.069s | 356.0MiB| timeout | 0 | | | |2019-Wolf-fmbench_2018E_VexRiscv-regch0-20-unrolled-nomem.smt2 | 300.069s | 467.0MiB| timeout | 0 | | | |log-slicing_bvsub_16961.smt2 | 300.071s | 726.0MiB| timeout | 0 | | | |brummayerbiere3_minxorminand128.smt2 | 300.071s | 1459.0MiB| timeout | 0 | | | |float_test_v7_r7_vr10_c1_s10625.smt2 | 300.071s | 456.0MiB| timeout | 0 | | | |float_mult2.c.40.smt2 | 300.071s | 460.0MiB| timeout | 0 | | | |pspace_ndist.a.26986.smt2 | 300.072s | 547.0MiB| timeout | 0 | | | |log-slicing_bvadd_29740.smt2 | 300.072s | 1035.0MiB| timeout | 0 | | | |20210219-Sydr_master_yices_predicate_11921.smt2 | 300.072s | 285.0MiB| timeout | 0 | | | |float_newton.4.3.i.smt2 | 300.072s | 428.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a93.smt2 | 300.072s | 522.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g54.smt2 | 300.072s | 980.0MiB| timeout | 0 | | | |log-slicing_bvadd_21757.smt2 | 300.073s | 940.0MiB| timeout | 0 | | | |pspace_ndist.a.27485.smt2 | 300.073s | 560.0MiB| timeout | 0 | | | |log-slicing_bvsub_15964.smt2 | 300.073s | 709.0MiB| timeout | 0 | | | |mcm_139.smt2 | 300.073s | 676.0MiB| timeout | 0 | | | |log-slicing_bvsub_19952.smt2 | 300.073s | 1017.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_a82.smt2 | 300.074s | 676.0MiB| timeout | 0 | | | |log-slicing_bvsub_12973.smt2 | 300.074s | 666.0MiB| timeout | 0 | | | |float_test_v5_r15_vr10_c1_s25268.smt2 | 300.074s | 653.0MiB| timeout | 0 | | | |brummayerbiere2_smulov2bw224.smt2 | 300.074s | 696.0MiB| timeout | 0 | | | |mcm_128.smt2 | 300.075s | 822.0MiB| timeout | 0 | | | |pspace_ndist.a.28483.smt2 | 300.075s | 569.0MiB| timeout | 0 | | | |mcm_116.smt2 | 300.075s | 905.0MiB| timeout | 0 | | | |pspace_ndist.a.24990.smt2 | 300.075s | 522.0MiB| timeout | 0 | | | |pspace_ndist.a.25988.smt2 | 300.075s | 540.0MiB| timeout | 0 | | | |pspace_ndist.a.22495.smt2 | 300.075s | 542.0MiB| timeout | 0 | | | |log-slicing_bvsub_11976.smt2 | 300.075s | 660.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g87.smt2 | 300.076s | 1028.0MiB| timeout | 0 | | | |log-slicing_bvslt_14659.smt2 | 300.076s | 886.0MiB| timeout | 0 | | | |mcm_134.smt2 | 300.077s | 1100.0MiB| timeout | 0 | | | |float_test_v5_r10_vr5_c1_s13679.smt2 | 300.077s | 447.0MiB| timeout | 0 | | | |float_test_v5_r15_vr10_c1_s14516.smt2 | 300.077s | 655.0MiB| timeout | 0 | | | |pspace_ndist.a.26487.smt2 | 300.077s | 550.0MiB| timeout | 0 | | | |float_test_v5_r15_vr5_c1_s23844.smt2 | 300.077s | 687.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g19.smt2 | 300.077s | 498.0MiB| timeout | 0 | | | |log-slicing_bvsub_17958.smt2 | 300.078s | 734.0MiB| timeout | 0 | | | |mcm_138.smt2 | 300.078s | 1085.0MiB| timeout | 0 | | | |log-slicing_bvsub_21946.smt2 | 300.078s | 1073.0MiB| timeout | 0 | | | |brummayerbiere2_umulov1bw224.smt2 | 300.078s | 615.0MiB| timeout | 0 | | | |pspace_ndist.a.21497.smt2 | 300.079s | 512.0MiB| timeout | 0 | | | |log-slicing_bvslt_11687.smt2 | 300.080s | 882.0MiB| timeout | 0 | | | |mcm_137.smt2 | 300.080s | 1127.0MiB| timeout | 0 | | | |float_test_v5_r15_vr1_c1_s8236.smt2 | 300.080s | 684.0MiB| timeout | 0 | | | |log-slicing_bvult_9988.smt2 | 300.080s | 880.0MiB| timeout | 0 | | | |float_test_v7_r12_vr1_c1_s703.smt2 | 300.080s | 775.0MiB| timeout | 0 | | | |log-slicing_bvsub_18955.smt2 | 300.080s | 1004.0MiB| timeout | 0 | | | |pspace_ndist.a.23493.smt2 | 300.080s | 516.0MiB| timeout | 0 | | | |log-slicing_bvadd_27966.smt2 | 300.081s | 1006.0MiB| timeout | 0 | | | |pspace_ndist.a.29481.smt2 | 300.081s | 685.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g92.smt2 | 300.081s | 1936.0MiB| timeout | 0 | | | |mcm_143.smt2 | 300.081s | 824.0MiB| timeout | 0 | | | |pspace_ndist.a.28982.smt2 | 300.081s | 574.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g24.smt2 | 300.082s | 992.0MiB| timeout | 0 | | | |log-slicing_bvult_8991.smt2 | 300.082s | 880.0MiB| timeout | 0 | | | |pspace_ndist.a.22994.smt2 | 300.082s | 517.0MiB| timeout | 0 | | | |float_test_v5_r15_vr5_c1_s26657.smt2 | 300.083s | 688.0MiB| timeout | 0 | | | |mcm_144.smt2 | 300.083s | 1212.0MiB| timeout | 0 | | | |log-slicing_bvult_13976.smt2 | 300.083s | 882.0MiB| timeout | 0 | | | |log-slicing_bvslt_10201.smt2 | 300.083s | 881.0MiB| timeout | 0 | | | |brummayerbiere2_umulov1bw256.smt2 | 300.083s | 839.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g44.smt2 | 300.083s | 972.0MiB| timeout | 0 | | | |float_test_v7_r12_vr10_c1_s30410.smt2 | 300.083s | 777.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g76.smt2 | 300.084s | 1006.0MiB| timeout | 0 | | | |mcm_141.smt2 | 300.084s | 1098.0MiB| timeout | 0 | | | |mcm_114.smt2 | 300.084s | 625.0MiB| timeout | 0 | | | |float_mult1.c.50.smt2 | 300.084s | 500.0MiB| timeout | 0 | | | |log-slicing_bvslt_12430.smt2 | 300.084s | 882.0MiB| timeout | 0 | | | |pspace_ndist.a.25489.smt2 | 300.084s | 527.0MiB| timeout | 0 | | | |float_test_v5_r10_vr10_c1_s15708.smt2 | 300.085s | 450.0MiB| timeout | 0 | | | |float_test_v7_r12_vr10_c1_s18160.smt2 | 300.085s | 776.0MiB| timeout | 0 | | | |brummayerbiere2_smulov2bw256.smt2 | 300.085s | 826.0MiB| timeout | 0 | | | |log-slicing_bvult_10985.smt2 | 300.086s | 881.0MiB| timeout | 0 | | | |float_test_v5_r15_vr5_c1_s8246.smt2 | 300.086s | 691.0MiB| timeout | 0 | | | |mcm_129.smt2 | 300.086s | 1122.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g43.smt2 | 300.087s | 971.0MiB| timeout | 0 | | | |mcm_106.smt2 | 300.088s | 835.0MiB| timeout | 0 | | | |log-slicing_bvslt_13173.smt2 | 300.088s | 884.0MiB| timeout | 0 | | | |log-slicing_bvslt_13916.smt2 | 300.088s | 884.0MiB| timeout | 0 | | | |log-slicing_bvsub_20949.smt2 | 300.089s | 1029.0MiB| timeout | 0 | | | |float_sin2.c.5.smt2 | 300.089s | 716.0MiB| timeout | 0 | | | |log-slicing_bvadd_25305.smt2 | 300.089s | 983.0MiB| timeout | 0 | | | |float_test_v7_r17_vr1_c1_s24331.smt2 | 300.090s | 972.0MiB| timeout | 0 | | | |log-slicing_bvult_14973.smt2 | 300.091s | 884.0MiB| timeout | 0 | | | |mcm_110.smt2 | 300.092s | 823.0MiB| timeout | 0 | | | |mcm_133.smt2 | 300.094s | 1062.0MiB| timeout | 0 | | | |log-slicing_bvult_12979.smt2 | 300.095s | 881.0MiB| timeout | 0 | | | |log-slicing_bvadd_26192.smt2 | 300.096s | 989.0MiB| timeout | 0 | | | |mcm_149.smt2 | 300.096s | 1028.0MiB| timeout | 0 | | | |mcm_157.smt2 | 300.096s | 1077.0MiB| timeout | 0 | | | |brummayerbiere3_maxor256.smt2 | 300.096s | 1663.0MiB| timeout | 0 | | | |float_test_v7_r17_vr1_c1_s23882.smt2 | 300.097s | 974.0MiB| timeout | 0 | | | |log-slicing_bvult_17964.smt2 | 300.097s | 1736.0MiB| timeout | 0 | | | |mcm_127.smt2 | 300.097s | 1088.0MiB| timeout | 0 | | | |mcm_147.smt2 | 300.098s | 992.0MiB| timeout | 0 | | | |brummayerbiere3_maxxormaxorand128.smt2 | 300.098s | 1534.0MiB| timeout | 0 | | | |mcm_120.smt2 | 300.099s | 1105.0MiB| timeout | 0 | | | |mcm_136.smt2 | 300.099s | 1118.0MiB| timeout | 0 | | | |float_div.c.30.smt2 | 300.099s | 750.0MiB| timeout | 0 | | | |mcm_105.smt2 | 300.099s | 671.0MiB| timeout | 0 | | | |mcm_130.smt2 | 300.100s | 799.0MiB| timeout | 0 | | | |float_test_v7_r17_vr5_c1_s4772.smt2 | 300.100s | 971.0MiB| timeout | 0 | | | |mcm_119.smt2 | 300.101s | 1101.0MiB| timeout | 0 | | | |mcm_142.smt2 | 300.102s | 1020.0MiB| timeout | 0 | | | |brummayerbiere3_minxor256.smt2 | 300.102s | 1490.0MiB| timeout | 0 | | | |brummayerbiere3_minand256.smt2 | 300.102s | 1498.0MiB| timeout | 0 | | | |mcm_135.smt2 | 300.104s | 1208.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g98.smt2 | 300.105s | 1936.0MiB| timeout | 0 | | | |log-slicing_bvsub_23940.smt2 | 300.106s | 1040.0MiB| timeout | 0 | | | |mcm_145.smt2 | 300.106s | 1081.0MiB| timeout | 0 | | | |mcm_150.smt2 | 300.107s | 831.0MiB| timeout | 0 | | | |log-slicing_bvult_19958.smt2 | 300.107s | 1737.0MiB| timeout | 0 | | | |float_test_v7_r17_vr1_c1_s30331.smt2 | 300.107s | 973.0MiB| timeout | 0 | | | |float_test_v7_r17_vr10_c1_s3680.smt2 | 300.108s | 972.0MiB| timeout | 0 | | | |mcm_132.smt2 | 300.108s | 1150.0MiB| timeout | 0 | | | |brummayerbiere2_smulov2bw320.smt2 | 300.108s | 1359.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g78.smt2 | 300.108s | 1935.0MiB| timeout | 0 | | | |log-slicing_bvsub_22943.smt2 | 300.109s | 885.0MiB| timeout | 0 | | | |mcm_151.smt2 | 300.109s | 987.0MiB| timeout | 0 | | | |float_sin2.c.10.smt2 | 300.109s | 1309.0MiB| timeout | 0 | | | |float_test_v7_r12_vr1_c1_s10576.smt2 | 300.110s | 774.0MiB| timeout | 0 | | | |log-slicing_bvult_11982.smt2 | 300.110s | 881.0MiB| timeout | 0 | | | |log-slicing_bvslt_18374.smt2 | 300.111s | 1736.0MiB| timeout | 0 | | | |log-slicing_bvult_16967.smt2 | 300.112s | 1739.0MiB| timeout | 0 | | | |log-slicing_bvslt_19117.smt2 | 300.112s | 1737.0MiB| timeout | 0 | | | |float_test_v7_r17_vr10_c1_s18654.smt2 | 300.113s | 968.0MiB| timeout | 0 | | | |20210312-Bouvier_vlsat3_g39.smt2 | 300.113s | 968.0MiB| timeout | 0 | | | |brummayerbiere_nextpoweroftwo512.smt2 | 300.113s | 1874.0MiB| timeout | 0 | | | |brummayerbiere3_maxand256.smt2 | 300.114s | 1487.0MiB| timeout | 0 | | | |mcm_126.smt2 | 300.114s | 1089.0MiB| timeout | 0 | | | |float_test_v7_r17_vr5_c1_s2807.smt2 | 300.115s | 974.0MiB| timeout | 0 | | | |log-slicing_bvult_23946.smt2 | 300.115s | 1739.0MiB| timeout | 0 | | | |float_test_v7_r17_vr10_c1_s8773.smt2 | 300.116s | 970.0MiB| timeout | 0 | | | |brummayerbiere3_minor256.smt2 | 300.117s | 1492.0MiB| timeout | 0 | | | |mcm_154.smt2 | 300.118s | 1090.0MiB| timeout | 0 | | | |float_test_v7_r17_vr5_c1_s25451.smt2 | 300.118s | 968.0MiB| timeout | 0 | | | |brummayerbiere2_smulov4bw0512.smt2 | 300.118s | 1184.0MiB| timeout | 0 | | | |log-slicing_bvult_25940.smt2 | 300.118s | 1740.0MiB| timeout | 0 | | | |mcm_153.smt2 | 300.121s | 1180.0MiB| timeout | 0 | | | |log-slicing_bvslt_19860.smt2 | 300.121s | 1739.0MiB| timeout | 0 | | | |log-slicing_bvult_18961.smt2 | 300.122s | 1736.0MiB| timeout | 0 | | | |2019-Wolf-fmbench_2019A_picorv32_mutCX_QF_BV_NONINCR.smt2 | 300.123s | 1962.0MiB| timeout | 0 | | | |log-slicing_bvult_22949.smt2 | 300.123s | 1739.0MiB| timeout | 0 | | | |mcm_148.smt2 | 300.124s | 1105.0MiB| timeout | 0 | | | |mcm_140.smt2 | 300.125s | 989.0MiB| timeout | 0 | | | |log-slicing_bvslt_17631.smt2 | 300.126s | 1735.0MiB| timeout | 0 | | | |brummayerbiere2_smulov4bw0640.smt2 | 300.127s | 1609.0MiB| timeout | 0 | | | |log-slicing_bvult_21952.smt2 | 300.128s | 1738.0MiB| timeout | 0 | | | |mcm_122.smt2 | 300.128s | 1088.0MiB| timeout | 0 | | | |log-slicing_bvslt_15402.smt2 | 300.129s | 887.0MiB| timeout | 0 | | | |log-slicing_bvslt_16888.smt2 | 300.132s | 1736.0MiB| timeout | 0 | | | |log-slicing_bvult_24943.smt2 | 300.133s | 1740.0MiB| timeout | 0 | | | |float_div.c.50.smt2 | 300.133s | 1317.0MiB| timeout | 0 | | | |brummayerbiere_countbitsrotate256.smt2 | 300.134s | 1045.0MiB| timeout | 0 | | | |log-slicing_bvsmod_17.smt2 | 300.135s | 231.0MiB| timeout | 0 | | | |mcm_146.smt2 | 300.136s | 1079.0MiB| timeout | 0 | | | |log-slicing_bvult_20955.smt2 | 300.139s | 1737.0MiB| timeout | 0 | | | |mcm_125.smt2 | 300.142s | 1178.0MiB| timeout | 0 | | | |mcm_159.smt2 | 300.143s | 1948.0MiB| timeout | 0 | | | |mcm_121.smt2 | 300.146s | 1211.0MiB| timeout | 0 | | | |brummayerbiere2_umulov2bw0640.smt2 | 300.146s | 1624.0MiB| timeout | 0 | | | |brummayerbiere_countbits512.smt2 | 300.147s | 1825.0MiB| timeout | 0 | | | |brummayerbiere2_smulov3bw0640.smt2 | 300.147s | 1607.0MiB| timeout | 0 | | | |brummayerbiere_countbitssrl256.smt2 | 300.147s | 3021.0MiB| timeout | 0 | | | |2019-Wolf-fmbench_2019A_picorv32_mutAY_QF_BV_NONINCR.smt2 | 300.151s | 1577.0MiB| timeout | 0 | | | |brummayerbiere3_maxandminor256.smt2 | 300.154s | 2952.0MiB| timeout | 0 | | | |float_sin2.c.15.smt2 | 300.156s | 2098.0MiB| timeout | 0 | | | |brummayerbiere3_maxxor256.smt2 | 300.157s | 2958.0MiB| timeout | 0 | | | |brummayerbiere3_minandmaxor256.smt2 | 300.158s | 3147.0MiB| timeout | 0 | | | |float_sqrt.c.10.smt2 | 300.161s | 1518.0MiB| timeout | 0 | | | |mcm_168.smt2 | 300.162s | 2157.0MiB| timeout | 0 | | | |2019-Wolf-fmbench_2018E_VexRiscv-regch0-30-unrolled-nomem.smt2 | 300.168s | 1632.0MiB| timeout | 0 | | | |mcm_161.smt2 | 300.173s | 2509.0MiB| timeout | 0 | | | |mcm_171.smt2 | 300.174s | 2470.0MiB| timeout | 0 | | | |brummayerbiere2_smulov2bw384.smt2 | 300.175s | 2051.0MiB| timeout | 0 | | | |mcm_158.smt2 | 300.179s | 2058.0MiB| timeout | 0 | | | |mcm_163.smt2 | 300.181s | 2739.0MiB| timeout | 0 | | | |2019-Wolf-fmbench_2019A_picorv32_mutAX_QF_BV_NONINCR.smt2 | 300.193s | 2356.0MiB| timeout | 0 | | | |galois_iffyInterleavedModMult-128.smt2 | 300.195s | 2191.0MiB| timeout | 0 | | | |brummayerbiere2_umulov2bw0768.smt2 | 300.197s | 2495.0MiB| timeout | 0 | | | |20210219-Sydr_symbolic_memory_bst_faad_predicate_1530.smt2 | 300.198s | 3269.0MiB| timeout | 0 | | | |brummayerbiere3_minxorminand256.smt2 | 300.200s | 5747.0MiB| timeout | 0 | | | |2019-Wolf-fmbench_2018E_picorv32-check-unrolled-nomem.smt2 | 300.200s | 3567.0MiB| timeout | 0 | | | |brummayerbiere2_smulov3bw0768.smt2 | 300.201s | 2528.0MiB| timeout | 0 | | | |mcm_160.smt2 | 300.208s | 2105.0MiB| timeout | 0 | | | |mcm_165.smt2 | 300.227s | 2558.0MiB| timeout | 0 | | | |brummayerbiere2_smulov2bw512.smt2 | 300.230s | 3008.0MiB| timeout | 0 | | | |brummayerbiere2_smulov3bw0896.smt2 | 300.230s | 3167.0MiB| timeout | 0 | | | |float_sqrt.c.20.smt2 | 300.233s | 2668.0MiB| timeout | 0 | | | |2018-Mann_arbiter_data_integrity_n4q8w8d8b30.smt2 | 300.234s | 3018.0MiB| timeout | 0 | | | |brummayerbiere2_smulov4bw0768.smt2 | 300.235s | 2512.0MiB| timeout | 0 | | | |float_sin2.c.20.smt2 | 300.245s | 2526.0MiB| timeout | 0 | | | |brummayerbiere2_smulov2bw448.smt2 | 300.252s | 2677.0MiB| timeout | 0 | | | |mcm_169.smt2 | 300.258s | 2915.0MiB| timeout | 0 | | | |float_sin.c.25.smt2 | 300.261s | 3730.0MiB| timeout | 0 | | | |brummayerbiere3_maxxormaxorand256.smt2 | 300.264s | 6005.0MiB| timeout | 0 | | | |brummayerbiere2_umulov2bw0896.smt2 | 300.265s | 3158.0MiB| timeout | 0 | | | |float_gaussian.c.75.smt2 | 300.265s | 3439.0MiB| timeout | 0 | | | |float_sin2.c.25.smt2 | 300.274s | 3730.0MiB| timeout | 0 | | | |20210219-Sydr_symbolic_memory_nested_faad_predicate_1529.smt2 | 300.277s | 6466.0MiB| timeout | 0 | | | |float_sqrt.c.25.smt2 | 300.282s | 2682.0MiB| timeout | 0 | | | |brummayerbiere2_smulov3bw1024.smt2 | 300.286s | 4662.0MiB| timeout | 0 | | | |brummayerbiere2_smulov4bw0896.smt2 | 300.288s | 3221.0MiB| timeout | 0 | | | |brummayerbiere2_smulov4bw1024.smt2 | 300.319s | 4662.0MiB| timeout | 0 | | | |mcm_175.smt2 | 300.322s | 4271.0MiB| timeout | 0 | | | |mcm_174.smt2 | 300.358s | 4160.0MiB| timeout | 0 | | | |2019-Wolf-fmbench_2018E_picorv32-pcregs-unrolled-nomem.smt2 | 300.364s | 6952.0MiB| timeout | 0 | | | |brummayerbiere_countbits1024.smt2 | 300.386s | 7115.0MiB| timeout | 0 | | | |brummayerbiere2_umulov2bw1024.smt2 | 300.388s | 4665.0MiB| timeout | 0 | | | |2019-Wolf-fmbench_2019A_picorv32_mutBX_QF_BV_NONINCR.smt2 | 300.395s | 7841.0MiB| timeout | 0 | | | |mcm_176.smt2 | 300.396s | 5319.0MiB| timeout | 0 | | | |mcm_173.smt2 | 300.396s | 5099.0MiB| timeout | 0 | | | |mcm_172.smt2 | 300.415s | 4222.0MiB| timeout | 0 | | | |mcm_179.smt2 | 300.444s | 5780.0MiB| timeout | 0 | | | |mcm_181.smt2 | 300.468s | 7474.0MiB| timeout | 0 | | | |mcm_178.smt2 | 300.483s | 5771.0MiB| timeout | 0 | | | |mcm_180.smt2 | 300.497s | 5658.0MiB| timeout | 0 | | | |float_sin.c.75.smt2 | 300.563s | 8642.0MiB| timeout | 0 | | | |2019-Wolf-fmbench_2019A_picorv32_mutBY_QF_BV_NONINCR.smt2 | 300.593s | 6836.0MiB| timeout | 0 | | | |float_qurt.c.25.smt2 | 300.619s | 9090.0MiB| timeout | 0 | | | |float_sin2.c.75.smt2 | 300.628s | 8642.0MiB| timeout | 0 | | | |float_qurt.c.20.smt2 | 300.641s | 9076.0MiB| timeout | 0 | | | |2019-Wolf-fmbench_2019A_picorv32_mutCY_QF_BV_NONINCR.smt2 | 300.700s | 7314.0MiB| timeout | 0 | | | |mcm_183.smt2 | 300.748s | 10.015GiB| timeout | 0 | | | |mcm_182.smt2 | 300.832s | 10.239GiB| timeout | 0 | | | |float_sin.c.125.smt2 | 301.034s | 15.608GiB| timeout | 0 | | | |float_sin.c.175.smt2 | 301.108s | 17.61GiB| timeout | 0 | | | |float_sin2.c.125.smt2 | 301.235s | 15.608GiB| timeout | 0 | | | |float_sin2.c.175.smt2 | 301.332s | 17.554GiB| timeout | 0 | | |