| Age | Commit message (Expand) | Author |
|---|
| 2012-11-15 | More fixes to model generation, with previously failing testcases | Clark Barrett |
| 2012-11-15 | Fixed another AUFBV model bug. BV equality subtheory needed to do something | Clark Barrett |
| 2012-11-13 | fixed failed bv regressions by refactoring out some rewrite rules from smt_en... | Liana Hadarean |
| 2012-11-13 | added support for division by zero for bit-vector division operators | Liana Hadarean |
| 2012-10-23 | fixed TheoryBV collectModel info to check for shared terms; this seems to fix... | Liana Hadarean |
| 2012-10-19 | BV theory model fix | Liana Hadarean |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 2012-10-10 | fixing the cvc bv parser and typechecker | Dejan Jovanović |
| 2012-10-09 | fixed bv rewriter to evaluate bvurem over constants | Liana Hadarean |
| 2012-10-04 | Implemented array type enumerator, more fixes for models | Clark Barrett |
| 2012-10-03 | implemented collectModelInfo for TheoryBV | Liana Hadarean |
| 2012-10-03 | added support for interrupting TheoryBV | Liana Hadarean |
| 2012-10-03 | adding ::getBooleanVariables to the PropEngine | Dejan Jovanović |
| 2012-09-24 | Fix the memout issue seen in recent nightly regressions (was due to a | Morgan Deters |
| 2012-09-22 | Separate public-facing and internal-facing interfaces to Statistics. | Morgan Deters |
| 2012-09-19 | General subscriber infrastructure for NodeManager, as discussed in the | Morgan Deters |
| 2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
| 2012-08-29 | * Numerous documentation fixes (fix doxygen warnings, add missing documentati... | Morgan Deters |
| 2012-08-28 | Improved compatibility layer, now supports quantifiers. Also incorporates | Morgan Deters |
| 2012-08-24 | * disallow internal uses of mkVar() (you have to mkSkolem()) | Morgan Deters |
| 2012-08-07 | Some items from the CVC4 public interface review: | Morgan Deters |
| 2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use isCon... | Morgan Deters |
| 2012-08-01 | add isFinished() to type enumerators (so we don't rely on exception-throwing ... | Morgan Deters |
| 2012-08-01 | some fixes for Mac OS | Morgan Deters |
| 2012-07-31 | Options merge. This commit: | Morgan Deters |
| 2012-07-14 | Type enumerator infrastructure and uninterpreted constant support. No suppor... | Morgan Deters |
| 2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
| 2012-07-08 | Bugs resolved by this commit: #314, #322, #359, #364, #365. | Morgan Deters |
| 2012-07-07 | Various fixes to documentation---typos, some incomplete documentation fixed, ... | Morgan Deters |
| 2012-06-28 | Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2 | Clark Barrett |
| 2012-06-15 | Reverting rewrite rule to working version | Clark Barrett |
| 2012-06-15 | Fixes some assertion failures | Clark Barrett |
| 2012-06-14 | fixing the problems with the bvminisat. there was a case when things would ge... | Dejan Jovanović |
| 2012-06-14 | fix for clark's bug | Dejan Jovanović |
| 2012-06-14 | * removing rewriteEquality from the rewriter | Dejan Jovanović |
| 2012-06-13 | Fixed definition of bvsmod | Clark Barrett |
| 2012-06-13 | Fixes more problems in bv rewrites | Clark Barrett |
| 2012-06-13 | Fixes lots of problems in bv rewrite rules and adds lots of assertions | Clark Barrett |
| 2012-06-12 | Changed bitvector theory rewriter so that equalities always get rewritten to | Clark Barrett |
| 2012-06-11 | fixing bitvector bugs | Dejan Jovanović |
| 2012-06-11 | OK, now the rewrite issues are fixed | Clark Barrett |
| 2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
| 2012-06-11 | Fix for array bug with decision heuristic | Clark Barrett |
| 2012-06-10 | Fixed one more bug in rewriter | Clark Barrett |
| 2012-06-10 | Added a very fruitful assertion to the rewriter: checks that rewriting after ... | Clark Barrett |
| 2012-06-10 | fixes for bug347 | Dejan Jovanović |
| 2012-06-06 | Changes to the combination mechanism, lots of details. Not done yet, there ar... | Dejan Jovanović |
| 2012-06-04 | Added preprocessing pass that propagates unconstrained values - solves all of | Clark Barrett |
| 2012-05-31 | Fixed bug in bv: one more case where non-shared equality was getting propagated | Clark Barrett |
| 2012-05-30 | Added BitwiseEq bitvector rewrite | Clark Barrett |
