| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
(#2234)
|
|
This should hopefully also take care of the open coverity issues for cvc4cpp.cpp.
|
|
|
|
(#2355)
There do not appear to be any instances these can be positive.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(#2321)
|
|
|
|
|
|
|
|
|
|
|
|
Currently, we can optionally specify an *.expect file with the metadata
of a regression test. This commit removes that option because it was not
widely used, adds maintenance overhead and makes the transition to a new
build system more cumbersome. Regression files can still be fed to a
solver without removing the metadata first since they are in comments of
the corresponding input format (note that this was not always the case,
it changed in efc6163629c6c5de446eccfe81777c93829995d5).
|
|
|
|
Disabled since 6 years, @mdeters commented when disabling it that it takes a very long time to build, see 868ee6d.
|
|
|
|
|
|
|
|
|
|
|
|
This is in preparation for migration to cmake since ctest determines failure via exit code.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This corrects a bug that was introduced in #2266 (the hack removed there was necessary).
This ensures that we handle operators like bvudiv, bvsdiv, bvurem, div, rem, / properly in sygus.
This also enables total semantics for BV div-by-zero for sygus.
|
|
Most of the PR is clang-format cruft from picking up the contents of a PROOF({ ... });
|
|
|
|
|
|
|
|
|
