Expects mata v1.6.9
What's Changed
- New length-based decision procedure for handling special equations with lengths (enabled by default, can be turned off with
str.try_length_proc=false
) - New decision procedure for handling not-contains and disequations based on counting automata (disabled by default, can be enabled with
str.ca_constr=true
) - Z3-Noodler can now produce models
- Minor bug fixes in axiomatizations for
replace_re
,prefix
,suffix
, and string-integer conversions
Full Changelog: v1.2.0...v1.3.0