Barcelogic for SMT is an efficient implementation of the DPLL(T) framework [Ganzingeretal2004CAV, Nieuwenhuisetal2005LPAR]. A DPLL(T) system consists of a general DPLL(X) engine, very similar in nature to a SAT solver, whose parameter X can be instantiated with a solver for a theory T. Once the DPLL(X) engine has been implemented, this approach becomes extremely flexible: new theories can be dealt with by simply plugging in new theory solvers. These solvers only must be able to deal with conjunctions of theory literals and conform to a minimal and simple interface [Ganzingeretal2004CAV]. Currently, Barcelogic for SMT supports difference logic over the integers of the reals, equality with uninterpreted function symbols (EUF) and the interpreted function symbols predecessor and successor, or combinations of these theories. The input formulas given to the system have to be in the SMT-LIB format.