Age | Commit message (Collapse) | Author | |
---|---|---|---|
2016-11-16 | exampleunsat_core_example | Andres Notzli | |
2016-11-08 | Minor fixes related to ExtTheory + incremental, fixes bug760. | ajreynol | |
2016-11-08 | Add a few options to separation logic and sets. Minor changes to separation ↵ | ajreynol | |
logic, change syntax for empty heap constraint. | |||
2016-11-07 | Merge pull request #104 from timothy-king/disabling-out-of-memory-tests-on-asan | Tim King | |
Disabling out of memory tests unit tests when ASAN is enabled. ASAN f… | |||
2016-11-07 | Disabling out of memory tests unit tests when ASAN is enabled. ASAN failures ↵ | Tim King | |
are too hard for the unit testing framework. | |||
2016-11-07 | Changing ArrayStoreAll's constructor to delay allocation until it is done ↵ | Tim King | |
checking error conditions. This prevents a memory leak in exception throwing branches. | |||
2016-11-07 | Fixing a memory leak in the CnfStream unit tests. | Tim King | |
2016-11-07 | Fixing a memory leak in the eager bitblaster. | Tim King | |
2016-11-06 | Merge pull request #102 from timothy-king/node-id-eq | Tim King | |
This switches the ZombieSet in the NodeManager to use NodeValue's id … | |||
2016-11-06 | This switches the ZombieSet in the NodeManager to use NodeValue's id for ↵ | Tim King | |
equality comparison. The previously used function NodeValueEq incorrectly identified VARIABLE nodes as being equal. This meant that on hash collisions these nodes could leak memory. | |||
2016-11-05 | Merge pull request #101 from 4tXJ7f/fix_leak | Clark Barrett | |
Fix three leaks in unit tests | |||
2016-11-04 | Fix three leaks in unit tests | Andres Notzli | |
The `testMultipleCollection` test case was allocating a ListenerCollection without deleting it. The helper function `countCommands` was not deleting the `Command`s returned from `InteractiveShell::readCommand`. In the `testEmptyFileInput` and `testSimpleFileInput` tests, the `filename` string was not deleted. This commit fixes all issues. | |||
2016-11-04 | Fix memory leak in node_black unit test. | Clark Barrett | |
2016-11-04 | Fix a few more minor memory leaks. | ajreynol | |
2016-11-03 | Make data points accurate in sep logic models. | ajreynol | |
2016-11-03 | Add priorities to getNextDecision. Properly handle case for finite types + ↵ | ajreynol | |
unbounded heaps in sep logic. Fix another simple memory leak in sygus. | |||
2016-11-03 | Merge pull request #100 from 4tXJ7f/fix_context_mm_black | Tim King | |
Fix back() of empty deque in context_mm_black test | |||
2016-11-02 | Fix back() of empty deque in context_mm_black test | Andres Notzli | |
The `testPushPop()` test case does a pop out of scope at the end that lead to UB in `ContextManager::pop()` because it did a `deque::back()` on an empty deque without checking. This commit adds an assertion in the `ContextManager` and checks that the test case triggers the assertion. | |||
2016-11-02 | Add missing regression. | ajreynol | |
2016-11-02 | Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ↵ | ajreynol | |
Fix a few more memory leaks. | |||
2016-11-02 | Fix a few obvious memory leaks in sygus and quantifiers. Minor fix cvc3_compat. | ajreynol | |
2016-11-01 | Minor fix to cvc3_compat. | ajreynol | |
2016-11-01 | Make tuple and record names unique. Do not print internal datatype ↵ | ajreynol | |
declaration in cvc printer. | |||
2016-11-01 | Fix memory leak in TheorySetsRels. Minor cleanup. | ajreynol | |
2016-11-01 | Revert change to Datatypes API to return vector of DatatypeTypes, as before. ↵ | ajreynol | |
ASAN failures with datatypes should now be mostly fixed. | |||
2016-11-01 | Revert change to datatypes API for passing pointers, instead make deep copy ↵ | ajreynol | |
during call to mkMutualDatatypes. | |||
2016-11-01 | Working memory leak free version, changes interface to pointers. | ajreynol | |
2016-10-31 | Minor refactoring in preparation for datatypes node cycle breaking. | ajreynol | |
2016-10-28 | Add get instantiations utilities to API. | ajreynol | |
2016-10-27 | Merge pull request #99 from 4tXJ7f/fix_dist_build3 | Clark Barrett | |
Fix typo in Makefile that makes distcheck fail | |||
2016-10-26 | Fix typo in Makefile that makes distcheck fail | Andres Notzli | |
2016-10-26 | Enable bv2nat regressions | ajreynol | |
2016-10-26 | Merge pull request #98 from 4tXJ7f/fix_dist_build | Andrew Reynolds | |
Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build | |||
2016-10-26 | New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵ | ajreynol | |
as extension of sets solver, add regressions. | |||
2016-10-23 | Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build | Andres Notzli | |
This commit adds regress4 to the `test/regress/Makefile.am`. | |||
2016-10-21 | Fix/add missing makefiles. | ajreynol | |
2016-10-21 | Move slow regress0 benchmarks to regress1, increment regress1 through regress3. | ajreynol | |
2016-10-19 | Merge pull request #97 from 4tXJ7f/fix_rewrite | Tim King | |
Fix minor bug and typo in boolean rewriter | |||
2016-10-19 | Fix minor bug and typo in boolean rewriterfix_rewrite | Andres Notzli | |
One of the rewrites in the boolean rewriter had the condition `n[0] == tt && n[0] == ff`, which could never be true. Another rewrite covers the same case but returns a `REWRITE_AGAIN` instead of a `REWRITE_DONE`. This commit also fixes a minor typo. | |||
2016-10-13 | Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory. | ajreynol | |
2016-10-13 | Initializes RoundingMode::roundNearestTiesToAway to a distinct value. | Tim King | |
2016-10-13 | Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git" | Tim King | |
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing changes made to 5f415d4585134612bc24e9a823289fee35541a01. | |||
2016-10-11 | Merge branch 'origin' of https://github.com/CVC4/CVC4.git | Paul Meng | |
Conflicts: src/options/quantifiers_options | |||
2016-10-11 | - fixed a memory leak issue with context dependent data structure | Paul Meng | |
- clean up | |||
2016-10-08 | Adding initializers for structs internal to ite_utilities. | Tim King | |
2016-10-05 | Added an option that allow empty dependencies when attempting to minimize ↵ | guykatzz | |
preprocessing holes | |||
2016-10-02 | Removing the throw specifiers from theory_uf_type_rules.h. | Tim King | |
2016-10-02 | Removing the throw specifiers from theory_fp_type_rules.h. | Tim King | |
2016-10-02 | Removing the throw specifiers from theory_datatypes_type_rules.h. | Tim King | |
2016-10-02 | Removing an unused member from TreeLog. | Tim King | |