Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-02-03 | Some cleanup of miplib regressions and options | Morgan Deters | |
2013-02-03 | Merge from mdeters/miplib branch (commit ↵ | Morgan Deters | |
'ce7c485182902ae43871057185095f71f74a8a58') | |||
2013-02-03 | new miplib pass, works for 1 or 2 vars | Morgan Deters | |
2013-02-01 | Merge branch '1.0.x' | Morgan Deters | |
2013-02-01 | Fix a tuple attribute bug that was causing model-generation problems for tuples | Morgan Deters | |
2013-01-29 | currently disabling bug486 regression. we need to discuss ↵ | Andrew Reynolds | |
getValue/collectModelInfo for quantifiers more. | |||
2013-01-28 | Fix the regression test for bug 486, and enable it | Morgan Deters | |
(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87) | |||
2013-01-28 | Fix the regression test for bug 486, and enable it | Morgan Deters | |
2013-01-28 | some fixes for win32, including ability to "make check" win32 builds via wine | Morgan Deters | |
2013-01-23 | partially address bug 486: allow some model inspection of quantifiers | Morgan Deters | |
2013-01-23 | partially address bug 486: allow some model inspection of quantifiers | Morgan Deters | |
2013-01-08 | SMT-LIB get-model output now is easier to machine-parse: contains (model...) ↵ | Morgan Deters | |
bracketing | |||
2012-12-14 | Merging in patch from branch '1.0.x'. | Tim King | |
2012-12-14 | Adding unit test for different versions of division. | Tim King | |
2012-12-11 | Merge branch '1.0.x', getting fix for bug 480 | Morgan Deters | |
2012-12-11 | SMT-LIB compliance fix to get-assignment; resolves bug 480 | Morgan Deters | |
2012-12-08 | Merge from 1.0.x (bugfix for 476). | Morgan Deters | |
2012-12-08 | Fix bug 476: when CxxTest is not found, make the error less fatal-looking | Morgan Deters | |
2012-12-06 | Fix for fuzzer-found model bug | Clark Barrett | |
(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79) | |||
2012-12-06 | * tuple and record support in compatibility library | Morgan Deters | |
(this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-12-03 | Fix for fuzzer-found model bug | Clark Barrett | |
2012-12-01 | remove an obsolete (and incorrect) assertion in boolean-terms; also add ↵ | Morgan Deters | |
failing regression for bug 472 | |||
2012-12-01 | fix java system test dependences | Morgan Deters | |
2012-12-01 | Some fixes for boolean arrays | Morgan Deters | |
also a regression for bug 411 (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-30 | Fixes for stricter compilers Andy brought to my attention. | Tim King | |
2012-11-30 | Committing 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-30 | Add some regressions for bug 438. | Morgan Deters | |
(this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-30 | fix rewrite-rules syntax in regression | Morgan Deters | |
2012-11-30 | fix 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-29 | reliable benchmark corresponding to bug468 | Kshitij Bansal | |
2012-11-27 | Functions 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-27 | First 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-27 | Tuples 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-26 | Improved implementation of Integer::length() with CLN enabled. Additional ↵ | Tim King | |
tests to sanity check both versions CLN and GMP versions of length. | |||
2012-11-26 | include new regression directories in summary test output | Morgan Deters | |
2012-11-26 | fixup for incremental solving | Dejan Jovanović | |
2012-11-26 | Removing 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-26 | Disabling 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-25 | Adding a regression test from bug 462. | Tim King | |
2012-11-23 | Example of rewrite rules use that comes from an harness test | François Bobot | |
2012-11-19 | Adding hand minimized test for bug 450. | Tim King | |
2012-11-17 | Fixed last currently known bug in array models | Clark Barrett | |
2012-11-17 | * enable previously-failing (now succeeding) datatype example that uses records | Morgan Deters | |
* some bindings cleanup (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-17 | * Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ↵ | Morgan Deters | |
ALL_SUPPORTED logic * Java bindings fixes: fixed access to ostreams, iterators * Make SmtEngine::setUserAttribute() (and others) take a const string& * Also a few compliance fixes (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-16 | Fix for bug451 | Clark Barrett | |
2012-11-15 | More fixes to model generation, with previously failing testcases | Clark Barrett | |
Also refactored some header file includes to reduce compile time | |||
2012-11-15 | fuzz15 should have been fuzz14 | Clark Barrett | |
2012-11-15 | Fix for bug 447. | Tim King | |
2012-11-15 | Fixed another AUFBV model bug. BV equality subtheory needed to do something | Clark Barrett | |
similar to arrays - limit the set of terms reported to those relevant in the current context. Also removed collectModelInfo from sharedTermsDatabase - doesn't seem to be needed any more. | |||
2012-11-15 | Fixing comments in print_lambda.cvc. | Tim King | |