Encode FStar strings as native Z3 strings
Open
component/libraries
kind/enhancement
- Dominant language
- F*
- Stars
- 3.1k
- Forks
- 266
- Avg merge
- 21h 1m
- Merged PRs (30d)
- 54
Description
The current master of Z3 has a primitive String sort, and Z3 may add support for reasoning about string operations in the future. See, for instance, the Z3 plug-in at https://github.com/z3str/Z3-str.
Contributor guide
Assessment
This issue has not been assessed yet.