| Benchmark | Answer | Time | Correct? |
|---|
| Averest/binary_search/BinarySearch_safe_bgmc001.smt |
unsat |
1.7 |
no (unsound)
|
| Averest/buble_sort/BubbleSort_live_bgmc010.smt |
timeout |
1208.2 |
yes |
| Averest/buble_sort/BubbleSort_live_bgmc011.smt |
unsat |
3.4 |
yes |
| Averest/buble_sort/BubbleSort_live_blmc003.smt |
timeout |
1208.1 |
yes |
| Averest/buble_sort/BubbleSort_live_blmc008.smt |
timeout |
1208.8 |
yes |
| Averest/buble_sort/BubbleSort_safe_bgmc003.smt |
unsat |
0.2 |
yes |
| Averest/buble_sort/BubbleSort_safe_blmc002.smt |
unsat |
1.1 |
yes |
| Averest/buble_sort/BubbleSort_safe_blmc005.smt |
timeout |
1208.0 |
yes |
| Averest/buble_sort/BubbleSort_safe_blmc007.smt |
timeout |
1208.1 |
yes |
| Averest/buble_sort/BubbleSort_safe_blmc013.smt |
timeout |
1208.3 |
yes |
| Averest/buble_sort/BubbleSort_safe_blmc014.smt |
unsat |
159.8 |
yes |
| Averest/buble_sort/BubbleSort_safe_blmc016.smt |
unsat |
240.5 |
yes |
| Averest/fast_max/FastMax_safe_blmc000.smt |
timeout |
1207.9 |
yes |
| Averest/insertion_sort/InsertionSort_live_bgmc004.smt |
timeout |
1208.0 |
yes |
| Averest/insertion_sort/InsertionSort_live_bgmc007.smt |
timeout |
1208.1 |
yes |
| Averest/insertion_sort/InsertionSort_live_bgmc008.smt |
timeout |
1208.4 |
yes |
| Averest/insertion_sort/InsertionSort_live_bgmc009.smt |
timeout |
1208.4 |
yes |
| Averest/insertion_sort/InsertionSort_live_blmc006.smt |
timeout |
1209.0 |
yes |
| Averest/insertion_sort/InsertionSort_safe_blmc001.smt |
timeout |
1208.1 |
yes |
| Averest/insertion_sort/InsertionSort_safe_blmc006.smt |
timeout |
1208.0 |
yes |
| Averest/linear_search/LinearSearch_live_bgmc002.smt |
timeout |
1207.9 |
yes |
| Averest/min_max/MinMax_live_bgmc000.smt |
timeout |
1207.8 |
yes |
| Averest/min_max/MinMax_live_bgmc003.smt |
unsat |
0.3 |
yes |
| Averest/parallel_search/ParallelSearch_live_blmc000.smt |
unsat |
0.1 |
yes |
| Averest/parallel_search/ParallelSearch_safe_bgmc002.smt |
timeout |
1207.8 |
yes |
| Averest/partition/Partition_live_bgmc000.smt |
timeout |
1207.7 |
yes |
| Averest/partition/Partition_live_bgmc004.smt |
timeout |
1207.9 |
yes |
| Averest/partition/Partition_safe_blmc004.smt |
timeout |
1208.1 |
yes |
| Averest/selection_sort/SelectionSort_live_bgmc010.smt |
unsat |
3.6 |
yes |
| Averest/selection_sort/SelectionSort_live_blmc000.smt |
timeout |
1208.0 |
yes |
| Averest/selection_sort/SelectionSort_live_blmc007.smt |
timeout |
1208.9 |
yes |
| Averest/selection_sort/SelectionSort_safe_bgmc010.smt |
timeout |
1208.3 |
yes |
| Averest/selection_sort/SelectionSort_safe_blmc004.smt |
unsat |
4.2 |
yes |
| Averest/selection_sort/SelectionSort_safe_blmc006.smt |
unsat |
11.6 |
yes |
| Averest/selection_sort/SelectionSort_safe_blmc008.smt |
unsat |
34.1 |
yes |
| Averest/selection_sort/SelectionSort_safe_blmc009.smt |
timeout |
1208.2 |
yes |
| Averest/selection_sort/SelectionSort_safe_blmc015.smt |
timeout |
1207.8 |
yes |
| Averest/sorting_network/SortingNetwork4_live_bgmc003.smt |
timeout |
1208.0 |
yes |
| Averest/sorting_network/SortingNetwork4_live_bgmc004.smt |
unsat |
0.0 |
yes |
| Averest/sorting_network/SortingNetwork4_live_blmc000.smt |
timeout |
1208.2 |
yes |
| Averest/sorting_network/SortingNetwork4_safe_blmc001.smt |
timeout |
1208.2 |
yes |
| Averest/sorting_network/SortingNetwork8_live_blmc003.smt |
timeout |
1209.0 |
yes |
| Averest/sorting_network/SortingNetwork8_live_blmc004.smt |
timeout |
1208.9 |
yes |
| Averest/sorting_network/SortingNetwork8_safe_blmc001.smt |
timeout |
1208.0 |
yes |
| DTP/DTP_k2_n35_c175_s13.smt |
timeout |
1207.7 |
yes |
| DTP/DTP_k2_n35_c175_s14.smt |
timeout |
1207.8 |
yes |
| DTP/DTP_k2_n35_c210_s10.smt |
timeout |
1208.1 |
yes |
| DTP/DTP_k2_n35_c210_s18.smt |
timeout |
1207.6 |
yes |
| DTP/DTP_k2_n35_c245_s19.smt |
timeout |
1207.9 |
yes |
| RTCL/b02_tf_20/ckt_PROP0_tf_20.smt |
unsat |
0.1 |
yes |
| RTCL/b13_tf_10/ckt_PROP1_tf_10.smt |
unsat |
0.1 |
yes |
| RTCL/b13_tf_20/ckt_PROP3_tf_20.smt |
unsat |
0.6 |
yes |
| RTCL/b13_tf_25/ckt_PROP3_tf_25.smt |
unsat |
1.0 |
yes |
| RTCL/b13_tf_9_PROP14/ckt_PROP14_tf_9.smt |
unsat |
0.1 |
no (unsound)
|
| check/bignum_idl1.smt |
unknown |
0.0 |
yes |
| check/bignum_idl2.smt |
unknown |
0.0 |
yes |
| check/int_incompleteness1.smt |
unsat |
0.0 |
yes |
| diamonds/diamonds.11.10.i.a.u.smt |
timeout |
1209.2 |
yes |
| job_shop/jobshop22-2-11-11-4-4-12.smt |
timeout |
1208.8 |
yes |
| job_shop/jobshop24-2-12-12-4-4-11.smt |
timeout |
1208.8 |
yes |
| job_shop/jobshop4-2-2-2-2-4-12.smt |
timeout |
1207.4 |
yes |
| mathsat/fischer/FISCHER11-11-ninc.smt |
unsat |
668.9 |
yes |
| mathsat/fischer/FISCHER12-11-ninc.smt |
timeout |
1208.1 |
yes |
| mathsat/fischer/FISCHER12-13-ninc.smt |
timeout |
1208.1 |
yes |
| mathsat/fischer/FISCHER13-2-ninc.smt |
unsat |
0.8 |
yes |
| mathsat/fischer/FISCHER14-12-ninc.smt |
timeout |
1207.9 |
yes |
| mathsat/fischer/FISCHER14-5-ninc.smt |
unsat |
4.9 |
yes |
| mathsat/fischer/FISCHER4-4-ninc.smt |
unsat |
0.3 |
yes |
| mathsat/fischer/FISCHER6-5-ninc.smt |
unsat |
1.0 |
yes |
| mathsat/fischer/FISCHER6-7-ninc.smt |
timeout |
1208.2 |
yes |
| mathsat/fischer/FISCHER7-6-ninc.smt |
unsat |
1.9 |
yes |
| mathsat/fischer/FISCHER7-7-ninc.smt |
unsat |
3.2 |
yes |
| mathsat/fischer/FISCHER7-8-ninc.smt |
timeout |
1208.0 |
yes |
| mathsat/post_office/PO3-2-PO3.smt |
unsat |
0.2 |
yes |
| mathsat/post_office/PO3-9-PO3.smt |
timeout |
1207.9 |
yes |
| planning/plan-17.cvc.smt |
unsat |
0.6 |
yes |
| planning/plan-29.cvc.smt |
unsat |
1.6 |
yes |
| planning/plan-45.cvc.smt |
unsat |
4.1 |
yes |
| qlock/qlock-4-10-12.base.cvc.smt |
timeout |
1208.8 |
yes |
| qlock/qlock-4-10-13.base.cvc.smt |
timeout |
1208.9 |
yes |
| qlock/qlock-4-10-15.base.cvc.smt |
timeout |
1209.1 |
yes |
| qlock/qlock-4-10-18.base.cvc.smt |
timeout |
1209.0 |
yes |
| qlock/qlock-4-10-21.base.cvc.smt |
timeout |
1208.7 |
yes |
| qlock/qlock-4-10-25.induction.cvc.smt |
timeout |
1209.1 |
yes |
| qlock/qlock-4-10-26.base.cvc.smt |
timeout |
1208.5 |
yes |
| qlock/qlock-4-10-29.base.cvc.smt |
timeout |
1209.2 |
yes |
| qlock/qlock-4-10-30.base.cvc.smt |
timeout |
1208.8 |
yes |
| qlock/qlock-4-10-32.base.cvc.smt |
timeout |
1208.6 |
yes |
| qlock/qlock-4-10-34.base.cvc.smt |
timeout |
1209.1 |
yes |
| qlock/qlock-4-10-35.induction.cvc.smt |
timeout |
1209.0 |
yes |
| qlock/qlock-4-10-39.induction.cvc.smt |
timeout |
1209.1 |
yes |
| qlock/qlock-4-10-40.induction.cvc.smt |
timeout |
1209.2 |
yes |
| queens_bench/n_queen/queen20-1.smt |
timeout |
1207.9 |
yes |
| queens_bench/n_queen/queen35-1.smt |
timeout |
1208.1 |
yes |
| queens_bench/n_queen/queen60-1.smt |
timeout |
1207.4 |
yes |
| queens_bench/super_queen/super_queen35-1.smt |
timeout |
1207.6 |
yes |
| queens_bench/toroidal_bench/toroidal_queen6-1.smt |
timeout |
1208.2 |
yes |
| queens_bench/toroidal_bench/toroidal_queen60-1.smt |
timeout |
1208.3 |
yes |
| sal/bakery/inf-bakery-invalid-2.smt |
unsat |
0.0 |
yes |
| sal/bakery/inf-bakery-invalid-4.smt |
timeout |
1208.1 |
yes |
| sal/lpsat/lpsat-goal-19.smt |
timeout |
1208.7 |
yes |
| sep/hardware/OOO_neg.2steps.smt |
unsat |
0.0 |
yes |
| sep/railroad/RailRoad1_neg_3.smt |
unsat |
198.6 |
no (unsound)
|