datalog-aa An implementation of the Andersen's algorithm using horn logic and z3. Tested on LLVM 8.0.1 and Z3 4.8.3 Testing cmake . make make test