summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
2016-12-16Fix dependency tracing for fewerPreprocessingHolesAndres Notzli
Previously, dependency tracing in `ite_removal.cpp` was only done with the `unsatCores` option but `fewerPreprocessingHoles` requires dependencies, too. This lead to errors during proof construction when `fewerPreprocessingHoles` was active. This commit fixes the condition and includes a test case that previously failed. Additionally, it fixes a similar issue in the theory engine. NOTE: this commit might not fix all instances of this problem. `smt_engine.cpp` turns certain flags off with `unsatCores`. Compatibility between those flags and `fewerPreprocessingHoles` needs to be checked separately.
2016-12-12Fix split-find-unsat-w-emp testAndres Notzli
Commit 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa did not update the split-find-unsat-w-emp test, this commit fixes that.
2016-12-08Fix (inactive) `MultSlice` rewriteAndres Notzli
The `MultSlice` rewrite was previously accepting multiplications of three and more variables even though it was designed for multiplications of two variables only. Fortunately, the rewrite was not actively used in the bitvector solver. This commit strengthens the condition in `applies()` and adds a unit test that checks that x * y * z and x * y do not get rewritten to the same term.
2016-12-08Enable remaining cardinality benchmarksajreynol
2016-12-07Add missing regressionajreynol
2016-12-07Add sets regression, fixes bug 754. Minor fix to regexp in strings.ajreynol
2016-12-07Added cardinality to cvc language, fixes bug 753. Throw logic exception when ↵ajreynol
using cardinality on sets with finite element type.
2016-12-07Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.ajreynol
2016-12-07Refactoring, generalization of bounded inference module. Simplification of ↵ajreynol
rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
2016-12-07Fix nf exp tracking for non-linear string equalities, fixes bug 768.ajreynol
2016-12-02Fix for bug 734Clark Barrett
2016-12-02Merge pull request #113 from 4tXJ7f/remove_extract_ruleClark Barrett
Remove wrong `ExtractMultLeadingBit` rule
2016-12-02Bug fixes and refactoring of parametric datatypes, add some regressions.ajreynol
2016-12-02Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and ↵ajreynol
--fmf-fun-rlv, fixes bug 723.
2016-12-01Fix quantifiers dynamic splitting module for incremental mode, fixes bug 765 ↵ajreynol
and 763.
2016-12-01Improvement and bug fix for str.indexof reduction, add regression. Other ↵ajreynol
minor changes.
2016-11-30Remove wrong `ExtractMultLeadingBit` ruleAndres Notzli
The rule `ExtractMultLeadingBit` estimated the number of leading zeros wrong: when there were ones in the leading constant parts of the factors, it was using the length of the non-zero part instead of the length of the zero part. This commit includes an example for which the previous version of the rule would cause a wrong answer.
2016-11-30Merge pull request #115 from 4tXJ7f/bug766Clark Barrett
Fix parsing of BVROTR by CVC parser
2016-11-30Fix parsing of BVROTR by CVC parserAndres Notzli
This commit fixes Bugzilla bug 766 as proposed by jacobly.alt@gmail.com.
2016-11-30Add unit test for `MultDistrib` ruleAndres Notzli
This unit test checks that the issue fixed by commit c0c424283c12cfce2874ea92188487d91acecdf3 has been resolved.
2016-11-21Remove unused, libstdc++-exclusive includeAndres Notzli
The file `ext/stdio_filebuf.h` does not seem to be available in libc++, which made compilation of the unit tests for macOS unnecessarily complicated given that it is not used anyway.
2016-11-18Fix for unit test after changing default "all supported" logic name.Clark Barrett
2016-11-18Merge pull request #110 from 4tXJ7f/fix_makefilesClark Barrett
Fix Makefiles in test
2016-11-18Modified a couple of regressoins to use ALL/QF_ALL instead of ↵Clark Barrett
ALL_SUPPORTED/QF_ALL_SUPPORTED
2016-11-17Fix Makefiles in testAndres Notzli
With the recent changes to the regress tests, some of the Makefiles were not in sync anymore. This commit fixes that.
2016-11-13Switching a large allocation to be heap allocated.Tim King
2016-11-13Deleting a parsed Command in the interactive_shell_black test.Tim King
2016-11-12Merge pull request #106 from timothy-king/cvc-parser-exception-leaksClark Barrett
Adding garbage collection for the CVC Parser for Commands when except…
2016-11-12Fixed a bug in cdhashmap in which doubly-linked list was not properly ↵Clark Barrett
cleaned up on a call to obliterate. Also, removed some experimental code and a unit test from cdmap_black that used it. This test created a CDList *in* context memory which seems like a very bad idea (and it was improperly implemented resulting in a memory leak).
2016-11-11Adding garbage collection for the CVC Parser for Commands when exceptions ↵Tim King
are thrown.
2016-11-11Merge pull request #105 from timothy-king/delete-maxed-outTim King
Adding garbage collection of nodes with maxed out reference counts.
2016-11-11Deleting successfully parsed commands in the parser_black unit test.Tim King
2016-11-11Add simple inferences for extended bitvector functions, add a few related ↵ajreynol
options. Use bv2nat, int2bv as triggers. Add regressions.
2016-11-10Fixing a delete vs free mismatch in parser_builder_black.h.Tim King
2016-11-10Adding garbage collection of nodes with maxed out reference counts.Tim King
2016-11-08Add a few options to separation logic and sets. Minor changes to separation ↵ajreynol
logic, change syntax for empty heap constraint.
2016-11-07Disabling out of memory tests unit tests when ASAN is enabled. ASAN failures ↵Tim King
are too hard for the unit testing framework.
2016-11-07Changing 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-07Fixing a memory leak in the CnfStream unit tests.Tim King
2016-11-04Fix three leaks in unit testsAndres 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-04Fix memory leak in node_black unit test.Clark Barrett
2016-11-03Add priorities to getNextDecision. Properly handle case for finite types + ↵ajreynol
unbounded heaps in sep logic. Fix another simple memory leak in sygus.
2016-11-02Fix back() of empty deque in context_mm_black testAndres 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-02Add missing regression.ajreynol
2016-11-02Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ↵ajreynol
Fix a few more memory leaks.
2016-10-26Enable bv2nat regressionsajreynol
2016-10-26Merge pull request #98 from 4tXJ7f/fix_dist_buildAndrew Reynolds
Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build
2016-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵ajreynol
as extension of sets solver, add regressions.
2016-10-23Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK buildAndres Notzli
This commit adds regress4 to the `test/regress/Makefile.am`.
2016-10-21Fix/add missing makefiles.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback