Playing a bit here, turns out the A=A+AB and A+B=A+!AB reductions have no effect in 32bit add. Guess that's what makes it a nice 32bit bijection.
Download logred_v4.zip which will be faster for your application.
You can disable those reduction algorithms by commenting out logred_set_reduce_2_A_AB() and logred_set_reduce_4_A_nAB_n() inside logred_set_reduce()
Been trying this out, so many questions...
1) logred_set_scanf(a, "a00 + a00");
logred_set_reduce(a);
logred_set_printf(a);
Shouldn't that always produce 0? for me it outputs a00
2) Similarly I would expect (a + !a) = 1
logred_set_scanf(a, "a00");
logred_set_not(b, a);
logred_set_xor(c, a, b);
= crash
3) Haven't debugged enough, but part 2 could be related to this?:
logred_set_scanf(a, "!a00!b00"); = works
logred_set_scanf(a, "!a00"); = crash
4) Actually, is there support for numeric literals (0, 1)? c = a+b is purely symbolic, but during SHA256 you add in those K-Constants which can sometimes help reduce things further.
4) x64 only? This is giving me heap problems:
#define VAR_T size_t
#define VAR_T_SIZE_BITS ( 8 * sizeof(VAR_T) )
#define VAR_A_BITS 256
#define VAR_A_LEN 4L
(worked around setting VAR_A_BITS = 128... maybe this is the source of all my problems?

)