| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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({ ... });
|
|
|
|
|
|
|
|
|
|
|
|
Since we are using C++11, we can replace the triple and quad classes
with std::tuple.
|
|
|
|
|
|
|
|
|
|
* Proposal for adding map utility functions to CVC4.
|
|
|
|
|
|
|
|
Removes some hacks due to Swig 2's incomplete C++11 support and adds
checks for version 3 at configuration time as well as in swig.h
|
|
|
