Recent work on weighted model counting has been very successfully applied to\nthe problem of probabilistic inference in Bayesian networks. The probability\ndistribution is encoded into a Boolean normal form and compiled to a target\nlanguage, in order to represent local structure expressed among conditional\nprobabilities more efficiently. We show that further improvements are possible,\nby exploiting the knowledge that is lost during the encoding phase and\nincorporating it into a compiler inspired by Satisfiability Modulo Theories.\nConstraints among variables are used as a background theory, which allows us to\noptimize the Shannon decomposition. We propose a new language, called Weighted\nPositive Binary Decision Diagrams, that reduces the cost of probabilistic\ninference by using this decomposition variant to induce an arithmetic circuit\nof reduced size.\n