Even more extended version of the InputAbsy simplifier that also rewrites certain array expression.
Class to simplify bit-vector expressions using information about the range of operands.
Extended version of the InputAbsy simplifier that also rewrites certain array expressions: \exists int a; x = store(a, b, c) is replaced with select(x, b) = c
Class representing the different kinds of partial interpolants that are used to annotate arithmetic literals.
Abstract class providing some functionality commonly needed for interpolation-based software verification, e.g., axioms and prover for bitvector arithmetic, arrays, etc.
Class to store information about the value range of constants; this information is later used to simplify expressions
Module for simplifying a proof (certificate) by eliminating as many rounding steps as possible; this is currently done in a rather naive way