EBVI is a word-level interpolating decision procedure for bit-vector logic.

Input and Output Format: Verilog Expressions

Features:

• Interpolation for formulae in bit-vector logic
• Uses a propositional SAT solver for satisfiability
• Lifts the propositional proof to a word-level proof