summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Expand)Author
2011-07-11remove some array regressions from "make check" so nightly regressions runMorgan Deters
2011-07-11status of examplesMorgan Deters
2011-07-11new array bugs ?Morgan Deters
2011-07-11mark the new minimized benchmark as unsatMorgan Deters
2011-07-11if running in QF_AX, equalities over terms of uninterpreted sort go to arrays...Morgan Deters
2011-07-11minimized exampleMorgan Deters
2011-07-11array benchmarksMorgan Deters
2011-07-11merge from symmetry branchMorgan Deters
2011-07-09minor fixupsMorgan Deters
2011-07-09surprize surprizeDejan Jovanović
2011-07-05missing test caseDejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-06-30only use theory registration if (1) a theory requests it, or (2) if there's m...Morgan Deters
2011-05-31This commit contains the code for allowing arbitrary equalities in the theory...Tim King
2011-05-23fixes for "make dist" and "make doc", minor cleanupsMorgan Deters
2011-05-23Merge from arrays2 branch.Morgan Deters
2011-05-13* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolioMorgan Deters
2011-05-06added 10 benchmarks to regress/regress0/datatypes from paperAndrew Reynolds
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
2011-05-02adding some previously-failing "bug" test cases for bitvectorsMorgan Deters
2011-05-02updating bv regressionsDejan Jovanović
2011-04-23fix for parser/tests for ANTLR 3.2 (it was working fine on 3.3)Morgan Deters
2011-04-23* reviewed BooleanSimplification, added documentation & unit testMorgan Deters
2011-04-23make run_regression script robust to DOS newlines :(Morgan Deters
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-18mostly CVC presentation language parsing and printingMorgan Deters
2011-04-18Partial merge from datatypes-merge branch:Morgan Deters
2011-04-11fix "make dist" issues in makefilesMorgan Deters
2011-03-30improve recent low-coverage complaintsMorgan Deters
2011-03-30Add Valuation::getSatValue() so that theories can access the currentMorgan 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-03-15small fixes for run_regression script to workaround bug in old mktemp, was ca...Morgan Deters
2011-03-15Merge from cudd branch. This mostly just adds support for linkingMorgan Deters
2011-03-14change to the run_regression script to better manage temporary files; hopeful...Morgan Deters
2011-03-10ITE removal in TheoryEngine was not properly handling PARAMETERIZED kinds. F...Morgan Deters
2011-03-05adding three features to CVC parser that drastically improve its support for ...Morgan Deters
2011-02-17some unit tests to work on slicingDejan Jovanović
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-12-14fix to static learning application in UF, resolves bug# 239Morgan Deters
2010-11-19Merge from ufprop branch, including:Morgan Deters
2010-11-16SmtEngine now fails with a ModalException if --incremental is not enabledMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback