leonbett

[FEATURE] Discussion: Compatibility with "theory of fixed size bit-vectors"

1

In order to model constraints imposed by general purpose programs, the operations used in the program have to be translated to an ISLa constraint. Currently, ISLa supports some arithmetic operations...

[BUG] Solving arithmetic constraints takes very long

6

**Describe the bug** ISLa takes a long time (~3-5 minutes) to solve a formula with many arithmetic constraints. **To Reproduce** 0. Two fixes probably need to be applied to ISLa...

[BUG] Correct result with infix AND, incorrect result with s-expr AND

1

**Describe the bug** Sometimes ISLa only produces a correct result for infix AND, but not for S-expr AND. It seems like the S-expr AND constraint is completely ignored. **To Reproduce**...

**Is your feature request related to a problem? Please describe.** [timeout_ms](https://github.com/rindPHI/isla/blob/main/src/isla/z3_helpers.py#L556) is set to 500 ms by default, and cannot be configured by a user, if I understand correctly. **Describe...

[FEATURE] Language syntax wishlist

1

- Unary minus would be cool. Currently, instead of writing `-48`, I use `(0 - 48)`. - For Infix-notation, could we have `%` and `/` operators instead of `mod` and...