summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
2013-02-07Merge branch '1.0.x'Morgan Deters
Conflicts: src/theory/quantifiers/theory_quantifiers.cpp
2013-02-07Significant work on bug #491 (not yet closed).Morgan Deters
2013-02-07More complete fix for bug 484 (includes fixes for records and tuples).Morgan Deters
2013-02-05Fix to miplib trick to make it less "cautious" and apply in more casesMorgan Deters
2013-02-04Merge branch '1.0.x'Morgan Deters
2013-02-04Fix NodeBuilder bug which could attempt to allocate beyond hard limitMorgan Deters
2013-02-04Model no longer adds subterms of quantifiers to equality engine, this fixed ↵Andrew Reynolds
bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.
2013-02-03Some cleanup of miplib regressions and optionsMorgan Deters
2013-02-03Merge from mdeters/miplib branch (commit ↵Morgan Deters
'ce7c485182902ae43871057185095f71f74a8a58')
2013-02-03new miplib pass, works for 1 or 2 varsMorgan Deters
2013-02-01Merge branch '1.0.x'Morgan Deters
2013-02-01Fix a tuple attribute bug that was causing model-generation problems for tuplesMorgan Deters
2013-01-29currently disabling bug486 regression. we need to discuss ↵Andrew Reynolds
getValue/collectModelInfo for quantifiers more.
2013-01-28Fix the regression test for bug 486, and enable itMorgan Deters
(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)
2013-01-28Fix the regression test for bug 486, and enable itMorgan Deters
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2013-01-23partially address bug 486: allow some model inspection of quantifiersMorgan Deters
2013-01-23partially address bug 486: allow some model inspection of quantifiersMorgan Deters
2013-01-08SMT-LIB get-model output now is easier to machine-parse: contains (model...) ↵Morgan Deters
bracketing
2012-12-14Merging in patch from branch '1.0.x'.Tim King
2012-12-14Adding unit test for different versions of division.Tim King
2012-12-11Merge branch '1.0.x', getting fix for bug 480Morgan Deters
2012-12-11SMT-LIB compliance fix to get-assignment; resolves bug 480Morgan Deters
2012-12-08Merge from 1.0.x (bugfix for 476).Morgan Deters
2012-12-08Fix bug 476: when CxxTest is not found, make the error less fatal-lookingMorgan Deters
2012-12-06Fix for fuzzer-found model bugClark Barrett
(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)
2012-12-06* tuple and record support in compatibility libraryMorgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-03Fix for fuzzer-found model bugClark Barrett
2012-12-01remove an obsolete (and incorrect) assertion in boolean-terms; also add ↵Morgan Deters
failing regression for bug 472
2012-12-01fix java system test dependencesMorgan Deters
2012-12-01Some fixes for boolean arraysMorgan Deters
also a regression for bug 411 (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-30Fixes for stricter compilers Andy brought to my attention.Tim King
2012-11-30Committing tests to potentially discover an obscure CLN library issue on 32 ↵Tim King
bit platforms. The issue is discussed here: http://www.ginac.de/CLN/cln_3.html#SEC15.
2012-11-30Add some regressions for bug 438.Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-30fix rewrite-rules syntax in regressionMorgan Deters
2012-11-30fix the syntax of assert-rewrite/-propagation/-reduction by putting the ↵François Bobot
pattern first just after the bindings Do it before the release in order to not break user files later
2012-11-29reliable benchmark corresponding to bug468Kshitij Bansal
2012-11-27Functions and predicates over Boolean now work with --check-models and ↵Morgan Deters
output correct models for such functions (though they are somewhat ugly at present). There's still a problem with model extraction, but it's not Boolean terms' fault. Sometimes checkModel() can report that the model is just fine, but if a user extracts values with getValue(), they find problems with the model (i.e., it doesn't satisfy some assertions). This appears to be due to an asymmetry between how checkModel() works and how Model::getValue() works. I'll open a bugzilla report to discuss this after thinking some more on it. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27First chunk of boolean-terms support.Morgan Deters
Passes simple tests and doesn't break existing functionality. Still need some work merged in for models. This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27Tuples and records merge. Resolves bug 270.Morgan Deters
Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-26Improved implementation of Integer::length() with CLN enabled. Additional ↵Tim King
tests to sanity check both versions CLN and GMP versions of length.
2012-11-26include new regression directories in summary test outputMorgan Deters
2012-11-26fixup for incremental solvingDejan Jovanović
2012-11-26Removing DioSolver::acceptableOriginalNodes(). This assertion was too ↵Tim King
strong, and was broken by r4620. This commit resolves bug463. Adding a previously triggering test case.
2012-11-26Disabling test/regress/regress0/push-pop/bug396.smt2. This takes 2m to run ↵Tim King
in debug mode. This is too long for a regress0 test.
2012-11-25Adding a regression test from bug 462.Tim King
2012-11-23Example of rewrite rules use that comes from an harness testFrançois Bobot
2012-11-19Adding hand minimized test for bug 450.Tim King
2012-11-17Fixed last currently known bug in array modelsClark Barrett
2012-11-17* enable previously-failing (now succeeding) datatype example that uses recordsMorgan Deters
* some bindings cleanup (this commit was certified error- and warning-free by the test-and-commit script.)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback