cvc5.git
2012-11-15 Clark Barrettfuzz15 should have been fuzz14
2012-11-15 Tim KingFix for bug 447.
2012-11-15 Clark BarrettFixed another AUFBV model bug. BV equality subtheory...
2012-11-15 Tim KingFixing comments in print_lambda.cvc.
2012-11-14 Tim KingFix for bug 407. mkAnonymousFunction() in the parser...
2012-11-14 Andrew Reynoldsreplaced all static member data from rewrite rule trigg...
2012-11-14 Tim KingFixed a typo in r4576
2012-11-14 Tim KingBeautifying smt_engine.cpp.
2012-11-14 Tim KingFix to bug449. Adds shared constants to the set of...
2012-11-14 Clark Barrettbug fixes to models, array rewriter with previously...
2012-11-14 Kshitij BansalQuantifiers enabled with portfolio, closing bug 423.
2012-11-14 Kshitij Bansalfix a race problem. due to interrupt mechanism minisat...
2012-11-13 Clark BarrettMore bugfixes for models
2012-11-13 Tim KingSmtEngine::checkModel() should only be called if the...
2012-11-13 Andrew Reynoldsrefactoring of quantifiers rewriter based on code revie...
2012-11-13 Liana Hadareanfixed failed bv regressions by refactoring out some...
2012-11-13 Liana Hadareanadded support for division by zero for bit-vector divis...
2012-11-13 Clark BarrettRelaxing too-strict assertion
2012-11-13 Clark BarrettFixed an array rewriting bug found by fuzzer
2012-11-13 Clark BarrettTestcases for fixed bugs
2012-11-13 Clark BarrettFixed bug in array constant normalization found by...
2012-11-12 Tim KingImproved error reporting for improperly using non-linea...
2012-11-12 Tim KingDelta is now generated in arithmetic to keep consistent...
2012-11-12 Liana Hadareanchanged BitVector::unsignedRem to match the behavior...
2012-11-12 Morgan DetersFix for bug 444, dealing with the placing of set-logic...
2012-11-12 Morgan Deters* Fix language bindings: various issues
2012-11-12 Andrew Reynoldsminor bug fixes for quantifiers, added sort inference...
2012-11-11 Tim KingFixes for the arithmetic normal form and rewriter to...
2012-11-10 Tim KingBeautifying integer_cln_imp.h
2012-11-10 Tim KingFix to quantifier rewritting not being idempotent....
2012-11-10 Tim KingRemoving rewriter call in SmtEngine::addFormula().
2012-11-10 Clark BarrettFixed missing \ in uflra/Makefile.ma
2012-11-10 Tim KingFix for bug 439. Delta computation now includes disequa...
2012-11-10 Morgan DetersChange run-regression script to *additionally* run...
2012-11-10 Morgan DetersUpdates to Clark's commit r4540:
2012-11-10 Morgan Detersfix typo in language bindings
2012-11-10 Clark BarrettFinally tracked down problems in regressions and fuzz...
2012-11-09 Morgan DetersTheoryEngineModelBuilder::buildModel() is only called...
2012-11-09 Kshitij Bansalexport null nodes (fixes a bug in portfolio model stuff)
2012-11-09 Tim KingTest that breaks arithmetic model building due to diseq...
2012-11-09 Tim KingArithmetic problem that fails --check-models due incomp...
2012-11-09 Morgan DetersBug-fix for a crash involving improperly-thrown excepti...
2012-11-09 Morgan DetersIn non-linear logics, rewrite DIVISION, INTS_DIVISION...
2012-11-09 Morgan Detersanother DISTCLEANFILES entry, for proper "make distclea...
2012-11-09 Clark BarrettFix for another model assertion failure
2012-11-08 Tim KingTurns on TheoryUF when non-linear arithmetic is turned...
2012-11-08 Morgan Detersfix "make distcheck"
2012-11-08 Morgan DetersReview of trunk r4525 (TypeNode::getBaseType()):
2012-11-08 Tim KingImproved support for division by zero. This adds the...
2012-11-08 Morgan Detersexception fix
2012-11-08 Clark BarrettFixed two small bugs in model generation
2012-11-08 Clark BarrettAdded getBaseType - Morgan please check
2012-11-08 Andrew Reynoldsadded support for parametric datatypes in smt2 parser...
2012-11-07 Morgan Deters* Type ascription bug fixed (resolves bug 432), but...
2012-11-07 Tim KingFix to a bug in integer mod lemmas.
2012-11-06 Morgan Detersfix issue in compatibility layer that could segfault
2012-11-05 Tim KingFix to the context dependent static learning code.
2012-11-05 Morgan Detersfixes for replacement function library
2012-11-05 Morgan Detersfixes for mac os
2012-11-05 Morgan Detersfix for tarball building (fixes debian and distcheck...
2012-11-02 Andrew Reynoldsmore minor updates to inst gen and representative selec...
2012-10-31 Andrew Reynoldscleaning up some of the equality query stuff, implement...
2012-10-30 Dejan Jovanovićdelta of a model-building failure case
2012-10-29 Andrew Reynoldsmore updates and minor bug fixes for fmf/inst-gen quant...
2012-10-29 Clark BarrettTweak to options configuration for turning off minisat...
2012-10-29 Clark BarrettDisable minisat elimination when models are on
2012-10-29 Clark BarrettDisable some array optimizations when models are on
2012-10-29 Clark Barrettauflia directory missing from regression summary -...
2012-10-26 Morgan DetersFix to subrange type enumerator, and its unit test...
2012-10-26 Andrew Reynoldsbug fix for parametric datatypes, previously datatypes...
2012-10-26 Tim KingFix for bug 430. d_delta in PartialModel was never...
2012-10-26 Morgan Detersbuild options sources into distribution tarballs (in...
2012-10-26 Morgan Detersnew boost.m4 makes boost-thread require boost-system...
2012-10-26 Morgan Detersbetter parametric datatype arity checking; fixes bug 433
2012-10-26 Clark BarrettFixed a failing datatype regression with check-models
2012-10-26 ACSYStoday's build system fix: sometimes examples weren...
2012-10-26 Andrew Reynoldsfixed bug in datatypes decision procedure enforcing...
2012-10-26 Clark BarrettMore bug fixes and more checks for models
2012-10-25 ACSYSlast build system fix for now: fix some typos affecting Mac
2012-10-25 Morgan Detersextra quoting for special character
2012-10-25 ACSYSmore minor fixes to build system
2012-10-25 Morgan DetersOne of my changes to the build system yesterday broke...
2012-10-24 Andrew Reynoldsfixed assertion failures in efficient e-matching
2012-10-24 Morgan DetersIncludes many fixes to build system for Solaris (thanks...
2012-10-24 Tim KingUpdated the ArithStaticLearner to be user context depen...
2012-10-24 Tim KingFix for systems that do not have the MAP_FILE macro...
2012-10-24 Dejan Jovanovićfix for bug 429
2012-10-24 Dejan Jovanovićtwo smaller random pure LRA push-pop cases that fail
2012-10-24 Andrew Reynoldsefficient e-matching now specific to rewrite rules
2012-10-23 Andrew Reynoldsmore major cleanup of quantifiers code, separating...
2012-10-23 Andrew Reynoldsfixed problem with datatypes giving incorrect explanati...
2012-10-23 Clark BarrettMore debugging info, small changes to model builder
2012-10-23 Morgan Deterssome fixes for "make examples" and "make install-exampl...
2012-10-23 Clark BarrettAdded reads that were missing in collectModelInfo
2012-10-23 Liana Hadareanfixed TheoryBV collectModel info to check for shared...
2012-10-23 Tim KingThe contrib/get-antlr-3.4 script:
2012-10-23 Andrew Reynoldsmore updates to inst gen: fixed partial instantiations...
2012-10-22 Morgan Detersfix parser generation in distributed tarballs (should...
2012-10-22 Morgan Detersone more incorrect #line fixed
2012-10-22 Morgan Detersfix misleading comment in example
next