cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2020-08-19	Require `--strings-exp` when using `str.substr` (#4916)	Andres Noetzli
	Fixes #4915. Previously, `str.substr` did not require `--strings-exp`. However, when `--strings-exp` is not active, we do not send terms to the extended solver for registration, which meant that `str.substr` was never reduced. This commit adds `str.substr` to the operators that require `--strings-exp`.
2020-07-28	Supporting seq.nth (#4723)	yoni206
	This PR adds support for seq.nth operator by eliminating it during expandDefinitions, based on sub-sequences. Tests that use this operator are also included.