# Proof Tree Preserving Interpolation

## TL;DR

This paper introduces a novel scheme for computing Craig interpolants in SMT solving that preserves proof trees and handles mixed literals without limiting inferences or transforming proof structures.

## Contribution

It presents a proof tree preserving interpolation scheme for SMT solvers that efficiently manages mixed literals without restricting inference steps.

## Key findings

- Implemented in SMTInterpol solver
- Handles uninterpreted functions and linear arithmetic
- Extensible to other theories

## Abstract

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 formulae. In this paper, we present a scheme to compute Craig interpolants in the presence of mixed literals. Contrary to existing approaches, this scheme neither limits the inferences done by the SMT solver, nor does it transform the proof tree before extracting interpolants. Our scheme works for the combination of uninterpreted functions and linear arithmetic but is extendable to other theories. The scheme is implemented in the interpolating SMT solver SMTInterpol.