Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since
re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) )
str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z )
This PR removes the above rewrite, which was implemented incorrectly and was dead code.
|
|
|
|
|
|
propagator. (#2421)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This should fix Coverity issues 1473025 and 1459599.
|
|
|
|
|
|
|
|
This should fix Coverity issue 1470214.
|
|
This is work towards #2305.
With this PR, CVC4's performance is fairly reasonable on the Kind2 BMC benchmarks with --decision=internal --ext-rew-prep --ext-rew-prep-agg.
|
|
This should also fix CIDs 1465687, 1465695, 1465696, and 1465701.
|
|
|
|
* Fix unsigned integer types in strings.
* Format
|
|
|
|
Moved `src/theory/quantifiers/macros.{cpp,h}` to `src/preprocessing/passes/quantifier_macros.{cpp,h}`,
and added the necessary methods for inheritance from PreprocessingPass.
No need to add a test - regress0 fails when adding Assert(false) when assertions had changed.
|
|
|
|
|
|
|
|
(#2234)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|