Open Bo-Yuan-Huang opened 2 years ago
Describe your feature request. Generate SMT formulas that use LIA or LRA for better support for CHC and other synthesis tasks.
Describe the solution you'd like An option (additional to the existing BV-based translation) to select the data type.
Additional context
Describe your feature request. Generate SMT formulas that use LIA or LRA for better support for CHC and other synthesis tasks.
Describe the solution you'd like An option (additional to the existing BV-based translation) to select the data type.
Additional context