cvc5.git
2012-11-26 Morgan Detersrolling back r4625 for now (closes bug 464), Andy we...
2012-11-26 Dejan Jovanovićfixup for incremental solving
2012-11-26 Tim KingRemoving DioSolver::acceptableOriginalNodes(). This...
2012-11-26 Dejan JovanovićAdding support for a master equality engine. Each theor...
2012-11-26 Tim KingImproving arithmetic debugging output.
2012-11-26 Tim KingDisabling test/regress/regress0/push-pop/bug396.smt2...
2012-11-26 Morgan Detersdon't include internal variables in model output
2012-11-26 Morgan Deterssome fixes to language bindings and function visibility
2012-11-26 Morgan DetersMakefile fix for new versions of Make (thanks Clark...
2012-11-25 Tim KingAdding a regression test from bug 462.
2012-11-25 Tim KingThis commit fixes two incompleteness bugs (461, 459...
2012-11-24 Tim KingAdds ensureConstraint(...) to ConstraintDatabase. This...
2012-11-23 François BobotExample of rewrite rules use that comes from an harness...
2012-11-21 Tim King- Removes getDeltaValueWithNonlinear() entirely
2012-11-21 Tim KingAdds a number of new capabilities to DeltaRational...
2012-11-21 Tim KingAdded debugging output to --check-models. I've found...
2012-11-19 Kshitij BansalRun lastWinner thread for all commands. Earlier behavio...
2012-11-19 Tim KingAdding hand minimized test for bug 450.
2012-11-19 Tim KingChanged the splitting-on-demand lemmas of arithmetic...
2012-11-19 Tim KingFix for bug452.
2012-11-18 Morgan DetersDisable predicate subtyping:
2012-11-18 Andrew Reynoldssupport for quantifiers macros, bug fix for bug 454...
2012-11-17 Clark BarrettFixed last currently known bug in array models
2012-11-17 Morgan Deters* enable previously-failing (now succeeding) datatype...
2012-11-17 Morgan Detersfix for language bindings (fixes debian build fail...
2012-11-17 Morgan Deters* Fix for bug 445 agreed to in meeting 11/13/2012:...
2012-11-16 Clark BarrettFix for bug451
2012-11-16 Dejan Jovanovićfixing and refactoring the equality iterator
2012-11-16 Morgan DetersFix dumping of array-select expressions in CVC native...
2012-11-16 Morgan Detersfix a compiler warning in models
2012-11-15 Kshitij Bansalsome fixes for --threads=1
2012-11-15 Morgan Detersfix for "make examples"
2012-11-15 Clark BarrettMore fixes to model generation, with previously failing...
2012-11-15 Liana Hadareanforgot to uncomment setLogicInternal for THEORY_BV
2012-11-15 Liana Hadareanchanged logic options so that justification is turned...
2012-11-15 Morgan Detersd_incomplete is context-dependent; we shouldn't be...
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...
next