| Benchmark | Answer | Time | Correct? |
|---|
| array_benchmarks/misc/pipeline-invalid.smt |
sat |
0.0 |
yes |
| array_benchmarks/misc/queue-th1-6.smt |
unsat |
0.0 |
yes |
| array_benchmarks/misc/stack-invalid-6.smt |
sat |
0.0 |
yes |
| array_benchmarks/pointer/pointer-invalid-10.smt |
sat |
0.2 |
yes |
| array_benchmarks/pointer/pointer-invalid-20.smt |
sat |
1.4 |
yes |
| array_benchmarks/pointer/pointer-invalid-5.smt |
sat |
0.0 |
yes |
| array_benchmarks/pointer/pointer-safe-10.smt |
unsat |
0.1 |
yes |
| array_benchmarks/pointer/pointer-safe-5.smt |
unsat |
0.0 |
yes |
| array_benchmarks/qlock/qlock-bug-10.smt |
sat |
0.2 |
yes |
| array_benchmarks/qlock/qlock-bug-15.smt |
sat |
0.4 |
yes |
| array_benchmarks/qlock/qlock-bug-20.smt |
sat |
3.2 |
yes |
| array_benchmarks/qlock/qlock-bug-5.smt |
sat |
0.1 |
yes |
| array_benchmarks/qlock/qlock-bug2-15.smt |
sat |
0.8 |
yes |
| array_benchmarks/qlock/qlock-bug2-20.smt |
sat |
1.6 |
yes |
| array_benchmarks/qlock/qlock-mutex-10.smt |
unsat |
4.6 |
yes |
| array_benchmarks/qlock/qlock-mutex-15.smt |
timeout |
1208.2 |
yes |
| array_benchmarks/qlock/qlock-mutex-20.smt |
timeout |
1209.2 |
yes |
| check/array_incompleteness1.smt |
unsat |
0.0 |
yes |
| check/bignum_lia1.smt |
unsat |
0.0 |
yes |
| check/bignum_lia2.smt |
sat |
0.0 |
yes |
| check/int_incompleteness1.smt |
unsat |
0.0 |
yes |
| check/int_incompleteness2.smt |
sat |
0.0 |
no (incomplete)
|
| check/int_incompleteness3.smt |
unsat |
0.0 |
yes |
| cvc/add4.smt |
unsat |
0.0 |
yes |
| cvc/add5.smt |
unsat |
0.0 |
yes |
| cvc/add6.smt |
unsat |
0.0 |
yes |
| cvc/dlx-dmem.smt |
unsat |
0.0 |
yes |
| cvc/dlx-pc.smt |
unsat |
0.0 |
yes |
| cvc/fb_var_12_11.smt |
unsat |
0.0 |
yes |
| cvc/fb_var_27_8.smt |
sat |
0.0 |
yes |
| cvc/fb_var_33_6.smt |
unsat |
0.0 |
yes |
| cvc/fb_var_5_12.smt |
unsat |
0.0 |
yes |
| cvc/fb_var_6_12.smt |
unsat |
0.0 |
yes |
| cvc/pp-bloaddata-a.smt |
unsat |
0.0 |
yes |
| cvc/pp-dmem-a.smt |
unsat |
0.0 |
yes |
| cvc/pp-dmem2.smt |
unsat |
0.0 |
yes |
| cvc/pp-pc-s2i.smt |
unsat |
0.0 |
yes |
| cvc/pp-regfile.smt |
timeout |
1207.2 |
yes |
| cvc/read6.smt |
unsat |
0.0 |
yes |
| ios/ios_t1_ios_np_sf_ai_00009_001.cvc.smt |
unsat |
0.0 |
yes |
| piVC/piVC_13f61c.smt |
unsat |
0.0 |
yes |
| piVC/piVC_39224f.smt |
unsat |
0.1 |
yes |
| piVC/piVC_408ff0.smt |
unsat |
0.0 |
yes |
| piVC/piVC_46582a.smt |
unsat |
0.1 |
yes |
| piVC/piVC_5b181b.smt |
unsat |
0.0 |
yes |
| piVC/piVC_7fd2c4.smt |
unsat |
0.0 |
yes |
| piVC/piVC_8caf76.smt |
unsat |
0.1 |
yes |
| piVC/piVC_cb19c7.smt |
unsat |
0.0 |
yes |
| piVC/piVC_d421cb.smt |
unsat |
0.0 |
yes |
| piVC/piVC_f5059f.smt |
unsat |
0.1 |
yes |
| piVC/piVC_ffa5fa.smt |
unsat |
0.0 |
yes |
| qlock2/qlock.base.10.smt |
unsat |
4.0 |
yes |
| qlock2/qlock.base.11.smt |
unsat |
12.7 |
yes |
| qlock2/qlock.base.12.smt |
unsat |
53.7 |
yes |
| qlock2/qlock.base.13.smt |
unsat |
137.3 |
yes |
| qlock2/qlock.base.14.smt |
unsat |
339.3 |
yes |
| qlock2/qlock.base.15.smt |
sat |
1.3 |
yes |
| qlock2/qlock.base.16.smt |
sat |
0.9 |
yes |
| qlock2/qlock.base.17.smt |
sat |
1.3 |
yes |
| qlock2/qlock.base.18.smt |
sat |
2.6 |
yes |
| qlock2/qlock.base.19.smt |
sat |
1.1 |
yes |
| qlock2/qlock.base.20.smt |
sat |
1.8 |
yes |
| qlock2/qlock.base.21.smt |
sat |
1.5 |
yes |
| qlock2/qlock.base.22.smt |
sat |
1.8 |
yes |
| qlock2/qlock.base.24.smt |
sat |
1.6 |
yes |
| qlock2/qlock.base.25.smt |
sat |
2.2 |
yes |
| qlock2/qlock.base.26.smt |
sat |
3.0 |
yes |
| qlock2/qlock.base.27.smt |
sat |
3.4 |
yes |
| qlock2/qlock.base.28.smt |
sat |
4.6 |
yes |
| qlock2/qlock.base.29.smt |
sat |
3.0 |
yes |
| qlock2/qlock.base.30.smt |
sat |
13.4 |
yes |
| qlock2/qlock.base.5.smt |
unsat |
0.1 |
yes |
| qlock2/qlock.base.6.smt |
unsat |
0.2 |
yes |
| qlock2/qlock.base.8.smt |
unsat |
1.2 |
yes |
| qlock2/qlock.base.9.smt |
unsat |
2.2 |
yes |
| qlock2/qlock.induction.10.smt |
sat |
0.2 |
yes |
| qlock2/qlock.induction.11.smt |
sat |
0.2 |
yes |
| qlock2/qlock.induction.12.smt |
sat |
0.2 |
yes |
| qlock2/qlock.induction.13.smt |
sat |
0.3 |
yes |
| qlock2/qlock.induction.14.smt |
sat |
0.4 |
yes |
| qlock2/qlock.induction.15.smt |
sat |
0.4 |
yes |
| qlock2/qlock.induction.16.smt |
sat |
0.5 |
yes |
| qlock2/qlock.induction.17.smt |
sat |
0.6 |
yes |
| qlock2/qlock.induction.18.smt |
sat |
0.6 |
yes |
| qlock2/qlock.induction.19.smt |
sat |
0.6 |
yes |
| qlock2/qlock.induction.20.smt |
sat |
0.8 |
yes |
| qlock2/qlock.induction.23.smt |
sat |
1.0 |
yes |
| qlock2/qlock.induction.24.smt |
sat |
1.6 |
yes |
| qlock2/qlock.induction.25.smt |
sat |
1.8 |
yes |
| qlock2/qlock.induction.26.smt |
sat |
2.0 |
yes |
| qlock2/qlock.induction.27.smt |
sat |
2.7 |
yes |
| qlock2/qlock.induction.30.smt |
sat |
3.4 |
yes |
| qlock2/qlock.induction.5.smt |
sat |
0.0 |
yes |
| qlock2/qlock.induction.6.smt |
sat |
0.1 |
yes |
| qlock2/qlock.induction.7.smt |
sat |
0.1 |
yes |
| qlock2/qlock.induction.8.smt |
sat |
0.1 |
yes |
| qlock2/qlock.induction.9.smt |
sat |
0.1 |
yes |
| storecomm/storecomm_invalid_t1_pp_sf_ai_00050_001.cvc.smt |
sat |
0.1 |
yes |
| storecomm/storecomm_invalid_t1_pp_sf_ai_00050_003.cvc.smt |
sat |
0.1 |
yes |
| storecomm/storecomm_invalid_t2_np_nf_ai_00010_009.cvc.smt |
sat |
0.0 |
yes |
| storecomm/storecomm_invalid_t2_np_sf_ai_00010_008.cvc.smt |
sat |
0.0 |
yes |
| storecomm/storecomm_invalid_t3_np_sf_ai_00060_003.cvc.smt |
sat |
0.1 |
yes |
| storecomm/storecomm_invalid_t3_pp_nf_ai_00060_004.cvc.smt |
sat |
0.1 |
yes |
| storeinv/storeinv_t2_np_nf_ai_00010_001.cvc.smt |
timeout |
1207.0 |
yes |
| storeinv/storeinv_t3_np_sf_ai_00009_001.cvc.smt |
unsat |
67.2 |
yes |
| storeinv/storeinv_t3_pp_nf_ai_00006_001.cvc.smt |
unsat |
0.1 |
yes |