We present Dryad_dec, a decidable logic that allows reasoning about tree data-structures with measurements. This logic supports user-defined recursive measure functions based on height or size, and measure-related recursive predicates such as AVL trees or red-black trees. We prove the logic’s satisfiability is decidable. The crux of the decidability proof is a small model property which allows us to reduce the satisfiability of Dryad_dec to quantifier-free linear arithmetic theory which can be solved efficiently using SMT solvers. We also show that Dryad_dec can encode natural proof verification conditions for functional correctness of recursive tree-manipulating programs, as well as synthesis conditions for conditional linear-integer arithmetic functions. We developed the decision procedure and successfully solved 100+ Dryad_dec formulas raised from various scenarios, including verifying full correctness of programs manipulating AVL trees, red-black trees and treaps, checking size lower bounds for AVL trees and red black trees, and synthesizing candidate solutions from a specification and a set of counterexamples. To our knowledge, this is the first decidable logic that can express these measure-related properties for trees.