| Benchmark | Answer | Time | Correct? |
|---|
| TM/p-0-bucket_s13.smt |
sat |
23.1 |
yes |
| TM/p-1-bucket_s9.smt |
sat |
63.4 |
yes |
| TM/p-2-bucket_s11.smt |
sat |
13.8 |
yes |
| TM/p-3-bucket_s10.smt |
sat |
352.5 |
yes |
| TM/p-DepotsNum_s8.msat.smt |
timeout |
1194.1 |
yes |
| TM/p5-zenonumeric_s5.smt |
sat |
27.6 |
yes |
| TM/p5-zenonumeric_s7.smt |
timeout |
1208.2 |
yes |
| TM/p6-zenonumeric_s9.smt |
unknown |
88.6 |
yes |
| check/bignum_lra1.smt |
sat |
0.0 |
yes |
| check/bignum_lra2.smt |
unsat |
0.0 |
yes |
| clock_synchro/clocksynchro_10clocks.main_invar.induct.smt |
timeout |
1207.9 |
yes |
| clock_synchro/clocksynchro_10clocks.worst_case_skew.induct.smt |
timeout |
1207.9 |
yes |
| clock_synchro/clocksynchro_3clocks.main_invar.base.smt |
unsat |
0.6 |
yes |
| clock_synchro/clocksynchro_3clocks.worst_case_skew.induct.smt |
unsat |
1.3 |
yes |
| clock_synchro/clocksynchro_5clocks.main_invar.induct.smt |
unsat |
223.2 |
yes |
| clock_synchro/clocksynchro_6clocks.main_invar.induct.smt |
unsat |
395.3 |
yes |
| clock_synchro/clocksynchro_8clocks.worst_case_skew.induct.smt |
unsat |
691.4 |
yes |
| sal/carpark/Carpark2-ausgabe-2.smt |
unsat |
0.0 |
yes |
| sal/carpark/Carpark2-ausgabe-7.smt |
unsat |
0.1 |
yes |
| sal/carpark/Carpark2-ausgabe-8.smt |
sat |
1.2 |
yes |
| sal/carpark/Carpark2-t1-3.smt |
unsat |
0.1 |
yes |
| sal/gasburner/gasburner-prop3-4.smt |
unsat |
0.1 |
yes |
| sal/gasburner/gasburner-prop3-5.smt |
unsat |
0.1 |
yes |
| sal/pursuit/pursuit-safety-10.smt |
unsat |
0.4 |
yes |
| sal/pursuit/pursuit-safety-20.smt |
unsat |
1.5 |
yes |
| sal/pursuit/pursuit-safety-4.smt |
unsat |
0.1 |
yes |
| sal/pursuit/pursuit-safety-5.smt |
unsat |
0.1 |
yes |
| sal/pursuit/pursuit-safety-6.smt |
unsat |
0.2 |
yes |
| sal/pursuit/pursuit-safety-7.smt |
unsat |
0.2 |
yes |
| sal/tgc/tgc_io-safe-11.smt |
unsat |
0.7 |
yes |
| sal/tgc/tgc_io-safe-16.smt |
unsat |
1.8 |
yes |
| sal/tgc/tgc_io-safe-7.smt |
unsat |
0.3 |
yes |
| sal/windowreal/windowreal-no_t_deadlock-12.smt |
unsat |
0.1 |
yes |
| sal/windowreal/windowreal-no_t_deadlock-17.smt |
unsat |
0.2 |
yes |
| sc/sc-10.induction.cvc.smt |
sat |
1.5 |
yes |
| sc/sc-11.induction.cvc.smt |
sat |
1.4 |
yes |
| sc/sc-12.induction2.cvc.smt |
sat |
4.8 |
yes |
| sc/sc-14.induction3.cvc.smt |
sat |
7.7 |
yes |
| sc/sc-15.base.cvc.smt |
unsat |
60.4 |
yes |
| sc/sc-16.induction2.cvc.smt |
sat |
12.1 |
yes |
| sc/sc-18.base.cvc.smt |
unsat |
150.6 |
yes |
| sc/sc-19.base.cvc.smt |
unsat |
159.7 |
yes |
| sc/sc-21.induction.cvc.smt |
sat |
27.2 |
yes |
| sc/sc-22.induction.cvc.smt |
sat |
17.0 |
yes |
| sc/sc-22.induction3.cvc.smt |
sat |
46.8 |
yes |
| sc/sc-23.induction3.cvc.smt |
sat |
72.9 |
yes |
| sc/sc-25.base.cvc.smt |
unsat |
564.4 |
yes |
| sc/sc-25.induction3.cvc.smt |
sat |
63.5 |
yes |
| sc/sc-27.base.cvc.smt |
unsat |
914.8 |
yes |
| sc/sc-27.induction2.cvc.smt |
sat |
92.3 |
yes |
| sc/sc-28.base.cvc.smt |
unsat |
1137.0 |
yes |
| sc/sc-28.induction3.cvc.smt |
sat |
107.4 |
yes |
| sc/sc-29.induction2.cvc.smt |
sat |
204.9 |
yes |
| sc/sc-29.induction3.cvc.smt |
sat |
69.7 |
yes |
| sc/sc-30.induction.cvc.smt |
sat |
74.2 |
yes |
| sc/sc-31.induction2.cvc.smt |
sat |
205.1 |
yes |
| sc/sc-31.induction3.cvc.smt |
sat |
365.1 |
yes |
| sc/sc-32.base.cvc.smt |
timeout |
1207.9 |
yes |
| sc/sc-33.induction3.cvc.smt |
sat |
162.2 |
yes |
| sc/sc-34.induction.cvc.smt |
sat |
160.0 |
yes |
| sc/sc-34.induction3.cvc.smt |
sat |
180.9 |
yes |
| sc/sc-35.base.cvc.smt |
timeout |
1207.9 |
yes |
| sc/sc-36.induction2.cvc.smt |
sat |
422.3 |
yes |
| sc/sc-37.base.cvc.smt |
timeout |
1207.9 |
yes |
| sc/sc-37.induction3.cvc.smt |
sat |
302.2 |
yes |
| sc/sc-38.induction.cvc.smt |
sat |
214.9 |
yes |
| sc/sc-38.induction3.cvc.smt |
sat |
349.4 |
yes |
| sc/sc-39.base.cvc.smt |
timeout |
1207.5 |
yes |
| sc/sc-40.base.cvc.smt |
timeout |
1208.0 |
yes |
| sc/sc-40.induction.cvc.smt |
sat |
823.1 |
yes |
| sc/sc-40.induction3.cvc.smt |
sat |
822.9 |
yes |
| sc/sc-6.induction3.cvc.smt |
sat |
0.6 |
yes |
| spider_benchmarks/bad_echos_ascend.induction.smt |
unsat |
0.1 |
yes |
| spider_benchmarks/fs_not_sc_seen.base.smt |
unsat |
0.1 |
yes |
| spider_benchmarks/synched.induction.smt |
unsat |
0.3 |
yes |
| tta_startup/simple_startup_10nodes.abstract.induct.smt |
timeout |
1208.1 |
yes |
| tta_startup/simple_startup_11nodes.bug.induct.smt |
timeout |
1207.8 |
yes |
| tta_startup/simple_startup_12nodes.abstract.induct.smt |
timeout |
1207.9 |
yes |
| tta_startup/simple_startup_12nodes.bug.induct.smt |
timeout |
1207.7 |
yes |
| tta_startup/simple_startup_14nodes.abstract.induct.smt |
timeout |
1207.6 |
yes |
| tta_startup/simple_startup_14nodes.bug.induct.smt |
timeout |
1193.8 |
yes |
| tta_startup/simple_startup_14nodes.synchro.base.smt |
unsat |
0.6 |
yes |
| tta_startup/simple_startup_15nodes.bug.induct.smt |
timeout |
1207.9 |
yes |
| tta_startup/simple_startup_4nodes.bug.induct.smt |
sat |
6.5 |
yes |
| tta_startup/simple_startup_5nodes.abstract.base.smt |
unsat |
0.1 |
yes |
| tta_startup/simple_startup_5nodes.bug.induct.smt |
sat |
13.3 |
yes |
| tta_startup/simple_startup_7nodes.bug.induct.smt |
sat |
208.0 |
yes |
| tta_startup/simple_startup_7nodes.missing.induct.smt |
sat |
54.8 |
yes |
| tta_startup/simple_startup_8nodes.bug.induct.smt |
sat |
188.7 |
yes |
| tta_startup/simple_startup_9nodes.bug.induct.smt |
sat |
600.3 |
yes |
| uart/uart-14.base.cvc.smt |
unsat |
25.5 |
yes |
| uart/uart-14.induction.cvc.smt |
sat |
17.5 |
yes |
| uart/uart-16.induction.cvc.smt |
sat |
24.5 |
yes |
| uart/uart-18.base.cvc.smt |
unsat |
69.9 |
yes |
| uart/uart-27.base.cvc.smt |
unsat |
422.1 |
yes |
| uart/uart-28.base.cvc.smt |
unsat |
470.0 |
yes |
| uart/uart-29.induction.cvc.smt |
sat |
144.6 |
yes |
| uart/uart-33.base.cvc.smt |
unsat |
1185.1 |
yes |
| uart/uart-34.base.cvc.smt |
timeout |
1208.0 |
yes |
| uart/uart-37.base.cvc.smt |
timeout |
1207.8 |
yes |
| uart/uart-39.base.cvc.smt |
timeout |
1208.0 |
yes |
| uart/uart-8.induction.cvc.smt |
sat |
4.1 |
yes |