The C3, SMT solver written in C. Currently WIP project...
C3 has support for DIMACS file format as input for SAT solver.
$ ./c3 -D <DIMACS format file>
You can also solve Sudoku by following command.
$ ./test/sudoku/gen_cnf.sh
C3 has also support SMT-LIB2 file format as input for SMT solver.
$ ./c3 -S <SMT-LIB2 format file>
You can try random test. All expression are generated by random.
$ make test