| Benchmark |
Time |
| |
ABsolver |
CVC Lite |
MathSAT |
| FISCHER1-1-fair AB SMT |
0m0.556s
|
0m0.020s
|
0m0.045s
|
| FISCHER2-1-fair AB SMT |
0m0.907s
|
0m0.023s
|
0m0.095s
|
| FISCHER3-1-fair AB SMT |
0m2.243s
|
0m0.027s
|
0m0.177s
|
| FISCHER4-1-fair AB SMT |
0m3.003s
|
0m0.031s
|
0m0.281s
|
| FISCHER5-1-fair AB SMT |
0m2.789s
|
0m0.036s
|
0m0.422s
|
| FISCHER6-1-fair AB SMT |
0m5.770s
|
0m0.040s
|
0m0.604s
|
| FISCHER7-1-fair AB SMT |
0m10.597s
|
0m0.043s
|
0m0.791s
|
| FISCHER8-1-fair AB SMT |
0m14.521s
|
0m0.052s
|
0m1.031s
|
| FISCHER9-1-fair AB SMT |
0m18.748s
|
0m0.057s
|
0m1.343s
|
| FISCHER10-1-fair AB SMT |
0m22.925s
|
0m0.067s
|
0m2.913s
|
| FISCHER11-1-fair AB SMT |
0m28.179s
|
0m0.073s
|
0m2.129s
|
| sudoku_zeit_2006_05_23_hard AB SMT |
0m0.283s
|
--
|
84m7.385s
|
| sudoku_zeit_2006_05_24_hard AB SMT |
0m0.283s
|
--
|
99m48.447s
|
| sudoku_zeit_2006_05_25_hard AB SMT |
0m0.282s
|
--
|
107m0.860s
|
| sudoku_zeit_2006_05_26_hard AB SMT |
0m0.289s
|
--
|
112m30.929s
|
| sudoku_zeit_2006_05_27_hard AB SMT |
0m0.289s
|
--
|
89m48.470s
|
| sudoku_zeit_2006_05_28_hard AB SMT |
0m0.282s
|
--
|
117m29.500s
|
| sudoku_zeit_2006_05_29_easy AB SMT |
0m0.279s
|
--
|
81m27.008s
|
| sudoku_zeit_2006_05_29_hard AB SMT |
0m0.283s
|
--
|
137m31.245s
|
| sudoku_zeit_2006_05_30_easy AB SMT |
0m0.287s
|
--
|
75m17.435s
|
| sudoku_zeit_2006_05_30_hard AB SMT |
0m0.283s
|
--
|
94m35.672s
|
| nonlinear_unsat AB |
0m0.260s
|
--
|
--
|
| div_operator AB |
0m0.233s
|
--
|
--
|
| esat_n11_m8_nonlinear AB |
0m0.469s
|
--
|
--
|