summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-02-07More complete fix for bug 484 (includes fixes for records and tuples).Morgan Deters
2013-02-07Fix error in tuple type-checking.Morgan Deters
2013-02-07Make --default-dag-thresh apply to stringstreamsMorgan Deters
2013-02-07Do not install the "private-library" headerMorgan Deters
2013-02-06make datatypes enumerator behavior clearer (no exceptions in normal operation)Morgan Deters
2013-02-05Fix a compiler warning in NodeBuilderMorgan Deters
2013-02-05Merge pull request #3 from kbansal/1.0.xKshitij Bansal
decision/ : save d_prvsIndex in JH
2013-02-05decision/ : save d_prvsIndex in JHKshitij Bansal
2013-02-05dos2unix conversion for a number of files; this avoids spurious conflicts ↵Morgan Deters
when merging to master
2013-02-04Fix NodeBuilder bug which could attempt to allocate beyond hard limitMorgan Deters
2013-02-04driver::totalTime statistic is now reported correctly on crashes, tooMorgan Deters
2013-02-04Model no longer adds subterms of quantifiers to equality engine, this fixed ↵Morgan Deters
bug 492 and resolves previous issue for bug 486. (cherry picked from *part* of commit e54c0f73712b25f1d6d49a3817c923eea077da81) Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-02-01Fix a tuple attribute bug that was causing model-generation problems for tuplesMorgan Deters
2013-01-30correct output language bug with --dump-toMorgan Deters
2013-01-28Fix the regression test for bug 486, and enable itMorgan Deters
(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)
2013-01-28made QuantifiersEngine::d_inst_match_trie and ↵Andrew Reynolds
QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486 (cherry-picked from master c5d1a5d8f898bf22c6bbc98f1d484b07706c035b)
2013-01-27some fixes for Intel benchmarks regarding quantifiers and datatypes, ↵Andrew Reynolds
datatypes theory still crashes for datatypes with boolean subfields (cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793)
2013-01-26another fix for quantifier models (related to bug 486)Morgan Deters
2013-01-25fix --check-model --finite-model-find when used together (related to bug 486)Morgan Deters
2013-01-23partially address bug 486: allow some model inspection of quantifiersMorgan Deters
2013-01-23update NEWS fileMorgan Deters
2013-01-22fix for theory preprocessing cache on clang, perhaps others.Morgan Deters
2013-01-22update ANTLR URLs (antlr.org -> antlr3.org)Morgan Deters
2013-01-19Fix an options-processing bug on some platforms (e.g., MacOS).Morgan Deters
2012-12-21adding copy constructor for the datatype enumeratorDejan Jovanović
fixes bug 484
2012-12-18Fix bug 483: readline checks must come after Boost checks in configureMorgan Deters
2012-12-15Fix printing of EXISTS in CVC language printerMorgan Deters
2012-12-14Adding unit test for different versions of division.Tim King
2012-12-14Merge remote-tracking branch 'main-repo/1.0.x' into 1.0.xTim King
2012-12-14Changing the rewriter to use Boute's Euclidean definition of division.Tim King
2012-12-12Merge pull request #1 from lianah/1.0.xDejan Jovanović
* fixed bug 481 by adding check for division by 0 in bit-vector division...
2012-12-12* fixed bug 481 by adding check for division by 0 in bit-vector division circuitlianah
* added printing for total bit-vector division kinds for debugging purposes
2012-12-11SMT-LIB compliance fix to get-assignment; resolves bug 480Morgan Deters
2012-12-11Ignore unknown term annotations (giving a warning). Resolves bug 479.Morgan Deters
2012-12-11adding cache for preprocessing datatypes terms to fix bug 475, fix for ↵Andrew Reynolds
handling user attributes in quantifiers (was broken) (cherry-picked from commit 206edb6f11674e954f5762a1db9712131151a276)
2012-12-08Fix bug 476: when CxxTest is not found, make the error less fatal-lookingMorgan Deters
2012-12-07Fix to portfolio buildsMorgan Deters
(cherry picked from commit f46ba71e78054af63b529eb3271952c55beba37e)
2012-12-07Fix performance issue in a DFS search (bug 474)Kshitij Bansal
(cherry picked from commit f056522a587d1b080224992355be070b73d97a3b)
2012-12-06* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issuesMorgan Deters
* build bugfix for win32 * also fix a bug re: tuples and records in the datatypes rewriter These fixes are for both trunk and 1.0.x branches. (cherry picked from commit 8c8985f024cec925f774ff32ebccc306be8e4b26)
2012-12-06distribute the find_public_interface.sh scriptMorgan Deters
(cherry picked from commit af44cd27d5b079f1279c407e610e557e81285d8f)
2012-12-06version numberingMorgan Deters
(cherry picked from commit 4cae70d893601a2070dc2b00c5640b48515b1a22)
2012-12-06Fix for fuzzer-found model bugClark Barrett
(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)
2012-12-01Cutting release 1.0.1.0Morgan Deters
2012-12-01fix cut-release sanity checksMorgan Deters
2012-12-01fix to TNode assertion (which is too strict, given lax ordering requirements ↵Morgan Deters
on static data initialization)---this should fix debug-staticbinary Mac builds, maybe others
2012-12-01Throw a logic exception if user makes an assertion using a STORE_ALLClark Barrett
2012-12-01remove instantiator frameworkMorgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-01Fix the way abstract values are typed; fixes some compliance issues.Morgan Deters
Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-01fix memory corruption issue in debug builds that led to unhelpful outputMorgan Deters
2012-12-01remove an obsolete (and incorrect) assertion in boolean-terms; also add ↵Morgan Deters
failing regression for bug 472
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback