cvc5.git
2013-07-24 Morgan DetersRegressions now checking models on unknown too. But...
2013-07-24 Morgan DetersFixes for building with mingw win64.
2013-07-24 Morgan DetersDon't allow --stats if not a statistics-enabled build
2013-07-24 Morgan Deterssome portfolio driver cleanup
2013-07-24 Morgan DetersSome fixes for (get-info :all-options)
2013-07-23 Morgan Detersfix for win32 option parsing via mingw32
2013-07-23 Morgan Deters(get-info :all-options) to get option values; also...
2013-07-22 Morgan DetersAllow BV and DT in either order in the logic string
2013-07-22 Andrew ReynoldsAdd option --cbqi-recurse.
2013-07-22 Andrew ReynoldsBug fix for --fmf-fmc for non-uninterpreted sort quanti...
2013-07-20 Morgan Detersenable bug521 regression tests
2013-07-19 Dejan Jovanovicpossible fix for bug 521
2013-07-19 Morgan DetersMinor fix for --no-condense-function-values
2013-07-18 Andrew ReynoldsFix quantifier instantiation bug in cbqi, add default...
2013-07-17 Morgan DetersFix bug 516; include some bug testcases.
2013-07-16 Liana Hadareanfixed seg fault when bv equality is turned off
2013-07-16 Liana Hadareanfixed bug520
2013-07-16 Morgan DetersFix for get-antlr script and PIC/non-PIC objects, on...
2013-07-16 Morgan Deters"Tabular"-style function definitions in models with...
2013-07-16 Morgan DetersMinor bugfixes to model-building
2013-07-13 Morgan DetersRemove now-unused language bindings interface file.
2013-07-13 Morgan DetersFix language bindings and portfolio builds.
2013-07-12 Morgan DetersFix for curious GCC 4.8 translation with -O.
2013-07-11 Morgan DetersRemove auto-aritization from TPTP parser
2013-07-11 Morgan DetersSupport for TPTP's TFF0 (with arithmetic)
2013-07-11 Morgan DetersFix for Boolean-term rewriting and LAMBDAs
2013-07-10 Morgan DetersFix for bug 519; don't involve ITESimplifier in model...
2013-07-09 Andrew Reynoldsadd relevant domain computation
2013-07-07 Morgan DetersModel output is now const; this related to bug 519
2013-07-05 Morgan DetersFix for a datatype parsing bug that Tim found.
2013-07-02 Andrew ReynoldsMake uf strong solver user-context dependent, fixes...
2013-07-02 Andrew ReynoldsMinor fixes for bounded integers, rewrite engine.
2013-06-28 Andrew ReynoldsMore bug fixes for interval models.
2013-06-28 Morgan DetersFix portfolio builds after yesterday's commits.
2013-06-27 Morgan DetersBetter check-models output for some kinds of problems...
2013-06-27 Morgan DetersFix minor warnings found by recent clang/gcc.
2013-06-27 Morgan DetersRemove output.h from public space, to avoid clashes...
2013-06-27 Morgan DetersSmall fix for IS_INTEGER.
2013-06-27 Morgan DetersRemove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_publ...
2013-06-27 Morgan DetersBetter user documentation for mkVar() and mkBoundVar().
2013-06-27 Morgan DetersMinor printer cleanup for SMT-LIBv2 symbols "div" and...
2013-06-26 Andrew ReynoldsAdd support for interval models in bounded integers...
2013-06-25 Morgan DetersMerge branch '1.2.x'
2013-06-25 Morgan DetersProposed fix for bug #513
2013-06-25 Andrew ReynoldsRefactoring of model engine to separate individual...
2013-06-25 Morgan DetersAdd files missing from last commit
2013-06-25 Morgan DetersSupport for abs, to_int, is_int, divisible in SMT-LIB...
2013-06-24 Andrew ReynoldsAdd options for symmetry breaking in uf+ss totality...
2013-06-21 Morgan DetersFix failure in non-assertion builds on incorrect SmtEng...
2013-06-19 Morgan DetersMerge branch '1.2.x'
2013-06-19 Morgan DetersWorkaround for suspected clang 3.0 codegen bug on Mac
2013-06-19 Morgan DetersFix to the "include" extended feature of the SMT-LIB...
2013-06-19 Morgan DetersGive a more useful parse error message for "undeclared...
2013-06-17 Morgan DetersJava streams example I forgot to add a long time ago
2013-06-17 Andrew ReynoldsMake --var-elim-quant true by default. Add rewrite...
2013-06-16 Andrew ReynoldsFix in SMT2 parser for parametric datatypes
2013-06-10 Morgan Detersanother fix for array-store-all printing
2013-06-10 Morgan DetersBetter array-store-all output for SMT-LIB.
2013-06-08 Morgan DetersFix typos in alttheoryskel
2013-06-08 Morgan DetersFixes for Boolean terms in arrays (including fix for...
2013-06-07 Morgan DetersOne more case for arrays of Boolean.
2013-06-07 Morgan DetersFix for bug 517.
2013-06-07 Morgan DetersAllow disabling include-file feature
2013-06-07 Dejan Jovanovićsmall parese issue in IDL
2013-06-06 Dejan Jovanovićtypo
2013-06-06 Dejan JovanovićIDL example theory (to be used with --use-theory=idl).
2013-06-05 Andrew ReynoldsFix bug in --fmf-fmc for producing models of functions...
2013-06-04 Morgan DetersFile inclusion in Smt2 parser.
2013-06-04 Morgan DetersAdd --no-condense-function-values option for explicit...
2013-06-04 Morgan DetersMerge branch '1.2.x'
2013-06-04 Morgan DetersFix clang static initialization order issue; fixes...
2013-06-04 Andrew ReynoldsAdd partial support for MBQI with arrays when using...
2013-06-03 Morgan DetersMerge tag 'casc24'
2013-06-03 Morgan DetersUpdated CASC scripts, as provided to Geoff Sutcliffe
2013-05-29 Morgan DetersMerge branch '1.2.x'
2013-05-29 Morgan DetersPer SMT-LIB spec, allow (set-info..) command to succeed...
2013-05-29 Morgan DetersSMT-LIB printer updates (some missing cases).
2013-05-29 Morgan DetersFix bug where strict mode didn't allow DIV or MOD,...
2013-05-28 Morgan DetersStandardize SMT-LIBv2 set of logics to use LogicInfo.
2013-05-23 Andrew ReynoldsRefactoring to prepare for MBQI with integer quantifica...
2013-05-22 Andrew ReynoldsMerge branch 'master' of https://github.com/CVC4/CVC4
2013-05-22 Andrew ReynoldsSignificant work on bounded integer quantification...
2013-05-22 Andrew ReynoldsAdd regressions for finite model finding
2013-05-21 Morgan DetersMerge branch '1.2.x'
2013-05-21 Morgan DetersFix bug 512: an assertion failure only appearing with...
2013-05-21 Morgan DetersFix an error that valgrind found.
2013-05-21 Morgan DetersMerge branch '1.2.x'
2013-05-21 Morgan DetersFix incremental bug in symmetry breaker.
2013-05-20 Morgan DetersMerge branch '1.2.x'
2013-05-20 Morgan DetersFix error reporting on use of (nonlinear) div,mod,...
2013-05-20 Morgan DetersUpdate THANKS to mention David Cok's contributions.
2013-05-20 Morgan DetersDetect multiply-defined :named annotations and issue...
2013-05-20 Morgan DetersFix parsing of SMT-LIBv2 |quoted| symbols that span...
2013-05-20 Morgan DetersCompliance fixes for :named annotations: they must...
2013-05-20 Morgan DetersDon't allow get-model & co after a user push/pop
2013-05-20 Morgan DetersAs per SMT-LIB standard: make - and xor take n>2 args...
2013-05-20 Morgan DetersFix for equality-chaining of Booleans in SMT-LIBv2.
2013-05-20 Morgan DetersFix destruction issue in GetValueCommand leading to...
2013-05-20 Morgan DetersBetter error on invalid logic strings.
2013-05-20 Morgan DetersBetter error on illegal (pop N); also more compliant...
next