How do I convert a series of mathematical constraints into a SAT or a SMT problem and get an answer?

I have an arbitrary set of constraints. For example:

A, B, C and D are 8-bit integers.

A + B + C + D = 50
(A + B) = 25
(C + D) = 30
A < 10

I can convert this to a SAT problem that can be solved by picosat (I can't get minisat to compile on my Mac), or to a SMT problem that can be solved by CVC4. To do that I need to:

1. Map these equations into a Boolean circuit.
2. Apply Tseitin's transformation to the circuit and convert it into DIMACS format.

My questions:

1. What tools do I use to do the conversion to the circuit?
2. What are the file formats for circuits and which ones are commonly used?
3. What tools do I use to transform the circuit to DIMACS format?

In MiniZinc, you could just write a constraint programming model:

set of int: I8 = 0..255;

var I8: A;
var I8: B;
var I8: C;
var I8: D;

constraint A + B + C + D == 50;

constraint (A + B) = 25;

constraint (C + D) = 30;

constraint A < 10;

solve satisfy;

The example constraints cannot be satisfied, because of 25 + 30 > 50.

The Python interface of Z3 would allow the following:

from z3 import *
A, B, C, D = Ints('A B C D')
s = Solver()
s.add(A >= 0, A < 256)
s.add(B >= 0, B < 256)
s.add(C >= 0, C < 256)
s.add(A+B+C+D == 50)
s.add((A+B) == 25)
s.add((C+D) == 30)
s.add(A < 10)
print(s.check())
print(s.model())