Age | Commit message (Expand) | Author |
2013-08-08 | Parameterized, uninterpreted sorts need no Boolean-term conversion | Morgan Deters |
2013-07-30 | Minor fixes to build system. | Morgan Deters |
2013-07-29 | Fix numerous compiler warnings on various platforms | Morgan Deters |
2013-07-24 | Regressions now checking models on unknown too. But quantifiers don't have t... | Morgan Deters |
2013-07-24 | Fixes for building with mingw win64. | Morgan Deters |
2013-07-24 | Don't allow --stats if not a statistics-enabled build | Morgan Deters |
2013-07-24 | some portfolio driver cleanup | Morgan Deters |
2013-07-23 | Some fixes for (get-info :all-options) | Morgan Deters |
2013-07-23 | fix for win32 option parsing via mingw32 | Morgan Deters |
2013-07-23 | (get-info :all-options) to get option values; also command-line option sugges... | Morgan Deters |
2013-07-22 | Allow BV and DT in either order in the logic string | Morgan Deters |
2013-07-22 | Add option --cbqi-recurse. | Andrew Reynolds |
2013-07-22 | Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastru... | Andrew Reynolds |
2013-07-19 | possible fix for bug 521 | Dejan Jovanovic |
2013-07-19 | Minor fix for --no-condense-function-values | Morgan Deters |
2013-07-18 | Fix quantifier instantiation bug in cbqi, add default priorities in rewrite e... | Andrew Reynolds |
2013-07-17 | Fix bug 516; include some bug testcases. | Morgan Deters |
2013-07-16 | fixed seg fault when bv equality is turned off | Liana Hadarean |
2013-07-16 | fixed bug520 | Liana Hadarean |
2013-07-16 | "Tabular"-style function definitions in models with --no-condense-function-va... | Morgan Deters |
2013-07-16 | Minor bugfixes to model-building | Morgan Deters |
2013-07-13 | Remove now-unused language bindings interface file. | Morgan Deters |
2013-07-13 | Fix language bindings and portfolio builds. | Morgan Deters |
2013-07-12 | Fix for curious GCC 4.8 translation with -O. | Morgan Deters |
2013-07-11 | Remove auto-aritization from TPTP parser | Morgan Deters |
2013-07-11 | Support for TPTP's TFF0 (with arithmetic) | Morgan Deters |
2013-07-11 | Fix for Boolean-term rewriting and LAMBDAs | Morgan Deters |
2013-07-09 | Fix for bug 519; don't involve ITESimplifier in model generation. | Morgan Deters |
2013-07-09 | add relevant domain computation | Andrew Reynolds |
2013-07-06 | Model output is now const; this related to bug 519 | Morgan Deters |
2013-07-05 | Fix for a datatype parsing bug that Tim found. | Morgan Deters |
2013-07-02 | Make uf strong solver user-context dependent, fixes bug 522. | Andrew Reynolds |
2013-07-02 | Minor fixes for bounded integers, rewrite engine. | Andrew Reynolds |
2013-06-28 | More bug fixes for interval models. | Andrew Reynolds |
2013-06-28 | Fix portfolio builds after yesterday's commits. | Morgan Deters |
2013-06-27 | Better check-models output for some kinds of problems; add anassertion that t... | Morgan Deters |
2013-06-27 | Fix minor warnings found by recent clang/gcc. | Morgan Deters |
2013-06-27 | Remove output.h from public space, to avoid clashes with symbols defined in u... | Morgan Deters |
2013-06-27 | Small fix for IS_INTEGER. | Morgan Deters |
2013-06-27 | Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they don'... | Morgan Deters |
2013-06-27 | Better user documentation for mkVar() and mkBoundVar(). | Morgan Deters |
2013-06-27 | Minor printer cleanup for SMT-LIBv2 symbols "div" and "mod". | Morgan Deters |
2013-06-26 | Add support for interval models in bounded integers MBQI (in progress). | Andrew Reynolds |
2013-06-25 | Merge branch '1.2.x' | Morgan Deters |
2013-06-25 | Proposed fix for bug #513 | Morgan Deters |
2013-06-25 | Refactoring of model engine to separate individual implementations of model b... | Andrew Reynolds |
2013-06-24 | Add files missing from last commit | Morgan Deters |
2013-06-24 | Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al... | Morgan Deters |
2013-06-24 | Add options for symmetry breaking in uf+ss totality axiom approach, option fo... | Andrew Reynolds |
2013-06-21 | Fix failure in non-assertion builds on incorrect SmtEngine use. | Morgan Deters |