cvc5.git
2012-11-29 Andrew Reynoldsrequire type ascriptions for parametric datatype constr...
2012-11-29 Morgan DetersFix for hidden symbols in library on Mac. It's a stran...
2012-11-29 Andrew Reynoldsfixes bug 438, incorporate subtypes into type unificati...
2012-11-29 Morgan Detersfix for andy: boolean terms stuff really shouldn't...
2012-11-29 Morgan Detersminor documentation fix
2012-11-29 Morgan Deterssvn:ignore property
2012-11-29 Clark BarrettFix for nasty corner case found by fuzzer...
2012-11-29 Kshitij BansalHack to support global variables for CVC language exten...
2012-11-29 Clark BarrettFixing function models with Boolean terms. Also, LAMBD...
2012-11-28 Tim KingAdding the helloworld.cpp example.
2012-11-28 Kshitij Bansalfix a potential race (have failed to reproduce)
2012-11-28 Clark BarrettFix for getValue. Now it can handle lambda applications
2012-11-28 Morgan DetersAttempted "quick-fix" for QF_UF performance regression...
2012-11-28 Kshitij Bansaltreat all get commands like getValue (send only to...
2012-11-28 Kshitij Bansalminor
2012-11-28 Morgan Detersupdate to release notes
2012-11-28 Morgan DetersBug fix:
2012-11-28 Morgan Detersfix: correct misleading comment in dump output
2012-11-27 Morgan DetersFunctions and predicates over Boolean now work with...
2012-11-27 Kshitij Bansalfix in CommandSequence invoke : maintain success/failur...
2012-11-27 Morgan Detersmore mac fixes
2012-11-27 Morgan Detersfix for some Mac builds
2012-11-27 Kshitij BansalSimplify --help=decision with only currently supported...
2012-11-27 Morgan Detersgive warning at configure-time about unsupported langua...
2012-11-27 Morgan Detersdo not turn on BV for QF_SAT
2012-11-27 Morgan DetersFirst chunk of boolean-terms support.
2012-11-27 Morgan DetersTuples and records merge. Resolves bug 270.
2012-11-27 Tim KingAdding an example to show how to use arithmetic.
2012-11-26 Tim KingImproved implementation of Integer::length() with CLN...
2012-11-26 Morgan Detersinclude new regression directories in summary test...
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...
next