Closed Bo-Yuan-Huang closed 3 years ago
Describe your feature request. Support ILA unroller with SmtShim.
Describe the solution you'd like New (or rewritten) ILA unroller that generates templated SMT formula instead of hard fixed z3::expr.
Additional context May have limited functionality such as substitution or smaller operation set.
Describe your feature request. Support ILA unroller with SmtShim.
Describe the solution you'd like New (or rewritten) ILA unroller that generates templated SMT formula instead of hard fixed z3::expr.
Additional context May have limited functionality such as substitution or smaller operation set.