Fix an off-the-end string pointer bug (showed up only in some Win32 builds).

Fixes an idempotency issue for non-linear multiplication with integer and real variables.

Fix for random-seed option.

Fix for portfolio.

Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok.

No diamond-breaking under quantifiers (resolves bug #550).

Fix two variants of Node::substitute().

Node::substitute() is overloaded.  One version was properly substituting
operators (e.g. the "f" in f(x) could be substituted).  The others were
ignoring anything in function position.  Fixed.  Thanks to Wei Wang for
pointing this out.

Stopping non-linear terms from entering the dio solver. Fixes bug 547.

URL update

Fix for quote-escaping in smt2 printer

enable search for html doc

gmp is again default, not cln, for build ID (reverting due to license discussion at Monday meeting)

Switch license default back to BSD, and add --best and --enable-gpl options.

Cache apt packages on Travis.

Fix LogicInfo parsing for string logics

Update copyright year.

Fix for ANTLR warning.

Better automatic handling of output language setting.

Better get-value parse error message for common user error.

Minor code cleanup.

cln now default w.r.t. build ID string

Fix to interactive mode determination.

Fix option specification.

Fix an autoconf issue with CLN in some configurations; also clarification re: license issues

[skip ci]

Fix configure handling for CLN (should fix win32 nightly builds)

Add missing regression-results directory.

configure --with-portfolio disables CLN.

some config changes: new --bsd option, readline gives warning, default build is now production.

Send Travis-CI emails to everyone

Fix for bug 544.

Another fix for clang.

Fix stack size on in-tree regressions.

cleanup

Fix link error when using clang.

Fix to Travis-CI config.

Travis-CI configuration.

Some minor cleanup.

Update NEWS.

Fix timer statistics to report correct time even on process abort.

Whitespace.

Fix warning.

Remove "NodeValue width" output

GLPK build identifier, license warnings.

mv prp to regress1

fix bug 542

Initializing 1.3.x branch.

Cutting release 1.3.

disable substring in default mode

Fix NodeValue bitfields for 32-bit; fix comment.

Minor cleanup.

Update copyrights, add missing file-level documentation; fix perms.

Fixes related to parametric datatype printing.

Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now works).

Script fixes; when determining authorship of source files, don't count copyright-updating commits.

Fix NEWS.

NEWS reorganization.

Remove a regression for which the portfolio takes forever (see bug 542).

Minor cleanup.

Partial kind branch merge, including new --rewrite-apply-to-const feature.

Don't put define-funs in model output; bug 411 testcase no longer relevant.

Updated acknowledgments.

More Java bindings fixes

Merge branch 'master' of github.com:tiliang/CVC4

adds LB strategy

adds LB strategy

Some fixes for swig warnings.

Merge branch 'master' of github.com:tiliang/CVC4

Last version for undelayed LB

Last version for undelayed LB

Work around a swig segfault issue when building on  Mac OS

change string news

Merge branch 'master' of github.com:tiliang/CVC4

string fmf perfomance fix

string fmf changes

string fmf perfomance fix

rm ChangeLog (use NEWS)

SExpr pretty-printing for :all-options and :all-statistics.

Minor cleanup.

Add test case for (previously resolved) bug 528.

Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a subtype of (Pair Real Real).  Resolves bug #541.

fixed rewriter bug where postRewrite was not caching properly

Another fix to Java destruction order issues.  Thanks to Zheng Manchun for the report.

Update NEWS file.

Fix proofs build.

Fix portfolio compile error.

Ignore config/compile file, which newer autotools create

Fix for compile error when using gcc 4.7 with -std=gnu++11.  Thanks to Martin Brain for the patch!

General pre-release cleanup commit

* Rename {model,util_model}.{h,cpp} files to match class names
* Fix alreadyVisited() issue in TheoryEngine
* Remove spurious Message that causes compliance issues
* Update copyrights, fix public/private markings in headers
* minor comment fixes
* remove EXTRACT_OP as a special-case in typechecker
* note about rewriters in theoryskel readme
* Clean up some compiler warnings
* Code typos and spacing

Java bindings improvements for CASCADE, minor cleanup.

Add missing template instanatiation in Java bindings

Some versioning in advance of the 1.3 release.

Incremental is now on by default when using from API, off for command-line driver except in interactive mode.

Bug fix for E-matching select terms, minor fix for bounded integers, bug fix to improve performance of quantifiers rewriter

Fix a segfault in the printer infrastructure when called from API and no language is set

Fix C++-to-Java exception translation.

Fix Java output stream adapter.

Merge branch 'master' of github.com:tiliang/CVC4

string fmf changes

Fix Java destruction order issue; thanks to Zheng Manchun for reporting this bug.

Minor fix for swig bindings.