# . * SAT 750 * UNSAT 501 * TIMEOUT 33 * UNKNOWN 0 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/QF_UFLRA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-QF_UFLRA.tar.zst-d
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 4a90d3105054796562079406e125b9480ac3472b
Z3 branch: master
Z3 options: "-T:20 model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_UFLRA.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.while_infinite_loop_3_true-unreach-call_false-termination.i.smt2 | 0.023s | 19.44MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--touchscreen--gunze.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.024s | 19.432MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.sum01_true-unreach-call_true-termination.i.smt2 | 0.025s | 20.368MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_26.smt2 | 0.025s | 20.364MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.1_3.c_false-unreach-call.i.smt2 | 0.026s | 20.512MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.pointer_extension2_false-unreach-call.i.smt2 | 0.028s | 20.144MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.kbfiltr_simpl2_false-unreach-call_true-termination.cil.c.smt2 | 0.029s | 20.876MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.m0_false-unreach-call_drivers-staging-comedi-drivers-ni_65xx-ko--107_1a--adbbc36-1.c.smt2 | 0.029s | 20.432MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.gcd_1_true-unreach-call.i.smt2 | 0.030s | 19.556MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_26.smt2 | 0.030s | 20.4MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--misc--mpu3050.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.031s | 19.628MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_9_true-unreach-call.c.smt2 | 0.033s | 20.892MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_10.smt2 | 0.033s | 20.772MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.integerpromotion_false-unreach-call.i.smt2 | 0.034s | 20.112MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_15.smt2 | 0.034s | 20.384MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_22.smt2 | 0.034s | 20.808MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_48.smt2 | 0.034s | 20.6MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.rule57_ebda_blast.c_false-unreach-call.i.smt2 | 0.035s | 20.404MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_25.smt2 | 0.036s | 20.556MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_41.smt2 | 0.036s | 21.076MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_10.smt2 | 0.037s | 20.844MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_28.smt2 | 0.037s | 21.18MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.string_true-unreach-call.i.smt2 | 0.038s | 20.14MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--joystick--stinger.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.038s | 19.64MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_27.smt2 | 0.038s | 20.392MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_24.smt2 | 0.038s | 20.412MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_11.smt2 | 0.038s | 20.528MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_46.smt2 | 0.038s | 20.684MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_14.smt2 | 0.039s | 21.048MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_18.smt2 | 0.039s | 20.592MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.count_up_down_true-unreach-call_true-termination.i.smt2 | 0.041s | 20.004MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_21.smt2 | 0.041s | 21.372MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_75.smt2 | 0.041s | 20.684MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.linear_sea.ch_true-unreach-call.i.smt2 | 0.042s | 20.64MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_12.smt2 | 0.043s | 21.04MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_10.smt2 | 0.043s | 20.336MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_63.smt2 | 0.043s | 21.04MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product28_false-unreach-call.cil.c.smt2 | 0.044s | 22.572MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_10.smt2 | 0.044s | 20.816MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_22.smt2 | 0.044s | 21.016MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_18.smt2 | 0.044s | 20.36MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_75.smt2 | 0.044s | 21.048MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--net--arcnet--rfc1201.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.045s | 19.448MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_23.smt2 | 0.046s | 21.316MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_26.smt2 | 0.046s | 21.52MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--touchscreen--touchit213.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.047s | 19.432MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_16.smt2 | 0.047s | 20.396MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_25.smt2 | 0.047s | 21.084MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_39.smt2 | 0.047s | 20.92MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_62.smt2 | 0.047s | 20.716MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_17.smt2 | 0.048s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_27.smt2 | 0.049s | 21.676MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_27.smt2 | 0.049s | 20.704MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_25.smt2 | 0.049s | 20.404MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_16.smt2 | 0.049s | 21.16MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_92.smt2 | 0.049s | 21.012MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_41.smt2 | 0.050s | 21.188MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_24.smt2 | 0.051s | 20.86MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_25.smt2 | 0.051s | 21.516MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_21.smt2 | 0.051s | 20.464MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_13.smt2 | 0.051s | 21.216MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_30.smt2 | 0.051s | 21.292MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.for_bounded_loop1_false-unreach-call_true-termination.i.smt2 | 0.052s | 20.432MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_5_true-unreach-call_false-termination.c.smt2 | 0.052s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_12.smt2 | 0.052s | 20.844MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_59.smt2 | 0.052s | 20.624MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_16.smt2 | 0.053s | 20.668MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_28.smt2 | 0.053s | 20.852MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_60.smt2 | 0.053s | 21.08MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--staging--iio--iio_dummy_evgen.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.054s | 19.82MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_23.smt2 | 0.054s | 20.444MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_29.smt2 | 0.054s | 21.008MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.list_search_false-unreach-call.i.smt2 | 0.055s | 20.776MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i.smt2 | 0.055s | 20.164MiB| sat | 0 | | | |non-incremental/QF_UFLRA/FFT/smtlib.620524.smt2 | 0.055s | 20.048MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.array_false-unreach-call.i.smt2 | 0.056s | 20.024MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.jain_7_true-unreach-call.i.smt2 | 0.056s | 20.104MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_17.smt2 | 0.056s | 21.336MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_68.smt2 | 0.056s | 21.276MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_7_true-unreach-call_false-termination.c.smt2 | 0.057s | 20.552MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_17.smt2 | 0.057s | 21.22MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_18.smt2 | 0.057s | 21.16MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_26.smt2 | 0.057s | 21.524MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_14.smt2 | 0.057s | 21.084MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_13.smt2 | 0.058s | 20.892MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_10.smt2 | 0.058s | 21.436MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_13.smt2 | 0.058s | 21.632MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_92.smt2 | 0.059s | 20.624MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.nec20_false-unreach-call.i.smt2 | 0.060s | 20.1MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--atm--adummy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.060s | 19.68MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.jain_2_true-unreach-call.i.smt2 | 0.060s | 20.156MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_27.smt2 | 0.060s | 21.892MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_21.smt2 | 0.060s | 20.42MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_19.smt2 | 0.060s | 21.78MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_10.smt2 | 0.060s | 21.76MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_25.smt2 | 0.060s | 20.98MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_00.smt2 | 0.060s | 21.224MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_82.smt2 | 0.060s | 20.576MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.pointer_extension3_false-unreach-call.i.smt2 | 0.061s | 20.112MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_21.smt2 | 0.061s | 20.592MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_24.smt2 | 0.061s | 20.58MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_22.smt2 | 0.061s | 20.836MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_21.smt2 | 0.061s | 21.264MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_85.smt2 | 0.061s | 20.704MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product24_false-unreach-call.cil.c.smt2 | 0.062s | 22.104MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_11.smt2 | 0.062s | 21.156MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_19.smt2 | 0.062s | 22.248MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_10.smt2 | 0.062s | 20.844MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_45.smt2 | 0.062s | 20.84MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_15.smt2 | 0.063s | 20.364MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_04.smt2 | 0.063s | 20.628MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_96.smt2 | 0.063s | 20.708MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_06.smt2 | 0.063s | 20.728MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_61.smt2 | 0.063s | 20.612MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_18.smt2 | 0.064s | 21.528MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_25.smt2 | 0.064s | 21.392MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_20.smt2 | 0.064s | 20.884MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_13.smt2 | 0.064s | 20.84MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_18.smt2 | 0.064s | 20.66MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_44.smt2 | 0.064s | 20.788MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_66.smt2 | 0.064s | 20.876MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_12.smt2 | 0.065s | 21.84MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_16.smt2 | 0.065s | 21.06MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_16.smt2 | 0.065s | 20.36MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_77.smt2 | 0.065s | 20.944MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_97.smt2 | 0.065s | 20.86MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_64.smt2 | 0.065s | 20.868MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_20.smt2 | 0.065s | 20.844MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.terminator_02_false-unreach-call_true-termination.i.smt2 | 0.066s | 20.376MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_13.smt2 | 0.066s | 21.764MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_25.smt2 | 0.066s | 20.816MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_18.smt2 | 0.066s | 20.936MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_24.smt2 | 0.067s | 20.924MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_11.smt2 | 0.067s | 20.908MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_14.smt2 | 0.067s | 20.376MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_49.smt2 | 0.067s | 20.852MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_95.smt2 | 0.067s | 20.776MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_63.smt2 | 0.067s | 21.08MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/FFT/smtlib.624898.smt2 | 0.067s | 19.892MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--misc--ab8500-ponkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.068s | 19.632MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.s3_srvr_10_false-unreach-call.cil.c.smt2 | 0.068s | 20.744MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_10.smt2 | 0.068s | 20.356MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_16.smt2 | 0.068s | 20.848MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_14.smt2 | 0.068s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_28.smt2 | 0.068s | 20.616MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/FFT/smtlib.626179.smt2 | 0.068s | 19.816MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.implicitfloatconversion_false-unreach-call.i.smt2 | 0.069s | 20.036MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.modulus_true-unreach-call.i.smt2 | 0.069s | 20.212MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_16.smt2 | 0.069s | 21.1MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_23.smt2 | 0.069s | 21.7MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_18.smt2 | 0.069s | 20.988MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_27.smt2 | 0.069s | 20.396MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_54.smt2 | 0.069s | 20.832MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_90.smt2 | 0.069s | 21.244MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_09.smt2 | 0.069s | 20.688MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_25.smt2 | 0.069s | 20.632MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_54.smt2 | 0.069s | 20.74MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_14.smt2 | 0.069s | 20.636MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--i2c--algos--i2c-algo-pca.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.070s | 19.604MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_15.smt2 | 0.070s | 20.68MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_12.smt2 | 0.070s | 20.492MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_23.smt2 | 0.070s | 20.352MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_22.smt2 | 0.070s | 20.372MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_05.smt2 | 0.070s | 20.552MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_21.smt2 | 0.070s | 21.116MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_99.smt2 | 0.070s | 20.652MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_13.smt2 | 0.071s | 20.644MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_13.smt2 | 0.071s | 20.828MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_29.smt2 | 0.071s | 20.432MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_08.smt2 | 0.071s | 20.644MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_18.smt2 | 0.071s | 21.256MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_26.smt2 | 0.071s | 21.372MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_27.smt2 | 0.072s | 20.796MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_23.smt2 | 0.072s | 20.896MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_12.smt2 | 0.072s | 20.504MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_25.smt2 | 0.072s | 20.96MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_11.smt2 | 0.072s | 21.228MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_25.smt2 | 0.072s | 20.388MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_94.smt2 | 0.072s | 21.36MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_05.smt2 | 0.072s | 21.128MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_10.smt2 | 0.073s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_26.smt2 | 0.073s | 20.336MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_17.smt2 | 0.073s | 20.62MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_12_true-unreach-call_false-termination.c.smt2 | 0.074s | 21.076MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_21.smt2 | 0.074s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_11.smt2 | 0.074s | 21.772MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_29.smt2 | 0.074s | 20.368MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_14.smt2 | 0.074s | 21.316MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_03.smt2 | 0.074s | 20.764MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_58.smt2 | 0.074s | 21.116MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_00.smt2 | 0.074s | 20.776MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.pointer_extension_true-unreach-call.i.smt2 | 0.075s | 20.112MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--mfd--tps6105x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.075s | 21.168MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_28.smt2 | 0.075s | 20.504MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_78.smt2 | 0.075s | 20.968MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_23.smt2 | 0.075s | 21.4MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_23.smt2 | 0.075s | 20.88MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.linear_search_false-unreach-call.i.smt2 | 0.076s | 20.632MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.rule60_list2.c_false-unreach-call_1.i.smt2 | 0.076s | 20.46MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_17.smt2 | 0.076s | 21.192MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_28.smt2 | 0.076s | 21.304MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_65.smt2 | 0.076s | 21.152MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_66.smt2 | 0.076s | 21.052MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_31.smt2 | 0.076s | 21.132MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_83.smt2 | 0.076s | 20.628MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_42.smt2 | 0.076s | 21.032MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_15.smt2 | 0.076s | 20.804MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.trex02_false-unreach-call_true-termination.i.smt2 | 0.077s | 19.972MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_14.smt2 | 0.077s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_24.smt2 | 0.077s | 20.46MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_18.smt2 | 0.077s | 22.04MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_20.smt2 | 0.077s | 20.856MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_65.smt2 | 0.077s | 20.864MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_39.smt2 | 0.077s | 20.54MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_20.smt2 | 0.077s | 20.912MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_17.smt2 | 0.078s | 21.424MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_20.smt2 | 0.078s | 21.82MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_95.smt2 | 0.078s | 21.136MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_19.smt2 | 0.078s | 21.412MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_14.smt2 | 0.078s | 21.288MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_73.smt2 | 0.078s | 21.448MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product32_false-unreach-call.cil.c.smt2 | 0.079s | 22.788MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_25.smt2 | 0.079s | 21.24MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_43.smt2 | 0.079s | 20.828MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_71.smt2 | 0.079s | 20.676MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_09.smt2 | 0.079s | 21.136MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_22.smt2 | 0.079s | 20.88MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_11.smt2 | 0.079s | 20.696MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_15.smt2 | 0.079s | 20.636MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_16.smt2 | 0.079s | 21.108MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_95.smt2 | 0.079s | 20.588MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_91.smt2 | 0.079s | 21.236MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_45.smt2 | 0.079s | 20.852MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_27.smt2 | 0.079s | 20.624MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_26.smt2 | 0.080s | 20.86MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_17.smt2 | 0.080s | 22.076MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_11.smt2 | 0.080s | 20.756MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_16.smt2 | 0.080s | 21.604MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_18.smt2 | 0.080s | 20.556MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_00.smt2 | 0.080s | 20.652MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_82.smt2 | 0.080s | 20.992MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_73.smt2 | 0.080s | 21.168MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_81.smt2 | 0.080s | 20.54MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_94.smt2 | 0.080s | 20.832MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_26.smt2 | 0.080s | 21.092MiB| sat | 0 | | | |non-incremental/QF_UFLRA/FFT/smtlib.624914.smt2 | 0.080s | 20.112MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_14_false-unreach-call.c.smt2 | 0.081s | 20.684MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_19.smt2 | 0.081s | 21.08MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_24.smt2 | 0.081s | 20.736MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_22.smt2 | 0.081s | 21.68MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_18.smt2 | 0.081s | 20.62MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_20.smt2 | 0.081s | 20.624MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_19.smt2 | 0.081s | 20.532MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_68.smt2 | 0.081s | 20.908MiB| sat | 0 | | | |non-incremental/QF_UFLRA/FFT/smtlib.624916.smt2 | 0.081s | 20.112MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_27.smt2 | 0.082s | 20.408MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_10.smt2 | 0.082s | 21.336MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_26.smt2 | 0.082s | 20.748MiB| sat | 0 | | | |non-incremental/QF_UFLRA/FFT/smtlib.626159.smt2 | 0.082s | 20.096MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--power--test_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.083s | 20.84MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.trex01_false-unreach-call_true-termination.i.smt2 | 0.083s | 20.184MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_11.smt2 | 0.083s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_86.smt2 | 0.083s | 20.768MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_59.smt2 | 0.083s | 20.892MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_38.smt2 | 0.083s | 20.548MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_80.smt2 | 0.083s | 20.656MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.while_infinite_loop_4_false-unreach-call_true-termination.i.smt2 | 0.084s | 20.164MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.callfpointer.c_false-unreach-call.i.smt2 | 0.084s | 20.016MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_6_true-unreach-call_false-termination.c.smt2 | 0.084s | 20.712MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.floppy_simpl4_false-unreach-call_true-termination.cil.c.smt2 | 0.084s | 21.232MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_23.smt2 | 0.084s | 21.636MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_28.smt2 | 0.084s | 20.9MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_10.smt2 | 0.084s | 20.876MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_25.smt2 | 0.084s | 20.92MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_84.smt2 | 0.084s | 21.168MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_75.smt2 | 0.084s | 20.776MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_03.smt2 | 0.084s | 20.992MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_65.smt2 | 0.084s | 20.712MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_39.smt2 | 0.084s | 20.624MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_52.smt2 | 0.084s | 21.136MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_84.smt2 | 0.084s | 20.556MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_51.smt2 | 0.084s | 20.84MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.s3_srvr_14_false-unreach-call.cil.c.smt2 | 0.085s | 22.836MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--touchscreen--tsc40.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.085s | 20.068MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_20.smt2 | 0.085s | 20.36MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_25.smt2 | 0.085s | 20.392MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_15.smt2 | 0.085s | 20.436MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_21.smt2 | 0.085s | 20.848MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_25.smt2 | 0.085s | 21.812MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_05.smt2 | 0.085s | 21.344MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_66.smt2 | 0.085s | 20.848MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_34.smt2 | 0.085s | 20.744MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_78.smt2 | 0.085s | 20.584MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_50.smt2 | 0.085s | 20.888MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/FFT/smtlib.627677.smt2 | 0.085s | 19.864MiB| sat | 0 | | | |non-incremental/QF_UFLRA/FFT/smtlib.623586.smt2 | 0.085s | 20.784MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.array_true-unreach-call.i.smt2 | 0.086s | 20.128MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.floppy_simpl3_false-unreach-call_true-termination.cil.c.smt2 | 0.086s | 20.892MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_23.smt2 | 0.086s | 21.204MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_74.smt2 | 0.086s | 20.712MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_55.smt2 | 0.086s | 20.956MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_33.smt2 | 0.086s | 20.628MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-alauda.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.087s | 21.808MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_22.smt2 | 0.087s | 20.368MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_28.smt2 | 0.087s | 21.404MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_34.smt2 | 0.087s | 20.624MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_95.smt2 | 0.087s | 20.912MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_70.smt2 | 0.087s | 21.3MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_68.smt2 | 0.087s | 20.592MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product29_false-unreach-call.cil.c.smt2 | 0.088s | 22.772MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_13.smt2 | 0.088s | 20.784MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_15.smt2 | 0.088s | 20.352MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_16.smt2 | 0.088s | 20.94MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_37.smt2 | 0.088s | 21.236MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_21.smt2 | 0.088s | 20.668MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_44.smt2 | 0.088s | 20.704MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_20.smt2 | 0.089s | 21.816MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_26.smt2 | 0.089s | 20.288MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_15.smt2 | 0.089s | 20.764MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_29.smt2 | 0.089s | 20.996MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_28.smt2 | 0.089s | 20.388MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_71.smt2 | 0.089s | 20.976MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_86.smt2 | 0.089s | 20.876MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_01.smt2 | 0.089s | 21.372MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_40.smt2 | 0.089s | 21.008MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_90.smt2 | 0.089s | 20.632MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_32.smt2 | 0.089s | 20.848MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_26.smt2 | 0.089s | 20.668MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.m0_false-unreach-call_drivers-staging-comedi-drivers-ni_660x-ko--107_1a--adbbc36-1.c.smt2 | 0.090s | 20.36MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_28.smt2 | 0.090s | 20.364MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_26.smt2 | 0.090s | 20.824MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_21.smt2 | 0.090s | 20.88MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_04.smt2 | 0.090s | 20.856MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_84.smt2 | 0.090s | 20.796MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_93.smt2 | 0.090s | 21.216MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_35.smt2 | 0.090s | 21.208MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_87.smt2 | 0.090s | 20.616MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_99.smt2 | 0.090s | 21.132MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.recursive_list.c_false-unreach-call.i.smt2 | 0.091s | 20.636MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_12.smt2 | 0.091s | 21.536MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_27.smt2 | 0.091s | 21.136MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_10.smt2 | 0.091s | 20.396MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_24.smt2 | 0.091s | 21.268MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_02.smt2 | 0.091s | 20.888MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_01.smt2 | 0.091s | 20.868MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_19.smt2 | 0.091s | 20.74MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_24.smt2 | 0.091s | 21.136MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_52.smt2 | 0.091s | 20.988MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_72.smt2 | 0.091s | 20.716MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_40.smt2 | 0.091s | 21.26MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_48.smt2 | 0.091s | 20.552MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_29.smt2 | 0.092s | 20.764MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_10.smt2 | 0.092s | 20.428MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_14.smt2 | 0.092s | 20.42MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_22.smt2 | 0.092s | 21.236MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_19.smt2 | 0.092s | 20.36MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_29.smt2 | 0.092s | 20.384MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_27.smt2 | 0.092s | 20.82MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_11.smt2 | 0.092s | 20.52MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_76.smt2 | 0.092s | 20.696MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_20.smt2 | 0.092s | 20.62MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_50.smt2 | 0.092s | 20.624MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_13.smt2 | 0.092s | 21.364MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_82.smt2 | 0.092s | 21.28MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.m0_false-unreach-call_drivers-staging-comedi-drivers-ni_670x-ko--107_1a--adbbc36-1.c.smt2 | 0.093s | 20.432MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_29.smt2 | 0.093s | 21.268MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_20.smt2 | 0.093s | 21.144MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_29.smt2 | 0.093s | 21.292MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_14.smt2 | 0.093s | 20.832MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_21.smt2 | 0.093s | 21.148MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_43.smt2 | 0.093s | 21.156MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_02.smt2 | 0.093s | 21.112MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_12.smt2 | 0.094s | 20.728MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_26.smt2 | 0.094s | 21.364MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_23.smt2 | 0.094s | 21.696MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_19.smt2 | 0.094s | 20.372MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_28.smt2 | 0.094s | 21.364MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_29.smt2 | 0.094s | 21.596MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_13.smt2 | 0.094s | 20.904MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_22.smt2 | 0.094s | 20.48MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_13.smt2 | 0.094s | 20.512MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_10.smt2 | 0.094s | 21.652MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_13.smt2 | 0.094s | 21.384MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_17.smt2 | 0.094s | 20.636MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_26.smt2 | 0.094s | 21.74MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_24.smt2 | 0.094s | 20.572MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_45.smt2 | 0.094s | 20.648MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.gcd_4_true-unreach-call.i.smt2 | 0.095s | 19.636MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.fo_test.c_false-unreach-call.i.smt2 | 0.095s | 20.32MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_13.smt2 | 0.095s | 20.848MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_24.smt2 | 0.095s | 21.136MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_15.smt2 | 0.095s | 20.752MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_16.smt2 | 0.095s | 20.876MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_24.smt2 | 0.095s | 21.14MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_26.smt2 | 0.095s | 20.892MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_36.smt2 | 0.095s | 20.752MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_61.smt2 | 0.095s | 21.176MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_76.smt2 | 0.095s | 20.644MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_60.smt2 | 0.095s | 21.252MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_07.smt2 | 0.095s | 21.096MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.sum01_bug02_false-unreach-call_true-termination.i.smt2 | 0.096s | 20.404MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_25.smt2 | 0.096s | 20.852MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_12.smt2 | 0.096s | 21.612MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_29.smt2 | 0.096s | 20.46MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_62.smt2 | 0.096s | 21.328MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_27.smt2 | 0.096s | 21.108MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_80.smt2 | 0.096s | 20.684MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_51.smt2 | 0.096s | 21.1MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_90.smt2 | 0.096s | 21.364MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_69.smt2 | 0.096s | 21.1MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_97.smt2 | 0.096s | 20.936MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_30.smt2 | 0.096s | 21.112MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_28.smt2 | 0.096s | 21.048MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product17_false-unreach-call.cil.c.smt2 | 0.097s | 22.412MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--rtc--rtc-ds1390.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.097s | 19.548MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--touchscreen--dynapro.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.097s | 19.828MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_19.smt2 | 0.097s | 21.392MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_20.smt2 | 0.097s | 20.248MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_85.smt2 | 0.097s | 20.624MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_99.smt2 | 0.097s | 20.596MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_97.smt2 | 0.097s | 21.152MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_47.smt2 | 0.097s | 20.752MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_56.smt2 | 0.097s | 20.76MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_55.smt2 | 0.097s | 20.676MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_59.smt2 | 0.097s | 21.144MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_37.smt2 | 0.097s | 20.604MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_67.smt2 | 0.097s | 20.708MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product34_false-unreach-call.cil.c.smt2 | 0.098s | 22.932MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_17.smt2 | 0.098s | 21.156MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_19.smt2 | 0.098s | 20.616MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_20.smt2 | 0.098s | 21.084MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_17.smt2 | 0.098s | 20.996MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_12.smt2 | 0.098s | 20.564MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_26.smt2 | 0.098s | 21.16MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_15.smt2 | 0.098s | 21.572MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_15.smt2 | 0.098s | 21.172MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_24.smt2 | 0.098s | 20.62MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_70.smt2 | 0.098s | 20.684MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_04.smt2 | 0.098s | 21.364MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_47.smt2 | 0.098s | 21.14MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_91.smt2 | 0.098s | 20.656MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_12.smt2 | 0.099s | 21.084MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_24.smt2 | 0.099s | 20.964MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_85.smt2 | 0.099s | 21.136MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_94.smt2 | 0.099s | 21.136MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_80.smt2 | 0.099s | 21.272MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_80.smt2 | 0.099s | 21.412MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_86.smt2 | 0.099s | 21.612MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_61.smt2 | 0.099s | 20.872MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.parity_true-unreach-call.i.smt2 | 0.100s | 20.196MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product13_false-unreach-call.cil.c.smt2 | 0.100s | 21.936MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_28.smt2 | 0.100s | 20.36MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_23.smt2 | 0.100s | 21.156MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_24.smt2 | 0.100s | 20.42MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_29.smt2 | 0.100s | 21.116MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_35.smt2 | 0.100s | 20.848MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_03.smt2 | 0.100s | 20.624MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_47.smt2 | 0.100s | 21.356MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_54.smt2 | 0.100s | 21.408MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_12.smt2 | 0.100s | 20.98MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_30.smt2 | 0.100s | 21.184MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_22.smt2 | 0.100s | 20.704MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_41.smt2 | 0.100s | 21.256MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_70.smt2 | 0.100s | 21.36MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_09.smt2 | 0.100s | 21.396MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_13.smt2 | 0.101s | 21.788MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_11.smt2 | 0.101s | 20.712MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_22.smt2 | 0.101s | 20.88MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_27.smt2 | 0.101s | 20.94MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_25.smt2 | 0.101s | 20.792MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_25.smt2 | 0.101s | 21.728MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_27.smt2 | 0.101s | 20.864MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_24.smt2 | 0.101s | 21.164MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_89.smt2 | 0.101s | 21.256MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_52.smt2 | 0.101s | 20.736MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_33.smt2 | 0.101s | 21.028MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_10.smt2 | 0.101s | 20.78MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_87.smt2 | 0.101s | 21.168MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_60.smt2 | 0.101s | 21.112MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_30.smt2 | 0.101s | 20.836MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_10.smt2 | 0.101s | 21.044MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_09.smt2 | 0.101s | 21.104MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_07.smt2 | 0.101s | 20.62MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_05.smt2 | 0.101s | 21.144MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_12.smt2 | 0.101s | 20.716MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_17.smt2 | 0.102s | 20.372MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_27.smt2 | 0.102s | 21.4MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_20.smt2 | 0.102s | 20.276MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_13.smt2 | 0.102s | 21.86MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_20.smt2 | 0.102s | 21.848MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_13.smt2 | 0.102s | 20.696MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_25.smt2 | 0.102s | 21.076MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_57.smt2 | 0.102s | 20.656MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_88.smt2 | 0.102s | 20.78MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_01.smt2 | 0.102s | 20.972MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_07.smt2 | 0.102s | 21.152MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_12.smt2 | 0.102s | 20.648MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_02.smt2 | 0.102s | 20.712MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_49.smt2 | 0.102s | 20.648MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_72.smt2 | 0.102s | 20.7MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_87.smt2 | 0.102s | 20.968MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_14.smt2 | 0.102s | 20.84MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_16.smt2 | 0.103s | 21.328MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_19.smt2 | 0.103s | 21.16MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_20.smt2 | 0.103s | 20.62MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_16.smt2 | 0.103s | 20.856MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_26.smt2 | 0.103s | 20.9MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_93.smt2 | 0.103s | 20.656MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_76.smt2 | 0.103s | 21.032MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_53.smt2 | 0.103s | 20.78MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_40.smt2 | 0.103s | 20.656MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_96.smt2 | 0.103s | 20.8MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_90.smt2 | 0.103s | 20.924MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_89.smt2 | 0.103s | 21.172MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_58.smt2 | 0.103s | 20.64MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_11.smt2 | 0.103s | 20.692MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_70.smt2 | 0.103s | 21.192MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_82.smt2 | 0.103s | 21.192MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_79.smt2 | 0.103s | 20.596MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_29.smt2 | 0.104s | 20.704MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_21.smt2 | 0.104s | 20.82MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_19.smt2 | 0.104s | 21.996MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_15.smt2 | 0.104s | 21.568MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_16.smt2 | 0.104s | 21.36MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_06.smt2 | 0.104s | 21.156MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_63.smt2 | 0.104s | 20.768MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_89.smt2 | 0.104s | 20.988MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_08.smt2 | 0.104s | 21.392MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_34.smt2 | 0.104s | 20.848MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_17.smt2 | 0.104s | 20.936MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_15_true-unreach-call_false-termination.c.smt2 | 0.105s | 21.4MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product30_false-unreach-call.cil.c.smt2 | 0.105s | 22.388MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_10.smt2 | 0.105s | 21.608MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_22.smt2 | 0.105s | 21.196MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_12.smt2 | 0.105s | 20.388MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_22.smt2 | 0.105s | 21.448MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_14.smt2 | 0.105s | 21.384MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_24.smt2 | 0.105s | 21.192MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_11.smt2 | 0.105s | 20.848MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_64.smt2 | 0.105s | 21.02MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_50.smt2 | 0.105s | 21.256MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_35.smt2 | 0.105s | 21.592MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_01.smt2 | 0.105s | 20.716MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_21.smt2 | 0.105s | 20.64MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_66.smt2 | 0.105s | 21.228MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_75.smt2 | 0.105s | 20.852MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_36.smt2 | 0.105s | 20.616MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/FFT/smtlib.626139.smt2 | 0.105s | 19.916MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.jain_4_true-unreach-call.i.smt2 | 0.106s | 20.252MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_15_false-unreach-call.c.smt2 | 0.106s | 20.876MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.alt_test.c_false-unreach-call.i.smt2 | 0.106s | 20.208MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_14.smt2 | 0.106s | 21.472MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_17.smt2 | 0.106s | 20.724MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_27.smt2 | 0.106s | 20.36MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_11.smt2 | 0.106s | 21.648MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_22.smt2 | 0.106s | 21.7MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_29.smt2 | 0.106s | 20.652MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_88.smt2 | 0.106s | 21.232MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_45.smt2 | 0.106s | 21.092MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_56.smt2 | 0.106s | 21.168MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_71.smt2 | 0.106s | 21.3MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_13.smt2 | 0.106s | 20.624MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_77.smt2 | 0.106s | 20.628MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_54.smt2 | 0.106s | 21.088MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_32.smt2 | 0.106s | 20.6MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/FFT/smtlib.624882.smt2 | 0.106s | 20.116MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--misc--pcap_keys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.107s | 19.824MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.mutex_lock_struct.c_false-unreach-call.i.smt2 | 0.107s | 20.18MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_11_true-unreach-call_false-termination.c.smt2 | 0.107s | 20.864MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_14.smt2 | 0.107s | 21.132MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_10.smt2 | 0.107s | 21.44MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_22.smt2 | 0.107s | 21.452MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_15.smt2 | 0.107s | 20.88MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_19.smt2 | 0.107s | 21.28MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_20.smt2 | 0.107s | 21.076MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_22.smt2 | 0.107s | 21.62MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_24.smt2 | 0.107s | 21.9MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_28.smt2 | 0.107s | 21.54MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_65.smt2 | 0.107s | 21.228MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_69.smt2 | 0.107s | 21.064MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_13.smt2 | 0.107s | 21.14MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_37.smt2 | 0.107s | 20.972MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_83.smt2 | 0.107s | 21.4MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_40.smt2 | 0.107s | 20.62MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product25_false-unreach-call.cil.c.smt2 | 0.108s | 22.46MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.gcd_2_true-unreach-call.i.smt2 | 0.108s | 19.852MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c.smt2 | 0.108s | 20.248MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_04.smt2 | 0.108s | 21.296MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_63.smt2 | 0.108s | 21.112MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_53.smt2 | 0.108s | 20.712MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_91.smt2 | 0.108s | 21.092MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_52.smt2 | 0.108s | 20.652MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product35_false-unreach-call.cil.c.smt2 | 0.109s | 22.804MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.terminator_03_false-unreach-call_true-termination.i.smt2 | 0.109s | 20.112MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_29.smt2 | 0.109s | 21.372MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_15.smt2 | 0.109s | 21.72MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_25.smt2 | 0.109s | 21.288MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_28.smt2 | 0.109s | 20.628MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_78.smt2 | 0.109s | 20.896MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_46.smt2 | 0.109s | 21.348MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_02.smt2 | 0.109s | 20.724MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_07.smt2 | 0.109s | 21.108MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_62.smt2 | 0.109s | 20.86MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_81.smt2 | 0.109s | 21.252MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_01.smt2 | 0.109s | 21.276MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_43.smt2 | 0.109s | 20.656MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_49.smt2 | 0.109s | 21.088MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_94.smt2 | 0.109s | 20.98MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_8_true-unreach-call_false-termination.c.smt2 | 0.110s | 20.664MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.pointer_extension_false-unreach-call.i.smt2 | 0.110s | 20.112MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.trex01_true-unreach-call.i.smt2 | 0.110s | 20.328MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_20.smt2 | 0.110s | 21.364MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_19.smt2 | 0.110s | 22.1MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_24.smt2 | 0.110s | 21.288MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_22.smt2 | 0.110s | 20.9MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_23.smt2 | 0.110s | 20.916MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_21.smt2 | 0.110s | 21.284MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_17.smt2 | 0.110s | 21.24MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_47.smt2 | 0.110s | 20.908MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_11.smt2 | 0.110s | 21.264MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_19.smt2 | 0.110s | 20.708MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.kbfiltr_false-unreach-call.i.cil.c.smt2 | 0.111s | 21.752MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--spi--spi-tle62x0.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.111s | 22.448MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_15.smt2 | 0.111s | 21.152MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_10.smt2 | 0.111s | 21.304MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_29.smt2 | 0.111s | 20.824MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_24.smt2 | 0.111s | 20.872MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_11.smt2 | 0.111s | 20.808MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_02.smt2 | 0.111s | 21.284MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_79.smt2 | 0.111s | 20.9MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_78.smt2 | 0.111s | 21.088MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_41.smt2 | 0.111s | 21.116MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_10.smt2 | 0.111s | 21.264MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_09.smt2 | 0.111s | 20.688MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_07.smt2 | 0.111s | 20.952MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_91.smt2 | 0.111s | 21.176MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_11.smt2 | 0.112s | 21.004MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_12.smt2 | 0.112s | 22.016MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_15.smt2 | 0.112s | 21.708MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_15.smt2 | 0.112s | 20.896MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_00.smt2 | 0.112s | 21.504MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_21.smt2 | 0.112s | 21.244MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_15.smt2 | 0.112s | 21.276MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_91.smt2 | 0.112s | 20.86MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_67.smt2 | 0.112s | 21.188MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_44.smt2 | 0.112s | 21.116MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_69.smt2 | 0.112s | 20.62MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.nec11_false-unreach-call.i.smt2 | 0.113s | 20.176MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_16.smt2 | 0.113s | 21.68MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_21.smt2 | 0.113s | 20.9MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_19.smt2 | 0.113s | 21.38MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_24.smt2 | 0.113s | 21.724MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_50.smt2 | 0.113s | 21.276MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_73.smt2 | 0.113s | 20.856MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_38.smt2 | 0.113s | 21.28MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--touchscreen--inexio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.114s | 19.472MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_16.smt2 | 0.114s | 21.056MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_12.smt2 | 0.114s | 21.728MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_15.smt2 | 0.114s | 21.4MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_10.smt2 | 0.114s | 21.632MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_28.smt2 | 0.114s | 21.776MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_18.smt2 | 0.114s | 21.38MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_24.smt2 | 0.114s | 21.052MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_80.smt2 | 0.114s | 20.88MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_56.smt2 | 0.114s | 20.728MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_17.smt2 | 0.114s | 21.232MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_11.smt2 | 0.114s | 21.136MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_84.smt2 | 0.114s | 21.164MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_23.smt2 | 0.115s | 20.844MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_19.smt2 | 0.115s | 21.072MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_51.smt2 | 0.115s | 20.66MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_77.smt2 | 0.115s | 21.328MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_73.smt2 | 0.115s | 20.84MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_33.smt2 | 0.115s | 21.128MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_64.smt2 | 0.115s | 21.224MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_69.smt2 | 0.115s | 21.264MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_49.smt2 | 0.115s | 21.076MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_13.smt2 | 0.115s | 21.396MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.trex03_true-unreach-call.i.smt2 | 0.116s | 20.384MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--net--arcnet--rfc1051.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.116s | 19.612MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_23.smt2 | 0.116s | 20.844MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_26.smt2 | 0.116s | 21.148MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_29.smt2 | 0.116s | 21.132MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_32.smt2 | 0.116s | 20.652MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_34.smt2 | 0.116s | 21.324MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_62.smt2 | 0.116s | 21.056MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_51.smt2 | 0.116s | 20.836MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_55.smt2 | 0.116s | 20.668MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_22.smt2 | 0.117s | 21.056MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_18.smt2 | 0.117s | 20.708MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_16.smt2 | 0.117s | 21.284MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_53.smt2 | 0.117s | 21.228MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_95.smt2 | 0.117s | 21.268MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_08.smt2 | 0.117s | 21.084MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_30.smt2 | 0.117s | 20.588MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_99.smt2 | 0.117s | 21.144MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_62.smt2 | 0.117s | 21.092MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_67.smt2 | 0.117s | 20.596MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_23.smt2 | 0.117s | 20.816MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_18.smt2 | 0.118s | 20.452MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_29.smt2 | 0.118s | 21.972MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_55.smt2 | 0.118s | 21.136MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_20.smt2 | 0.118s | 21.184MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_25.smt2 | 0.118s | 21.312MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_44.smt2 | 0.118s | 21.176MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_26.smt2 | 0.119s | 20.88MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_13.smt2 | 0.119s | 21.316MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_16.smt2 | 0.119s | 20.36MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_17.smt2 | 0.119s | 20.448MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_92.smt2 | 0.119s | 21.144MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_87.smt2 | 0.119s | 20.624MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_43.smt2 | 0.119s | 21.276MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_60.smt2 | 0.119s | 20.636MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_66.smt2 | 0.119s | 21.04MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_03.smt2 | 0.119s | 21.216MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_65.smt2 | 0.119s | 20.98MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_28.smt2 | 0.119s | 21.104MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_10.smt2 | 0.119s | 21.276MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_88.smt2 | 0.119s | 20.916MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_84.smt2 | 0.119s | 21.008MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_20.smt2 | 0.120s | 21.28MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_11.smt2 | 0.120s | 21.736MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_21.smt2 | 0.120s | 22.22MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_93.smt2 | 0.120s | 21.352MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_79.smt2 | 0.120s | 21.312MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_15.smt2 | 0.120s | 21.308MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_33.smt2 | 0.120s | 20.528MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_52.smt2 | 0.120s | 21.204MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_96.smt2 | 0.120s | 21.16MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_77.smt2 | 0.121s | 20.88MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_81.smt2 | 0.121s | 20.672MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_45.smt2 | 0.121s | 21.072MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_39.smt2 | 0.121s | 21.396MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_93.smt2 | 0.121s | 21.288MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_72.smt2 | 0.121s | 21.148MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_98.smt2 | 0.121s | 21.028MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_32.smt2 | 0.121s | 21.284MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_36.smt2 | 0.121s | 20.892MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.terminator_01_false-unreach-call_false-termination.i.smt2 | 0.122s | 20.048MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_23.smt2 | 0.122s | 20.88MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_28.smt2 | 0.122s | 21.292MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_16.smt2 | 0.122s | 20.74MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_18.smt2 | 0.122s | 22.068MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_19.smt2 | 0.122s | 20.956MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_12.smt2 | 0.122s | 21.512MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_27.smt2 | 0.122s | 21.404MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_06.smt2 | 0.122s | 20.62MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_08.smt2 | 0.122s | 21.188MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_68.smt2 | 0.122s | 21.22MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-jumpshot.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.123s | 21.892MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_17.smt2 | 0.123s | 21.84MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_22.smt2 | 0.123s | 21.56MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_28.smt2 | 0.123s | 20.876MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_19.smt2 | 0.123s | 22.064MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_38.smt2 | 0.123s | 20.9MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_79.smt2 | 0.123s | 21.384MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_76.smt2 | 0.123s | 21.384MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_27.smt2 | 0.123s | 20.808MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_88.smt2 | 0.123s | 20.872MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_00.smt2 | 0.123s | 21.096MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_25.smt2 | 0.123s | 21.16MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_41.smt2 | 0.123s | 20.96MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_28.smt2 | 0.124s | 21.76MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_18.smt2 | 0.124s | 21.32MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_15.smt2 | 0.124s | 21.944MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_22.smt2 | 0.124s | 20.44MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product33_false-unreach-call.cil.c.smt2 | 0.125s | 22.66MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--touchscreen--hampshire.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.125s | 19.82MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--touchscreen--touchwin.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.125s | 19.48MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--touchscreen--touchright.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.125s | 19.636MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_14.smt2 | 0.125s | 20.9MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_22.smt2 | 0.125s | 21.792MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_31.smt2 | 0.125s | 20.608MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_32.smt2 | 0.125s | 21.12MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_18.smt2 | 0.125s | 20.86MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_74.smt2 | 0.125s | 21.14MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_17.smt2 | 0.125s | 21.32MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.sum01_false-unreach-call_true-termination.i.smt2 | 0.126s | 20.084MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.jain_6_true-unreach-call.i.smt2 | 0.126s | 20.172MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.count_up_down_false-unreach-call_true-termination.i.smt2 | 0.126s | 20.32MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_14.smt2 | 0.126s | 21.516MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_29.smt2 | 0.126s | 21.712MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_15.smt2 | 0.126s | 21.184MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_25.smt2 | 0.126s | 21.828MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_19.smt2 | 0.126s | 20.936MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_28.smt2 | 0.126s | 21.152MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_98.smt2 | 0.126s | 20.928MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.verisec_NetBSD-libc__loop_false-unreach-call.i.smt2 | 0.127s | 20.648MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--touchscreen--mtouch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.127s | 19.856MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_26.smt2 | 0.127s | 21.836MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_40.smt2 | 0.127s | 21.024MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_34.smt2 | 0.127s | 21.448MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_36.smt2 | 0.127s | 21.084MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_42.smt2 | 0.127s | 20.684MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_59.smt2 | 0.127s | 21.74MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_17.smt2 | 0.127s | 20.692MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.m0_true-unreach-call_drivers-staging-comedi-drivers-ni_pcidio-ko--107_1a--adbbc36.c.smt2 | 0.128s | 20.128MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_17.smt2 | 0.128s | 20.784MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_15.smt2 | 0.128s | 20.372MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_29.smt2 | 0.128s | 21.668MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0450_10_18.smt2 | 0.128s | 21.412MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_16.smt2 | 0.128s | 21.648MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_20.smt2 | 0.128s | 21.16MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_72.smt2 | 0.128s | 21.332MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_53.smt2 | 0.128s | 21.356MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_23.smt2 | 0.128s | 20.708MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product23_false-unreach-call.cil.c.smt2 | 0.129s | 22.44MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_22.smt2 | 0.129s | 22.2MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_10.smt2 | 0.129s | 20.948MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.m0_false-unreach-call_drivers-staging-comedi-drivers-ni_pcidio-ko--107_1a--adbbc36-1.c.smt2 | 0.130s | 20.628MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.m0_false-unreach-call_drivers-staging-comedi-drivers-ni_6527-ko--107_1a--adbbc36-1.c.smt2 | 0.130s | 20.604MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.s3_srvr_6_false-unreach-call.cil.c.smt2 | 0.130s | 20.68MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.trex03_false-unreach-call_true-termination.i.smt2 | 0.130s | 20.36MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.jain_1_true-unreach-call.i.smt2 | 0.130s | 20.392MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.mutex_lock_int.c_false-unreach-call.i.smt2 | 0.130s | 20.148MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_14_true-unreach-call.c.smt2 | 0.130s | 21.388MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_14.smt2 | 0.130s | 22.128MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_11.smt2 | 0.130s | 21.772MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_98.smt2 | 0.130s | 21.176MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_31.smt2 | 0.130s | 21.12MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_87.smt2 | 0.130s | 21.284MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_12.smt2 | 0.130s | 21.304MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_89.smt2 | 0.130s | 20.612MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.sum03_true-unreach-call_false-termination.i.smt2 | 0.131s | 20.108MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2408.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.131s | 20.624MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_23.smt2 | 0.131s | 20.408MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_19.smt2 | 0.131s | 21.408MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_16.smt2 | 0.131s | 21.116MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_81.smt2 | 0.131s | 20.704MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_48.smt2 | 0.131s | 21.132MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_10_true-unreach-call.c.smt2 | 0.132s | 20.916MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--joystick--turbografx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.132s | 24.764MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_20.smt2 | 0.132s | 20.876MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_11.smt2 | 0.132s | 20.36MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_19.smt2 | 0.132s | 21.296MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_03.smt2 | 0.132s | 21.38MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_58.smt2 | 0.132s | 20.764MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_60.smt2 | 0.132s | 20.604MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_85.smt2 | 0.132s | 20.956MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_13.smt2 | 0.132s | 20.66MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.test_locks_13_true-unreach-call.c.smt2 | 0.133s | 21.176MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_23.smt2 | 0.133s | 21.956MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_14.smt2 | 0.133s | 21.116MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_67.smt2 | 0.133s | 20.88MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_17.smt2 | 0.133s | 20.872MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_46.smt2 | 0.133s | 20.928MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_31.smt2 | 0.133s | 20.96MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_64.smt2 | 0.133s | 20.652MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_83.smt2 | 0.133s | 21.596MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_23.smt2 | 0.134s | 21.528MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_24.smt2 | 0.134s | 21.632MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_16.smt2 | 0.134s | 21.508MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_93.smt2 | 0.134s | 20.696MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_68.smt2 | 0.134s | 20.812MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_70.smt2 | 0.134s | 20.74MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_89.smt2 | 0.134s | 20.872MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.cdaudio_simpl1_false-unreach-call_true-termination.cil.c.smt2 | 0.135s | 21.164MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--edac--mce_amd_inj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.135s | 21.14MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_56.smt2 | 0.135s | 21.456MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_26.smt2 | 0.135s | 21.116MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_48.smt2 | 0.135s | 21.056MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_08.smt2 | 0.135s | 20.772MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_74.smt2 | 0.135s | 20.84MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.m0_true-unreach-call_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a.c.smt2 | 0.136s | 20.972MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_26.smt2 | 0.136s | 22.024MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_20.smt2 | 0.136s | 21.46MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_25.smt2 | 0.136s | 20.616MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_33.smt2 | 0.136s | 20.952MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_58.smt2 | 0.136s | 21.504MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_82.smt2 | 0.136s | 20.624MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_28.smt2 | 0.136s | 20.616MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_50.smt2 | 0.136s | 21.172MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_18.smt2 | 0.137s | 22.032MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_21.smt2 | 0.137s | 20.264MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_21.smt2 | 0.137s | 21.592MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_29.smt2 | 0.137s | 21.288MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_35.smt2 | 0.137s | 20.504MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_74.smt2 | 0.137s | 21.1MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_64.smt2 | 0.137s | 21.512MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_31.smt2 | 0.137s | 20.616MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_43.smt2 | 0.137s | 20.928MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_71.smt2 | 0.137s | 20.548MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product27_false-unreach-call.cil.c.smt2 | 0.138s | 22.428MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_37.smt2 | 0.138s | 20.74MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_16.smt2 | 0.138s | 20.596MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_47.smt2 | 0.138s | 20.628MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_94.smt2 | 0.138s | 20.764MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_18.smt2 | 0.139s | 20.824MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_13.smt2 | 0.139s | 20.88MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_57.smt2 | 0.139s | 20.848MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_06.smt2 | 0.139s | 21.188MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_77.smt2 | 0.139s | 21.312MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_21.smt2 | 0.139s | 21.312MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_90.smt2 | 0.139s | 20.772MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_96.smt2 | 0.139s | 20.888MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product19_false-unreach-call.cil.c.smt2 | 0.140s | 22.132MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product31_false-unreach-call.cil.c.smt2 | 0.140s | 22.38MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_10.smt2 | 0.140s | 21.436MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_12.smt2 | 0.140s | 22.056MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_27.smt2 | 0.140s | 21.268MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_18.smt2 | 0.140s | 20.684MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_21.smt2 | 0.140s | 21.276MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_16.smt2 | 0.140s | 21.272MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_37.smt2 | 0.140s | 21.14MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_98.smt2 | 0.140s | 20.704MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_46.smt2 | 0.140s | 20.668MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_25.smt2 | 0.141s | 21.416MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_25.smt2 | 0.141s | 21.624MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_48.smt2 | 0.141s | 20.836MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_36.smt2 | 0.141s | 21.384MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_28.smt2 | 0.142s | 21.6MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_19.smt2 | 0.142s | 20.912MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_96.smt2 | 0.142s | 21.388MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_83.smt2 | 0.142s | 21.028MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_27.smt2 | 0.142s | 20.904MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_24.smt2 | 0.143s | 21.992MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_72.smt2 | 0.143s | 21.084MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_88.smt2 | 0.143s | 21.148MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_54.smt2 | 0.143s | 20.944MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_44.smt2 | 0.143s | 21.296MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_product18_false-unreach-call.cil.c.smt2 | 0.144s | 22.376MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--sgi-xp--xp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.144s | 21.44MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_18.smt2 | 0.144s | 21.436MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0100_10_12.smt2 | 0.144s | 20.496MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0600_10_29.smt2 | 0.144s | 20.84MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_99.smt2 | 0.144s | 21.12MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_42.smt2 | 0.144s | 21.132MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_21.smt2 | 0.145s | 21.336MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0200_10_23.smt2 | 0.145s | 20.444MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_46.smt2 | 0.145s | 21.128MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_05.smt2 | 0.145s | 20.656MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_53.smt2 | 0.145s | 20.956MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_20.smt2 | 0.146s | 21.424MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_29.smt2 | 0.146s | 21.872MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_28.smt2 | 0.146s | 21.068MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_20.smt2 | 0.146s | 21.468MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_06.smt2 | 0.146s | 21.092MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_75.smt2 | 0.146s | 21.608MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_26.smt2 | 0.147s | 21.76MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_21.smt2 | 0.147s | 21.768MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_38.smt2 | 0.147s | 21.208MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_29.smt2 | 0.148s | 20.592MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_19.smt2 | 0.148s | 20.368MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_79.smt2 | 0.148s | 20.872MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_39.smt2 | 0.148s | 21.228MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_55.smt2 | 0.148s | 21.364MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_57.smt2 | 0.148s | 21.124MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_59.smt2 | 0.148s | 21.268MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_42.smt2 | 0.148s | 20.652MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_97.smt2 | 0.148s | 20.548MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_27.smt2 | 0.149s | 21.24MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_22.smt2 | 0.149s | 21.328MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_51.smt2 | 0.149s | 21.276MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_86.smt2 | 0.149s | 21.084MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_57.smt2 | 0.149s | 20.672MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_63.smt2 | 0.149s | 20.876MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_18.smt2 | 0.149s | 21.172MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_11.smt2 | 0.149s | 21.016MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem01_00_true-unreach-call.c.smt2 | 0.150s | 24.976MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_27.smt2 | 0.150s | 21.904MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_27.smt2 | 0.150s | 21.9MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_42.smt2 | 0.150s | 21.28MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_49.smt2 | 0.150s | 21.224MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_21.smt2 | 0.151s | 21.588MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_21.smt2 | 0.151s | 21.644MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_73.smt2 | 0.151s | 20.672MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_58.smt2 | 0.151s | 21.256MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_23.smt2 | 0.152s | 20.688MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0500_10_14.smt2 | 0.152s | 20.948MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_24.smt2 | 0.152s | 21.204MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_26.smt2 | 0.153s | 21.272MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_17.smt2 | 0.153s | 21.708MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_11.smt2 | 0.153s | 22.008MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_67.smt2 | 0.153s | 21.032MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_81.smt2 | 0.153s | 21.3MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_20.smt2 | 0.154s | 22.056MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_13.smt2 | 0.154s | 21.56MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_98.smt2 | 0.154s | 20.82MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_12.smt2 | 0.154s | 21.244MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_11.smt2 | 0.155s | 21.368MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_22.smt2 | 0.155s | 21.136MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_11.smt2 | 0.157s | 21.224MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_29.smt2 | 0.157s | 21.2MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_27.smt2 | 0.157s | 21.656MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_86.smt2 | 0.157s | 21.08MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_92.smt2 | 0.157s | 21.272MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_61.smt2 | 0.158s | 21.236MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_35.smt2 | 0.158s | 21.272MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1200_10_15.smt2 | 0.159s | 21.896MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0250_10_27.smt2 | 0.159s | 20.376MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0300_10_26.smt2 | 0.159s | 20.592MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_56.smt2 | 0.159s | 21.36MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_10_0150_10_14.smt2 | 0.160s | 20.432MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_71.smt2 | 0.160s | 21.288MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-sddr55.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.161s | 21.864MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_12.smt2 | 0.161s | 20.88MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0750_10_12.smt2 | 0.161s | 21.528MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_97.smt2 | 0.161s | 21.136MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0400_10_28.smt2 | 0.162s | 20.928MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-usbat.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.163s | 21.976MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_12.smt2 | 0.163s | 21.788MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_10.smt2 | 0.164s | 21.592MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0300_10_11.smt2 | 0.164s | 21.176MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0200_10_17.smt2 | 0.164s | 20.668MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_18.smt2 | 0.165s | 22.188MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-datafab.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.166s | 21.704MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0900_10_13.smt2 | 0.168s | 21.504MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_20_0300_10_15.smt2 | 0.169s | 20.772MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_30_0600_10_14.smt2 | 0.169s | 21.788MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_17.smt2 | 0.169s | 22.204MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_75_45_92.smt2 | 0.172s | 20.856MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_74.smt2 | 0.172s | 21.044MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_83.smt2 | 0.172s | 20.884MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_17.smt2 | 0.173s | 22.204MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_61.smt2 | 0.173s | 20.728MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_76.smt2 | 0.174s | 21.284MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_30_60_45_29.smt2 | 0.175s | 20.784MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_38.smt2 | 0.176s | 21.032MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_85.smt2 | 0.178s | 21.296MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_22.smt2 | 0.179s | 20.956MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_150_30_19.smt2 | 0.181s | 21.284MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-freecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.183s | 21.792MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_23.smt2 | 0.183s | 22.244MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_78.smt2 | 0.187s | 21.312MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_23.smt2 | 0.189s | 21.132MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0400_10_14.smt2 | 0.191s | 21.864MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_27.smt2 | 0.194s | 22.22MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_23.smt2 | 0.209s | 22.06MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_40_80_60_04.smt2 | 0.210s | 21.344MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.s3_srvr.blast.10_false-unreach-call.i.cil.c.smt2 | 0.211s | 22.252MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_12.smt2 | 0.211s | 22.004MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_69.smt2 | 0.212s | 21.828MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_13.smt2 | 0.213s | 21.972MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_28.smt2 | 0.216s | 22.076MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product14_false-unreach-call.cil.c.smt2 | 0.224s | 22.16MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product21_false-unreach-call.cil.c.smt2 | 0.231s | 22.932MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomDecoupled/pb_real_50_100_30_57.smt2 | 0.232s | 21.66MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product40_false-unreach-call.cil.c.smt2 | 0.243s | 23.144MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product46_true-unreach-call.cil.c.smt2 | 0.246s | 22.924MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_16.smt2 | 0.248s | 22.288MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product33_false-unreach-call.cil.c.smt2 | 0.256s | 22.144MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product17_false-unreach-call.cil.c.smt2 | 0.260s | 22.304MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product61_true-unreach-call.cil.c.smt2 | 0.263s | 23.544MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.s3_srvr.blast.12_false-unreach-call.i.cil.c.smt2 | 0.268s | 22.272MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.s3_srvr.blast.06_false-unreach-call.i.cil.c.smt2 | 0.273s | 22.404MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_1000_10_14.smt2 | 0.278s | 22.272MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product09_false-unreach-call.cil.c.smt2 | 0.287s | 21.844MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product49_true-unreach-call.cil.c.smt2 | 0.288s | 22.8MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.s3_srvr.blast.08_false-unreach-call.i.cil.c.smt2 | 0.289s | 22.256MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product29_false-unreach-call.cil.c.smt2 | 0.293s | 23.032MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product36_false-unreach-call.cil.c.smt2 | 0.299s | 22.172MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product46_true-unreach-call.cil.c.smt2 | 0.308s | 22.84MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product61_true-unreach-call.cil.c.smt2 | 0.310s | 23.44MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.s3_srvr.blast.16_false-unreach-call.i.cil.c.smt2 | 0.311s | 22.412MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.s3_srvr.blast.14_false-unreach-call.i.cil.c.smt2 | 0.311s | 22.452MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--apanel.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.313s | 24.552MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product06_false-unreach-call.cil.c.smt2 | 0.316s | 22.096MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product05_false-unreach-call.cil.c.smt2 | 0.317s | 22.044MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--video--backlight--lms283gf05.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.318s | 23.936MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product19_false-unreach-call.cil.c.smt2 | 0.322s | 22.332MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product02_false-unreach-call.cil.c.smt2 | 0.322s | 21.892MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--tda18218.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.322s | 22.18MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product36_false-unreach-call.cil.c.smt2 | 0.325s | 22.444MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product16_false-unreach-call.cil.c.smt2 | 0.327s | 22.172MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product34_false-unreach-call.cil.c.smt2 | 0.328s | 22.152MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i.smt2 | 0.328s | 21.264MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product53_true-unreach-call.cil.c.smt2 | 0.332s | 23.144MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product26_false-unreach-call.cil.c.smt2 | 0.333s | 22.208MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product34_true-unreach-call.cil.c.smt2 | 0.334s | 22.14MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product50_true-unreach-call.cil.c.smt2 | 0.335s | 22.896MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product51_false-unreach-call.cil.c.smt2 | 0.335s | 23.24MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product39_false-unreach-call.cil.c.smt2 | 0.337s | 23.172MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product45_true-unreach-call.cil.c.smt2 | 0.337s | 22.676MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product07_false-unreach-call.cil.c.smt2 | 0.338s | 22.188MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product52_false-unreach-call.cil.c.smt2 | 0.338s | 23.16MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product57_true-unreach-call.cil.c.smt2 | 0.341s | 22.904MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product18_false-unreach-call.cil.c.smt2 | 0.341s | 22.32MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product08_false-unreach-call.cil.c.smt2 | 0.341s | 22.152MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product42_true-unreach-call.cil.c.smt2 | 0.342s | 22.364MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product37_true-unreach-call.cil.c.smt2 | 0.343s | 22.704MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt2060.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.343s | 24.564MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--addac--adt7316-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.344s | 24.568MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product04_false-unreach-call.cil.c.smt2 | 0.345s | 21.908MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product37_false-unreach-call.cil.c.smt2 | 0.345s | 22.984MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product30_false-unreach-call.cil.c.smt2 | 0.345s | 23.08MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_24.smt2 | 0.346s | 22.652MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-gl861.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.348s | 24.008MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product35_false-unreach-call.cil.c.smt2 | 0.348s | 22.412MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--keyboard--xtkbd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.351s | 23.784MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product37_true-unreach-call.cil.c.smt2 | 0.352s | 22.248MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_finepix.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.354s | 24.148MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-ce6230.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.354s | 23.904MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product55_false-unreach-call.cil.c.smt2 | 0.356s | 24.076MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product03_false-unreach-call.cil.c.smt2 | 0.357s | 21.896MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product22_false-unreach-call.cil.c.smt2 | 0.358s | 23.012MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product25_false-unreach-call.cil.c.smt2 | 0.360s | 22.22MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--media--dvb--dvb-usb--dvb-usb-vp7045.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.361s | 24.244MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product13_false-unreach-call.cil.c.smt2 | 0.361s | 22.204MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--keyboard--stowaway.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.362s | 23.944MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product41_true-unreach-call.cil.c.smt2 | 0.363s | 22.388MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product23_false-unreach-call.cil.c.smt2 | 0.363s | 22.896MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-nova-t-usb2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.364s | 24.16MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_sq905c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.365s | 25.388MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.s3_srvr.blast.15_false-unreach-call.i.cil.c.smt2 | 0.366s | 22.268MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product38_true-unreach-call.cil.c.smt2 | 0.367s | 22.504MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product38_false-unreach-call.cil.c.smt2 | 0.370s | 23.128MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product64_true-unreach-call.cil.c.smt2 | 0.371s | 24.22MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product32_false-unreach-call.cil.c.smt2 | 0.372s | 22.904MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product38_true-unreach-call.cil.c.smt2 | 0.372s | 22.7MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product46_true-unreach-call.cil.c.smt2 | 0.374s | 23.288MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product35_false-unreach-call.cil.c.smt2 | 0.375s | 22.208MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-au6610.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.377s | 23.908MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.sll_to_dll_rev_false-unreach-call.i.smt2 | 0.377s | 22.692MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product31_false-unreach-call.cil.c.smt2 | 0.377s | 23.084MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product10_false-unreach-call.cil.c.smt2 | 0.377s | 21.824MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product54_false-unreach-call.cil.c.smt2 | 0.377s | 23.784MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product51_false-unreach-call.cil.c.smt2 | 0.378s | 23.108MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product01_false-unreach-call.cil.c.smt2 | 0.380s | 21.82MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--backlight--vgg2432a4.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.382s | 23.82MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.main1_true-unreach-call_drivers-media-video-tlg2300-poseidon-ko--32_7a--4a349aa-1.c.smt2 | 0.385s | 22.368MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--mtd--ubi--gluebi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.386s | 26.208MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product63_true-unreach-call.cil.c.smt2 | 0.389s | 24.16MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.main1_true-unreach-call_drivers-media-video-tlg2300-poseidon-ko--32_7a--4a349aa.c.smt2 | 0.392s | 22.58MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product24_false-unreach-call.cil.c.smt2 | 0.392s | 22.872MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product62_true-unreach-call.cil.c.smt2 | 0.393s | 23.952MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product50_false-unreach-call.cil.c.smt2 | 0.397s | 23.156MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product52_false-unreach-call.cil.c.smt2 | 0.403s | 23.148MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product53_true-unreach-call.cil.c.smt2 | 0.405s | 23.268MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--joystick--twidjoy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.405s | 23.172MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product45_true-unreach-call.cil.c.smt2 | 0.407s | 23.016MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--keyboard--newtonkbd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.407s | 24.04MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product63_true-unreach-call.cil.c.smt2 | 0.411s | 24.22MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--magellan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.414s | 26.432MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product28_false-unreach-call.cil.c.smt2 | 0.421s | 22.56MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--joystick--magellan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.427s | 25.392MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--mtdoops.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.433s | 29.744MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product62_true-unreach-call.cil.c.smt2 | 0.434s | 23.616MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--vmw_balloon.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.444s | 24.912MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_stv0680.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.446s | 23.676MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product54_true-unreach-call.cil.c.smt2 | 0.447s | 23.116MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product54_true-unreach-call.cil.c.smt2 | 0.447s | 22.988MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product20_false-unreach-call.cil.c.smt2 | 0.458s | 22.24MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product56_false-unreach-call.cil.c.smt2 | 0.460s | 23.804MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product53_false-unreach-call.cil.c.smt2 | 0.460s | 23.736MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product12_false-unreach-call.cil.c.smt2 | 0.461s | 21.904MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_pac207.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.462s | 27.832MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.c.smt2 | 0.463s | 23.728MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product58_true-unreach-call.cil.c.smt2 | 0.481s | 23.112MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product43_false-unreach-call.cil.c.smt2 | 0.485s | 22.976MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--egalax_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.487s | 27.056MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-sddr09.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.491s | 23.076MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--staging--telephony--ixj_pcmcia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.492s | 27.0MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--watchdog--cpu5wdt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.493s | 24.412MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--xen--xenfs--xenfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.494s | 22.904MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.diskperf_false-unreach-call.i.cil.c.smt2 | 0.501s | 29.064MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product11_false-unreach-call.cil.c.smt2 | 0.501s | 21.796MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product15_false-unreach-call.cil.c.smt2 | 0.501s | 22.396MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product27_false-unreach-call.cil.c.smt2 | 0.506s | 22.228MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_18.smt2 | 0.507s | 22.656MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product33_true-unreach-call.cil.c.smt2 | 0.514s | 22.28MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product49_false-unreach-call.cil.c.smt2 | 0.516s | 23.196MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem14_60_false-unreach-call.c.smt2 | 0.527s | 26.288MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt2131.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.528s | 29.324MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product44_false-unreach-call.cil.c.smt2 | 0.529s | 22.9MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product61_true-unreach-call.cil.c.smt2 | 0.537s | 23.872MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--ad7879-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.548s | 26.748MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--cyttsp_spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.555s | 27.64MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--scsi--dmx3191d.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.584s | 25.936MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--image--microtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.601s | 31.676MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product62_true-unreach-call.cil.c.smt2 | 0.620s | 23.944MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product40_false-unreach-call.cil.c.smt2 | 0.637s | 23.196MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.pc_sfifo_2_false-unreach-call_false-termination.cil.c.smt2 | 0.640s | 22.296MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product45_true-unreach-call.cil.c.smt2 | 0.643s | 23.008MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--joystick--spaceorb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.655s | 28.704MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--max1586.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.655s | 32.66MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--misc--phantom.ko-main.cil.out.c.smt2 | 0.655s | 35.068MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product60_false-unreach-call.cil.c.smt2 | 0.672s | 23.808MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_soft.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.678s | 32.776MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product39_false-unreach-call.cil.c.smt2 | 0.709s | 23.296MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.parport_false-unreach-call.i.cil.c.smt2 | 0.729s | 36.7MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.diskperf_true-unreach-call.i.cil.c.smt2 | 0.740s | 25.76MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product59_false-unreach-call.cil.c.smt2 | 0.778s | 23.796MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2431.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.792s | 35.544MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--ubi--gluebi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.801s | 34.316MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product55_false-unreach-call.cil.c.smt2 | 0.822s | 23.808MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-rtl28xxu.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.826s | 30.888MiB| sat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0800_10_14.smt2 | 0.864s | 22.364MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-az6027.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.873s | 33.284MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--tty--serial--altera_jtaguart.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.879s | 30.78MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product63_false-unreach-call.cil.c.smt2 | 0.894s | 24.492MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product56_false-unreach-call.cil.c.smt2 | 0.896s | 23.988MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product64_false-unreach-call.cil.c.smt2 | 0.927s | 24.444MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--media--video--videobuf-vmalloc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 0.932s | 30.8MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem14_00_true-unreach-call.c.smt2 | 0.938s | 25.02MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product48_false-unreach-call.cil.c.smt2 | 0.943s | 23.664MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.pc_sfifo_3_true-unreach-call_false-termination.cil.c.smt2 | 0.975s | 22.0MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec3_product47_false-unreach-call.cil.c.smt2 | 0.975s | 23.74MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.floppy_false-unreach-call.i.cil.c.smt2 | 1.005s | 35.184MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem14_30_true-unreach-call.c.smt2 | 1.026s | 25.044MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mxl5007t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 1.028s | 37.844MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem02_00_true-unreach-call.c.smt2 | 1.033s | 25.676MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/mathsat/RandomCoupled/pb_real_40_0600_10_14.smt2 | 1.051s | 22.072MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem10_00_true-unreach-call.c.smt2 | 1.081s | 23.624MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem10_10_true-unreach-call.c.smt2 | 1.102s | 23.724MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--max2165.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 1.118s | 30.828MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem10_20_true-unreach-call.c.smt2 | 1.140s | 23.804MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.main3_true-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa-1.c.smt2 | 1.197s | 37.924MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.main3_false-unreach-call_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.c.smt2 | 1.201s | 41.9MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem01_30_true-unreach-call.c.smt2 | 1.211s | 25.836MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-lp5521.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 1.218s | 33.568MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-r9701.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 1.227s | 36.7MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec27_product13_true-unreach-call.cil.c.smt2 | 1.240s | 28.396MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-bd2802.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 1.243s | 37.788MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.ddv_machzwd_inw_false-unreach-call.i.smt2 | 1.247s | 45.704MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem01_40_true-unreach-call.c.smt2 | 1.250s | 25.808MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem14_20_true-unreach-call.c.smt2 | 1.277s | 25.004MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-m41t94.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 1.286s | 26.744MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec8_product14_true-unreach-call.cil.c.smt2 | 1.317s | 35.22MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem02_10_true-unreach-call.c.smt2 | 1.398s | 25.724MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem02_40_true-unreach-call.c.smt2 | 1.479s | 25.628MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--tda18271c2dd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 1.486s | 87.272MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--watchdog--wm831x_wdt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 1.525s | 32.544MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem01_10_true-unreach-call.c.smt2 | 1.584s | 25.768MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem02_30_true-unreach-call.c.smt2 | 1.603s | 25.644MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c.smt2 | 1.748s | 69.028MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.rekh_ctm_true-unreach-call.2.c.smt2 | 1.753s | 214.0MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.ddv_machzwd_outb_false-unreach-call.i.smt2 | 1.840s | 61.748MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem01_60_false-unreach-call.c.smt2 | 1.874s | 27.032MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem15_60_false-unreach-call.c.smt2 | 1.928s | 35.844MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem16_60_false-unreach-call.c.smt2 | 2.298s | 34.244MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem16_50_true-unreach-call.c.smt2 | 2.313s | 31.548MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.linux-3.8-rc1-32_7a-drivers--hwmon--w83793.ko-ldv_main0_true-unreach-call.cil.out.c.smt2 | 2.412s | 63.536MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--infiniband--hw--cxgb3--iw_cxgb3.ko-ldv_main6_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 2.613s | 99.752MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--power--wm831x_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 2.717s | 92.1MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt20xx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 3.524s | 97.032MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--infiniband--hw-cxgb3--iw_cxgb3.ko-main.cil.out.c.smt2 | 3.589s | 108.0MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--mem2mem_testdev.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 3.689s | 95.088MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem17_60_false-unreach-call.c.smt2 | 4.343s | 47.608MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.linux-3.8-rc1-32_7a-drivers--input--misc--uinput.ko-ldv_main0_true-unreach-call.cil.out.c.smt2 | 4.611s | 75.136MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--platform--x86--samsung-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 4.867s | 126.0MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--usb--hso.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 4.938s | 116.0MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.rekh_ctm_true-unreach-call.1.c.smt2 | 5.375s | 260.0MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.rekh_ctm_false-unreach-call.2.c.smt2 | 5.676s | 254.0MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem18_60_false-unreach-call.c.smt2 | 6.013s | 61.396MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem03_10_true-unreach-call.c.smt2 | 7.151s | 42.608MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem03_60_false-unreach-call.c.smt2 | 7.181s | 46.66MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem03_30_true-unreach-call.c.smt2 | 7.641s | 42.564MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem03_40_true-unreach-call.c.smt2 | 7.706s | 42.508MiB| unsat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem12_60_false-unreach-call.c.smt2 | 11.610s | 69.576MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.module_get_put-drivers-bluetooth-btmrvl.ko_true-unreach-call.cil.out.i.pp.i.smt2 | 14.139s | 297.0MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem13_60_false-unreach-call.c.smt2 | 14.294s | 78.8MiB| sat | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem04_60_false-unreach-call.c.smt2 | 20.019s | 109.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--usb--serial--mos7840.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 20.059s | 295.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem04_50_true-unreach-call.c.smt2 | 20.063s | 109.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem06_60_false-unreach-call.c.smt2 | 20.063s | 195.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem04_20_true-unreach-call.c.smt2 | 20.093s | 109.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem04_00_true-unreach-call.c.smt2 | 20.095s | 109.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem04_30_true-unreach-call.c.smt2 | 20.104s | 109.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem05_60_false-unreach-call.c.smt2 | 20.110s | 199.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec3_productSimulator_false-unreach-call.cil.c.smt2 | 20.116s | 532.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem04_10_true-unreach-call.c.smt2 | 20.119s | 109.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem19_60_false-unreach-call.c.smt2 | 20.124s | 99.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.m0_true-unreach-call_drivers-net-slip-ko--108_1a--1b0b0ac.c.smt2 | 20.139s | 277.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem07_50_true-unreach-call.c.smt2 | 20.148s | 1541.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec27_productSimulator_false-unreach-call.cil.c.smt2 | 20.157s | 1027.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--vhost--vhost_net.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c.smt2 | 20.158s | 1048.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.cs_fib_false-unreach-call.i.smt2 | 20.169s | 2015.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.cs_stack_true-unreach-call.i.smt2 | 20.171s | 2000.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem07_10_true-unreach-call.c.smt2 | 20.176s | 1541.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.cs_stack_false-unreach-call.i.smt2 | 20.237s | 2001.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.rekh_ctm_true-unreach-call.3.c.smt2 | 20.238s | 1313.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem07_00_true-unreach-call.c.smt2 | 20.249s | 1541.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem07_60_false-unreach-call.c.smt2 | 20.256s | 1541.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.Problem08_60_false-unreach-call.c.smt2 | 20.291s | 2962.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.rekh_ctm_true-unreach-call.4.c.smt2 | 20.295s | 2548.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.rekcba_ctm_true-unreach-call.1.c.smt2 | 20.321s | 2552.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.cs_fib_true-unreach-call.i.smt2 | 20.328s | 3960.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.rekcba_ctm_true-unreach-call.2.c.smt2 | 20.334s | 2553.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.rekcba_ctm_false-unreach-call.2.c.smt2 | 20.341s | 2552.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.cs_fib_longer_true-unreach-call.i.smt2 | 20.361s | 3961.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.cs_fib_longer_false-unreach-call.i.smt2 | 20.368s | 3961.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.rekcba_ctm_false-unreach-call.3.c.smt2 | 20.431s | 4946.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.rekcba_ctm_true-unreach-call.3.c.smt2 | 20.444s | 4946.0MiB| timeout | 0 | | | |non-incremental/QF_UFLRA/cpachecker-bmc-svcomp14/cpachecker-bmc.rekcba_ctm_true-unreach-call.4.c.smt2 | 20.519s | 4983.0MiB| timeout | 0 | | |