cvc5.git
2012-12-01 Morgan Detersfix java system test dependences
2012-12-01 Andrew Reynoldsdrastic simplification of quantifiers code regarding...
2012-12-01 Tim KingFix for a CLN related bug on 32 bit systems. Integer...
2012-12-01 Morgan DetersSome fixes for boolean arrays
2012-12-01 Morgan Detersfix #line annotation warning
2012-12-01 Morgan Detersupdated examples
2012-12-01 Liana Hadareanadded a new example for the combination of bit-vectors...
2012-12-01 Morgan Detersanother part of last commit
2012-12-01 Morgan Detersdefinition-expansion fixed for get-model, resolves...
2012-12-01 Tim KingPolishing API examples.
2012-12-01 Tim KingAdding SmtEngine::setLogic(const char* logic) so that...
2012-11-30 Tim KingFixes for stricter compilers Andy brought to my attention.
2012-11-30 Tim KingChanging the documentation of ARR_TABLE_FUN to say...
2012-11-30 Morgan Detersall API examples now have java versions too; bitvectors...
2012-11-30 Morgan Detersincorporating some comments from Clark
2012-11-30 Clark BarrettFix assertion in smt_engine's getValue
2012-11-30 Tim KingUpdating the combination.cpp example.
2012-11-30 Tim KingCommitting tests to potentially discover an obscure...
2012-11-30 Morgan Detersrenaming --smtlib to --smtlib-strict; removing --smtlib...
2012-11-30 Morgan Detersinternal variables (skolems) aren't printed as part...
2012-11-30 Morgan Deterschange detection/handling of output language more reaso...
2012-11-30 Andrew Reynoldsquantifiers now uses master equality engine, preparatio...
2012-11-30 Andrew Reynoldsparametric datatypes fix related to non-ascribed type...
2012-11-30 Liana Hadareanadded a simple API example example showing how to use...
2012-11-30 Tim KingChanges to SExpr to accept autoconversion from bool...
2012-11-30 Tim KingAdding smtname level options for tlimit, rlimit, etc...
2012-11-30 Morgan DetersPartial fix for bug 435; still needs some effort.
2012-11-30 Morgan DetersAdd some regressions for bug 438.
2012-11-30 Morgan Detersfix rewrite-rules syntax in regression
2012-11-30 Morgan Detersminor fix to release script
2012-11-30 François Bobotfix the syntax of assert-rewrite/-propagation/-reductio...
2012-11-29 Kshitij Bansalreliable benchmark corresponding to bug468
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.
next