Open AnzhelaSukhanova opened 1 year ago
PR implements the quantifier elimination for BV formulas of a certain structure according to the paper. Supported structure: a conjunction of inequalities/equalities between a bound variable in a linear term and a term without that variable.
PR implements the quantifier elimination for BV formulas of a certain structure according to the paper. Supported structure: a conjunction of inequalities/equalities between a bound variable in a linear term and a term without that variable.