Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-12-16 | Support ackermannization on uninterpreted sorts in BV (#3372) | Ying Sheng | |
Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1. |