A Concurrency Problem with Exponential DPLL(T) Proofs

Liana Hadarean, Alex Horn, Tim King

Many satisfiability modulo theories solvers implement a variant of the DPLL(T ) framework which separates theory-specific reasoning from reasoning on the propositional abstraction…