1 paper
Jürgen Christ, Jochen Hoenicke, Alexander Nutz
Craig interpolation in SMT is difficult because, e. g., theory combination and integer cuts introduce mixed literals, i. e., literals containing local symbols from both input formu…