summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv
AgeCommit message (Expand)Author
2013-04-26Merge experimental decisionweight branchKshitij Bansal
2013-03-23non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)lianah
2013-03-21added regression test for constant evallianah
2013-03-20added more testslianah
2013-03-20generalized bv inequality reasoning to handle both strict and non-strict ineq...lianah
2013-03-20one more ineq regressionLiana Hadarean
2013-03-19fixed reversed concat in core theoryLiana Hadarean
2013-03-19inequality reasoning works on small examples added to regressions (not increm...Liana Hadarean
2013-03-16started work on the inequality bv subtheorylianah
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2012-11-13Testcases for fixed bugsClark Barrett
2012-10-10fixing the cvc bv parser and typecheckerDejan Jovanović
2012-10-08added reduced bv model failing test caseLiana Hadarean
2012-08-28fix regression tests for automake 1.11 and automake 1.12---both versions shou...Morgan Deters
2012-06-28Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2Clark Barrett
2012-06-14fix for clark's bugDejan Jovanović
2012-06-13enabling regressions from last night, all fixedDejan Jovanović
2012-06-13!(*child_it).isConst() assertion failDejan Jovanović
2012-06-13r2.node == response.node failure Dejan Jovanović
2012-06-13!current[0].isConst() failureDejan Jovanović
2012-06-13benchmark to show that we don't rewrite bvsmod correctlyDejan Jovanović
2012-06-12wrong answer for bvDejan Jovanović
2012-06-12bv reduced with decision: sat instead of unsatKshitij Bansal
2012-06-12wrong answer benchmarksDejan Jovanović
2012-06-11another benchmark that used to fail Dejan Jovanović
2012-06-11fixing bitvector bugsDejan Jovanović
2012-06-11failing bv examplesDejan Jovanović
2012-06-08very small fast example for the bv failDejan Jovanović
2012-06-08small fuzz examples where bv fails Dejan Jovanović
2012-06-06Changes to the combination mechanism, lots of details. Not done yet, there ar...Dejan Jovanović
2012-05-08Merging in bvprop branch, with proper bit-vector propagation. Liana Hadarean
2012-04-05Support to test the "dumper" mechanism in regressions (feeding dump output ba...Morgan Deters
2012-04-04 * added propagation as lemmas to TheoryBV:Liana Hadarean
2012-02-20portfolio mergeMorgan Deters
2011-10-29support for proof regressions in other parts of the test treeMorgan Deters
2011-05-02adding some previously-failing "bug" test cases for bitvectorsMorgan Deters
2011-05-02updating bv regressionsDejan Jovanović
2011-04-20Minor mixed-bag commit. Expected performance impact negligible.Morgan Deters
2011-04-20Tuesday end-of-day commit.Morgan Deters
2011-04-18more work on CVC languageMorgan Deters
2011-04-11fix "make dist" issues in makefilesMorgan Deters
2011-03-26fix for bug 253, was propagating an asserted literalDejan Jovanović
2011-03-26fix typoMorgan Deters
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
2011-03-21more bugfixes, some basic propagation, and testcases to cover themDejan Jovanović
2011-03-21fixing a bug in the BV rewrite, off by one error when merging constantsDejan Jovanović
2011-03-20more bugfixes for bitvectorsDejan Jovanović
2011-03-20missed one caseDejan Jovanović
2011-03-20commit for the version of bitvectors that passes all the unit testsDejan Jovanović
2011-02-17some unit tests to work on slicingDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback